/* This is s formulation of the undecidability of the halting problem for Turing machines. I just copied it from somewhere without looking at how the coding was done. */ c(oskc1) . c(oskc0) . c(oskc2) . a(oskc3) . c(oskf1(U)) . c(oskf0(U)) . c(oskf2(U)) . c(oskf3(U)) . skp1(U,V), c(V) . skp0(U,V), c(U) . skp1(U,V) <- h2(V,V). skp0(U,V) <- h2(U,U). d(oskc3,U,V) <- c(U). d(oskc0,U,V) <- c(U), ska2. h2(oskc1,U), h2(U,U) <- c(U), ska1. o(dd,b), h2(U,U) <- c(U), ska1. skp0(V,U) <- o(dd,b), h2(U,V). h2(oskc2,U), h2(U,U) <- c(U), ska0. o(oskc2,b), h2(U,U) <- c(U), ska0. ska2 <- d(U,oskf3(U),skf3(U)), a(U). h2(U,V), o(W,b) <- c(U), skp2(W). skp1(U,V) <- o(U,b), h3(U,V,V). h2(oskc1,U) <- h2(U,U), c(U), ska1. o(dd,g) <- h2(U,U), c(U), ska1. skp2(U) <- d(U,oskf2(U),skf2(U)), c(U). o(W,g) <- c(U), h2(U,V), skp2(W). h2(U,V), h3(W,U,V) <- c(U), skp2(W). [] <- h2(oskc2,U), c(U), h2(U,U), ska0. h3(W,U,V) <- c(U), h2(U,V), skp2(W). h2(oskf1(U),oskf1(U)), ska1 <- c(U), skp1(U,skf1(U)). h2(oskf0(U),oskf0(U)), ska0 <- c(U), skp0(skf0(U),U). ska0 <- c(U), o(dd,g), h2(U,oskf0(U)), skp0(skf0(U),U). ska1 <- c(U), o(U,g), h3(U,oskf1(U),oskf1(U)), skp1(U,skf1(U)). /* with strategy halteproblem.ord Proof: ====== 1 : c(oskc1) [axiom] 2 : c(oskc0) [axiom] 3 : c(oskc2) [axiom] 4 : a(oskc3) [axiom] 5 : c(oskf1(B)) [axiom] 6 : c(oskf0(B)) [axiom] 7 : c(oskf2(B)) [axiom] 9 : skp1(B,C),c(C) [axiom] 10 : skp0(B,C),c(B) [axiom] 11 : h2(B,B) -> skp1(C,B) [axiom] 12 : h2(B,B) -> skp0(B,C) [axiom] 13 : c(B) -> d(oskc3,B,C) [axiom] 14 : c(B),ska2 -> d(oskc0,B,C) [axiom] 15 : c(B),ska1 -> h2(oskc1,B),h2(B,B) [axiom] 16 : c(B),ska1 -> o(d,b),h2(B,B) [axiom] 17 : o(d,b),h2(B,C) -> skp0(C,B) [axiom] 18 : c(B),ska0 -> h2(oskc2,B),h2(B,B) [axiom] 20 : d(B,oskf3(B),skf3(B)),a(B) -> ska2 [axiom] 21 : c(B),skp2(C) -> h2(B,D),o(C,b) [axiom] 22 : o(B,b),h3(B,C,C) -> skp1(B,C) [axiom] 23 : h2(B,B),c(B),ska1 -> h2(oskc1,B) [axiom] 24 : h2(B,B),c(B),ska1 -> o(d,g) [axiom] 25 : d(B,oskf2(B),skf2(B)),c(B) -> skp2(B) [axiom] 26 : c(B),h2(B,C),skp2(D) -> o(D,g) [axiom] 27 : c(B),skp2(C) -> h2(B,D),h3(C,B,D) [axiom] 28 : h2(oskc2,B),c(B),h2(B,B),ska0 -> [axiom] 29 : c(B),h2(B,C),skp2(D) -> h3(D,B,C) [axiom] 30 : c(B),skp1(B,skf1(B)) -> h2(oskf1(B),oskf1(B)),ska1 [axiom] 32 : c(B),o(d,g),h2(B,oskf0(B)),skp0(skf0(B),B) -> ska0 [axiom] 33 : c(B),o(B,g),h3(B,oskf1(B),oskf1(B)),skp1(B,skf1(B)) -> ska1 [axiom] 34 : true,ska1,c(B) -> h2(oskc1,B) [reduction of 23 by [15]] 35 : true,d(oskc3,oskf3(oskc3),skf3(oskc3)) -> ska2 [negative chaining of 4 from 20] 36 : ska2 [reduction of 35 by [13]] 37 : c(B) -> d(oskc0,B,C) [reduction of 14 by [36]] 38 : true,ska1,c(B),h2(C,D) -> h2(B,B),skp0(D,C) [negative chaining of 16 from 17] 40 : true,c(oskf2(oskc0)),c(oskc0) -> skp2(oskc0) [negative chaining of 37 from 25] 42 : skp2(oskc0) [reduction of 40 by [7,2]] 43 : true,c(B),h2(B,C) -> o(oskc0,g) [negative chaining of 42 from 26] 44 : true,c(B),h2(B,C) -> h3(oskc0,B,C) [negative chaining of 42 from 29] 47 : true,c(B) -> h2(B,C),o(oskc0,b) [negative chaining of 42 from 21] 49 : true,c(B) -> h2(B,C),h3(oskc0,B,C) [negative chaining of 42 from 27] 51 : c(B) -> h3(oskc0,B,C) [reduction of 49 by [44]] 57 : true,c(B),ska1,h2(B,B),c(C),h2(C,oskf0(C)),skp0(skf0(C),C) -> ska0 [negative chaining of 24 from 32] 59 : true,c(B) -> c(skf1(B)),ska1,h2(oskf1(B),oskf1(B)) [negative chaining of 9 from 30] 60 : true,o(B,b),h3(B,skf1(B),skf1(B)),c(B) -> ska1,h2(oskf1(B),oskf1(B)) [negative chaining of 22 from 30] 63 : true,h2(skf1(B),skf1(B)),c(B),o(B,g),h3(B,oskf1(B),oskf1(B)) -> ska1 [negative chaining of 11 from 33] 64 : true,c(B),o(B,g),h3(B,oskf1(B),oskf1(B)) -> c(skf1(B)),ska1 [negative chaining of 9 from 33] 65 : true,o(B,b),h3(B,skf1(B),skf1(B)),c(B),o(B,g),h3(B,oskf1(B),oskf1(B)) -> ska1 [negative chaining of 22 from 33] 71 : true,c(B),c(B) -> o(oskc0,b),o(oskc0,g) [negative chaining of 47 from 43] 98 : true,c(skf1(B)),c(B),o(B,g),h3(B,oskf1(B),oskf1(B)) -> o(oskc0,b),ska1 [negative chaining of 47 from 63] 100 : true,c(oskf1(oskc0)),c(oskc0),o(oskc0,g) -> ska1,c(skf1(oskc0)) [negative chaining of 51 from 64] 101 : o(oskc0,g) -> c(skf1(oskc0)),ska1 [reduction of 100 by [5,2]] 105 : true,ska1,c(B),c(C),h2(B,B),h2(C,oskf0(C)) -> c(skf0(C)),ska0 [negative chaining of 10 from 57] 106 : true,c(B),c(oskf1(B)) -> ska1,c(skf1(B)),o(oskc0,g) [negative chaining of 59 from 43] 108 : c(B) -> o(oskc0,g),c(skf1(B)),ska1 [reduction of 106 by [5]] 110 : true,c(B) -> ska1,c(skf1(B)),c(skf1(oskc0)),ska1 [negative chaining of 108 from 101] 111 : c(oskc0) -> c(skf1(oskc0)),ska1 [factoring on 110] 115 : ska1,c(skf1(oskc0)) [reduction of 111 by [2]] 122 : true,c(oskf1(oskc0)),c(oskc0),o(oskc0,g),o(oskc0,b),h3(oskc0,skf1(oskc0),skf1(oskc0)) -> ska1 [negative chaining of 51 from 65] 123 : h3(oskc0,skf1(oskc0),skf1(oskc0)),o(oskc0,b),o(oskc0,g) -> ska1 [reduction of 122 by [5,2]] 124 : true,c(skf1(oskc0)),o(oskc0,b),o(oskc0,g) -> ska1 [negative chaining of 51 from 123] 125 : o(oskc0,g),o(oskc0,b) -> ska1 [reduction of 124 by [115]] 132 : true,c(oskf1(oskc0)),c(oskc0),c(skf1(oskc0)),o(oskc0,g) -> ska1,o(oskc0,b) [negative chaining of 51 from 98] 133 : o(oskc0,g) -> ska1 [reduction of 132 by [5,2,115,125]] 135 : c(B) -> c(skf1(B)),ska1 [reduction of 108 by [133]] 144 : true,c(B),o(B,b),h3(B,skf1(B),skf1(B)),c(oskf1(B)) -> ska1,o(oskc0,g) [negative chaining of 60 from 43] 146 : c(B),o(B,b),h3(B,skf1(B),skf1(B)) -> ska1 [reduction of 144 by [5,133]] 147 : true,c(skf1(oskc0)),c(oskc0),o(oskc0,b) -> ska1 [negative chaining of 51 from 146] 148 : o(oskc0,b) -> ska1 [reduction of 147 by [135,2]] 149 : true,c(B) -> o(oskc0,g),ska1 [negative chaining of 71 from 148] 151 : c(B) -> ska1 [reduction of 149 by [133]] 152 : ska1 [reduction of 115 by [151]] 155 : c(B) -> h2(oskc1,B) [reduction of 34 by [152]] 158 : h2(B,C),c(D) -> h2(D,D),skp0(C,B) [reduction of 38 by [152]] 159 : skp0(skf0(B),B),h2(B,oskf0(B)),h2(C,C),c(B),c(C) -> ska0 [reduction of 57 by [152]] 160 : h2(B,B),h2(C,oskf0(C)),c(C),c(B) -> c(skf0(C)),ska0 [reduction of 105 by [152]] 164 : true,h2(skf0(B),skf0(B)),h2(B,oskf0(B)),h2(C,C),c(B),c(C) -> ska0 [negative chaining of 12 from 159] 166 : true,c(B),h2(C,skf0(C)),h2(C,oskf0(C)),h2(D,D),c(C),c(D) -> h2(B,B),ska0 [negative chaining of 158 from 159] 173 : true,c(oskc1),h2(B,oskf0(B)),c(B),c(oskc1) -> c(skf0(B)),ska0 [negative chaining of 155 from 160] 174 : c(B),h2(B,oskf0(B)) -> ska0,c(skf0(B)) [reduction of 173 by [1]] 175 : true,c(oskf0(oskc1)),c(oskc1) -> ska0,c(skf0(oskc1)) [negative chaining of 155 from 174] 176 : c(skf0(oskc1)),ska0 [reduction of 175 by [6,1]] 184 : true,c(oskf0(oskc1)),h2(B,B),c(C),c(oskc1),c(B),h2(oskc1,skf0(oskc1)) -> h2(C,C),ska0 [negative chaining of 155 from 166] 185 : h2(B,B),c(C),h2(oskc1,skf0(oskc1)),c(B) -> ska0,h2(C,C) [reduction of 184 by [6,1]] 186 : true,c(oskc1),h2(oskc1,skf0(oskc1)),c(B),c(oskc1) -> h2(B,B),ska0 [negative chaining of 155 from 185] 187 : c(B),h2(oskc1,skf0(oskc1)) -> ska0,h2(B,B) [reduction of 186 by [1]] 188 : true,c(skf0(oskc1)),c(B) -> h2(B,B),ska0 [negative chaining of 155 from 187] 189 : c(B) -> ska0,h2(B,B) [reduction of 188 by [176]] 192 : h2(skf0(B),skf0(B)),c(C),c(B),h2(B,oskf0(B)) -> ska0 [reduction of 164 by [189]] 193 : h2(skf0(B),skf0(B)),c(B),h2(B,oskf0(B)) -> ska0 [condensement of 192] 199 : true,c(skf0(B)),c(B),h2(B,oskf0(B)) -> ska0,ska0 [negative chaining of 189 from 193] 200 : true,c(oskf0(oskc1)),c(oskc1),c(skf0(oskc1)) -> ska0 [negative chaining of 155 from 199] 201 : ska0 [reduction of 200 by [6,1,176]] 202 : c(B),h2(B,B),h2(oskc2,B) -> [reduction of 28 by [201]] 203 : c(B) -> h2(B,B),h2(oskc2,B) [reduction of 18 by [201]] 211 : c(oskc2) -> h2(oskc2,oskc2) [factoring on 203] 215 : h2(oskc2,oskc2) [reduction of 211 by [3]] 216 : true,h2(oskc2,oskc2),c(oskc2) -> [negative chaining of 215 from 202] 217 : false [reduction of 216 by [215,3]] Length = 99, Depth = 39 Total time: 18350 milliseconds Number of search inferences: 115 Number of kept clauses: 131 */