%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 : Sun Sep 27 06:59:26 AM UTC 2026
% Result : Theorem 0.12s 0.38s
% Output : CNFRefutation 0.12s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 10
% Syntax : Number of formulae : 70 ( 18 unt; 0 def)
% Number of atoms : 207 ( 0 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 255 ( 118 ~; 101 |; 25 &)
% ( 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 : 108 ( 30 sgn 39 !; 14 ?)
% Comments :
%------------------------------------------------------------------------------
fof(program_program_decides_def,axiom,
! [X] :
( program_program_decides(X)
<=> ( program_decides(X)
& program(X) ) ),
file('theBenchmark.p',program_program_decides_def) ).
fof(program_halts2_def,axiom,
! [X,Y] :
( program_halts2(X,Y)
<=> ( halts2(X,Y)
& program(X) ) ),
file('theBenchmark.p',program_halts2_def) ).
fof(program_not_halts2_def,axiom,
! [X,Y] :
( program_not_halts2(X,Y)
<=> ( ~ halts2(X,Y)
& program(X) ) ),
file('theBenchmark.p',program_not_halts2_def) ).
fof(halts2_outputs_def,axiom,
! [X,Y,W] :
( halts2_outputs(X,Y,W)
<=> ( outputs(X,W)
& halts2(X,Y) ) ),
file('theBenchmark.p',halts2_outputs_def) ).
fof(program_not_halts2_halts2_outputs_def,axiom,
! [X,Y,W] :
( program_not_halts2_halts2_outputs(X,Y,W)
<=> ( program_not_halts2(Y,Y)
=> halts2_outputs(X,Y,W) ) ),
file('theBenchmark.p',program_not_halts2_halts2_outputs_def) ).
fof(p1,axiom,
( ? [X] : algorithm_program_decides(X)
=> ? [W] : program_program_decides(W) ),
file('theBenchmark.p',p1) ).
fof(p2,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('theBenchmark.p',p2) ).
fof(p3,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('theBenchmark.p',p3) ).
fof(p4,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('theBenchmark.p',p4) ).
fof(prove_this,conjecture,
~ ? [X] : algorithm_program_decides(X),
file('theBenchmark.p',prove_this) ).
fof(prove_this_neg,negated_conjecture,
~ ~ ? [X] : algorithm_program_decides(X),
inference(assume_negation,[status(cth)],[prove_this]) ).
cnf(c_29,plain,
( program_not_halts2_halts3_outputs(A,B,C,bad)
| ~ program_program_decides(A) ),
inference(clausify,[status(thm)],[p2]) ).
cnf(c_30,plain,
( program_halts2_halts3_outputs(A,B,C,good)
| ~ program_program_decides(A) ),
inference(clausify,[status(thm)],[p2]) ).
fof(nnf_12,plain,
( ? [W] : program_program_decides(W)
| ! [X] : ~ algorithm_program_decides(X) ),
inference(fof_nnf,[status(thm)],[p1]) ).
fof(sk_p1_sk,plain,
( program_program_decides(sK0)
| ! [X] : ~ algorithm_program_decides(X) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(W,sK0)],[nnf_12]) ).
fof(sk_p1,plain,
! [VAR_0] :
( program_program_decides(sK0)
| ~ algorithm_program_decides(VAR_0) ),
inference(cnf_transformation,[status(thm)],[sk_p1_sk]) ).
cnf(c_31,plain,
( program_program_decides(sK0)
| ~ algorithm_program_decides(A) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_32,plain,
( program(A)
| ~ program_program_decides(A) ),
inference(clausify,[status(thm)],[program_program_decides_def]) ).
fof(nnf_16,plain,
? [X] : algorithm_program_decides(X),
inference(fof_nnf,[status(thm)],[prove_this_neg]) ).
fof(sk_prove_this_neg,plain,
algorithm_program_decides(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X,sK1)],[nnf_16]) ).
cnf(c_39,negated_conjecture,
algorithm_program_decides(sK1),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
cnf(c_44,plain,
( program_halts2_halts3_outputs(sK0,B,C,good)
| ~ algorithm_program_decides(A) ),
inference(resolve,[status(thm)],[c_31,c_30]) ).
cnf(c_45,plain,
( program_not_halts2_halts3_outputs(sK0,B,C,bad)
| ~ algorithm_program_decides(A) ),
inference(resolve,[status(thm)],[c_31,c_29]) ).
cnf(c_47,plain,
( ~ algorithm_program_decides(A)
| program(sK0) ),
inference(resolve,[status(thm)],[c_32,c_31]) ).
cnf(c_48,plain,
( ~ halts2(A,B)
| ~ program(A)
| program_halts2(A,B) ),
inference(clausify,[status(thm)],[program_halts2_def]) ).
fof(nnf_15,plain,
( ? [U] :
( ! [Y] :
( program_not_halts2_halts2_outputs(U,Y,good)
& ( ~ halts2(U,Y)
| ~ program_halts2(Y,Y) ) )
& program(U) )
| ! [V] :
( ? [X0] :
( ~ program_not_halts2_halts2_outputs(V,X0,bad)
| ~ program_halts2_halts2_outputs(V,X0,good) )
| ~ program(V) ) ),
inference(fof_nnf,[status(thm)],[p4]) ).
fof(sk_p4_sk,plain,
( ( ! [Y] :
( program_not_halts2_halts2_outputs(sK3,Y,good)
& ( ~ halts2(sK3,Y)
| ~ program_halts2(Y,Y) ) )
& program(sK3) )
| ! [V] :
( ~ program_not_halts2_halts2_outputs(V,sK2(V),bad)
| ~ program_halts2_halts2_outputs(V,sK2(V),good)
| ~ program(V) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3]),skolemize(X0,sK2(V)),skolemize(U,sK3)],[nnf_15]) ).
fof(sk_p4,plain,
( ! [VAR_0,VAR_1] :
( program_not_halts2_halts2_outputs(sK3,VAR_1,good)
| ~ program_not_halts2_halts2_outputs(VAR_0,sK2(VAR_0),bad)
| ~ program_halts2_halts2_outputs(VAR_0,sK2(VAR_0),good)
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ halts2(sK3,VAR_1)
| ~ program_halts2(VAR_1,VAR_1)
| ~ program_not_halts2_halts2_outputs(VAR_0,sK2(VAR_0),bad)
| ~ program_halts2_halts2_outputs(VAR_0,sK2(VAR_0),good)
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK3)
| ~ program_not_halts2_halts2_outputs(VAR_0,sK2(VAR_0),bad)
| ~ program_halts2_halts2_outputs(VAR_0,sK2(VAR_0),good)
| ~ program(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_p4_sk]) ).
cnf(c_55,plain,
( ~ halts2(sK3,B)
| ~ program_halts2(B,B)
| ~ program_not_halts2_halts2_outputs(A,sK2(A),bad)
| ~ program_halts2_halts2_outputs(A,sK2(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p4]) ).
cnf(c_128,negated_conjecture,
program(sK0),
inference(resolve,[status(thm)],[c_47,c_39]) ).
cnf(c_130,negated_conjecture,
program_not_halts2_halts3_outputs(sK0,A,B,bad),
inference(resolve,[status(thm)],[c_45,c_39]) ).
cnf(c_131,negated_conjecture,
program_halts2_halts3_outputs(sK0,A,B,good),
inference(resolve,[status(thm)],[c_44,c_39]) ).
cnf(c_141,plain,
( halts2(A,B)
| ~ program(A)
| program_not_halts2(A,B) ),
inference(clausify,[status(thm)],[program_not_halts2_def]) ).
cnf(c_142,plain,
( halts2(A,B)
| ~ halts2_outputs(A,B,C) ),
inference(clausify,[status(thm)],[halts2_outputs_def]) ).
cnf(c_145,plain,
( halts2_outputs(A,B,C)
| ~ program_not_halts2(B,B)
| ~ program_not_halts2_halts2_outputs(A,B,C) ),
inference(clausify,[status(thm)],[program_not_halts2_halts2_outputs_def]) ).
fof(nnf_14,plain,
( ? [V] :
( ! [Y] :
( program_not_halts2_halts2_outputs(V,Y,bad)
& program_halts2_halts2_outputs(V,Y,good) )
& program(V) )
| ! [W] :
( ? [X0] :
( ~ program_not_halts2_halts3_outputs(W,X0,X0,bad)
| ~ program_halts2_halts3_outputs(W,X0,X0,good) )
| ~ program(W) ) ),
inference(fof_nnf,[status(thm)],[p3]) ).
fof(sk_p3_sk,plain,
( ( ! [Y] :
( program_not_halts2_halts2_outputs(sK5,Y,bad)
& program_halts2_halts2_outputs(sK5,Y,good) )
& program(sK5) )
| ! [W] :
( ~ program_not_halts2_halts3_outputs(W,sK4(W),sK4(W),bad)
| ~ program_halts2_halts3_outputs(W,sK4(W),sK4(W),good)
| ~ program(W) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4(W)),skolemize(V,sK5)],[nnf_14]) ).
fof(sk_p3,plain,
( ! [VAR_0,VAR_1] :
( program_not_halts2_halts2_outputs(sK5,VAR_1,bad)
| ~ program_not_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),bad)
| ~ program_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),good)
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( program_halts2_halts2_outputs(sK5,VAR_1,good)
| ~ program_not_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),bad)
| ~ program_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),good)
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK5)
| ~ program_not_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),bad)
| ~ program_halts2_halts3_outputs(VAR_0,sK4(VAR_0),sK4(VAR_0),good)
| ~ program(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_p3_sk]) ).
cnf(c_148,plain,
( program(sK5)
| ~ program_not_halts2_halts3_outputs(A,sK4(A),sK4(A),bad)
| ~ program_halts2_halts3_outputs(A,sK4(A),sK4(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_149,plain,
( program_halts2_halts2_outputs(sK5,B,good)
| ~ program_not_halts2_halts3_outputs(A,sK4(A),sK4(A),bad)
| ~ program_halts2_halts3_outputs(A,sK4(A),sK4(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_150,plain,
( program_not_halts2_halts2_outputs(sK5,B,bad)
| ~ program_not_halts2_halts3_outputs(A,sK4(A),sK4(A),bad)
| ~ program_halts2_halts3_outputs(A,sK4(A),sK4(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_151,plain,
( program(sK3)
| ~ program_not_halts2_halts2_outputs(A,sK2(A),bad)
| ~ program_halts2_halts2_outputs(A,sK2(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p4]) ).
cnf(c_152,plain,
( program_not_halts2_halts2_outputs(sK3,B,good)
| ~ program_not_halts2_halts2_outputs(A,sK2(A),bad)
| ~ program_halts2_halts2_outputs(A,sK2(A),good)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p4]) ).
cnf(c_164,plain,
( ~ halts2(B,B)
| ~ program(B)
| ~ halts2(sK3,B)
| ~ program_not_halts2_halts2_outputs(A,sK2(A),bad)
| ~ program_halts2_halts2_outputs(A,sK2(A),good)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_55,c_48]) ).
cnf(c_290,negated_conjecture,
( program(sK5)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good)
| ~ program(sK0) ),
inference(resolve,[status(thm)],[c_148,c_130]) ).
cnf(c_291,negated_conjecture,
( program(sK5)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good) ),
inference(resolve,[status(thm)],[c_128,c_290]) ).
cnf(c_215,negated_conjecture,
program(sK5),
inference(resolve,[status(thm)],[c_131,c_291]) ).
cnf(c_292,negated_conjecture,
( program_halts2_halts2_outputs(sK5,A,good)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good)
| ~ program(sK0) ),
inference(resolve,[status(thm)],[c_149,c_130]) ).
cnf(c_293,negated_conjecture,
( program_halts2_halts2_outputs(sK5,A,good)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good) ),
inference(resolve,[status(thm)],[c_128,c_292]) ).
cnf(c_217,negated_conjecture,
program_halts2_halts2_outputs(sK5,A,good),
inference(resolve,[status(thm)],[c_131,c_293]) ).
cnf(c_294,negated_conjecture,
( program_not_halts2_halts2_outputs(sK5,A,bad)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good)
| ~ program(sK0) ),
inference(resolve,[status(thm)],[c_150,c_130]) ).
cnf(c_295,negated_conjecture,
( program_not_halts2_halts2_outputs(sK5,A,bad)
| ~ program_halts2_halts3_outputs(sK0,sK4(sK0),sK4(sK0),good) ),
inference(resolve,[status(thm)],[c_128,c_294]) ).
cnf(c_219,negated_conjecture,
program_not_halts2_halts2_outputs(sK5,A,bad),
inference(resolve,[status(thm)],[c_131,c_295]) ).
cnf(c_296,plain,
( ~ halts2(A,A)
| ~ program(A)
| ~ halts2(sK3,A)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good)
| ~ program(sK5) ),
inference(resolve,[status(thm)],[c_219,c_164]) ).
cnf(c_297,plain,
( ~ halts2(A,A)
| ~ program(A)
| ~ halts2(sK3,A)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good) ),
inference(resolve,[status(thm)],[c_215,c_296]) ).
cnf(c_265,plain,
( ~ halts2(A,A)
| ~ program(A)
| ~ halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_217,c_297]) ).
cnf(c_298,plain,
( program_not_halts2_halts2_outputs(sK3,A,good)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good)
| ~ program(sK5) ),
inference(resolve,[status(thm)],[c_219,c_152]) ).
cnf(c_299,plain,
( program_not_halts2_halts2_outputs(sK3,A,good)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good) ),
inference(resolve,[status(thm)],[c_215,c_298]) ).
cnf(c_268,plain,
program_not_halts2_halts2_outputs(sK3,A,good),
inference(resolve,[status(thm)],[c_217,c_299]) ).
cnf(c_300,plain,
( program(sK3)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good)
| ~ program(sK5) ),
inference(resolve,[status(thm)],[c_219,c_151]) ).
cnf(c_301,plain,
( program(sK3)
| ~ program_halts2_halts2_outputs(sK5,sK2(sK5),good) ),
inference(resolve,[status(thm)],[c_215,c_300]) ).
cnf(c_269,plain,
program(sK3),
inference(resolve,[status(thm)],[c_217,c_301]) ).
cnf(c_302,plain,
( ~ program(sK3)
| ~ halts2(sK3,sK3) ),
inference(factor,[status(thm)],[c_265]) ).
cnf(c_271,plain,
~ halts2(sK3,sK3),
inference(resolve,[status(thm)],[c_269,c_302]) ).
cnf(c_280,plain,
~ halts2_outputs(sK3,sK3,A),
inference(resolve,[status(thm)],[c_142,c_271]) ).
cnf(c_303,plain,
( halts2_outputs(sK3,A,good)
| ~ program_not_halts2(A,A) ),
inference(resolve,[status(thm)],[c_145,c_268]) ).
cnf(c_286,plain,
~ program_not_halts2(sK3,sK3),
inference(resolve,[status(thm)],[c_303,c_280]) ).
cnf(c_304,plain,
( halts2(sK3,sK3)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_141,c_286]) ).
cnf(c_305,plain,
~ program(sK3),
inference(resolve,[status(thm)],[c_304,c_271]) ).
cnf(c_289,plain,
$false,
inference(resolve,[status(thm)],[c_269,c_305]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM003+2 : TPTP v9.3.1. Bugfixed v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 23:19:30 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 1405481 was started by sandbox2 on n009,
% 0.08/0.35 % Sat Sep 26 23:19:30 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.12/0.36
% 0.12/0.36 % From the command line: assign(max_seconds, 300).
% 0.12/0.38
% 0.12/0.38 % SZS status Theorem for theBenchmark
% 0.12/0.38
% 0.12/0.38 % Proof 1 at 0.01 (+ 0.00) seconds.
% 0.12/0.38 % Length of proof is 42.
% 0.12/0.38 % Level of proof is 9.
% 0.12/0.38 % Maximum clause weight is 30.000.
% 0.12/0.38 % Given clauses 98.
% 0.12/0.38
% 0.12/0.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------