%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:03:17 PM UTC 2026
% Result : Theorem 34.74s 5.26s
% Output : Proof 34.74s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f2,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3) ).
fof(f2_nnf,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) )
| ? [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) ) )
| ~ program(W) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [W,Y] :
( ( ( ( outputs(sk7(W),bad)
& halts2(sk7(W),Y) )
| ~ outputs(W,bad)
| ~ halts3(W,Y,Y)
| ~ program(Y) )
& ( ~ halts2(sk7(W),Y)
| ~ outputs(W,good)
| ~ halts3(W,Y,Y)
| ~ program(Y) )
& program(sk7(W)) )
| ( ( ~ outputs(W,bad)
| ~ halts3(W,sk5(W),sk6(W)) )
& ~ halts2(sk5(W),sk6(W))
& program(sk5(W)) )
| ( ( ~ outputs(W,good)
| ~ halts3(W,sk5(W),sk6(W)) )
& halts2(sk5(W),sk6(W))
& program(sk5(W)) )
| ~ program(W) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5,sk6,sk7])],[f2_nnf]) ).
cnf(c45,plain,
( ~ halts2(sk7(X0),X1)
| ~ outputs(X0,good)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p272,plain,
( ~ halts2(sk7(X0),X1)
| ~ outputs(X0,good)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c45]) ).
cnf(p1382,plain,
( ~ halts2(sk7(X0),X1)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p272]) ).
cnf(p1679,plain,
( ~ halts2(sk7(X0),X0)
| ~ halts3(X0,X0,X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p1382]) ).
fof(f0,axiom,
( ? [X] :
( ! [Y] :
( program(Y)
=> ! [Z] : decides(X,Y,Z) )
& algorithm(X) )
=> ? [W] :
( ! [Y] :
( program(Y)
=> ! [Z] : decides(W,Y,Z) )
& program(W) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p1) ).
fof(f0_nnf,plain,
( ? [W] :
( ! [Y] :
( ! [Z] : decides(W,Y,Z)
| ~ program(Y) )
& program(W) )
| ! [X] :
( ? [Y] :
( ? [Z] : ~ decides(X,Y,Z)
& program(Y) )
| ~ algorithm(X) ) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] :
( ( ( decides(sk2,Y,Z)
| ~ program(Y) )
& program(sk2) )
| ( ~ decides(X,sk0(X),sk1(X))
& program(sk0(X)) )
| ~ algorithm(X) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f0_nnf]) ).
cnf(c2,plain,
( program(sk2)
| ~ decides(X0,sk0(X0),sk1(X0))
| ~ algorithm(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
fof(f3,conjecture,
~ ? [X1] :
( ! [Y1] :
( program(Y1)
=> ! [Z1] : decides(X1,Y1,Z1) )
& algorithm(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f3_neg,negated_conjecture,
~ ~ ? [X1] :
( ! [Y1] :
( program(Y1)
=> ! [Z1] : decides(X1,Y1,Z1) )
& algorithm(X1) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f3_nnf,plain,
? [X1] :
( ! [Y1] :
( ! [Z1] : decides(X1,Y1,Z1)
| ~ program(Y1) )
& algorithm(X1) ),
inference(nnf_transformation,[status(thm)],[f3_neg]) ).
fof(f3_sk,plain,
! [Y1,Z1] :
( ( decides(sk8,Y1,Z1)
| ~ program(Y1) )
& algorithm(sk8) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk8])],[f3_nnf]) ).
cnf(c48,plain,
algorithm(sk8),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p53,plain,
( program(sk2)
| ~ decides(sk8,sk0(sk8),sk1(sk8)) ),
inference(resolution,[status(thm)],[c2,c48]) ).
cnf(c0,plain,
( program(sk2)
| program(sk0(X0))
| ~ algorithm(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p50,plain,
( program(sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[c0,c48]) ).
cnf(c49,plain,
( decides(sk8,X1,X2)
| ~ program(X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p51,plain,
( decides(sk8,sk0(sk8),X0)
| program(sk2) ),
inference(resolution,[status(thm)],[p50,c49]) ).
cnf(p54,plain,
( program(sk2)
| program(sk2) ),
inference(resolution,[status(thm)],[p53,p51]) ).
cnf(p56,plain,
program(sk2),
inference(factoring,[status(thm)],[p54]) ).
cnf(p1694,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1679,p56]) ).
cnf(c14,plain,
( halts2(sk7(X0),X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| program(sk5(X0))
| program(sk5(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p137,plain,
( halts2(sk7(X0),X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| program(sk5(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c14]) ).
cnf(p223,plain,
( halts2(sk7(sk2),X0)
| ~ outputs(sk2,bad)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p137,p56]) ).
cnf(c12,plain,
( program(sk7(X0))
| program(sk5(X0))
| program(sk5(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p61,plain,
( program(sk7(X0))
| program(sk5(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c12]) ).
cnf(p62,plain,
( program(sk7(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p61,p56]) ).
cnf(p237,plain,
( program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| ~ halts3(sk2,sk7(sk2),sk7(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p223,p62]) ).
cnf(p274,plain,
( halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| ~ halts3(sk2,sk7(sk2),sk7(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p237]) ).
fof(f1,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2) ).
fof(f1_nnf,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) ) )
| ? [Y] :
( ? [Z] : ~ decides(W,Y,Z)
& program(Y) )
| ~ program(W) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_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,sk3(W),sk4(W))
& program(sk3(W)) )
| ~ program(W) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk3,sk4])],[f1_nnf]) ).
cnf(c6,plain,
( halts3(X0,X1,X2)
| halts2(X1,X2)
| ~ program(X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p79,plain,
( halts3(sk2,X0,X1)
| halts2(X0,X1)
| ~ program(X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[c6,p56]) ).
cnf(p107,plain,
( program(sk5(sk2))
| halts3(sk2,sk7(sk2),X0)
| halts2(sk7(sk2),X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p79,p62]) ).
cnf(p275,plain,
( program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p274,p107]) ).
cnf(p353,plain,
( program(sk5(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p275]) ).
cnf(p354,plain,
( program(sk3(sk2))
| halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p353]) ).
cnf(c7,plain,
( outputs(X0,bad)
| halts2(X1,X2)
| ~ program(X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p87,plain,
( outputs(X0,bad)
| halts2(X0,X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c7]) ).
cnf(p91,plain,
( outputs(sk2,bad)
| halts2(sk2,X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p87,p56]) ).
cnf(p355,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p354,p91]) ).
cnf(p357,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p355]) ).
cnf(c5,plain,
( outputs(X0,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p68,plain,
( outputs(sk2,good)
| ~ halts2(X0,X1)
| ~ program(X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[c5,p56]) ).
cnf(p82,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p68,p62]) ).
cnf(p359,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| program(sk3(sk2))
| halts2(sk2,X0)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p357,p82]) ).
cnf(p378,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| halts2(sk2,X0)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p359]) ).
cnf(p380,plain,
( outputs(sk2,good)
| halts2(sk2,X0)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p378]) ).
cnf(p67,plain,
( outputs(X0,good)
| ~ halts2(X0,X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c5]) ).
cnf(p75,plain,
( outputs(sk2,good)
| ~ halts2(sk2,X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p67,p56]) ).
cnf(p381,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| outputs(sk2,good)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p380,p75]) ).
cnf(p387,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p381]) ).
cnf(p389,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p387]) ).
cnf(c13,plain,
( ~ halts2(sk7(X0),X1)
| ~ outputs(X0,good)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| program(sk5(X0))
| program(sk5(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p130,plain,
( ~ halts2(sk7(X0),X1)
| ~ outputs(X0,good)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| program(sk5(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c13]) ).
cnf(p203,plain,
( ~ halts2(sk7(X0),X0)
| ~ outputs(X0,good)
| ~ halts3(X0,X0,X0)
| program(sk5(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p130]) ).
cnf(p210,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk2,sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p203,p56]) ).
cnf(p78,plain,
( halts3(X0,X0,X1)
| halts2(X0,X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c6]) ).
cnf(p104,plain,
( halts3(sk2,sk2,X0)
| halts2(sk2,X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p78,p56]) ).
cnf(p214,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p210,p104]) ).
cnf(p390,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p389,p214]) ).
cnf(p393,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p390]) ).
cnf(p395,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p393]) ).
cnf(p222,plain,
( halts2(sk7(X0),X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,X0,X0)
| program(sk5(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p137]) ).
cnf(p227,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| ~ halts3(sk2,sk2,sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p222,p56]) ).
cnf(p231,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p227,p104]) ).
cnf(p240,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p231,p91]) ).
cnf(p276,plain,
( halts2(sk2,X0)
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p240]) ).
cnf(p281,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p276]) ).
cnf(p396,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p395,p281]) ).
cnf(p397,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p396]) ).
cnf(p400,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p397]) ).
cnf(p402,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p400]) ).
cnf(c4,plain,
( halts3(X0,X1,X2)
| ~ halts2(X1,X2)
| ~ program(X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p59,plain,
( halts3(X0,X0,X1)
| ~ halts2(X0,X1)
| program(sk3(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c4]) ).
cnf(p84,plain,
( halts3(sk2,sk2,X0)
| ~ halts2(sk2,X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p59,p56]) ).
cnf(p403,plain,
( halts3(sk2,sk2,sk2)
| program(sk3(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p402,p84]) ).
cnf(p409,plain,
( halts3(sk2,sk2,sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p403]) ).
cnf(p410,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p409,p210]) ).
cnf(p413,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p410]) ).
cnf(p414,plain,
( program(sk3(sk2))
| program(sk5(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p413,p389]) ).
cnf(p468,plain,
( program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p414]) ).
cnf(p470,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p468]) ).
cnf(p88,plain,
( outputs(sk2,bad)
| halts2(X0,X1)
| ~ program(X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[c7,p56]) ).
cnf(p96,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p88,p62]) ).
cnf(p471,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| program(sk3(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p470,p96]) ).
cnf(p473,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p471]) ).
cnf(p479,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p473]) ).
cnf(p411,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p409,p227]) ).
cnf(p418,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p411]) ).
cnf(p481,plain,
( halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p479,p418]) ).
cnf(p501,plain,
( halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p481]) ).
cnf(p503,plain,
( halts2(sk7(sk2),sk2)
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p501]) ).
cnf(p506,plain,
( program(sk3(sk2))
| program(sk5(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p503,p470]) ).
cnf(p507,plain,
( program(sk3(sk2))
| program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p506]) ).
cnf(p509,plain,
( program(sk3(sk2))
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p507]) ).
cnf(p525,plain,
( halts3(sk2,sk5(sk2),X0)
| halts2(sk5(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p509,p79]) ).
cnf(p596,plain,
( halts3(sk2,sk5(sk2),X0)
| halts2(sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p525]) ).
cnf(p1708,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good) ),
inference(resolution,[status(thm)],[p1694,p596]) ).
cnf(c34,plain,
( halts2(sk7(X0),X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| halts2(sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p201,plain,
( halts2(sk7(X0),X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,X0,X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| halts2(sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c34]) ).
cnf(p850,plain,
( halts2(sk7(X0),X0)
| ~ halts3(X0,X0,X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| halts2(sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p201]) ).
cnf(p1415,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p850,p56]) ).
cnf(p1428,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1415,p596]) ).
cnf(p1530,plain,
( program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p1428]) ).
cnf(p1531,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1530,p91]) ).
cnf(p1535,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p1531]) ).
cnf(p1536,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1535,p104]) ).
cnf(p1537,plain,
( halts2(sk2,sk2)
| halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p1536]) ).
cnf(p1539,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p1537]) ).
cnf(p517,plain,
( outputs(sk2,good)
| ~ halts2(sk5(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p509,p68]) ).
cnf(p584,plain,
( outputs(sk2,good)
| ~ halts2(sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p517]) ).
cnf(p1540,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p1539,p584]) ).
cnf(p1548,plain,
( outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1540]) ).
cnf(c32,plain,
( program(sk7(X0))
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| halts2(sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p188,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| ~ halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[c32,p56]) ).
cnf(p597,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p596,p188]) ).
cnf(p661,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p597]) ).
cnf(p662,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p661,p91]) ).
cnf(p666,plain,
( halts2(sk2,X0)
| program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p662]) ).
cnf(p668,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| halts2(sk2,X0)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p666,p584]) ).
cnf(p674,plain,
( outputs(sk2,good)
| halts2(sk2,X0)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p668]) ).
cnf(p675,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| outputs(sk2,good)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p674,p75]) ).
cnf(p680,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p675]) ).
cnf(p682,plain,
( outputs(sk2,good)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p680]) ).
cnf(p60,plain,
( halts3(sk2,X0,X1)
| ~ halts2(X0,X1)
| ~ program(X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[c4,p56]) ).
cnf(p522,plain,
( halts3(sk2,sk5(sk2),X0)
| ~ halts2(sk5(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p509,p60]) ).
cnf(p591,plain,
( halts3(sk2,sk5(sk2),X0)
| ~ halts2(sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p522]) ).
cnf(p521,plain,
( outputs(sk2,bad)
| halts2(sk5(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p509,p88]) ).
cnf(p587,plain,
( outputs(sk2,bad)
| halts2(sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p521]) ).
cnf(p592,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| halts3(sk2,sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p591,p587]) ).
cnf(p594,plain,
( outputs(sk2,bad)
| halts3(sk2,sk5(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p592]) ).
cnf(c40,plain,
( program(sk7(X0))
| ~ halts2(sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p197,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[c40,p56]) ).
cnf(p595,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p594,p197]) ).
cnf(p683,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk3(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p682,p595]) ).
cnf(p734,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p683]) ).
cnf(p736,plain,
( ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p734]) ).
cnf(p737,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p736,p587]) ).
cnf(p739,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p737]) ).
cnf(p742,plain,
( outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p739]) ).
cnf(p743,plain,
( program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p742,p661]) ).
cnf(p744,plain,
( program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p743]) ).
cnf(p746,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p744]) ).
cnf(p747,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p746,p591]) ).
cnf(p749,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p747]) ).
cnf(c44,plain,
( program(sk7(X0))
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p264,plain,
( program(sk7(X0))
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c44]) ).
cnf(p266,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p264,p56]) ).
cnf(p751,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p749,p266]) ).
cnf(p752,plain,
( ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p751]) ).
cnf(p753,plain,
( program(sk7(sk2))
| program(sk3(sk2))
| ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p752,p682]) ).
cnf(p754,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p753]) ).
cnf(p756,plain,
( ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p754]) ).
cnf(p757,plain,
( program(sk7(sk2))
| program(sk3(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p756,p742]) ).
cnf(p758,plain,
( program(sk7(sk2))
| program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p757]) ).
cnf(p760,plain,
( program(sk7(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p758]) ).
cnf(p768,plain,
( outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p760,p68]) ).
cnf(p841,plain,
( outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p768]) ).
cnf(p1549,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p1548,p841]) ).
cnf(p1557,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1549]) ).
cnf(p1559,plain,
( outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1557]) ).
cnf(p1717,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p1708,p1559]) ).
cnf(p1958,plain,
( halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(factoring,[status(thm)],[p1717]) ).
cnf(p1959,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(resolution,[status(thm)],[p1958,p91]) ).
cnf(p1962,plain,
( halts2(sk2,X0)
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(factoring,[status(thm)],[p1959]) ).
cnf(p1964,plain,
( halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(factoring,[status(thm)],[p1962]) ).
cnf(p1967,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p1964,p104]) ).
cnf(p1968,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1967]) ).
cnf(p1970,plain,
( halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1968]) ).
cnf(c46,plain,
( halts2(sk7(X0),X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p279,plain,
( halts2(sk7(X0),X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c46]) ).
cnf(p1389,plain,
( halts2(sk7(X0),X1)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p279]) ).
cnf(p1718,plain,
( halts2(sk7(X0),X0)
| ~ halts3(X0,X0,X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p1389]) ).
cnf(p1733,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1718,p56]) ).
cnf(p1542,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p1539,p591]) ).
cnf(p1560,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1542]) ).
cnf(p1747,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good) ),
inference(resolution,[status(thm)],[p1733,p1560]) ).
cnf(p1810,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good) ),
inference(factoring,[status(thm)],[p1747]) ).
cnf(p1811,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p1810,p1559]) ).
cnf(p1812,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(factoring,[status(thm)],[p1811]) ).
cnf(p1814,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(factoring,[status(thm)],[p1812]) ).
cnf(p1815,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(resolution,[status(thm)],[p1814,p91]) ).
cnf(p1816,plain,
( halts2(sk2,X0)
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(factoring,[status(thm)],[p1815]) ).
cnf(p1818,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(factoring,[status(thm)],[p1816]) ).
cnf(p1819,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p1818,p104]) ).
cnf(p1820,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1819]) ).
cnf(p1822,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p1820]) ).
cnf(p1971,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p1970,p1822]) ).
cnf(p1975,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1971]) ).
cnf(p1977,plain,
( halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1975]) ).
cnf(p1978,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p1977,p591]) ).
cnf(p1983,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1978]) ).
cnf(p1986,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p1983,p1694]) ).
cnf(p1992,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p1986,p1559]) ).
cnf(p1998,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1992]) ).
cnf(p2000,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p1998]) ).
cnf(p2001,plain,
( halts2(sk2,X0)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2000,p91]) ).
cnf(p2005,plain,
( halts2(sk2,X0)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2001]) ).
cnf(p2007,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2005]) ).
cnf(p2008,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2007,p104]) ).
cnf(p2009,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2008]) ).
cnf(p2016,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2009]) ).
cnf(p2017,plain,
( halts2(sk2,sk2)
| program(sk3(sk2))
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2016,p1822]) ).
cnf(p2018,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2017]) ).
cnf(p2020,plain,
( halts2(sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2018]) ).
cnf(p2022,plain,
( outputs(sk2,good)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2020,p75]) ).
cnf(p2032,plain,
( outputs(sk2,good)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2022]) ).
cnf(p2034,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2032,p1708]) ).
cnf(p2279,plain,
( halts2(sk5(sk2),sk6(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2034]) ).
cnf(c41,plain,
( ~ halts2(sk7(X0),X1)
| ~ outputs(X0,good)
| ~ halts3(X0,X1,X1)
| ~ program(X1)
| ~ halts2(sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p220,plain,
( ~ halts2(sk7(X0),X0)
| ~ outputs(X0,good)
| ~ halts3(X0,X0,X0)
| ~ halts2(sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c41]) ).
cnf(p988,plain,
( ~ halts2(sk7(X0),X0)
| ~ halts3(X0,X0,X0)
| ~ halts2(sk5(X0),sk6(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,sk5(X0),sk6(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[p220]) ).
cnf(p1469,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p988,p56]) ).
cnf(p1482,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good) ),
inference(resolution,[status(thm)],[p1469,p594]) ).
cnf(p2033,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2032,p1482]) ).
cnf(p2133,plain,
( outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2033]) ).
cnf(p2134,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2133,p587]) ).
cnf(p2139,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2134]) ).
cnf(p2141,plain,
( outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2139]) ).
cnf(p2023,plain,
( halts3(sk2,sk2,sk2)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2020,p84]) ).
cnf(p2042,plain,
( halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2023]) ).
cnf(p2147,plain,
( program(sk3(sk2))
| outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2141,p2042]) ).
cnf(p2148,plain,
( outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2147]) ).
cnf(p772,plain,
( outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p760,p88]) ).
cnf(p842,plain,
( outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p772]) ).
cnf(p2149,plain,
( outputs(sk2,bad)
| program(sk3(sk2))
| outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2148,p842]) ).
cnf(p2154,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2149]) ).
cnf(p2156,plain,
( outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2154]) ).
cnf(p2280,plain,
( program(sk3(sk2))
| halts2(sk5(sk2),sk6(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2279,p2156]) ).
cnf(p2289,plain,
( halts2(sk5(sk2),sk6(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2280]) ).
cnf(p2290,plain,
( program(sk3(sk2))
| halts2(sk5(sk2),sk6(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2289,p2042]) ).
cnf(p2291,plain,
( halts2(sk5(sk2),sk6(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2290]) ).
cnf(p2157,plain,
( program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2156,p1530]) ).
cnf(p2175,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2157]) ).
cnf(p2176,plain,
( program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2175,p2042]) ).
cnf(p2177,plain,
( halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2176]) ).
cnf(p2179,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2177,p591]) ).
cnf(p2184,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2179]) ).
cnf(p2187,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2184,p1733]) ).
cnf(p2226,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2187]) ).
cnf(p2228,plain,
( program(sk3(sk2))
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2226,p2032]) ).
cnf(p2229,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2228]) ).
cnf(p2230,plain,
( program(sk3(sk2))
| ~ halts3(sk2,sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2229,p2156]) ).
cnf(p2231,plain,
( ~ halts3(sk2,sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2230]) ).
cnf(p2232,plain,
( program(sk3(sk2))
| halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2231,p2042]) ).
cnf(p2233,plain,
( halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2232]) ).
cnf(p2292,plain,
( program(sk3(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2291,p2233]) ).
cnf(p2293,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2292]) ).
cnf(p2294,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2293,p591]) ).
cnf(p2299,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2294]) ).
cnf(p2302,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2299,p1694]) ).
cnf(p2317,plain,
( program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2302,p2032]) ).
cnf(p2318,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2317]) ).
cnf(p2319,plain,
( program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2318,p2156]) ).
cnf(p2320,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2319]) ).
cnf(p2325,plain,
( program(sk3(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2320,p2042]) ).
cnf(p2326,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk3(sk2)) ),
inference(factoring,[status(thm)],[p2325]) ).
cnf(p2330,plain,
( program(sk3(sk2))
| program(sk3(sk2)) ),
inference(resolution,[status(thm)],[p2326,p2233]) ).
cnf(p2331,plain,
program(sk3(sk2)),
inference(factoring,[status(thm)],[p2330]) ).
cnf(c1,plain,
( decides(sk2,X1,X2)
| ~ program(X1)
| program(sk0(X0))
| ~ algorithm(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p52,plain,
( decides(sk2,X0,X1)
| ~ program(X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[c1,c48]) ).
cnf(p2335,plain,
( decides(sk2,sk3(sk2),X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2331,p52]) ).
cnf(c10,plain,
( halts3(X0,X1,X2)
| halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p116,plain,
( halts3(sk2,X0,X1)
| halts2(X0,X1)
| ~ program(X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[c10,p56]) ).
cnf(p2412,plain,
( halts3(sk2,X0,X1)
| halts2(X0,X1)
| ~ program(X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p116]) ).
cnf(p2529,plain,
( program(sk5(sk2))
| halts3(sk2,sk7(sk2),X0)
| halts2(sk7(sk2),X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2412,p62]) ).
cnf(p2682,plain,
( halts2(sk7(sk2),sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2529,p274]) ).
cnf(p3138,plain,
( ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p2682]) ).
cnf(p3140,plain,
( ~ outputs(sk2,bad)
| program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3138]) ).
cnf(c11,plain,
( outputs(X0,bad)
| halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p122,plain,
( outputs(X0,bad)
| halts2(X0,X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c11]) ).
cnf(p126,plain,
( outputs(sk2,bad)
| halts2(sk2,X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[p122,p56]) ).
cnf(p2407,plain,
( outputs(sk2,bad)
| halts2(sk2,X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p126]) ).
cnf(p3141,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3140,p2407]) ).
cnf(p3144,plain,
( halts2(sk2,X0)
| program(sk5(sk2))
| halts2(sk7(sk2),sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3141]) ).
cnf(c9,plain,
( outputs(X0,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p110,plain,
( outputs(sk2,good)
| ~ halts2(X0,X1)
| ~ program(X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[c9,p56]) ).
cnf(p2406,plain,
( outputs(sk2,good)
| ~ halts2(X0,X1)
| ~ program(X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p110]) ).
cnf(p2504,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2406,p62]) ).
cnf(p3157,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| program(sk0(sk8))
| halts2(sk2,X0)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3144,p2504]) ).
cnf(p3194,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| halts2(sk2,X0)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3157]) ).
cnf(p3198,plain,
( outputs(sk2,good)
| halts2(sk2,X0)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3194]) ).
cnf(p109,plain,
( outputs(X0,good)
| ~ halts2(X0,X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c9]) ).
cnf(p119,plain,
( outputs(sk2,good)
| ~ halts2(sk2,X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[p109,p56]) ).
cnf(p2405,plain,
( outputs(sk2,good)
| ~ halts2(sk2,X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p119]) ).
cnf(p3203,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| outputs(sk2,good)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3198,p2405]) ).
cnf(p3211,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3203]) ).
cnf(p3213,plain,
( outputs(sk2,good)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3211]) ).
cnf(p115,plain,
( halts3(X0,X0,X1)
| halts2(X0,X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c10]) ).
cnf(p143,plain,
( halts3(sk2,sk2,X0)
| halts2(sk2,X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[p115,p56]) ).
cnf(p2411,plain,
( halts3(sk2,sk2,X0)
| halts2(sk2,X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p143]) ).
cnf(p2500,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2411,p210]) ).
cnf(p3215,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3213,p2500]) ).
cnf(p3224,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3215]) ).
cnf(p3226,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3224]) ).
cnf(p2501,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2411,p227]) ).
cnf(p2707,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2501,p2407]) ).
cnf(p2946,plain,
( halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p2707]) ).
cnf(p2950,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p2946]) ).
cnf(p3230,plain,
( program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8))
| halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3226,p2950]) ).
cnf(p3231,plain,
( program(sk5(sk2))
| halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3230]) ).
cnf(p3234,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3231]) ).
cnf(p3236,plain,
( halts2(sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3234]) ).
cnf(c8,plain,
( halts3(X0,X1,X2)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p100,plain,
( halts3(X0,X0,X1)
| ~ halts2(X0,X1)
| ~ decides(X0,sk3(X0),sk4(X0))
| ~ program(X0) ),
inference(factoring,[status(thm)],[c8]) ).
cnf(p138,plain,
( halts3(sk2,sk2,X0)
| ~ halts2(sk2,X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[p100,p56]) ).
cnf(p2409,plain,
( halts3(sk2,sk2,X0)
| ~ halts2(sk2,X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p138]) ).
cnf(p3246,plain,
( halts3(sk2,sk2,sk2)
| program(sk0(sk8))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3236,p2409]) ).
cnf(p3251,plain,
( halts3(sk2,sk2,sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3246]) ).
cnf(p3252,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3251,p210]) ).
cnf(p3261,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3252]) ).
cnf(p3262,plain,
( program(sk5(sk2))
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3261,p3213]) ).
cnf(p3268,plain,
( program(sk5(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3262]) ).
cnf(p3272,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3268]) ).
cnf(p123,plain,
( outputs(sk2,bad)
| halts2(X0,X1)
| ~ program(X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[c11,p56]) ).
cnf(p2408,plain,
( outputs(sk2,bad)
| halts2(X0,X1)
| ~ program(X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p123]) ).
cnf(p2512,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2408,p62]) ).
cnf(p3275,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| program(sk0(sk8))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3272,p2512]) ).
cnf(p3278,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3275]) ).
cnf(p3280,plain,
( outputs(sk2,bad)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3278]) ).
cnf(p3253,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3251,p227]) ).
cnf(p3263,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3253]) ).
cnf(p3287,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk0(sk8))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3280,p3263]) ).
cnf(p3316,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3287]) ).
cnf(p3318,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3316]) ).
cnf(p3323,plain,
( program(sk5(sk2))
| program(sk0(sk8))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3318,p3272]) ).
cnf(p3324,plain,
( program(sk5(sk2))
| program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3323]) ).
cnf(p3326,plain,
( program(sk5(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3324]) ).
cnf(p3370,plain,
( halts3(sk2,sk5(sk2),X0)
| halts2(sk5(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3326,p2412]) ).
cnf(p3456,plain,
( halts3(sk2,sk5(sk2),X0)
| halts2(sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3370]) ).
cnf(p3459,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3456,p1415]) ).
cnf(p5069,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3459]) ).
cnf(p5070,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5069,p2407]) ).
cnf(p5072,plain,
( halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5070]) ).
cnf(p5073,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5072,p2411]) ).
cnf(p5074,plain,
( halts2(sk2,sk2)
| halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5073]) ).
cnf(p5076,plain,
( halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5074]) ).
cnf(p3367,plain,
( outputs(sk2,good)
| ~ halts2(sk5(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3326,p2406]) ).
cnf(p3440,plain,
( outputs(sk2,good)
| ~ halts2(sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3367]) ).
cnf(p5077,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5076,p3440]) ).
cnf(p5087,plain,
( outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5077]) ).
cnf(p3457,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3456,p188]) ).
cnf(p3604,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3457]) ).
cnf(p3605,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3604,p2407]) ).
cnf(p3607,plain,
( halts2(sk2,X0)
| program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3605]) ).
cnf(p3613,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| halts2(sk2,X0)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3607,p3440]) ).
cnf(p3621,plain,
( outputs(sk2,good)
| halts2(sk2,X0)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3613]) ).
cnf(p3622,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| outputs(sk2,good)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3621,p2405]) ).
cnf(p3630,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3622]) ).
cnf(p3632,plain,
( outputs(sk2,good)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3630]) ).
cnf(p101,plain,
( halts3(sk2,X0,X1)
| ~ halts2(X0,X1)
| ~ program(X0)
| ~ decides(sk2,sk3(sk2),sk4(sk2)) ),
inference(resolution,[status(thm)],[c8,p56]) ).
cnf(p2410,plain,
( halts3(sk2,X0,X1)
| ~ halts2(X0,X1)
| ~ program(X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p2335,p101]) ).
cnf(p3369,plain,
( halts3(sk2,sk5(sk2),X0)
| ~ halts2(sk5(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3326,p2410]) ).
cnf(p3448,plain,
( halts3(sk2,sk5(sk2),X0)
| ~ halts2(sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3369]) ).
cnf(p3368,plain,
( outputs(sk2,bad)
| halts2(sk5(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3326,p2408]) ).
cnf(p3441,plain,
( outputs(sk2,bad)
| halts2(sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3368]) ).
cnf(p3449,plain,
( outputs(sk2,bad)
| program(sk0(sk8))
| halts3(sk2,sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3448,p3441]) ).
cnf(p3452,plain,
( outputs(sk2,bad)
| halts3(sk2,sk5(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3449]) ).
cnf(p3453,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3452,p197]) ).
cnf(p3633,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk0(sk8))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3632,p3453]) ).
cnf(p3749,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3633]) ).
cnf(p3751,plain,
( ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3749]) ).
cnf(p3752,plain,
( outputs(sk2,bad)
| program(sk0(sk8))
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3751,p3441]) ).
cnf(p3756,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3752]) ).
cnf(p3767,plain,
( outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3756]) ).
cnf(p3768,plain,
( program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3767,p3604]) ).
cnf(p3769,plain,
( program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3768]) ).
cnf(p3771,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3769]) ).
cnf(p3854,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3771,p3448]) ).
cnf(p3857,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3854]) ).
cnf(p3859,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3857,p266]) ).
cnf(p3868,plain,
( ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3859]) ).
cnf(p3879,plain,
( program(sk7(sk2))
| program(sk0(sk8))
| ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3868,p3632]) ).
cnf(p3880,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3879]) ).
cnf(p3882,plain,
( ~ outputs(sk2,bad)
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3880]) ).
cnf(p3883,plain,
( program(sk7(sk2))
| program(sk0(sk8))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3882,p3767]) ).
cnf(p3884,plain,
( program(sk7(sk2))
| program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3883]) ).
cnf(p3886,plain,
( program(sk7(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3884]) ).
cnf(p3927,plain,
( outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3886,p2406]) ).
cnf(p4016,plain,
( outputs(sk2,good)
| ~ halts2(sk7(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3927]) ).
cnf(p5088,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5087,p4016]) ).
cnf(p5098,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5088]) ).
cnf(p5100,plain,
( outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5098]) ).
cnf(p3463,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3456,p1694]) ).
cnf(p5101,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5100,p3463]) ).
cnf(p5752,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5101]) ).
cnf(p5753,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5752,p2407]) ).
cnf(p5766,plain,
( halts2(sk2,X0)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5753]) ).
cnf(p5769,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5766]) ).
cnf(p5770,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5769,p2411]) ).
cnf(p5771,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5770]) ).
cnf(p5773,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5771]) ).
cnf(p5079,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5076,p3448]) ).
cnf(p5103,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5079]) ).
cnf(p5106,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5103,p1733]) ).
cnf(p5333,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5106]) ).
cnf(p5334,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5333,p5100]) ).
cnf(p5337,plain,
( halts2(sk2,sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5334]) ).
cnf(p5339,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5337]) ).
cnf(p5340,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5339,p2407]) ).
cnf(p5341,plain,
( halts2(sk2,X0)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5340]) ).
cnf(p5346,plain,
( ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5341]) ).
cnf(p5347,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5346,p2411]) ).
cnf(p5348,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5347]) ).
cnf(p5350,plain,
( halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5348]) ).
cnf(p5774,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5773,p5350]) ).
cnf(p5775,plain,
( halts2(sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5774]) ).
cnf(p5777,plain,
( halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5775]) ).
cnf(p5778,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5777,p3448]) ).
cnf(p5785,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5778]) ).
cnf(p5788,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5785,p1694]) ).
cnf(p5800,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5788,p5100]) ).
cnf(p5804,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5800]) ).
cnf(p5806,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5804]) ).
cnf(p5807,plain,
( halts2(sk2,X0)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5806,p2407]) ).
cnf(p5808,plain,
( halts2(sk2,X0)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5807]) ).
cnf(p5810,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5808]) ).
cnf(p5811,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5810,p2411]) ).
cnf(p5812,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5811]) ).
cnf(p5814,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5812]) ).
cnf(p5821,plain,
( halts2(sk2,sk2)
| program(sk0(sk8))
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5814,p5350]) ).
cnf(p5822,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5821]) ).
cnf(p5824,plain,
( halts2(sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5822]) ).
cnf(p5825,plain,
( outputs(sk2,good)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5824,p2405]) ).
cnf(p5840,plain,
( outputs(sk2,good)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5825]) ).
cnf(p5842,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5840,p3463]) ).
cnf(p6187,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5842]) ).
cnf(p3454,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3452,p1469]) ).
cnf(p5841,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5840,p3454]) ).
cnf(p5989,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5841]) ).
cnf(p5990,plain,
( outputs(sk2,bad)
| program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5989,p3441]) ).
cnf(p5997,plain,
( outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5990]) ).
cnf(p6017,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5997]) ).
cnf(p5826,plain,
( halts3(sk2,sk2,sk2)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p5824,p2409]) ).
cnf(p5852,plain,
( halts3(sk2,sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p5826]) ).
cnf(p6025,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6017,p5852]) ).
cnf(p6026,plain,
( ~ halts2(sk7(sk2),sk2)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6025]) ).
cnf(p3928,plain,
( outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p3886,p2408]) ).
cnf(p4017,plain,
( outputs(sk2,bad)
| halts2(sk7(sk2),X0)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p3928]) ).
cnf(p6027,plain,
( outputs(sk2,bad)
| program(sk0(sk8))
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6026,p4017]) ).
cnf(p6035,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6027]) ).
cnf(p6037,plain,
( outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6035]) ).
cnf(p6188,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6187,p6037]) ).
cnf(p6189,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6188]) ).
cnf(p6191,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6189,p5852]) ).
cnf(p6192,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6191]) ).
cnf(p6038,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6037,p5069]) ).
cnf(p6068,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6038]) ).
cnf(p6071,plain,
( program(sk0(sk8))
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6068,p5852]) ).
cnf(p6072,plain,
( halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6071]) ).
cnf(p6073,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6072,p3448]) ).
cnf(p6080,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6073]) ).
cnf(p6101,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6080,p1733]) ).
cnf(p6135,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6101]) ).
cnf(p6136,plain,
( program(sk0(sk8))
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6135,p5840]) ).
cnf(p6137,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6136]) ).
cnf(p6144,plain,
( program(sk0(sk8))
| ~ halts3(sk2,sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6137,p6037]) ).
cnf(p6145,plain,
( ~ halts3(sk2,sk2,sk2)
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6144]) ).
cnf(p6147,plain,
( program(sk0(sk8))
| halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6145,p5852]) ).
cnf(p6148,plain,
( halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6147]) ).
cnf(p6193,plain,
( program(sk0(sk8))
| halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6192,p6148]) ).
cnf(p6194,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6193]) ).
cnf(p6195,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6194,p3448]) ).
cnf(p6202,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6195]) ).
cnf(p6205,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6202,p1694]) ).
cnf(p6213,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6205,p5840]) ).
cnf(p6214,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6213]) ).
cnf(p6215,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6214,p6037]) ).
cnf(p6216,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6215]) ).
cnf(p6224,plain,
( program(sk0(sk8))
| ~ halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6216,p5852]) ).
cnf(p6225,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk0(sk8)) ),
inference(factoring,[status(thm)],[p6224]) ).
cnf(p6231,plain,
( program(sk0(sk8))
| program(sk0(sk8)) ),
inference(resolution,[status(thm)],[p6225,p6148]) ).
cnf(p6232,plain,
program(sk0(sk8)),
inference(factoring,[status(thm)],[p6231]) ).
cnf(p6234,plain,
decides(sk8,sk0(sk8),X0),
inference(resolution,[status(thm)],[p6232,c49]) ).
cnf(c3,plain,
( decides(sk2,X1,X2)
| ~ program(X1)
| ~ decides(X0,sk0(X0),sk1(X0))
| ~ algorithm(X0) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p55,plain,
( decides(sk2,X0,X1)
| ~ program(X0)
| ~ decides(sk8,sk0(sk8),sk1(sk8)) ),
inference(resolution,[status(thm)],[c3,c48]) ).
cnf(p6327,plain,
( decides(sk2,X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[p6234,p55]) ).
cnf(p6334,plain,
decides(sk2,sk3(sk2),X0),
inference(resolution,[status(thm)],[p6327,p2331]) ).
cnf(p6347,plain,
( halts3(sk2,sk2,X0)
| halts2(sk2,X0) ),
inference(resolution,[status(thm)],[p6334,p143]) ).
cnf(p6382,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p6347,p227]) ).
cnf(p6343,plain,
( outputs(sk2,bad)
| halts2(sk2,X0) ),
inference(resolution,[status(thm)],[p6334,p126]) ).
cnf(p6660,plain,
( halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p6382,p6343]) ).
cnf(p6765,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p6660]) ).
cnf(p6342,plain,
( outputs(sk2,good)
| ~ halts2(X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[p6334,p110]) ).
cnf(p6479,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| ~ halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p6342,p62]) ).
cnf(p6776,plain,
( program(sk5(sk2))
| outputs(sk2,good)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p6765,p6479]) ).
cnf(p6778,plain,
( outputs(sk2,good)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p6776]) ).
cnf(p6381,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p6347,p210]) ).
cnf(p6780,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p6778,p6381]) ).
cnf(p7148,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p6780]) ).
cnf(p7150,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p7148]) ).
cnf(p7151,plain,
( program(sk5(sk2))
| halts2(sk2,sk2)
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p7150,p6765]) ).
cnf(p7152,plain,
( program(sk5(sk2))
| program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p7151]) ).
cnf(p7154,plain,
( program(sk5(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p7152]) ).
cnf(p6345,plain,
( halts3(sk2,sk2,X0)
| ~ halts2(sk2,X0) ),
inference(resolution,[status(thm)],[p6334,p138]) ).
cnf(p7169,plain,
( halts3(sk2,sk2,sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7154,p6345]) ).
cnf(p7181,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7169,p227]) ).
cnf(p7213,plain,
( halts2(sk7(sk2),sk2)
| ~ outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7181]) ).
cnf(p6341,plain,
( outputs(sk2,good)
| ~ halts2(sk2,X0) ),
inference(resolution,[status(thm)],[p6334,p119]) ).
cnf(p7168,plain,
( outputs(sk2,good)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7154,p6341]) ).
cnf(p6380,plain,
( outputs(sk2,bad)
| halts3(sk2,sk2,X0) ),
inference(resolution,[status(thm)],[p6345,p6343]) ).
cnf(p6384,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p6380,p210]) ).
cnf(p7172,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2))
| outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7168,p6384]) ).
cnf(p7189,plain,
( ~ halts2(sk7(sk2),sk2)
| outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7172]) ).
cnf(p6344,plain,
( outputs(sk2,bad)
| halts2(X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[p6334,p123]) ).
cnf(p6491,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p6344,p62]) ).
cnf(p7195,plain,
( program(sk5(sk2))
| outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7189,p6491]) ).
cnf(p7197,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7195]) ).
cnf(p7199,plain,
( outputs(sk2,bad)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7197]) ).
cnf(p7215,plain,
( program(sk5(sk2))
| halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7213,p7199]) ).
cnf(p7250,plain,
( halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7215]) ).
cnf(p7180,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7169,p210]) ).
cnf(p7204,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ outputs(sk2,good)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7180]) ).
cnf(p7205,plain,
( program(sk5(sk2))
| ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7204,p7168]) ).
cnf(p7206,plain,
( ~ halts2(sk7(sk2),sk2)
| program(sk5(sk2)) ),
inference(factoring,[status(thm)],[p7205]) ).
cnf(p7257,plain,
( program(sk5(sk2))
| program(sk5(sk2)) ),
inference(resolution,[status(thm)],[p7250,p7206]) ).
cnf(p7258,plain,
program(sk5(sk2)),
inference(factoring,[status(thm)],[p7257]) ).
cnf(p6348,plain,
( halts3(sk2,X0,X1)
| halts2(X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[p6334,p116]) ).
cnf(p7318,plain,
( halts3(sk2,sk5(sk2),X0)
| halts2(sk5(sk2),X0) ),
inference(resolution,[status(thm)],[p7258,p6348]) ).
cnf(p7409,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7318,p1415]) ).
cnf(p9951,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p7409]) ).
cnf(p9952,plain,
( halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p9951,p6343]) ).
cnf(p9954,plain,
( halts2(sk2,sk2)
| halts2(sk2,X0)
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p9952,p6347]) ).
cnf(p9955,plain,
( halts2(sk2,sk2)
| halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p9954]) ).
cnf(p6346,plain,
( halts3(sk2,X0,X1)
| ~ halts2(X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[p6334,p101]) ).
cnf(p7317,plain,
( halts3(sk2,sk5(sk2),X0)
| ~ halts2(sk5(sk2),X0) ),
inference(resolution,[status(thm)],[p7258,p6346]) ).
cnf(p9957,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p9955,p7317]) ).
cnf(p9997,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p9957,p1733]) ).
cnf(p10706,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p9997]) ).
cnf(p7315,plain,
( outputs(sk2,good)
| ~ halts2(sk5(sk2),X0) ),
inference(resolution,[status(thm)],[p7258,p6342]) ).
cnf(p9956,plain,
( outputs(sk2,good)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p9955,p7315]) ).
cnf(p7407,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7318,p188]) ).
cnf(p7625,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p7407]) ).
cnf(p7626,plain,
( halts2(sk2,X0)
| program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7625,p6343]) ).
cnf(p7636,plain,
( outputs(sk2,good)
| halts2(sk2,X0)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7626,p7315]) ).
cnf(p7651,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7636,p6341]) ).
cnf(p7657,plain,
( outputs(sk2,good)
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7651]) ).
cnf(p7316,plain,
( outputs(sk2,bad)
| halts2(sk5(sk2),X0) ),
inference(resolution,[status(thm)],[p7258,p6344]) ).
cnf(p7403,plain,
( outputs(sk2,bad)
| halts3(sk2,sk5(sk2),X0) ),
inference(resolution,[status(thm)],[p7317,p7316]) ).
cnf(p7404,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p7403,p197]) ).
cnf(p7660,plain,
( program(sk7(sk2))
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7657,p7404]) ).
cnf(p7724,plain,
( ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7660]) ).
cnf(p7726,plain,
( outputs(sk2,bad)
| outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7724,p7316]) ).
cnf(p7730,plain,
( outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7726]) ).
cnf(p7731,plain,
( program(sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7730,p7625]) ).
cnf(p7732,plain,
( halts2(sk5(sk2),sk6(sk2))
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7731]) ).
cnf(p7735,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7732,p7317]) ).
cnf(p7743,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7735,p266]) ).
cnf(p7757,plain,
( ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7743]) ).
cnf(p7758,plain,
( program(sk7(sk2))
| ~ outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7757,p7657]) ).
cnf(p7759,plain,
( ~ outputs(sk2,bad)
| program(sk7(sk2)) ),
inference(factoring,[status(thm)],[p7758]) ).
cnf(p7762,plain,
( program(sk7(sk2))
| program(sk7(sk2)) ),
inference(resolution,[status(thm)],[p7759,p7730]) ).
cnf(p7770,plain,
program(sk7(sk2)),
inference(factoring,[status(thm)],[p7762]) ).
cnf(p7827,plain,
( outputs(sk2,good)
| ~ halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p7770,p6342]) ).
cnf(p9974,plain,
( outputs(sk2,good)
| outputs(sk2,good)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p9956,p7827]) ).
cnf(p9992,plain,
( outputs(sk2,good)
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p9974]) ).
cnf(p10707,plain,
( halts2(sk2,sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p10706,p9992]) ).
cnf(p10708,plain,
( ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p10707]) ).
cnf(p10711,plain,
( halts2(sk2,X0)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p10708,p6343]) ).
cnf(p10712,plain,
( ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p10711]) ).
cnf(p10713,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(resolution,[status(thm)],[p10712,p6347]) ).
cnf(p10714,plain,
( halts2(sk2,sk2)
| halts2(sk7(sk2),sk2) ),
inference(factoring,[status(thm)],[p10713]) ).
cnf(p7413,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7318,p1694]) ).
cnf(p9993,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p9992,p7413]) ).
cnf(p10004,plain,
( halts2(sk2,X0)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p9993,p6343]) ).
cnf(p10006,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10004]) ).
cnf(p10007,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10006,p6347]) ).
cnf(p10008,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10007]) ).
cnf(p10732,plain,
( halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10714,p10008]) ).
cnf(p10737,plain,
( halts2(sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10732]) ).
cnf(p10738,plain,
( halts3(sk2,sk5(sk2),sk6(sk2))
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10737,p7317]) ).
cnf(p10766,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10738,p1694]) ).
cnf(p10808,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10766,p9992]) ).
cnf(p10810,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10808]) ).
cnf(p10812,plain,
( halts2(sk2,X0)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10810,p6343]) ).
cnf(p10813,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10812]) ).
cnf(p10814,plain,
( halts2(sk2,sk2)
| ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10813,p6347]) ).
cnf(p10815,plain,
( ~ halts2(sk7(sk2),sk2)
| halts2(sk2,sk2) ),
inference(factoring,[status(thm)],[p10814]) ).
cnf(p10835,plain,
( halts2(sk2,sk2)
| halts2(sk2,sk2) ),
inference(resolution,[status(thm)],[p10815,p10714]) ).
cnf(p10836,plain,
halts2(sk2,sk2),
inference(factoring,[status(thm)],[p10835]) ).
cnf(p10842,plain,
outputs(sk2,good),
inference(resolution,[status(thm)],[p10836,p6341]) ).
cnf(p1719,plain,
( halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1389,p56]) ).
cnf(p7416,plain,
( halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7318,p1719]) ).
cnf(p10860,plain,
( halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p10842,p7416]) ).
cnf(p7405,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| ~ outputs(sk2,good)
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p7403,p1469]) ).
cnf(p10856,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ halts2(sk5(sk2),sk6(sk2))
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p10842,p7405]) ).
cnf(p11015,plain,
( outputs(sk2,bad)
| ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p10856,p7316]) ).
cnf(p11024,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| outputs(sk2,bad) ),
inference(factoring,[status(thm)],[p11015]) ).
cnf(p10843,plain,
halts3(sk2,sk2,sk2),
inference(resolution,[status(thm)],[p10836,p6345]) ).
cnf(p11035,plain,
( ~ halts2(sk7(sk2),sk2)
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p11024,p10843]) ).
cnf(p7828,plain,
( outputs(sk2,bad)
| halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p7770,p6344]) ).
cnf(p11036,plain,
( outputs(sk2,bad)
| outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p11035,p7828]) ).
cnf(p11045,plain,
outputs(sk2,bad),
inference(factoring,[status(thm)],[p11036]) ).
cnf(p11238,plain,
( halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p10860,p11045]) ).
cnf(p11249,plain,
( halts2(sk7(sk2),sk7(sk2))
| ~ halts3(sk2,sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11238,p7770]) ).
cnf(p7830,plain,
( halts3(sk2,sk7(sk2),X0)
| halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p7770,p6348]) ).
cnf(p11289,plain,
( halts2(sk7(sk2),sk7(sk2))
| halts2(sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11249,p7830]) ).
cnf(p11290,plain,
( halts2(sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p11289]) ).
cnf(p7829,plain,
( halts3(sk2,sk7(sk2),X0)
| ~ halts2(sk7(sk2),X0) ),
inference(resolution,[status(thm)],[p7770,p6346]) ).
cnf(p11291,plain,
( halts3(sk2,sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11290,p7829]) ).
cnf(p1680,plain,
( ~ halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| ~ halts3(sk2,sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p1382,p56]) ).
cnf(p7414,plain,
( ~ halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p7318,p1680]) ).
cnf(p10859,plain,
( ~ halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| ~ outputs(sk2,bad)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p10842,p7414]) ).
cnf(p11216,plain,
( ~ halts2(sk7(sk2),X0)
| ~ halts3(sk2,X0,X0)
| ~ program(X0)
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p10859,p11045]) ).
cnf(p11228,plain,
( ~ halts2(sk7(sk2),sk7(sk2))
| ~ halts3(sk2,sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11216,p7770]) ).
cnf(p11300,plain,
( ~ halts2(sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11291,p11228]) ).
cnf(p11301,plain,
( ~ halts2(sk7(sk2),sk7(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(factoring,[status(thm)],[p11300]) ).
cnf(p11302,plain,
( halts2(sk5(sk2),sk6(sk2))
| halts2(sk5(sk2),sk6(sk2)) ),
inference(resolution,[status(thm)],[p11301,p11290]) ).
cnf(p11303,plain,
halts2(sk5(sk2),sk6(sk2)),
inference(factoring,[status(thm)],[p11302]) ).
cnf(p11304,plain,
halts3(sk2,sk5(sk2),sk6(sk2)),
inference(resolution,[status(thm)],[p11303,p7317]) ).
cnf(p11317,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good) ),
inference(resolution,[status(thm)],[p11304,p1733]) ).
cnf(p11350,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p11317,p10842]) ).
cnf(p11351,plain,
( halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(resolution,[status(thm)],[p11350,p11045]) ).
cnf(p11353,plain,
halts2(sk7(sk2),sk2),
inference(resolution,[status(thm)],[p11351,p10843]) ).
cnf(p11315,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad)
| ~ outputs(sk2,good) ),
inference(resolution,[status(thm)],[p11304,p1694]) ).
cnf(p11321,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2)
| ~ outputs(sk2,bad) ),
inference(resolution,[status(thm)],[p11315,p10842]) ).
cnf(p11322,plain,
( ~ halts2(sk7(sk2),sk2)
| ~ halts3(sk2,sk2,sk2) ),
inference(resolution,[status(thm)],[p11321,p11045]) ).
cnf(p11333,plain,
~ halts2(sk7(sk2),sk2),
inference(resolution,[status(thm)],[p11322,p10843]) ).
cnf(p11363,plain,
$false,
inference(resolution,[status(thm)],[p11353,p11333]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COM003+3 : TPTP v9.3.1. Released v2.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 07:44:29 UTC 2026
% 0.12/0.36 % CPUTime :
% 0.12/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.74/5.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.74/5.26 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------