%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:03:17 PM UTC 2026
% Result : Theorem 4.96s 1.11s
% Output : Proof 4.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 10
% Syntax : Number of formulae : 77 ( 18 unt; 0 def)
% Number of atoms : 235 ( 0 equ)
% Maximal formula atoms : 7 ( 3 avg)
% Number of connectives : 270 ( 112 ~; 104 |; 43 &)
% ( 5 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-1 aty)
% Number of variables : 117 ( 22 sgn 56 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f13,axiom,
( ? [W] :
( ! [Y] :
( program_not_halts2_halts3_outputs(W,Y,Y,bad)
& program_halts2_halts3_outputs(W,Y,Y,good) )
& program(W) )
=> ? [V] :
( ! [Y] :
( program_not_halts2_halts2_outputs(V,Y,bad)
& program_halts2_halts2_outputs(V,Y,good) )
& program(V) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p3) ).
fof(f13_nnf,plain,
( ? [V] :
( ! [Y] :
( program_not_halts2_halts2_outputs(V,Y,bad)
& program_halts2_halts2_outputs(V,Y,good) )
& program(V) )
| ! [W] :
( ? [Y] :
( ~ program_not_halts2_halts3_outputs(W,Y,Y,bad)
| ~ program_halts2_halts3_outputs(W,Y,Y,good) )
| ~ program(W) ) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [W,Y] :
( ( program_not_halts2_halts2_outputs(sk4,Y,bad)
& program_halts2_halts2_outputs(sk4,Y,good)
& program(sk4) )
| ~ program_not_halts2_halts3_outputs(W,sk3(W),sk3(W),bad)
| ~ program_halts2_halts3_outputs(W,sk3(W),sk3(W),good)
| ~ program(W) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4])],[f13_nnf]) ).
cnf(c36,plain,
( program(sk4)
| ~ program_not_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),bad)
| ~ program_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
fof(f11,axiom,
( ? [X] : algorithm_program_decides(X)
=> ? [W] : program_program_decides(W) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p1) ).
fof(f11_nnf,plain,
( ? [W] : program_program_decides(W)
| ! [X] : ~ algorithm_program_decides(X) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] :
( program_program_decides(sk2)
| ~ algorithm_program_decides(X) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f11_nnf]) ).
cnf(c33,plain,
( program_program_decides(sk2)
| ~ algorithm_program_decides(X0) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f15,conjecture,
~ ? [X] : algorithm_program_decides(X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this) ).
fof(f15_neg,negated_conjecture,
~ ~ ? [X] : algorithm_program_decides(X),
inference(negated_conjecture,[status(cth)],[f15]) ).
fof(f15_nnf,plain,
? [X] : algorithm_program_decides(X),
inference(nnf_transformation,[status(thm)],[f15_neg]) ).
fof(f15_sk,plain,
algorithm_program_decides(sk7),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f15_nnf]) ).
cnf(c42,plain,
algorithm_program_decides(sk7),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p46,plain,
program_program_decides(sk2),
inference(resolution,[status(thm)],[c33,c42]) ).
fof(f1,axiom,
! [X] :
( program_program_decides(X)
<=> ( program_decides(X)
& program(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',program_program_decides_def) ).
fof(f1_nnf,plain,
! [X] :
( ( ~ program_decides(X)
| ~ program(X)
| program_program_decides(X) )
& ( ( program_decides(X)
& program(X) )
| ~ program_program_decides(X) ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] :
( ( ~ program_decides(X)
| ~ program(X)
| program_program_decides(X) )
& ( ( program_decides(X)
& program(X) )
| ~ program_program_decides(X) ) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c3,plain,
( program(X0)
| ~ program_program_decides(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p47,plain,
program(sk2),
inference(resolution,[status(thm)],[p46,c3]) ).
cnf(p95,plain,
( program(sk4)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad)
| ~ program_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),good) ),
inference(resolution,[status(thm)],[c36,p47]) ).
fof(f12,axiom,
! [W] :
( program_program_decides(W)
=> ! [Y,Z] :
( program_not_halts2_halts3_outputs(W,Y,Z,bad)
& program_halts2_halts3_outputs(W,Y,Z,good) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p2) ).
fof(f12_nnf,plain,
! [W] :
( ! [Y,Z] :
( program_not_halts2_halts3_outputs(W,Y,Z,bad)
& program_halts2_halts3_outputs(W,Y,Z,good) )
| ~ program_program_decides(W) ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [W,Y,Z] :
( ( program_not_halts2_halts3_outputs(W,Y,Z,bad)
& program_halts2_halts3_outputs(W,Y,Z,good) )
| ~ program_program_decides(W) ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c34,plain,
( program_halts2_halts3_outputs(X0,X1,X2,good)
| ~ program_program_decides(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p61,plain,
program_halts2_halts3_outputs(sk2,X0,X1,good),
inference(resolution,[status(thm)],[c34,p46]) ).
cnf(p147,plain,
( program(sk4)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad) ),
inference(resolution,[status(thm)],[p95,p61]) ).
cnf(c35,plain,
( program_not_halts2_halts3_outputs(X0,X1,X2,bad)
| ~ program_program_decides(X0) ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(p62,plain,
program_not_halts2_halts3_outputs(sk2,X0,X1,bad),
inference(resolution,[status(thm)],[c35,p46]) ).
cnf(p159,plain,
program(sk4),
inference(resolution,[status(thm)],[p147,p62]) ).
fof(f14,axiom,
( ? [V] :
( ! [Y] :
( program_not_halts2_halts2_outputs(V,Y,bad)
& program_halts2_halts2_outputs(V,Y,good) )
& program(V) )
=> ? [U] :
( ! [Y] :
( program_not_halts2_halts2_outputs(U,Y,good)
& ( program_halts2(Y,Y)
=> ~ halts2(U,Y) ) )
& program(U) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p4) ).
fof(f14_nnf,plain,
( ? [U] :
( ! [Y] :
( program_not_halts2_halts2_outputs(U,Y,good)
& ( ~ halts2(U,Y)
| ~ program_halts2(Y,Y) ) )
& program(U) )
| ! [V] :
( ? [Y] :
( ~ program_not_halts2_halts2_outputs(V,Y,bad)
| ~ program_halts2_halts2_outputs(V,Y,good) )
| ~ program(V) ) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [V,Y] :
( ( program_not_halts2_halts2_outputs(sk6,Y,good)
& ( ~ halts2(sk6,Y)
| ~ program_halts2(Y,Y) )
& program(sk6) )
| ~ program_not_halts2_halts2_outputs(V,sk5(V),bad)
| ~ program_halts2_halts2_outputs(V,sk5(V),good)
| ~ program(V) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5,sk6])],[f14_nnf]) ).
cnf(c40,plain,
( ~ halts2(sk6,X1)
| ~ program_halts2(X1,X1)
| ~ program_not_halts2_halts2_outputs(X0,sk5(X0),bad)
| ~ program_halts2_halts2_outputs(X0,sk5(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p169,plain,
( ~ halts2(sk6,X0)
| ~ program_halts2(X0,X0)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad)
| ~ program_halts2_halts2_outputs(sk4,sk5(sk4),good) ),
inference(resolution,[status(thm)],[p159,c40]) ).
cnf(c37,plain,
( program_halts2_halts2_outputs(sk4,X1,good)
| ~ program_not_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),bad)
| ~ program_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p104,plain,
( program_halts2_halts2_outputs(sk4,X0,good)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad)
| ~ program_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),good) ),
inference(resolution,[status(thm)],[c37,p47]) ).
cnf(p171,plain,
( program_halts2_halts2_outputs(sk4,X0,good)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad) ),
inference(resolution,[status(thm)],[p104,p61]) ).
cnf(p210,plain,
program_halts2_halts2_outputs(sk4,X0,good),
inference(resolution,[status(thm)],[p171,p62]) ).
cnf(p462,plain,
( ~ halts2(sk6,X0)
| ~ program_halts2(X0,X0)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad) ),
inference(resolution,[status(thm)],[p169,p210]) ).
cnf(c38,plain,
( program_not_halts2_halts2_outputs(sk4,X1,bad)
| ~ program_not_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),bad)
| ~ program_halts2_halts3_outputs(X0,sk3(X0),sk3(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(p107,plain,
( program_not_halts2_halts2_outputs(sk4,X0,bad)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad)
| ~ program_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),good) ),
inference(resolution,[status(thm)],[c38,p47]) ).
cnf(p192,plain,
( program_not_halts2_halts2_outputs(sk4,X0,bad)
| ~ program_not_halts2_halts3_outputs(sk2,sk3(sk2),sk3(sk2),bad) ),
inference(resolution,[status(thm)],[p107,p61]) ).
cnf(p237,plain,
program_not_halts2_halts2_outputs(sk4,X0,bad),
inference(resolution,[status(thm)],[p192,p62]) ).
cnf(p980,plain,
( ~ halts2(sk6,X0)
| ~ program_halts2(X0,X0) ),
inference(resolution,[status(thm)],[p462,p237]) ).
cnf(c41,plain,
( program_not_halts2_halts2_outputs(sk6,X1,good)
| ~ program_not_halts2_halts2_outputs(X0,sk5(X0),bad)
| ~ program_halts2_halts2_outputs(X0,sk5(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p170,plain,
( program_not_halts2_halts2_outputs(sk6,X0,good)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad)
| ~ program_halts2_halts2_outputs(sk4,sk5(sk4),good) ),
inference(resolution,[status(thm)],[p159,c41]) ).
cnf(p475,plain,
( program_not_halts2_halts2_outputs(sk6,X0,good)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad) ),
inference(resolution,[status(thm)],[p170,p210]) ).
cnf(p648,plain,
program_not_halts2_halts2_outputs(sk6,X0,good),
inference(resolution,[status(thm)],[p475,p237]) ).
fof(f10,axiom,
! [X,Y,W] :
( program_not_halts2_halts2_outputs(X,Y,W)
<=> ( program_not_halts2(Y,Y)
=> halts2_outputs(X,Y,W) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',program_not_halts2_halts2_outputs_def) ).
fof(f10_nnf,plain,
! [X,Y,W] :
( ( ( ~ halts2_outputs(X,Y,W)
& program_not_halts2(Y,Y) )
| program_not_halts2_halts2_outputs(X,Y,W) )
& ( halts2_outputs(X,Y,W)
| ~ program_not_halts2(Y,Y)
| ~ program_not_halts2_halts2_outputs(X,Y,W) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X,Y,W] :
( ( ( ~ halts2_outputs(X,Y,W)
& program_not_halts2(Y,Y) )
| program_not_halts2_halts2_outputs(X,Y,W) )
& ( halts2_outputs(X,Y,W)
| ~ program_not_halts2(Y,Y)
| ~ program_not_halts2_halts2_outputs(X,Y,W) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c30,plain,
( halts2_outputs(X0,X1,X2)
| ~ program_not_halts2(X1,X1)
| ~ program_not_halts2_halts2_outputs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p649,plain,
( halts2_outputs(sk6,X0,good)
| ~ program_not_halts2(X0,X0) ),
inference(resolution,[status(thm)],[p648,c30]) ).
cnf(c39,plain,
( program(sk6)
| ~ program_not_halts2_halts2_outputs(X0,sk5(X0),bad)
| ~ program_halts2_halts2_outputs(X0,sk5(X0),good)
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p168,plain,
( program(sk6)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad)
| ~ program_halts2_halts2_outputs(sk4,sk5(sk4),good) ),
inference(resolution,[status(thm)],[p159,c39]) ).
cnf(p439,plain,
( program(sk6)
| ~ program_not_halts2_halts2_outputs(sk4,sk5(sk4),bad) ),
inference(resolution,[status(thm)],[p168,p210]) ).
cnf(p447,plain,
program(sk6),
inference(resolution,[status(thm)],[p439,p237]) ).
fof(f5,axiom,
! [X,Y] :
( program_not_halts2(X,Y)
<=> ( ~ halts2(X,Y)
& program(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',program_not_halts2_def) ).
fof(f5_nnf,plain,
! [X,Y] :
( ( halts2(X,Y)
| ~ program(X)
| program_not_halts2(X,Y) )
& ( ( ~ halts2(X,Y)
& program(X) )
| ~ program_not_halts2(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] :
( ( halts2(X,Y)
| ~ program(X)
| program_not_halts2(X,Y) )
& ( ( ~ halts2(X,Y)
& program(X) )
| ~ program_not_halts2(X,Y) ) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c17,plain,
( halts2(X0,X1)
| ~ program(X0)
| program_not_halts2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(p452,plain,
( halts2(sk6,X0)
| program_not_halts2(sk6,X0) ),
inference(resolution,[status(thm)],[p447,c17]) ).
cnf(p653,plain,
( halts2(sk6,sk6)
| halts2_outputs(sk6,sk6,good) ),
inference(resolution,[status(thm)],[p649,p452]) ).
fof(f6,axiom,
! [X,Y,W] :
( halts2_outputs(X,Y,W)
<=> ( outputs(X,W)
& halts2(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',halts2_outputs_def) ).
fof(f6_nnf,plain,
! [X,Y,W] :
( ( ~ outputs(X,W)
| ~ halts2(X,Y)
| halts2_outputs(X,Y,W) )
& ( ( outputs(X,W)
& halts2(X,Y) )
| ~ halts2_outputs(X,Y,W) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,W] :
( ( ~ outputs(X,W)
| ~ halts2(X,Y)
| halts2_outputs(X,Y,W) )
& ( ( outputs(X,W)
& halts2(X,Y) )
| ~ halts2_outputs(X,Y,W) ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c18,plain,
( halts2(X0,X1)
| ~ halts2_outputs(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(p678,plain,
( halts2(sk6,sk6)
| halts2(sk6,sk6) ),
inference(resolution,[status(thm)],[p653,c18]) ).
cnf(p680,plain,
halts2(sk6,sk6),
inference(factoring,[status(thm)],[p678]) ).
fof(f3,axiom,
! [X,Y] :
( program_halts2(X,Y)
<=> ( halts2(X,Y)
& program(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',program_halts2_def) ).
fof(f3_nnf,plain,
! [X,Y] :
( ( ~ halts2(X,Y)
| ~ program(X)
| program_halts2(X,Y) )
& ( ( halts2(X,Y)
& program(X) )
| ~ program_halts2(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] :
( ( ~ halts2(X,Y)
| ~ program(X)
| program_halts2(X,Y) )
& ( ( halts2(X,Y)
& program(X) )
| ~ program_halts2(X,Y) ) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c11,plain,
( ~ halts2(X0,X1)
| ~ program(X0)
| program_halts2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p451,plain,
( ~ halts2(sk6,X0)
| program_halts2(sk6,X0) ),
inference(resolution,[status(thm)],[p447,c11]) ).
cnf(p692,plain,
program_halts2(sk6,sk6),
inference(resolution,[status(thm)],[p680,p451]) ).
cnf(p996,plain,
~ halts2(sk6,sk6),
inference(resolution,[status(thm)],[p980,p692]) ).
cnf(p1009,plain,
$false,
inference(resolution,[status(thm)],[p996,p680]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.37 % Computer : n007.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Fri Sep 25 07:41:38 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.96/1.11 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.96/1.11 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------