%-------------------------------------------------------------------------- % File : COM003-1 : TPTP v2.1.0. Bugfixed v1.0.1. % Domain : Computing Theory % Problem : The halting problem is undecidable % Version : [Bur87b] axioms. % English : % Refs : [Bur87a] Burkholder (1987), The Halting Problem % : [Bur87b] Burkholder (1987), A 76th Automated Theorem Proving Pr % Source : [Bur87b] % Names : - [Bur87b] % Status : unsatisfiable % Rating : 0.89 v2.1.0, 0.00 v2.0.0 % Syntax : Number of clauses : 50 ( 32 non-Horn; 1 unit; 43 RR) % Number of literals : 275 ( 0 equality) % Maximal clause size : 7 ( 5 average) % Number of predicates : 6 ( 0 propositional; 1-3 arity) % Number of functors : 12 ( 6 constant; 0-1 arity) % Number of variables : 98 ( 7 singleton) % Maximal term depth : 2 ( 1 average) % Comments : % : tptp2X -f dfg -t rm_equality:rstfp COM003-1.p % Bugfixes : v1.0.1 - All the axiom clauses replaced. Error due % to incorrect use of formed in the conversion (my fault). %-------------------------------------------------------------------------- begin_problem(TPTP_Problem). list_of_descriptions. name({*[ File : COM003-1 : TPTP v2.1.0. Bugfixed v1.0.1.],[ Names : - [Bur87b]]*}). author({*[ Source : [Bur87b]]*}). status(unsatisfiable). description({*[ Refs : [Bur87a] Burkholder (1987), The Halting Problem, : [Bur87b] Burkholder (1987), A 76th Automated Theorem Proving Pr]*}). end_of_list. list_of_symbols. functions[(bad,0), (c1,0), (c2,0), (c3,0), (c4,0), (f1,1), (f2,1), (f3,1), (f4,1), (f5,1), (f6,1), (good,0)]. predicates[(algorithm,1), (decides,3), (halts2,2), (halts3,3), (outputs,2), (program,1)]. end_of_list. list_of_clauses(axioms,cnf). end_of_list. list_of_clauses(conjectures,cnf). clause( %(hypothesis) forall([X], or( not(algorithm(X)), program(f2(X)), program(c1))), hypothesis_1_1 ). clause( %(hypothesis) forall([X,Y,Z], or( not(algorithm(X)), not(program(Y)), program(f2(X)), decides(c1,Y,Z))), hypothesis_1_2 ). clause( %(hypothesis) forall([X], or( not(algorithm(X)), not(decides(X,f2(X),f1(X))), program(c1))), hypothesis_1_3 ). clause( %(hypothesis) forall([X,Y,Z], or( not(algorithm(X)), not(decides(X,f2(X),f1(X))), not(program(Y)), decides(c1,Y,Z))), hypothesis_1_4 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(program(Y)), not(halts2(Y,Z)), program(f4(W)), halts3(W,Y,Z))), hypothesis_2_1 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(program(Y)), not(halts2(Y,Z)), program(f4(W)), outputs(W,good))), hypothesis_2_2 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(program(Y)), program(f4(W)), halts2(Y,Z), halts3(W,Y,Z))), hypothesis_2_3 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(program(Y)), program(f4(W)), halts2(Y,Z), outputs(W,bad))), hypothesis_2_4 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(decides(W,f4(W),f3(W))), not(program(Y)), not(halts2(Y,Z)), halts3(W,Y,Z))), hypothesis_2_5 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(decides(W,f4(W),f3(W))), not(program(Y)), not(halts2(Y,Z)), outputs(W,good))), hypothesis_2_6 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(decides(W,f4(W),f3(W))), not(program(Y)), halts2(Y,Z), halts3(W,Y,Z))), hypothesis_2_7 ). clause( %(hypothesis) forall([W,Y,Z], or( not(program(W)), not(decides(W,f4(W),f3(W))), not(program(Y)), halts2(Y,Z), outputs(W,bad))), hypothesis_2_8 ). clause( %(hypothesis) forall([W], or( not(program(W)), program(f5(W)), program(c2))), hypothesis_3_1 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(program(Y)), not(halts2(Y,Y)), program(f5(W)), halts2(c2,Y))), hypothesis_3_2 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(program(Y)), not(halts2(Y,Y)), program(f5(W)), outputs(c2,good))), hypothesis_3_3 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(program(Y)), program(f5(W)), halts2(Y,Y), halts2(c2,Y))), hypothesis_3_4 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(program(Y)), program(f5(W)), halts2(Y,Y), outputs(c2,bad))), hypothesis_3_5 ). clause( %(hypothesis) forall([W], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,bad)), halts2(f5(W),f5(W)), program(c2))), hypothesis_3_6 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,bad)), not(program(Y)), not(halts2(Y,Y)), halts2(f5(W),f5(W)), halts2(c2,Y))), hypothesis_3_7 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,bad)), not(program(Y)), not(halts2(Y,Y)), halts2(f5(W),f5(W)), outputs(c2,good))), hypothesis_3_8 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,bad)), not(program(Y)), halts2(f5(W),f5(W)), halts2(Y,Y), halts2(c2,Y))), hypothesis_3_9 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,bad)), not(program(Y)), halts2(f5(W),f5(W)), halts2(Y,Y), outputs(c2,bad))), hypothesis_3_10 ). clause( %(hypothesis) forall([W], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(halts2(f5(W),f5(W))), program(c2))), hypothesis_3_11 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(halts2(f5(W),f5(W))), not(program(Y)), not(halts2(Y,Y)), halts2(c2,Y))), hypothesis_3_12 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(halts2(f5(W),f5(W))), not(program(Y)), not(halts2(Y,Y)), outputs(c2,good))), hypothesis_3_13 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(halts2(f5(W),f5(W))), not(program(Y)), halts2(Y,Y), halts2(c2,Y))), hypothesis_3_14 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(halts2(f5(W),f5(W))), not(program(Y)), halts2(Y,Y), outputs(c2,bad))), hypothesis_3_15 ). clause( %(hypothesis) forall([W], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(outputs(W,bad)), program(c2))), hypothesis_3_16 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(outputs(W,bad)), not(program(Y)), not(halts2(Y,Y)), halts2(c2,Y))), hypothesis_3_17 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(outputs(W,bad)), not(program(Y)), not(halts2(Y,Y)), outputs(c2,good))), hypothesis_3_18 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(outputs(W,bad)), not(program(Y)), halts2(Y,Y), halts2(c2,Y))), hypothesis_3_19 ). clause( %(hypothesis) forall([W,Y], or( not(program(W)), not(halts3(W,f5(W),f5(W))), not(outputs(W,good)), not(outputs(W,bad)), not(program(Y)), halts2(Y,Y), outputs(c2,bad))), hypothesis_3_20 ). clause( %(hypothesis) forall([V], or( not(program(V)), program(f6(V)), program(c3))), hypothesis_4_1 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(program(Y)), not(halts2(Y,Y)), not(halts2(c3,Y)), program(f6(V)))), hypothesis_4_2 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(program(Y)), program(f6(V)), halts2(Y,Y), halts2(c3,Y))), hypothesis_4_3 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(program(Y)), program(f6(V)), halts2(Y,Y), outputs(c3,bad))), hypothesis_4_4 ). clause( %(hypothesis) forall([V], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,bad)), halts2(f6(V),f6(V)), program(c3))), hypothesis_4_5 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,bad)), not(program(Y)), not(halts2(Y,Y)), not(halts2(c3,Y)), halts2(f6(V),f6(V)))), hypothesis_4_6 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,bad)), not(program(Y)), halts2(f6(V),f6(V)), halts2(Y,Y), halts2(c3,Y))), hypothesis_4_7 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,bad)), not(program(Y)), halts2(f6(V),f6(V)), halts2(Y,Y), outputs(c3,bad))), hypothesis_4_8 ). clause( %(hypothesis) forall([V], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(halts2(f6(V),f6(V))), program(c3))), hypothesis_4_9 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(halts2(f6(V),f6(V))), not(program(Y)), not(halts2(Y,Y)), not(halts2(c3,Y)))), hypothesis_4_10 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(halts2(f6(V),f6(V))), not(program(Y)), halts2(Y,Y), halts2(c3,Y))), hypothesis_4_11 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(halts2(f6(V),f6(V))), not(program(Y)), halts2(Y,Y), outputs(c3,bad))), hypothesis_4_12 ). clause( %(hypothesis) forall([V], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(outputs(V,bad)), program(c3))), hypothesis_4_13 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(outputs(V,bad)), not(program(Y)), not(halts2(Y,Y)), not(halts2(c3,Y)))), hypothesis_4_14 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(outputs(V,bad)), not(program(Y)), halts2(Y,Y), halts2(c3,Y))), hypothesis_4_15 ). clause( %(hypothesis) forall([V,Y], or( not(program(V)), not(halts2(V,f6(V))), not(outputs(V,good)), not(outputs(V,bad)), not(program(Y)), halts2(Y,Y), outputs(c3,bad))), hypothesis_4_17 ). clause( %(conjecture) or( algorithm(c4)), a_deciding_algorithm ). clause( %(conjecture) forall([Y1,Z1], or( not(program(Y1)), decides(c4,Y1,Z1))), prove_the_algorithm_doesnt_exist ). end_of_list. list_of_general_settings. hypothesis[hypothesis_1_1,hypothesis_1_2,hypothesis_1_3,hypothesis_1_4,hypothesis_2_1,hypothesis_2_2,hypothesis_2_3,hypothesis_2_4,hypothesis_2_5,hypothesis_2_6,hypothesis_2_7,hypothesis_2_8,hypothesis_3_1,hypothesis_3_2,hypothesis_3_3,hypothesis_3_4,hypothesis_3_5,hypothesis_3_6,hypothesis_3_7,hypothesis_3_8,hypothesis_3_9,hypothesis_3_10,hypothesis_3_11,hypothesis_3_12,hypothesis_3_13,hypothesis_3_14,hypothesis_3_15,hypothesis_3_16,hypothesis_3_17,hypothesis_3_18,hypothesis_3_19,hypothesis_3_20,hypothesis_4_1,hypothesis_4_2,hypothesis_4_3,hypothesis_4_4,hypothesis_4_5,hypothesis_4_6,hypothesis_4_7,hypothesis_4_8,hypothesis_4_9,hypothesis_4_10,hypothesis_4_11,hypothesis_4_12,hypothesis_4_13,hypothesis_4_14,hypothesis_4_15,hypothesis_4_17]. end_of_list. end_problem. %--------------------------------------------------------------------------