%--------------------------------------------------------------------------
% File     : COM003+1 : TPTP v2.1.0. Released v2.0.0.
% 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   : theorem
% Rating   : ? v2.0.0
% Syntax   : Number of formulae    :    5 (   0 unit)
%            Number of atoms       :   55 (   0 equality)
%            Maximal formula depth :    9 (   8 average)
%            Number of connectives :   57 (   7 ~  ;   0  |;  32  &)
%                                         (   0 <=>;  18 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    6 (   0 propositional; 1-3 arity)
%            Number of functors    :    2 (   2 constant; 0-0 arity)
%            Number of variables   :   16 (   0 singleton;  15 !;   7 ?)
%            Maximal term depth    :    1 (   1 average)

% Comments : 
%          : tptp2X -f dfg -t rm_equality:rstfp COM003+1.p 
%--------------------------------------------------------------------------

begin_problem(TPTP_Problem).

list_of_descriptions.
name({*[ File     : COM003+1 : TPTP v2.1.0. Released v2.0.0.],[ 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), (good,0)].
predicates[(algorithm,1), (decides,3), (halts2,2), (halts3,3), (outputs,2), (program,1)].
end_of_list.

list_of_formulae(axioms).

formula(
 implies(
  exists([X],
   and(
    algorithm(X),
    forall([Y],
     implies(
      program(Y),
      forall([Z],
       decides(X,Y,Z)))))),
  exists([W],
   and(
    program(W),
    forall([Y],
     implies(
      program(Y),
      forall([Z],
       decides(W,Y,Z))))))),
p1 ).

formula(
 forall([W],
  implies(
   and(
    program(W),
    forall([Y],
     implies(
      program(Y),
      forall([Z],
       decides(W,Y,Z))))),
   forall([Y,Z],
    and(
     implies(
      and(
       program(Y),
       halts2(Y,Z)),
      and(
       halts3(W,Y,Z),
       outputs(W,good))),
     implies(
      and(
       program(Y),
       not(
        halts2(Y,Z))),
      and(
       halts3(W,Y,Z),
       outputs(W,bad))))))),
p2 ).

formula(
 implies(
  exists([W],
   and(
    program(W),
    forall([Y],
     and(
      implies(
       and(
        program(Y),
        halts2(Y,Y)),
       and(
        halts3(W,Y,Y),
        outputs(W,good))),
      implies(
       and(
        program(Y),
        not(
         halts2(Y,Y))),
       and(
        halts3(W,Y,Y),
        outputs(W,bad))))))),
  exists([V],
   and(
    program(V),
    forall([Y],
     and(
      implies(
       and(
        program(Y),
        halts2(Y,Y)),
       and(
        halts2(V,Y),
        outputs(V,good))),
      implies(
       and(
        program(Y),
        not(
         halts2(Y,Y))),
       and(
        halts2(V,Y),
        outputs(V,bad)))))))),
p3 ).

formula(
 implies(
  exists([V],
   and(
    program(V),
    forall([Y],
     and(
      implies(
       and(
        program(Y),
        halts2(Y,Y)),
       and(
        halts2(V,Y),
        outputs(V,good))),
      implies(
       and(
        program(Y),
        not(
         halts2(Y,Y))),
       and(
        halts2(V,Y),
        outputs(V,bad))))))),
  exists([U],
   and(
    program(U),
    forall([Y],
     and(
      implies(
       and(
        program(Y),
        halts2(Y,Y)),
       not(
        halts2(U,Y))),
      implies(
       and(
        program(Y),
        not(
         halts2(Y,Y))),
       and(
        halts2(U,Y),
        outputs(U,bad)))))))),
p4 ).

end_of_list.

list_of_formulae(conjectures).

formula(  %(conjecture)
 not(
  exists([X1],
   and(
    algorithm(X1),
    forall([Y1],
     implies(
      program(Y1),
      forall([Z1],
       decides(X1,Y1,Z1))))))),
prove_this ).

end_of_list.

end_problem.
%--------------------------------------------------------------------------