%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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 1.64s 0.68s
% Output : CNFRefutation 1.64s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(p1,axiom,
( ? [X] :
( ! [Y] :
( program(Y)
=> ! [Z] : decides(X,Y,Z) )
& algorithm(X) )
=> ? [W] :
( ! [Y] :
( program(Y)
=> ! [Z] : decides(W,Y,Z) )
& program(W) ) ),
file('theBenchmark.p',p1) ).
fof(p2,axiom,
! [W] :
( ( ! [Y] :
( program(Y)
=> ! [Z] : decides(W,Y,Z) )
& program(W) )
=> ! [Y,Z] :
( ( ( ~ halts2(Y,Z)
& program(Y) )
=> ( outputs(W,bad)
& halts3(W,Y,Z) ) )
& ( ( halts2(Y,Z)
& program(Y) )
=> ( outputs(W,good)
& halts3(W,Y,Z) ) ) ) ),
file('theBenchmark.p',p2) ).
fof(p3,axiom,
! [W] :
( ( ! [Y,Z] :
( ( ( ~ halts2(Y,Z)
& program(Y) )
=> ( outputs(W,bad)
& halts3(W,Y,Z) ) )
& ( ( halts2(Y,Z)
& program(Y) )
=> ( outputs(W,good)
& halts3(W,Y,Z) ) ) )
& program(W) )
=> ? [V] :
( ! [Y] :
( ( ( outputs(W,bad)
& halts3(W,Y,Y)
& program(Y) )
=> ( outputs(V,bad)
& halts2(V,Y) ) )
& ( ( outputs(W,good)
& halts3(W,Y,Y)
& program(Y) )
=> ~ halts2(V,Y) ) )
& program(V) ) ),
file('theBenchmark.p',p3) ).
fof(prove_this,conjecture,
~ ? [X1] :
( ! [Y1] :
( program(Y1)
=> ! [Z1] : decides(X1,Y1,Z1) )
& algorithm(X1) ),
file('theBenchmark.p',prove_this) ).
fof(prove_this_neg,negated_conjecture,
~ ~ ? [X1] :
( ! [Y1] :
( program(Y1)
=> ! [Z1] : decides(X1,Y1,Z1) )
& algorithm(X1) ),
inference(assume_negation,[status(cth)],[prove_this]) ).
fof(nnf_4,plain,
? [X1] :
( ! [Y1] :
( ! [Z1] : decides(X1,Y1,Z1)
| ~ program(Y1) )
& algorithm(X1) ),
inference(fof_nnf,[status(thm)],[prove_this_neg]) ).
fof(sk_prove_this_neg_sk,plain,
( ! [Y1] :
( ! [Z1] : decides(sK0,Y1,Z1)
| ~ program(Y1) )
& algorithm(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X1,sK0)],[nnf_4]) ).
fof(sk_prove_this_neg,plain,
( ! [VAR_0,VAR_1] :
( decides(sK0,VAR_0,VAR_1)
| ~ program(VAR_0) )
& algorithm(sK0) ),
inference(cnf_transformation,[status(thm)],[sk_prove_this_neg_sk]) ).
cnf(c_5,negated_conjecture,
algorithm(sK0),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
fof(nnf_1,plain,
( ? [W] :
( ! [Y] :
( ! [Z] : decides(W,Y,Z)
| ~ program(Y) )
& program(W) )
| ! [X] :
( ? [X0] :
( ? [X2] : ~ decides(X,X0,X2)
& program(X0) )
| ~ algorithm(X) ) ),
inference(fof_nnf,[status(thm)],[p1]) ).
fof(sk_p1_sk,plain,
( ( ! [Y] :
( ! [Z] : decides(sK3,Y,Z)
| ~ program(Y) )
& program(sK3) )
| ! [X] :
( ( ~ decides(X,sK1(X),sK2(X))
& program(sK1(X)) )
| ~ algorithm(X) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2,sK3]),skolemize(X0,sK1(X)),skolemize(X2,sK2(X)),skolemize(W,sK3)],[nnf_1]) ).
fof(sk_p1,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( decides(sK3,VAR_1,VAR_2)
| ~ program(VAR_1)
| ~ decides(VAR_0,sK1(VAR_0),sK2(VAR_0))
| ~ algorithm(VAR_0) )
& ! [VAR_0] :
( program(sK3)
| ~ decides(VAR_0,sK1(VAR_0),sK2(VAR_0))
| ~ algorithm(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( decides(sK3,VAR_1,VAR_2)
| ~ program(VAR_1)
| program(sK1(VAR_0))
| ~ algorithm(VAR_0) )
& ! [VAR_0] :
( program(sK3)
| program(sK1(VAR_0))
| ~ algorithm(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_p1_sk]) ).
cnf(c_6,plain,
( decides(sK3,B,C)
| ~ program(B)
| ~ decides(A,sK1(A),sK2(A))
| ~ algorithm(A) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_7,plain,
( program(sK3)
| ~ decides(A,sK1(A),sK2(A))
| ~ algorithm(A) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_8,plain,
( decides(sK3,B,C)
| ~ program(B)
| program(sK1(A))
| ~ algorithm(A) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_9,plain,
( program(sK3)
| program(sK1(A))
| ~ algorithm(A) ),
inference(split_conjunct,[status(thm)],[sk_p1]) ).
cnf(c_10,negated_conjecture,
( program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_9]) ).
cnf(c_11,negated_conjecture,
( decides(sK3,A,B)
| ~ program(A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_8]) ).
cnf(c_12,negated_conjecture,
( program(sK3)
| ~ decides(sK0,sK1(sK0),sK2(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_7]) ).
cnf(c_13,negated_conjecture,
( decides(sK3,A,B)
| ~ program(A)
| ~ decides(sK0,sK1(sK0),sK2(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_6]) ).
cnf(c_14,negated_conjecture,
( decides(sK0,A,B)
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_prove_this_neg]) ).
fof(nnf_3,plain,
! [W] :
( ? [V] :
( ! [Y] :
( ( ( outputs(V,bad)
& halts2(V,Y) )
| ~ outputs(W,bad)
| ~ halts3(W,Y,Y)
| ~ program(Y) )
& ( ~ halts2(V,Y)
| ~ outputs(W,good)
| ~ halts3(W,Y,Y)
| ~ program(Y) ) )
& program(V) )
| ? [X0,Z] :
( ( ( ~ outputs(W,bad)
| ~ halts3(W,X0,Z) )
& ~ halts2(X0,Z)
& program(X0) )
| ( ( ~ outputs(W,good)
| ~ halts3(W,X0,Z) )
& halts2(X0,Z)
& program(X0) ) )
| ~ program(W) ),
inference(fof_nnf,[status(thm)],[p3]) ).
fof(sk_p3_sk,plain,
! [W] :
( ( ! [Y] :
( ( ( outputs(sK6(W),bad)
& halts2(sK6(W),Y) )
| ~ outputs(W,bad)
| ~ halts3(W,Y,Y)
| ~ program(Y) )
& ( ~ halts2(sK6(W),Y)
| ~ outputs(W,good)
| ~ halts3(W,Y,Y)
| ~ program(Y) ) )
& program(sK6(W)) )
| ( ( ~ outputs(W,bad)
| ~ halts3(W,sK4(W),sK5(W)) )
& ~ halts2(sK4(W),sK5(W))
& program(sK4(W)) )
| ( ( ~ outputs(W,good)
| ~ halts3(W,sK4(W),sK5(W)) )
& halts2(sK4(W),sK5(W))
& program(sK4(W)) )
| ~ program(W) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5,sK6]),skolemize(X0,sK4(W)),skolemize(Z,sK5(W)),skolemize(V,sK6(W))],[nnf_3]) ).
fof(sk_p3,plain,
( ! [VAR_0,VAR_1] :
( outputs(sK6(VAR_0),bad)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ outputs(VAR_0,bad)
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( halts2(sK6(VAR_0),VAR_1)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ outputs(VAR_0,bad)
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ halts2(sK6(VAR_0),VAR_1)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ outputs(VAR_0,bad)
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK6(VAR_0))
| ~ outputs(VAR_0,bad)
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ halts2(sK6(VAR_0),VAR_1)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ halts2(sK4(VAR_0),sK5(VAR_0))
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK6(VAR_0))
| ~ halts2(sK4(VAR_0),sK5(VAR_0))
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( outputs(sK6(VAR_0),bad)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ outputs(VAR_0,bad)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| halts2(sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( halts2(sK6(VAR_0),VAR_1)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| ~ outputs(VAR_0,bad)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| halts2(sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK6(VAR_0))
| ~ outputs(VAR_0,bad)
| ~ halts3(VAR_0,sK4(VAR_0),sK5(VAR_0))
| halts2(sK4(VAR_0),sK5(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( outputs(sK6(VAR_0),bad)
| ~ outputs(VAR_0,bad)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| program(sK4(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( halts2(sK6(VAR_0),VAR_1)
| ~ outputs(VAR_0,bad)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| program(sK4(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ halts2(sK6(VAR_0),VAR_1)
| ~ outputs(VAR_0,good)
| ~ halts3(VAR_0,VAR_1,VAR_1)
| ~ program(VAR_1)
| program(sK4(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0] :
( program(sK6(VAR_0))
| program(sK4(VAR_0))
| ~ program(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_p3_sk]) ).
cnf(c_16,plain,
( halts2(sK6(A),B)
| ~ halts3(A,B,B)
| ~ program(B)
| ~ outputs(A,bad)
| ~ outputs(A,good)
| ~ halts3(A,sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_17,plain,
( ~ halts2(sK6(A),B)
| ~ halts3(A,B,B)
| ~ program(B)
| ~ outputs(A,bad)
| ~ outputs(A,good)
| ~ halts3(A,sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_19,plain,
( ~ halts2(sK6(A),B)
| ~ halts3(A,B,B)
| ~ program(B)
| ~ halts2(sK4(A),sK5(A))
| ~ outputs(A,good)
| ~ halts3(A,sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_20,plain,
( program(sK6(A))
| ~ halts2(sK4(A),sK5(A))
| ~ outputs(A,good)
| ~ halts3(A,sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_22,plain,
( halts2(sK6(A),B)
| ~ halts3(A,B,B)
| ~ program(B)
| ~ outputs(A,bad)
| ~ halts3(A,sK4(A),sK5(A))
| halts2(sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_23,plain,
( program(sK6(A))
| ~ outputs(A,bad)
| ~ halts3(A,sK4(A),sK5(A))
| halts2(sK4(A),sK5(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_25,plain,
( halts2(sK6(A),B)
| ~ outputs(A,bad)
| ~ halts3(A,B,B)
| ~ program(B)
| program(sK4(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_26,plain,
( ~ halts2(sK6(A),B)
| ~ outputs(A,good)
| ~ halts3(A,B,B)
| ~ program(B)
| program(sK4(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
cnf(c_27,plain,
( program(sK6(A))
| program(sK4(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p3]) ).
fof(nnf_2,plain,
! [W] :
( ! [Y,Z] :
( ( ( outputs(W,bad)
& halts3(W,Y,Z) )
| halts2(Y,Z)
| ~ program(Y) )
& ( ( outputs(W,good)
& halts3(W,Y,Z) )
| ~ halts2(Y,Z)
| ~ program(Y) ) )
| ? [X0] :
( ? [X2] : ~ decides(W,X0,X2)
& program(X0) )
| ~ program(W) ),
inference(fof_nnf,[status(thm)],[p2]) ).
fof(sk_p2_sk,plain,
! [W] :
( ! [Y,Z] :
( ( ( outputs(W,bad)
& halts3(W,Y,Z) )
| halts2(Y,Z)
| ~ program(Y) )
& ( ( outputs(W,good)
& halts3(W,Y,Z) )
| ~ halts2(Y,Z)
| ~ program(Y) ) )
| ( ~ decides(W,sK7(W),sK8(W))
& program(sK7(W)) )
| ~ program(W) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7,sK8]),skolemize(X0,sK7(W)),skolemize(X2,sK8(W))],[nnf_2]) ).
fof(sk_p2,plain,
( ! [VAR_0,VAR_1,VAR_2] :
( outputs(VAR_0,bad)
| halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| ~ decides(VAR_0,sK7(VAR_0),sK8(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( halts3(VAR_0,VAR_1,VAR_2)
| halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| ~ decides(VAR_0,sK7(VAR_0),sK8(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( outputs(VAR_0,good)
| ~ halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| ~ decides(VAR_0,sK7(VAR_0),sK8(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( halts3(VAR_0,VAR_1,VAR_2)
| ~ halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| ~ decides(VAR_0,sK7(VAR_0),sK8(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( outputs(VAR_0,bad)
| halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| program(sK7(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( halts3(VAR_0,VAR_1,VAR_2)
| halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| program(sK7(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( outputs(VAR_0,good)
| ~ halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| program(sK7(VAR_0))
| ~ program(VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( halts3(VAR_0,VAR_1,VAR_2)
| ~ halts2(VAR_1,VAR_2)
| ~ program(VAR_1)
| program(sK7(VAR_0))
| ~ program(VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_p2_sk]) ).
cnf(c_28,plain,
( outputs(A,bad)
| halts2(B,C)
| ~ program(B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_29,plain,
( halts3(A,B,C)
| halts2(B,C)
| ~ program(B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_30,plain,
( outputs(A,good)
| ~ halts2(B,C)
| ~ program(B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_31,plain,
( halts3(A,B,C)
| ~ halts2(B,C)
| ~ program(B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_32,plain,
( outputs(A,bad)
| halts2(B,C)
| ~ program(B)
| program(sK7(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_33,plain,
( halts3(A,B,C)
| halts2(B,C)
| ~ program(B)
| program(sK7(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_34,plain,
( outputs(A,good)
| ~ halts2(B,C)
| ~ program(B)
| program(sK7(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_35,plain,
( halts3(A,B,C)
| ~ halts2(B,C)
| ~ program(B)
| program(sK7(A))
| ~ program(A) ),
inference(split_conjunct,[status(thm)],[sk_p2]) ).
cnf(c_39,plain,
( ~ halts2(sK6(A),A)
| ~ halts3(A,A,A)
| ~ halts2(sK4(A),sK5(A))
| ~ outputs(A,good)
| ~ halts3(A,sK4(A),sK5(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_19]) ).
cnf(c_43,plain,
( halts2(sK6(A),A)
| ~ outputs(A,bad)
| ~ halts3(A,A,A)
| program(sK4(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_25]) ).
cnf(c_44,plain,
( ~ halts2(sK6(A),A)
| ~ outputs(A,good)
| ~ halts3(A,A,A)
| program(sK4(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_26]) ).
cnf(c_45,plain,
( outputs(A,bad)
| halts2(A,B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_28]) ).
cnf(c_46,plain,
( halts3(A,A,B)
| halts2(A,B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_29]) ).
cnf(c_47,plain,
( outputs(A,good)
| ~ halts2(A,B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_30]) ).
cnf(c_48,plain,
( halts3(A,A,B)
| ~ halts2(A,B)
| ~ decides(A,sK7(A),sK8(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_31]) ).
cnf(c_49,plain,
( outputs(A,bad)
| halts2(A,B)
| program(sK7(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_32]) ).
cnf(c_50,plain,
( halts3(A,A,B)
| halts2(A,B)
| program(sK7(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_33]) ).
cnf(c_51,plain,
( outputs(A,good)
| ~ halts2(A,B)
| program(sK7(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_34]) ).
cnf(c_52,plain,
( halts3(A,A,B)
| ~ halts2(A,B)
| program(sK7(A))
| ~ program(A) ),
inference(factor,[status(thm)],[c_35]) ).
cnf(c_53,plain,
( program(sK3)
| decides(sK0,sK1(sK0),A) ),
inference(resolve,[status(thm)],[c_14,c_10]) ).
cnf(c_1105,negated_conjecture,
( program(sK3)
| program(sK3) ),
inference(resolve,[status(thm)],[c_53,c_12]) ).
cnf(c_62,negated_conjecture,
program(sK3),
inference(copy,[status(thm)],[c_1105]) ).
cnf(c_63,plain,
( halts3(sK3,sK3,A)
| halts2(sK3,A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_50]) ).
cnf(c_64,plain,
( outputs(sK3,bad)
| halts2(sK3,A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_49]) ).
cnf(c_66,plain,
( halts3(sK3,A,B)
| halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_33]) ).
cnf(c_68,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_32]) ).
cnf(c_69,plain,
( program(sK6(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_27]) ).
cnf(c_1106,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_32,c_62]) ).
cnf(c_83,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1106,c_69]) ).
cnf(c_1107,plain,
( halts3(sK3,sK3,A)
| program(sK7(sK3))
| ~ program(sK3)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_64,c_52]) ).
cnf(c_1108,plain,
( halts3(sK3,sK3,A)
| ~ program(sK3)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1107]) ).
cnf(c_85,plain,
( halts3(sK3,sK3,A)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1108]) ).
cnf(c_1109,plain,
( outputs(sK3,good)
| program(sK7(sK3))
| ~ program(sK3)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_64,c_51]) ).
cnf(c_1110,plain,
( outputs(sK3,good)
| ~ program(sK3)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1109]) ).
cnf(c_86,plain,
( outputs(sK3,good)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1110]) ).
cnf(c_1111,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1112,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1111,c_85]) ).
cnf(c_1113,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1112,c_86]) ).
cnf(c_1114,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1113,c_83]) ).
cnf(c_1115,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1114]) ).
cnf(c_1116,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1115]) ).
cnf(c_1117,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1116]) ).
cnf(c_1118,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1117]) ).
cnf(c_105,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1118]) ).
cnf(c_1119,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1120,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1119,c_63]) ).
cnf(c_1121,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1120,c_105]) ).
cnf(c_1122,plain,
( program(sK7(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1121]) ).
cnf(c_106,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1122]) ).
cnf(c_1123,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_34,c_62]) ).
cnf(c_1124,plain,
( program(sK4(sK3))
| outputs(sK3,good)
| ~ halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1123,c_69]) ).
cnf(c_1125,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1124,c_106]) ).
cnf(c_1126,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1125]) ).
cnf(c_115,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1126]) ).
cnf(c_1127,plain,
( outputs(sK3,good)
| program(sK7(sK3))
| ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_115,c_51]) ).
cnf(c_1128,plain,
( outputs(sK3,good)
| ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1127]) ).
cnf(c_1129,plain,
( ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1128]) ).
cnf(c_117,plain,
( program(sK4(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1129]) ).
cnf(c_1130,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1131,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1130,c_63]) ).
cnf(c_1132,plain,
( program(sK4(sK3))
| program(sK7(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1131,c_117]) ).
cnf(c_1133,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1132,c_106]) ).
cnf(c_1134,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1133]) ).
cnf(c_1135,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1134]) ).
cnf(c_1136,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1135]) ).
cnf(c_1137,plain,
( halts2(sK3,sK3)
| halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1136]) ).
cnf(c_118,plain,
( halts2(sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1137]) ).
cnf(c_1138,plain,
( halts3(sK3,sK3,sK3)
| program(sK7(sK3))
| ~ program(sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_118,c_52]) ).
cnf(c_1139,plain,
( halts3(sK3,sK3,sK3)
| ~ program(sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1138]) ).
cnf(c_119,plain,
( halts3(sK3,sK3,sK3)
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1139]) ).
cnf(c_1140,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1141,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1140,c_119]) ).
cnf(c_1142,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1141,c_105]) ).
cnf(c_1143,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1142]) ).
cnf(c_1144,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1143]) ).
cnf(c_136,plain,
( program(sK7(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1144]) ).
cnf(c_1145,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1146,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1145,c_119]) ).
cnf(c_1147,plain,
( program(sK4(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1146,c_117]) ).
cnf(c_1148,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1147,c_136]) ).
cnf(c_1149,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1148]) ).
cnf(c_1150,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1149]) ).
cnf(c_1151,plain,
( program(sK7(sK3))
| program(sK4(sK3))
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1150]) ).
cnf(c_1152,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1151]) ).
cnf(c_141,plain,
( program(sK7(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1152]) ).
cnf(c_1153,plain,
( outputs(sK3,bad)
| halts2(sK4(sK3),A)
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_141,c_68]) ).
cnf(c_142,plain,
( outputs(sK3,bad)
| halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1153]) ).
cnf(c_1154,plain,
( halts3(sK3,sK4(sK3),A)
| halts2(sK4(sK3),A)
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_141,c_66]) ).
cnf(c_144,plain,
( halts3(sK3,sK4(sK3),A)
| halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1154]) ).
cnf(c_1155,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_35,c_62]) ).
cnf(c_1156,plain,
( program(sK7(sK3))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1155,c_141]) ).
cnf(c_1157,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| program(sK7(sK3))
| halts3(sK3,sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1156,c_142]) ).
cnf(c_1158,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| halts3(sK3,sK4(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1157]) ).
cnf(c_160,plain,
( outputs(sK3,bad)
| halts3(sK3,sK4(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1158]) ).
cnf(c_1159,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1160,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1159,c_160]) ).
cnf(c_1161,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1160,c_86]) ).
cnf(c_1162,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1161,c_142]) ).
cnf(c_1163,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1162]) ).
cnf(c_1164,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1163]) ).
cnf(c_1165,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1164]) ).
cnf(c_171,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1165]) ).
cnf(c_1166,plain,
( program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_23,c_62]) ).
cnf(c_1167,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1166,c_144]) ).
cnf(c_1168,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1167,c_171]) ).
cnf(c_1169,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1168]) ).
cnf(c_1170,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1169]) ).
cnf(c_187,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1170]) ).
cnf(c_1171,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_35,c_62]) ).
cnf(c_1172,plain,
( program(sK7(sK3))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1171,c_141]) ).
cnf(c_1173,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1172,c_187]) ).
cnf(c_1174,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1173]) ).
cnf(c_194,plain,
( program(sK6(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1174]) ).
cnf(c_1175,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_34,c_62]) ).
cnf(c_1176,plain,
( program(sK7(sK3))
| outputs(sK3,good)
| ~ halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1175,c_141]) ).
cnf(c_1177,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1176,c_187]) ).
cnf(c_1178,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1177]) ).
cnf(c_195,plain,
( program(sK6(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1178]) ).
cnf(c_1179,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1180,plain,
( program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1179,c_194]) ).
cnf(c_1181,plain,
( program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1180,c_195]) ).
cnf(c_1182,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1181,c_187]) ).
cnf(c_1183,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1182]) ).
cnf(c_1184,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1183]) ).
cnf(c_1185,plain,
( program(sK7(sK3))
| program(sK6(sK3))
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1184]) ).
cnf(c_1186,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1185]) ).
cnf(c_204,plain,
( program(sK7(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1186]) ).
cnf(c_1187,plain,
( outputs(sK3,bad)
| halts2(sK6(sK3),A)
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_204,c_68]) ).
cnf(c_205,plain,
( outputs(sK3,bad)
| halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1187]) ).
cnf(c_1188,plain,
( halts3(sK3,sK6(sK3),A)
| halts2(sK6(sK3),A)
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_204,c_66]) ).
cnf(c_207,plain,
( halts3(sK3,sK6(sK3),A)
| halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1188]) ).
cnf(c_1189,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_39,c_62]) ).
cnf(c_1190,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1189,c_160]) ).
cnf(c_1191,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1190,c_86]) ).
cnf(c_1192,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1191,c_142]) ).
cnf(c_1193,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK3) ),
inference(resolve,[status(thm)],[c_1192,c_85]) ).
cnf(c_1194,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1193,c_205]) ).
cnf(c_1195,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1194]) ).
cnf(c_1196,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1195]) ).
cnf(c_1197,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1196]) ).
cnf(c_1198,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1197]) ).
cnf(c_1199,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1198]) ).
cnf(c_1200,plain,
( outputs(sK3,bad)
| program(sK7(sK3))
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1199]) ).
cnf(c_1201,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1200]) ).
cnf(c_228,plain,
( outputs(sK3,bad)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1201]) ).
cnf(c_1202,plain,
( halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_22,c_62]) ).
cnf(c_1203,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1202,c_144]) ).
cnf(c_1204,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1203,c_228]) ).
cnf(c_1205,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1204,c_204]) ).
cnf(c_1206,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1205,c_207]) ).
cnf(c_1207,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1206]) ).
cnf(c_1208,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1207]) ).
cnf(c_1209,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1208]) ).
cnf(c_1210,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1209]) ).
cnf(c_235,plain,
( program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1210]) ).
cnf(c_1211,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_35,c_62]) ).
cnf(c_1212,plain,
( program(sK7(sK3))
| halts3(sK3,sK6(sK3),A)
| ~ halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1211,c_204]) ).
cnf(c_1213,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1212,c_235]) ).
cnf(c_1214,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1213]) ).
cnf(c_243,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1214]) ).
cnf(c_1215,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_34,c_62]) ).
cnf(c_1216,plain,
( program(sK7(sK3))
| outputs(sK3,good)
| ~ halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1215,c_204]) ).
cnf(c_1217,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1216,c_235]) ).
cnf(c_1218,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1217]) ).
cnf(c_245,plain,
( halts2(sK4(sK3),sK5(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1218]) ).
cnf(c_1219,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_34,c_62]) ).
cnf(c_1220,plain,
( program(sK7(sK3))
| outputs(sK3,good)
| ~ halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1219,c_141]) ).
cnf(c_1221,plain,
( outputs(sK3,good)
| program(sK7(sK3))
| program(sK7(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1220,c_245]) ).
cnf(c_1222,plain,
( outputs(sK3,good)
| program(sK7(sK3))
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1221]) ).
cnf(c_1223,plain,
( outputs(sK3,good)
| outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1222]) ).
cnf(c_255,plain,
( outputs(sK3,good)
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1223]) ).
cnf(c_1224,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_17,c_62]) ).
cnf(c_1225,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1224,c_144]) ).
cnf(c_1226,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1225,c_255]) ).
cnf(c_1227,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1226,c_228]) ).
cnf(c_1228,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1227,c_204]) ).
cnf(c_1229,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1228,c_243]) ).
cnf(c_1230,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1229,c_235]) ).
cnf(c_1231,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1230]) ).
cnf(c_1232,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1231]) ).
cnf(c_1233,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1232]) ).
cnf(c_1234,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1233]) ).
cnf(c_1235,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1234]) ).
cnf(c_1236,plain,
( program(sK7(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1235]) ).
cnf(c_259,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1236]) ).
cnf(c_1237,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_35,c_62]) ).
cnf(c_1238,plain,
( program(sK7(sK3))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1237,c_141]) ).
cnf(c_1239,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1238,c_259]) ).
cnf(c_1240,plain,
( program(sK7(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1239]) ).
cnf(c_267,plain,
( halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1240]) ).
cnf(c_1241,plain,
( halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_16,c_62]) ).
cnf(c_1242,plain,
( program(sK7(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1241,c_267]) ).
cnf(c_1243,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1242,c_255]) ).
cnf(c_1244,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1243,c_228]) ).
cnf(c_1245,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1244,c_204]) ).
cnf(c_1246,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1245,c_207]) ).
cnf(c_1247,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1246]) ).
cnf(c_1248,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1247]) ).
cnf(c_1249,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1248]) ).
cnf(c_1250,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1249]) ).
cnf(c_279,plain,
( program(sK7(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1250]) ).
cnf(c_1251,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_35,c_62]) ).
cnf(c_1252,plain,
( program(sK7(sK3))
| halts3(sK3,sK6(sK3),A)
| ~ halts2(sK6(sK3),A)
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1251,c_204]) ).
cnf(c_1253,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1252,c_279]) ).
cnf(c_1254,plain,
( program(sK7(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1253]) ).
cnf(c_287,plain,
( halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1254]) ).
cnf(c_1255,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_19,c_62]) ).
cnf(c_1256,plain,
( program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1255,c_267]) ).
cnf(c_1257,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1256,c_255]) ).
cnf(c_1258,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1257,c_259]) ).
cnf(c_1259,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1258,c_204]) ).
cnf(c_1260,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| ~ halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1259,c_287]) ).
cnf(c_1261,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(resolve,[status(thm)],[c_1260,c_279]) ).
cnf(c_1262,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1261]) ).
cnf(c_1263,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1262]) ).
cnf(c_1264,plain,
( program(sK7(sK3))
| program(sK7(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1263]) ).
cnf(c_1265,plain,
( program(sK7(sK3))
| program(sK7(sK3)) ),
inference(copy,[status(thm)],[c_1264]) ).
cnf(c_291,plain,
program(sK7(sK3)),
inference(copy,[status(thm)],[c_1265]) ).
cnf(c_305,plain,
( decides(sK3,sK7(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_291,c_11]) ).
cnf(c_1266,plain,
( outputs(sK3,good)
| ~ halts2(sK3,A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_47]) ).
cnf(c_310,plain,
( outputs(sK3,good)
| ~ halts2(sK3,A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1266]) ).
cnf(c_1267,plain,
( halts3(sK3,sK3,A)
| halts2(sK3,A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_46]) ).
cnf(c_311,plain,
( halts3(sK3,sK3,A)
| halts2(sK3,A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1267]) ).
cnf(c_1268,plain,
( outputs(sK3,bad)
| halts2(sK3,A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_45]) ).
cnf(c_312,plain,
( outputs(sK3,bad)
| halts2(sK3,A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1268]) ).
cnf(c_1269,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_31]) ).
cnf(c_313,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1269]) ).
cnf(c_1270,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_30]) ).
cnf(c_314,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1270]) ).
cnf(c_1271,plain,
( halts3(sK3,A,B)
| halts2(A,B)
| ~ program(A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_29]) ).
cnf(c_315,plain,
( halts3(sK3,A,B)
| halts2(A,B)
| ~ program(A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1271]) ).
cnf(c_1272,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| ~ program(sK3)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_305,c_28]) ).
cnf(c_316,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1272]) ).
cnf(c_1273,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| ~ decides(sK3,sK7(sK3),sK8(sK3)) ),
inference(resolve,[status(thm)],[c_28,c_62]) ).
cnf(c_1274,plain,
( program(sK1(sK0))
| outputs(sK3,bad)
| halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1273,c_305]) ).
cnf(c_322,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| outputs(sK3,bad)
| halts2(sK6(sK3),A) ),
inference(resolve,[status(thm)],[c_1274,c_69]) ).
cnf(c_1275,plain,
( outputs(sK3,good)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_312,c_310]) ).
cnf(c_323,plain,
( outputs(sK3,good)
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1275]) ).
cnf(c_1276,plain,
( halts3(sK3,sK3,A)
| ~ halts2(sK3,A)
| ~ decides(sK3,sK7(sK3),sK8(sK3)) ),
inference(resolve,[status(thm)],[c_48,c_62]) ).
cnf(c_1277,plain,
( program(sK1(sK0))
| halts3(sK3,sK3,A)
| ~ halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_1276,c_305]) ).
cnf(c_1278,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| program(sK1(sK0))
| halts3(sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_1277,c_312]) ).
cnf(c_326,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| halts3(sK3,sK3,A) ),
inference(copy,[status(thm)],[c_1278]) ).
cnf(c_1279,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1280,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1279,c_326]) ).
cnf(c_1281,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1280,c_323]) ).
cnf(c_1282,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1281,c_322]) ).
cnf(c_1283,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1282]) ).
cnf(c_1284,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1283]) ).
cnf(c_1285,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1284]) ).
cnf(c_1286,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1285]) ).
cnf(c_428,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1286]) ).
cnf(c_1287,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1288,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1287,c_311]) ).
cnf(c_1289,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1288,c_428]) ).
cnf(c_1290,plain,
( program(sK1(sK0))
| halts2(sK3,sK3)
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1289]) ).
cnf(c_429,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1290]) ).
cnf(c_1291,plain,
( program(sK4(sK3))
| outputs(sK3,good)
| ~ halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_314,c_69]) ).
cnf(c_1292,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1291,c_429]) ).
cnf(c_1293,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1292]) ).
cnf(c_439,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1293]) ).
cnf(c_1294,plain,
( outputs(sK3,good)
| ~ program(sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_439,c_314]) ).
cnf(c_1295,plain,
( outputs(sK3,good)
| ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1294]) ).
cnf(c_1296,plain,
( ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1295]) ).
cnf(c_449,plain,
( program(sK4(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_62,c_1296]) ).
cnf(c_1297,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1298,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1297,c_311]) ).
cnf(c_1299,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| halts2(sK3,sK3)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1298,c_449]) ).
cnf(c_1300,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK1(sK0))
| halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1299,c_429]) ).
cnf(c_1301,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1300]) ).
cnf(c_1302,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1301]) ).
cnf(c_1303,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1302]) ).
cnf(c_1304,plain,
( halts2(sK3,sK3)
| halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1303]) ).
cnf(c_457,plain,
( halts2(sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1304]) ).
cnf(c_1305,plain,
( halts3(sK3,sK3,sK3)
| ~ program(sK3)
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_457,c_313]) ).
cnf(c_1306,plain,
( halts3(sK3,sK3,sK3)
| ~ program(sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1305]) ).
cnf(c_458,plain,
( halts3(sK3,sK3,sK3)
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1306]) ).
cnf(c_1307,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1308,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1307,c_458]) ).
cnf(c_1309,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK1(sK0))
| program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1308,c_428]) ).
cnf(c_1310,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1309]) ).
cnf(c_1311,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1310]) ).
cnf(c_473,plain,
( program(sK1(sK0))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1311]) ).
cnf(c_1312,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1313,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1312,c_458]) ).
cnf(c_1314,plain,
( program(sK4(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1313,c_449]) ).
cnf(c_1315,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1314,c_473]) ).
cnf(c_1316,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1315]) ).
cnf(c_1317,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1316]) ).
cnf(c_1318,plain,
( program(sK1(sK0))
| program(sK4(sK3))
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1317]) ).
cnf(c_1319,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1318]) ).
cnf(c_480,plain,
( program(sK1(sK0))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1319]) ).
cnf(c_1320,plain,
( outputs(sK3,bad)
| halts2(sK4(sK3),A)
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_480,c_316]) ).
cnf(c_481,plain,
( outputs(sK3,bad)
| halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1320]) ).
cnf(c_1321,plain,
( halts3(sK3,sK4(sK3),A)
| halts2(sK4(sK3),A)
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_480,c_315]) ).
cnf(c_482,plain,
( halts3(sK3,sK4(sK3),A)
| halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1321]) ).
cnf(c_1322,plain,
( program(sK1(sK0))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_480]) ).
cnf(c_1323,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| program(sK1(sK0))
| halts3(sK3,sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1322,c_481]) ).
cnf(c_1324,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| halts3(sK3,sK4(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1323]) ).
cnf(c_508,plain,
( outputs(sK3,bad)
| halts3(sK3,sK4(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1324]) ).
cnf(c_1325,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1326,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1325,c_508]) ).
cnf(c_1327,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1326,c_323]) ).
cnf(c_1328,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1327,c_481]) ).
cnf(c_1329,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1328]) ).
cnf(c_1330,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1329]) ).
cnf(c_1331,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1330]) ).
cnf(c_516,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1331]) ).
cnf(c_1332,plain,
( program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_23,c_62]) ).
cnf(c_1333,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1332,c_482]) ).
cnf(c_1334,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1333,c_516]) ).
cnf(c_1335,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1334]) ).
cnf(c_1336,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1335]) ).
cnf(c_532,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1336]) ).
cnf(c_1337,plain,
( program(sK1(sK0))
| outputs(sK3,good)
| ~ halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_314,c_480]) ).
cnf(c_1338,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1337,c_532]) ).
cnf(c_1339,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1338]) ).
cnf(c_539,plain,
( program(sK6(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1339]) ).
cnf(c_1340,plain,
( program(sK1(sK0))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_480]) ).
cnf(c_1341,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1340,c_532]) ).
cnf(c_1342,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1341]) ).
cnf(c_540,plain,
( program(sK6(sK3))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1342]) ).
cnf(c_1343,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1344,plain,
( program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1343,c_540]) ).
cnf(c_1345,plain,
( program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1344,c_539]) ).
cnf(c_1346,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1345,c_532]) ).
cnf(c_1347,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1346]) ).
cnf(c_1348,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1347]) ).
cnf(c_1349,plain,
( program(sK1(sK0))
| program(sK6(sK3))
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1348]) ).
cnf(c_1350,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1349]) ).
cnf(c_555,plain,
( program(sK1(sK0))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1350]) ).
cnf(c_1351,plain,
( outputs(sK3,bad)
| halts2(sK6(sK3),A)
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_555,c_316]) ).
cnf(c_556,plain,
( outputs(sK3,bad)
| halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1351]) ).
cnf(c_1352,plain,
( halts3(sK3,sK6(sK3),A)
| halts2(sK6(sK3),A)
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_555,c_315]) ).
cnf(c_557,plain,
( halts3(sK3,sK6(sK3),A)
| halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1352]) ).
cnf(c_1353,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_39,c_62]) ).
cnf(c_1354,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1353,c_508]) ).
cnf(c_1355,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1354,c_323]) ).
cnf(c_1356,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1355,c_481]) ).
cnf(c_1357,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK3) ),
inference(resolve,[status(thm)],[c_1356,c_326]) ).
cnf(c_1358,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1357,c_556]) ).
cnf(c_1359,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1358]) ).
cnf(c_1360,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1359]) ).
cnf(c_1361,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1360]) ).
cnf(c_1362,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1361]) ).
cnf(c_1363,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1362]) ).
cnf(c_1364,plain,
( outputs(sK3,bad)
| program(sK1(sK0))
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1363]) ).
cnf(c_1365,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1364]) ).
cnf(c_590,plain,
( outputs(sK3,bad)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1365]) ).
cnf(c_1366,plain,
( halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_22,c_62]) ).
cnf(c_1367,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1366,c_482]) ).
cnf(c_1368,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1367,c_590]) ).
cnf(c_1369,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1368,c_555]) ).
cnf(c_1370,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1369,c_557]) ).
cnf(c_1371,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1370]) ).
cnf(c_1372,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1371]) ).
cnf(c_1373,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1372]) ).
cnf(c_1374,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1373]) ).
cnf(c_599,plain,
( program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1374]) ).
cnf(c_1375,plain,
( program(sK1(sK0))
| outputs(sK3,good)
| ~ halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_314,c_555]) ).
cnf(c_1376,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1375,c_599]) ).
cnf(c_1377,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1376]) ).
cnf(c_606,plain,
( halts2(sK4(sK3),sK5(sK3))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1377]) ).
cnf(c_1378,plain,
( program(sK1(sK0))
| halts3(sK3,sK6(sK3),A)
| ~ halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_555]) ).
cnf(c_1379,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1378,c_599]) ).
cnf(c_1380,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1379]) ).
cnf(c_607,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1380]) ).
cnf(c_1381,plain,
( program(sK1(sK0))
| outputs(sK3,good)
| ~ halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_314,c_480]) ).
cnf(c_1382,plain,
( outputs(sK3,good)
| program(sK1(sK0))
| program(sK1(sK0))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1381,c_606]) ).
cnf(c_1383,plain,
( outputs(sK3,good)
| program(sK1(sK0))
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1382]) ).
cnf(c_1384,plain,
( outputs(sK3,good)
| outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1383]) ).
cnf(c_617,plain,
( outputs(sK3,good)
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1384]) ).
cnf(c_1385,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_17,c_62]) ).
cnf(c_1386,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1385,c_482]) ).
cnf(c_1387,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1386,c_617]) ).
cnf(c_1388,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1387,c_590]) ).
cnf(c_1389,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1388,c_555]) ).
cnf(c_1390,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1389,c_607]) ).
cnf(c_1391,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1390,c_599]) ).
cnf(c_1392,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1391]) ).
cnf(c_1393,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1392]) ).
cnf(c_1394,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1393]) ).
cnf(c_1395,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1394]) ).
cnf(c_1396,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1395]) ).
cnf(c_1397,plain,
( program(sK1(sK0))
| halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1396]) ).
cnf(c_621,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1397]) ).
cnf(c_1398,plain,
( program(sK1(sK0))
| halts3(sK3,sK4(sK3),A)
| ~ halts2(sK4(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_480]) ).
cnf(c_1399,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1398,c_621]) ).
cnf(c_1400,plain,
( program(sK1(sK0))
| halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1399]) ).
cnf(c_627,plain,
( halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1400]) ).
cnf(c_1401,plain,
( halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_16,c_62]) ).
cnf(c_1402,plain,
( program(sK1(sK0))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1401,c_627]) ).
cnf(c_1403,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1402,c_617]) ).
cnf(c_1404,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1403,c_590]) ).
cnf(c_1405,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1404,c_555]) ).
cnf(c_1406,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1405,c_557]) ).
cnf(c_1407,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1406]) ).
cnf(c_1408,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1407]) ).
cnf(c_1409,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1408]) ).
cnf(c_1410,plain,
( halts2(sK6(sK3),sK6(sK3))
| program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1409]) ).
cnf(c_646,plain,
( program(sK1(sK0))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1410]) ).
cnf(c_1411,plain,
( program(sK1(sK0))
| halts3(sK3,sK6(sK3),A)
| ~ halts2(sK6(sK3),A)
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_313,c_555]) ).
cnf(c_1412,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1411,c_646]) ).
cnf(c_1413,plain,
( program(sK1(sK0))
| halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1412]) ).
cnf(c_655,plain,
( halts3(sK3,sK6(sK3),sK6(sK3))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1413]) ).
cnf(c_1414,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_19,c_62]) ).
cnf(c_1415,plain,
( program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1414,c_627]) ).
cnf(c_1416,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1415,c_617]) ).
cnf(c_1417,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1416,c_621]) ).
cnf(c_1418,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1417,c_555]) ).
cnf(c_1419,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| ~ halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1418,c_655]) ).
cnf(c_1420,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_1419,c_646]) ).
cnf(c_1421,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1420]) ).
cnf(c_1422,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1421]) ).
cnf(c_1423,plain,
( program(sK1(sK0))
| program(sK1(sK0))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1422]) ).
cnf(c_1424,plain,
( program(sK1(sK0))
| program(sK1(sK0)) ),
inference(copy,[status(thm)],[c_1423]) ).
cnf(c_663,plain,
program(sK1(sK0)),
inference(copy,[status(thm)],[c_1424]) ).
cnf(c_679,plain,
decides(sK0,sK1(sK0),A),
inference(resolve,[status(thm)],[c_663,c_14]) ).
cnf(c_693,negated_conjecture,
( decides(sK3,A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_679,c_13]) ).
cnf(c_696,plain,
decides(sK3,sK7(sK3),A),
inference(resolve,[status(thm)],[c_693,c_291]) ).
cnf(c_1425,plain,
( outputs(sK3,good)
| ~ halts2(sK3,A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_47]) ).
cnf(c_701,plain,
( outputs(sK3,good)
| ~ halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_62,c_1425]) ).
cnf(c_1426,plain,
( halts3(sK3,sK3,A)
| halts2(sK3,A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_46]) ).
cnf(c_702,plain,
( halts3(sK3,sK3,A)
| halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_62,c_1426]) ).
cnf(c_1427,plain,
( outputs(sK3,bad)
| halts2(sK3,A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_45]) ).
cnf(c_703,plain,
( outputs(sK3,bad)
| halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_62,c_1427]) ).
cnf(c_1428,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_31]) ).
cnf(c_704,plain,
( halts3(sK3,A,B)
| ~ halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_62,c_1428]) ).
cnf(c_1429,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_30]) ).
cnf(c_705,plain,
( outputs(sK3,good)
| ~ halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_62,c_1429]) ).
cnf(c_1430,plain,
( halts3(sK3,A,B)
| halts2(A,B)
| ~ program(A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_29]) ).
cnf(c_706,plain,
( halts3(sK3,A,B)
| halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_62,c_1430]) ).
cnf(c_1431,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| ~ program(sK3) ),
inference(resolve,[status(thm)],[c_696,c_28]) ).
cnf(c_707,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_62,c_1431]) ).
cnf(c_1432,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A)
| ~ decides(sK3,sK7(sK3),sK8(sK3)) ),
inference(resolve,[status(thm)],[c_28,c_62]) ).
cnf(c_1433,plain,
( outputs(sK3,bad)
| halts2(A,B)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1432,c_696]) ).
cnf(c_720,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| halts2(sK6(sK3),A) ),
inference(resolve,[status(thm)],[c_1433,c_69]) ).
cnf(c_721,plain,
( outputs(sK3,good)
| outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_703,c_701]) ).
cnf(c_1434,plain,
( halts3(sK3,sK3,A)
| ~ halts2(sK3,A)
| ~ decides(sK3,sK7(sK3),sK8(sK3)) ),
inference(resolve,[status(thm)],[c_48,c_62]) ).
cnf(c_1435,plain,
( halts3(sK3,sK3,A)
| ~ halts2(sK3,A) ),
inference(resolve,[status(thm)],[c_1434,c_696]) ).
cnf(c_724,plain,
( outputs(sK3,bad)
| halts3(sK3,sK3,A) ),
inference(resolve,[status(thm)],[c_1435,c_703]) ).
cnf(c_1436,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1437,plain,
( outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1436,c_724]) ).
cnf(c_1438,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1437,c_721]) ).
cnf(c_1439,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1438,c_720]) ).
cnf(c_1440,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1439]) ).
cnf(c_1441,plain,
( program(sK4(sK3))
| outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1440]) ).
cnf(c_788,plain,
( outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1441]) ).
cnf(c_1442,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1443,plain,
( halts2(sK3,sK3)
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1442,c_702]) ).
cnf(c_1444,plain,
( program(sK4(sK3))
| halts2(sK3,sK3)
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1443,c_788]) ).
cnf(c_789,plain,
( halts2(sK3,sK3)
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1444]) ).
cnf(c_1445,plain,
( program(sK4(sK3))
| outputs(sK3,good)
| ~ halts2(sK6(sK3),A) ),
inference(resolve,[status(thm)],[c_705,c_69]) ).
cnf(c_1446,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| program(sK4(sK3))
| outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1445,c_789]) ).
cnf(c_801,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| outputs(sK3,good) ),
inference(copy,[status(thm)],[c_1446]) ).
cnf(c_1447,plain,
( outputs(sK3,good)
| ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_801,c_705]) ).
cnf(c_1448,plain,
( ~ program(sK3)
| program(sK4(sK3))
| outputs(sK3,good) ),
inference(copy,[status(thm)],[c_1447]) ).
cnf(c_813,plain,
( program(sK4(sK3))
| outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_62,c_1448]) ).
cnf(c_1449,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1450,plain,
( halts2(sK3,sK3)
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1449,c_702]) ).
cnf(c_1451,plain,
( program(sK4(sK3))
| halts2(sK3,sK3)
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1450,c_813]) ).
cnf(c_1452,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1451,c_789]) ).
cnf(c_1453,plain,
( halts2(sK3,sK3)
| program(sK4(sK3))
| halts2(sK3,sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1452]) ).
cnf(c_1454,plain,
( halts2(sK3,sK3)
| halts2(sK3,sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1453]) ).
cnf(c_814,plain,
( halts2(sK3,sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1454]) ).
cnf(c_1455,plain,
( halts3(sK3,sK3,sK3)
| ~ program(sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_814,c_704]) ).
cnf(c_815,plain,
( halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1455]) ).
cnf(c_1456,plain,
( halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_43,c_62]) ).
cnf(c_1457,plain,
( program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| ~ outputs(sK3,bad)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1456,c_815]) ).
cnf(c_1458,plain,
( program(sK4(sK3))
| program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1457,c_788]) ).
cnf(c_1459,plain,
( program(sK4(sK3))
| halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1458]) ).
cnf(c_832,plain,
( halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1459]) ).
cnf(c_1460,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK3,sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_44,c_62]) ).
cnf(c_1461,plain,
( program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| ~ outputs(sK3,good)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1460,c_815]) ).
cnf(c_1462,plain,
( program(sK4(sK3))
| program(sK4(sK3))
| ~ halts2(sK6(sK3),sK3)
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1461,c_813]) ).
cnf(c_1463,plain,
( program(sK4(sK3))
| program(sK4(sK3))
| program(sK4(sK3))
| program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1462,c_832]) ).
cnf(c_1464,plain,
( program(sK4(sK3))
| program(sK4(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1463]) ).
cnf(c_1465,plain,
( program(sK4(sK3))
| program(sK4(sK3)) ),
inference(copy,[status(thm)],[c_1464]) ).
cnf(c_839,plain,
program(sK4(sK3)),
inference(copy,[status(thm)],[c_1465]) ).
cnf(c_850,plain,
( outputs(sK3,bad)
| halts2(sK4(sK3),A) ),
inference(resolve,[status(thm)],[c_839,c_707]) ).
cnf(c_851,plain,
( halts3(sK3,sK4(sK3),A)
| halts2(sK4(sK3),A) ),
inference(resolve,[status(thm)],[c_839,c_706]) ).
cnf(c_1466,plain,
( halts3(sK3,sK4(sK3),A)
| ~ program(sK4(sK3))
| outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_850,c_704]) ).
cnf(c_881,plain,
( halts3(sK3,sK4(sK3),A)
| outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_839,c_1466]) ).
cnf(c_1467,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1468,plain,
( outputs(sK3,bad)
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1467,c_881]) ).
cnf(c_1469,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1468,c_721]) ).
cnf(c_1470,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1469,c_850]) ).
cnf(c_1471,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1470]) ).
cnf(c_891,plain,
( outputs(sK3,bad)
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1471]) ).
cnf(c_1472,plain,
( program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_23,c_62]) ).
cnf(c_1473,plain,
( halts2(sK4(sK3),sK5(sK3))
| program(sK6(sK3))
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1472,c_851]) ).
cnf(c_1474,plain,
( program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1473,c_891]) ).
cnf(c_1475,plain,
( program(sK6(sK3))
| program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1474]) ).
cnf(c_916,plain,
( program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1475]) ).
cnf(c_1476,plain,
( outputs(sK3,good)
| ~ program(sK4(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_916,c_705]) ).
cnf(c_917,plain,
( outputs(sK3,good)
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_839,c_1476]) ).
cnf(c_1477,plain,
( halts3(sK3,sK4(sK3),sK5(sK3))
| ~ program(sK4(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_916,c_704]) ).
cnf(c_918,plain,
( halts3(sK3,sK4(sK3),sK5(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_839,c_1477]) ).
cnf(c_1478,plain,
( program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_20,c_62]) ).
cnf(c_1479,plain,
( program(sK6(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1478,c_918]) ).
cnf(c_1480,plain,
( program(sK6(sK3))
| program(sK6(sK3))
| program(sK6(sK3))
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1479,c_917]) ).
cnf(c_1481,plain,
( program(sK6(sK3))
| program(sK6(sK3))
| program(sK6(sK3))
| program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1480,c_916]) ).
cnf(c_1482,plain,
( program(sK6(sK3))
| program(sK6(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1481]) ).
cnf(c_1483,plain,
( program(sK6(sK3))
| program(sK6(sK3)) ),
inference(copy,[status(thm)],[c_1482]) ).
cnf(c_937,plain,
program(sK6(sK3)),
inference(copy,[status(thm)],[c_1483]) ).
cnf(c_938,plain,
( outputs(sK3,bad)
| halts2(sK6(sK3),A) ),
inference(resolve,[status(thm)],[c_937,c_707]) ).
cnf(c_939,plain,
( halts3(sK3,sK6(sK3),A)
| halts2(sK6(sK3),A) ),
inference(resolve,[status(thm)],[c_937,c_706]) ).
cnf(c_1484,plain,
( ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_39,c_62]) ).
cnf(c_1485,plain,
( outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1484,c_881]) ).
cnf(c_1486,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1485,c_721]) ).
cnf(c_1487,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3)
| ~ halts3(sK3,sK3,sK3) ),
inference(resolve,[status(thm)],[c_1486,c_850]) ).
cnf(c_1488,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| ~ halts2(sK6(sK3),sK3) ),
inference(resolve,[status(thm)],[c_1487,c_724]) ).
cnf(c_1489,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1488,c_938]) ).
cnf(c_1490,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad) ),
inference(copy,[status(thm)],[c_1489]) ).
cnf(c_1491,plain,
( outputs(sK3,bad)
| outputs(sK3,bad)
| outputs(sK3,bad) ),
inference(copy,[status(thm)],[c_1490]) ).
cnf(c_1492,plain,
( outputs(sK3,bad)
| outputs(sK3,bad) ),
inference(copy,[status(thm)],[c_1491]) ).
cnf(c_986,plain,
outputs(sK3,bad),
inference(copy,[status(thm)],[c_1492]) ).
cnf(c_1493,plain,
( halts2(sK6(sK3),sK6(sK3))
| ~ program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| ~ program(sK3)
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_939,c_16]) ).
cnf(c_1494,plain,
( ~ program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| ~ program(sK3)
| halts2(sK6(sK3),sK6(sK3)) ),
inference(copy,[status(thm)],[c_1493]) ).
cnf(c_1495,plain,
( ~ program(sK6(sK3))
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_62,c_1494]) ).
cnf(c_1496,plain,
( ~ program(sK6(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_986,c_1495]) ).
cnf(c_1022,plain,
( ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_937,c_1496]) ).
cnf(c_1497,plain,
( halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_22,c_62]) ).
cnf(c_1498,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1497,c_851]) ).
cnf(c_1499,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1498,c_986]) ).
cnf(c_1500,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1499,c_937]) ).
cnf(c_1501,plain,
( halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1500,c_939]) ).
cnf(c_1502,plain,
( halts2(sK6(sK3),sK6(sK3))
| halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1501]) ).
cnf(c_1023,plain,
( halts2(sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1502]) ).
cnf(c_1503,plain,
( outputs(sK3,good)
| ~ program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1023,c_705]) ).
cnf(c_1024,plain,
( outputs(sK3,good)
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_937,c_1503]) ).
cnf(c_1504,plain,
( halts3(sK3,sK6(sK3),sK6(sK3))
| ~ program(sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1023,c_704]) ).
cnf(c_1025,plain,
( halts3(sK3,sK6(sK3),sK6(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_937,c_1504]) ).
cnf(c_1505,plain,
( outputs(sK3,good)
| ~ program(sK4(sK3))
| outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1024,c_705]) ).
cnf(c_1506,plain,
( ~ program(sK4(sK3))
| outputs(sK3,good) ),
inference(copy,[status(thm)],[c_1505]) ).
cnf(c_1038,plain,
outputs(sK3,good),
inference(resolve,[status(thm)],[c_839,c_1506]) ).
cnf(c_1039,plain,
( ~ halts3(sK3,sK4(sK3),sK5(sK3))
| halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1038,c_1022]) ).
cnf(c_1507,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_17,c_62]) ).
cnf(c_1508,plain,
( halts2(sK4(sK3),sK5(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad)
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1507,c_851]) ).
cnf(c_1509,plain,
( halts2(sK4(sK3),sK5(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ outputs(sK3,bad) ),
inference(resolve,[status(thm)],[c_1508,c_1038]) ).
cnf(c_1510,plain,
( halts2(sK4(sK3),sK5(sK3))
| ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1509,c_986]) ).
cnf(c_1511,plain,
( halts2(sK4(sK3),sK5(sK3))
| ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1510,c_937]) ).
cnf(c_1512,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| ~ halts2(sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1511,c_1025]) ).
cnf(c_1513,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1512,c_1023]) ).
cnf(c_1514,plain,
( halts2(sK4(sK3),sK5(sK3))
| halts2(sK4(sK3),sK5(sK3)) ),
inference(copy,[status(thm)],[c_1513]) ).
cnf(c_1064,plain,
halts2(sK4(sK3),sK5(sK3)),
inference(copy,[status(thm)],[c_1514]) ).
cnf(c_1515,plain,
( halts3(sK3,sK4(sK3),sK5(sK3))
| ~ program(sK4(sK3)) ),
inference(resolve,[status(thm)],[c_1064,c_704]) ).
cnf(c_1065,plain,
halts3(sK3,sK4(sK3),sK5(sK3)),
inference(resolve,[status(thm)],[c_839,c_1515]) ).
cnf(c_1090,plain,
halts2(sK6(sK3),sK6(sK3)),
inference(resolve,[status(thm)],[c_1065,c_1039]) ).
cnf(c_1516,plain,
( halts3(sK3,sK6(sK3),sK6(sK3))
| ~ program(sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1090,c_704]) ).
cnf(c_1091,plain,
halts3(sK3,sK6(sK3),sK6(sK3)),
inference(resolve,[status(thm)],[c_937,c_1516]) ).
cnf(c_1517,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good)
| ~ halts3(sK3,sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_19,c_62]) ).
cnf(c_1518,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3))
| ~ outputs(sK3,good) ),
inference(resolve,[status(thm)],[c_1517,c_1065]) ).
cnf(c_1519,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A)
| ~ halts2(sK4(sK3),sK5(sK3)) ),
inference(resolve,[status(thm)],[c_1518,c_1038]) ).
cnf(c_1520,plain,
( ~ halts2(sK6(sK3),A)
| ~ halts3(sK3,A,A)
| ~ program(A) ),
inference(resolve,[status(thm)],[c_1519,c_1064]) ).
cnf(c_1521,plain,
( ~ halts2(sK6(sK3),sK6(sK3))
| ~ halts3(sK3,sK6(sK3),sK6(sK3)) ),
inference(resolve,[status(thm)],[c_1520,c_937]) ).
cnf(c_1522,plain,
~ halts3(sK3,sK6(sK3),sK6(sK3)),
inference(resolve,[status(thm)],[c_1521,c_1090]) ).
cnf(c_1104,plain,
$false,
inference(resolve,[status(thm)],[c_1091,c_1522]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n003.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 23:20:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 4062596 was started by sandbox on n003,
% 0.10/0.37 % Sat Sep 26 23:20:55 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 1.64/0.68
% 1.64/0.68 % SZS status Theorem for theBenchmark
% 1.64/0.68
% 1.64/0.68 % Proof 1 at 0.19 (+ 0.05) seconds.
% 1.64/0.68 % Length of proof is 162.
% 1.64/0.68 % Level of proof is 86.
% 1.64/0.68 % Maximum clause weight is 36.000.
% 1.64/0.68 % Given clauses 217.
% 1.64/0.68
% 1.64/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------