%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : COM003-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n006.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:04:14 PM UTC 2026
% Result : Unsatisfiable 1.40s 11.41s
% Output : CNFRefutation 1.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 44
% Syntax : Number of formulae : 315 ( 18 unt; 0 def)
% Number of atoms : 1349 ( 0 equ)
% Maximal formula atoms : 8 ( 4 avg)
% Number of connectives : 1955 ( 921 ~;1034 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 32 ( 31 usr; 26 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 6 con; 0-1 aty)
% Number of variables : 335 ( 0 sgn 335 !; 0 ?; 248 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( program(c1)
| program(f2(X0))
| ~ algorithm(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_1_1) ).
fof(f2,axiom,
! [X2,X0,X1] :
( decides(c1,X1,X2)
| ~ program(X1)
| program(f2(X0))
| ~ algorithm(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_1_2) ).
fof(f3,axiom,
! [X0] :
( program(c1)
| ~ decides(X0,f2(X0),f1(X0))
| ~ algorithm(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_1_3) ).
fof(f4,axiom,
! [X2,X0,X1] :
( decides(c1,X1,X2)
| ~ program(X1)
| ~ decides(X0,f2(X0),f1(X0))
| ~ algorithm(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_1_4) ).
fof(f5,axiom,
! [X2,X0,X1] :
( halts3(X0,X1,X2)
| ~ halts2(X1,X2)
| ~ program(X1)
| program(f4(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_1) ).
fof(f6,axiom,
! [X2,X0,X1] :
( outputs(X0,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| program(f4(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_2) ).
fof(f7,axiom,
! [X2,X0,X1] :
( halts3(X0,X1,X2)
| halts2(X1,X2)
| ~ program(X1)
| program(f4(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_3) ).
fof(f8,axiom,
! [X2,X0,X1] :
( outputs(X0,bad)
| halts2(X1,X2)
| ~ program(X1)
| program(f4(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_4) ).
fof(f9,axiom,
! [X2,X0,X1] :
( halts3(X0,X1,X2)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,f4(X0),f3(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_5) ).
fof(f10,axiom,
! [X2,X0,X1] :
( outputs(X0,good)
| ~ halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,f4(X0),f3(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_6) ).
fof(f11,axiom,
! [X2,X0,X1] :
( halts3(X0,X1,X2)
| halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,f4(X0),f3(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_7) ).
fof(f12,axiom,
! [X2,X0,X1] :
( outputs(X0,bad)
| halts2(X1,X2)
| ~ program(X1)
| ~ decides(X0,f4(X0),f3(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_2_8) ).
fof(f13,axiom,
! [X0] :
( program(c2)
| program(f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_1) ).
fof(f14,axiom,
! [X0,X1] :
( halts2(c2,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| program(f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_2) ).
fof(f15,axiom,
! [X0,X1] :
( outputs(c2,good)
| ~ halts2(X1,X1)
| ~ program(X1)
| program(f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_3) ).
fof(f16,axiom,
! [X0,X1] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| program(f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_4) ).
fof(f17,axiom,
! [X0,X1] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| program(f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_5) ).
fof(f18,axiom,
! [X0] :
( program(c2)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_6) ).
fof(f19,axiom,
! [X0,X1] :
( halts2(c2,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_7) ).
fof(f21,axiom,
! [X0,X1] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_9) ).
fof(f22,axiom,
! [X0,X1] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_10) ).
fof(f23,axiom,
! [X0] :
( program(c2)
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_11) ).
fof(f24,axiom,
! [X0,X1] :
( halts2(c2,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_12) ).
fof(f25,axiom,
! [X0,X1] :
( outputs(c2,good)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_13) ).
fof(f26,axiom,
! [X0,X1] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_14) ).
fof(f28,axiom,
! [X0] :
( program(c2)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_16) ).
fof(f29,axiom,
! [X0,X1] :
( halts2(c2,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_17) ).
fof(f30,axiom,
! [X0,X1] :
( outputs(c2,good)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_18) ).
fof(f31,axiom,
! [X0,X1] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_19) ).
fof(f32,axiom,
! [X0,X1] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_3_20) ).
fof(f33,axiom,
! [X0] :
( program(c3)
| program(f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_1) ).
fof(f34,axiom,
! [X0,X1] :
( ~ halts2(c3,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| program(f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_2) ).
fof(f35,axiom,
! [X0,X1] :
( halts2(c3,X1)
| halts2(X1,X1)
| ~ program(X1)
| program(f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_3) ).
fof(f36,axiom,
! [X0,X1] :
( outputs(c3,bad)
| halts2(X1,X1)
| ~ program(X1)
| program(f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_4) ).
fof(f41,axiom,
! [X0] :
( program(c3)
| ~ halts2(f6(X0),f6(X0))
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_9) ).
fof(f42,axiom,
! [X0,X1] :
( ~ halts2(c3,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f6(X0),f6(X0))
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_10) ).
fof(f43,axiom,
! [X0,X1] :
( halts2(c3,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f6(X0),f6(X0))
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_11) ).
fof(f44,axiom,
! [X0,X1] :
( outputs(c3,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ halts2(f6(X0),f6(X0))
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_12) ).
fof(f45,axiom,
! [X0] :
( program(c3)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_13) ).
fof(f46,axiom,
! [X0,X1] :
( ~ halts2(c3,X1)
| ~ halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_14) ).
fof(f47,axiom,
! [X0,X1] :
( halts2(c3,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_15) ).
fof(f48,axiom,
! [X0,X1] :
( outputs(c3,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',hypothesis_4_17) ).
fof(f49,negated_conjecture,
algorithm(c4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_deciding_algorithm) ).
fof(f50,negated_conjecture,
! [X0,X1] :
( decides(c4,X0,X1)
| ~ program(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_the_algorithm_doesnt_exist) ).
tcf(c_99,plain,
! [X0: $i] :
( program(c1)
| program(f2(X0))
| ~ algorithm(X0) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i] :
( program(f2(X0))
| decides(c1,X1,X2)
| ~ program(X1)
| ~ algorithm(X0) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_101,plain,
! [X0: $i] :
( program(c1)
| ~ algorithm(X0)
| ~ decides(X0,f2(X0),f1(X0)) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] :
( decides(c1,X1,X2)
| ~ program(X1)
| ~ algorithm(X0)
| ~ decides(X0,f2(X0),f1(X0)) ),
inference(cnf_transformation,[],[f4]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] :
( program(f4(X2))
| halts3(X2,X0,X1)
| ~ program(X2)
| ~ program(X0)
| ~ halts2(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i] :
( outputs(X2,good)
| program(f4(X2))
| ~ program(X2)
| ~ program(X0)
| ~ halts2(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] :
( program(f4(X0))
| halts2(X1,X2)
| halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i] :
( outputs(X0,bad)
| program(f4(X0))
| halts2(X1,X2)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i] :
( halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0)
| ~ halts2(X1,X2)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i] :
( outputs(X0,good)
| ~ program(X1)
| ~ program(X0)
| ~ halts2(X1,X2)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i] :
( halts2(X1,X2)
| halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i] :
( outputs(X0,bad)
| halts2(X1,X2)
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_111,plain,
! [X0: $i] :
( program(c2)
| program(f5(X0))
| ~ program(X0) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X0)
| program(f5(X1))
| ~ program(X1)
| ~ program(X0)
| ~ halts2(X0,X0) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| program(f5(X1))
| ~ program(X1)
| ~ program(X0)
| ~ halts2(X0,X0) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_114,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f5(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| program(f5(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_116,plain,
! [X0: $i] :
( program(c2)
| halts2(f5(X0),f5(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts2(X1,X1)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(X1,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_121,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(X1,X1)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(X1,X1)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_126,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X1,X1)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X1,X1)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_129,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_130,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_131,plain,
! [X0: $i] :
( program(c3)
| program(f6(X0))
| ~ program(X0) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_132,plain,
! [X0: $i,X1: $i] :
( program(f6(X1))
| ~ program(X1)
| ~ program(X0)
| ~ halts2(c3,X0)
| ~ halts2(X0,X0) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i] :
( halts2(c3,X1)
| program(f6(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] :
( outputs(c3,bad)
| program(f6(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_139,plain,
! [X0: $i] :
( program(c3)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ halts2(f6(X0),f6(X0)) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_140,plain,
! [X0: $i,X1: $i] :
( ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(c3,X1)
| ~ halts2(X1,X1)
| ~ halts2(X0,f6(X0))
| ~ halts2(f6(X0),f6(X0)) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i] :
( halts2(c3,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ halts2(f6(X0),f6(X0)) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i] :
( outputs(c3,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0))
| ~ halts2(f6(X0),f6(X0)) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_143,plain,
! [X0: $i] :
( program(c3)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0)) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_144,plain,
! [X0: $i,X1: $i] :
( ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(c3,X1)
| ~ halts2(X1,X1)
| ~ halts2(X0,f6(X0)) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i] :
( halts2(c3,X1)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0)) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] :
( outputs(c3,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0)) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_147,negated_conjecture,
algorithm(c4),
inference(cnf_transformation,[],[f49]) ).
tcf(c_148,negated_conjecture,
! [X0: $i,X1: $i] :
( decides(c4,X0,X1)
| ~ program(X0) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_198,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ decides(X0,f4(X0),f3(X0))
| ~ program(X0)
| ~ program(X1)
| halts3(X0,X1,X2) ),
inference(global_subsumption_just,[status(thm)],[c_109,c_109,c_107]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i] :
( halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(renaming,[status(thm)],[c_198]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i,X2: $i] :
( halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_107,c_199]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ outputs(X0,bad)
| ~ program(X0)
| ~ program(X1) ),
inference(global_subsumption_just,[status(thm)],[c_129,c_129,c_127]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(renaming,[status(thm)],[c_203]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_127,c_204]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ outputs(X0,bad)
| ~ program(X0)
| ~ program(X1)
| halts2(f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_119,c_119,c_117]) ).
tcf(c_209,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(renaming,[status(thm)],[c_208]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ program(X0)
| ~ program(X1) ),
inference(global_subsumption_just,[status(thm)],[c_124,c_124,c_122]) ).
tcf(c_212,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(renaming,[status(thm)],[c_211]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_117,c_209]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts3(X0,f5(X0),f5(X0))
| ~ halts2(f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_122,c_212]) ).
tcf(c_217,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ halts3(X0,f5(X0),f5(X0)) ),
inference(renaming,[status(thm)],[c_216]) ).
tcf(c_287,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f5(X0))
| ~ program(X1)
| ~ program(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_114,c_112]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i,X2: $i] :
( program(f4(X0))
| halts3(X0,X1,X2)
| ~ program(X1)
| ~ program(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_105,c_103]) ).
tcf(c_706,plain,
! [X0: $i,X1: $i] :
( decides(c1,X0,X1)
| ~ program(X0)
| ~ decides(c4,f2(c4),f1(c4)) ),
inference(resolution,[status(thm)],[c_102,c_147]) ).
tcf(c_717,plain,
( program(c1)
| ~ decides(c4,f2(c4),f1(c4)) ),
inference(resolution,[status(thm)],[c_101,c_147]) ).
tcf(c_724,plain,
! [X0: $i,X1: $i] :
( program(f2(c4))
| decides(c1,X0,X1)
| ~ program(X0) ),
inference(resolution,[status(thm)],[c_100,c_147]) ).
tcf(c_735,plain,
( program(c1)
| program(f2(c4)) ),
inference(resolution,[status(thm)],[c_99,c_147]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f4(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ program(f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_214]) ).
tcf(c_777,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f4(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad) ),
inference(global_subsumption_just,[status(thm)],[c_775,c_287,c_775]) ).
tcf(c_798,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f4(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_206]) ).
tcf(c_800,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| program(f4(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good) ),
inference(global_subsumption_just,[status(thm)],[c_798,c_287,c_798]) ).
tcf(c_821,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| program(f4(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_130]) ).
tcf(c_823,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| program(f4(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good) ),
inference(global_subsumption_just,[status(thm)],[c_821,c_115,c_821]) ).
tcf(c_840,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| program(f4(X0))
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good) ),
inference(forward_subsumption_resolution,[status(thm)],[c_823,c_106]) ).
tcf(c_848,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| program(f4(X1))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X1,bad)
| ~ outputs(X1,good)
| ~ program(f5(X1))
| ~ halts2(X0,X0) ),
inference(resolution,[status(thm)],[c_346,c_128]) ).
tcf(c_850,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| program(f4(X1))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X1,bad)
| ~ outputs(X1,good)
| ~ halts2(X0,X0) ),
inference(global_subsumption_just,[status(thm)],[c_848,c_113,c_848]) ).
tcf(c_867,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| program(f4(X1))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X1,bad)
| ~ halts2(X0,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_850,c_104]) ).
tcf(c_875,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_126]) ).
tcf(c_877,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good) ),
inference(global_subsumption_just,[status(thm)],[c_875,c_111,c_875]) ).
tcf(c_922,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ halts2(f5(X0),f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_121]) ).
tcf(c_924,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_922,c_111,c_922]) ).
tcf(c_973,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ program(f5(X0)) ),
inference(resolution,[status(thm)],[c_346,c_116]) ).
tcf(c_975,plain,
! [X0: $i] :
( program(c2)
| program(f4(X0))
| halts2(f5(X0),f5(X0))
| ~ program(X0)
| ~ outputs(X0,bad) ),
inference(global_subsumption_just,[status(thm)],[c_973,c_111,c_973]) ).
tcf(c_993,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_217]) ).
tcf(c_995,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0))
| ~ halts2(f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_993,c_287,c_993]) ).
tcf(c_996,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(renaming,[status(thm)],[c_995]) ).
tcf(c_1016,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_214]) ).
tcf(c_1018,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1016,c_287,c_1016]) ).
tcf(c_1039,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_206]) ).
tcf(c_1041,plain,
! [X0: $i,X1: $i] :
( halts2(c2,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1039,c_996,c_1018]) ).
tcf(c_1062,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_130]) ).
tcf(c_1064,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1062,c_115,c_1062]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1064,c_110]) ).
tcf(c_1089,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ halts2(X1,X1)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_128]) ).
tcf(c_1107,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ halts2(X1,X1)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1089,c_108,c_113]) ).
tcf(c_1115,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_126]) ).
tcf(c_1117,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1115,c_111,c_1115]) ).
tcf(c_1139,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ halts2(X1,X1)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_123]) ).
tcf(c_1141,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0))
| ~ halts2(f5(X0),f5(X0))
| ~ halts2(X1,X1)
| ~ program(f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1139,c_110,c_108,c_1107,c_1139]) ).
tcf(c_1142,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ program(f5(X0))
| ~ halts2(X1,X1)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(renaming,[status(thm)],[c_1141]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i] :
( outputs(c2,good)
| ~ program(X1)
| ~ program(X0)
| ~ halts2(X1,X1)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1142,c_113]) ).
tcf(c_1166,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ program(f5(X0))
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_121]) ).
tcf(c_1168,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0))
| ~ halts2(f5(X0),f5(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1166,c_111,c_1166]) ).
tcf(c_1169,plain,
! [X0: $i] :
( program(c2)
| ~ program(X0)
| ~ outputs(X0,good)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(renaming,[status(thm)],[c_1168]) ).
tcf(c_1186,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_120]) ).
tcf(c_1188,plain,
! [X0: $i,X1: $i] :
( outputs(c2,bad)
| halts2(X1,X1)
| halts2(f5(X0),f5(X0))
| ~ program(X1)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1186,c_115,c_110,c_108,c_1081,c_1186]) ).
tcf(c_1213,plain,
! [X0: $i] :
( program(c2)
| halts2(f5(X0),f5(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ program(f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(resolution,[status(thm)],[c_201,c_116]) ).
tcf(c_1215,plain,
! [X0: $i] :
( program(c2)
| halts2(f5(X0),f5(X0))
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1213,c_111,c_1213]) ).
tcf(c_1865,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ program(X0)
| halts2(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_1188]) ).
tcf(c_1866,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ program(X0)
| halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_1188]) ).
tcf(c_1867,plain,
( iPr_def_11
| iPr_def_10
| outputs(c2,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1188]) ).
tcf(c_1868,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ program(X0)
| ~ halts2(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_1158]) ).
tcf(c_1871,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ program(X0)
| ~ outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_1107]) ).
tcf(c_1872,plain,
( iPr_def_14
| iPr_def_12
| outputs(c2,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1107]) ).
tcf(c_1873,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ program(X0)
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_1081]) ).
tcf(c_1874,plain,
( iPr_def_15
| iPr_def_10
| outputs(c2,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1081]) ).
tcf(c_1875,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ program(X0)
| halts2(c2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_1041]) ).
tcf(c_1876,plain,
! [X0: $i] :
( ~ iPr_def_17
| ~ program(X0)
| ~ outputs(X0,good)
| ~ outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_1041]) ).
tcf(c_1877,plain,
( iPr_def_17
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1041]) ).
tcf(c_1878,plain,
! [X0: $i] :
( ~ iPr_def_18
| ~ program(X0)
| halts2(f5(X0),f5(X0))
| ~ outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_1018]) ).
tcf(c_1879,plain,
( iPr_def_18
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_1018]) ).
tcf(c_1880,plain,
! [X0: $i] :
( ~ iPr_def_19
| ~ program(X0)
| ~ halts2(f5(X0),f5(X0))
| ~ outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_996]) ).
tcf(c_1886,plain,
! [X0: $i] :
( ~ iPr_def_22
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_867]) ).
tcf(c_1887,plain,
( iPr_def_22
| iPr_def_12
| outputs(c2,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_867]) ).
tcf(c_1888,plain,
! [X0: $i] :
( ~ iPr_def_23
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_840]) ).
tcf(c_1889,plain,
( iPr_def_23
| iPr_def_10
| outputs(c2,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_840]) ).
tcf(c_1890,plain,
! [X0: $i] :
( ~ iPr_def_24
| program(f4(X0))
| ~ program(X0)
| ~ outputs(X0,good)
| ~ outputs(X0,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_800]) ).
tcf(c_1891,plain,
( iPr_def_24
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_800]) ).
tcf(c_1892,plain,
! [X0: $i] :
( ~ iPr_def_25
| program(f4(X0))
| ~ program(X0)
| halts2(f5(X0),f5(X0))
| ~ outputs(X0,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_777]) ).
tcf(c_1893,plain,
( iPr_def_25
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_777]) ).
tcf(c_1896,plain,
! [X0: $i] :
( ~ iPr_def_27
| program(f5(X0))
| ~ program(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_287]) ).
tcf(c_1897,plain,
( iPr_def_27
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_287]) ).
tcf(c_1898,plain,
! [X0: $i] :
( ~ iPr_def_28
| ~ program(X0)
| ~ halts2(X0,f6(X0))
| ~ outputs(X0,good)
| ~ outputs(X0,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_146]) ).
tcf(c_1900,plain,
! [X0: $i] :
( ~ iPr_def_29
| ~ program(X0)
| halts2(c3,X0)
| halts2(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_145]) ).
tcf(c_1901,plain,
( iPr_def_29
| iPr_def_28 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_145]) ).
tcf(c_1902,plain,
! [X0: $i] :
( ~ iPr_def_30
| ~ program(X0)
| ~ halts2(c3,X0)
| ~ halts2(X0,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_144]) ).
tcf(c_1903,plain,
( iPr_def_30
| iPr_def_28 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_144]) ).
tcf(c_1904,plain,
! [X0: $i] :
( ~ iPr_def_31
| program(f6(X0))
| ~ program(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_134]) ).
tcf(c_1906,plain,
( iPr_def_31
| iPr_def_29 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_133]) ).
tcf(c_1908,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_32
| ~ program(X0)
| halts2(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_106]) ).
tcf(c_1909,plain,
! [X0: $i] :
( ~ iPr_def_33
| program(f4(X0))
| ~ program(X0)
| outputs(X0,bad) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_106]) ).
tcf(c_1910,plain,
( iPr_def_33
| iPr_def_32 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_106]) ).
tcf(c_1911,plain,
! [X0: $i] :
( ~ iPr_def_34
| ~ program(X0)
| ~ halts2(f6(X0),f6(X0))
| ~ halts2(X0,f6(X0))
| ~ outputs(X0,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_142]) ).
tcf(c_1913,plain,
( iPr_def_34
| iPr_def_29 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_141]) ).
tcf(c_1914,plain,
( iPr_def_34
| iPr_def_30 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_140]) ).
tcf(c_1919,plain,
( iPr_def_31
| iPr_def_30 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_132]) ).
tcf(c_1920,plain,
( iPr_def_27
| iPr_def_12
| outputs(c2,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_113]) ).
tcf(c_1921,plain,
! [X0: $i] :
( ~ iPr_def_36
| ~ program(X0)
| outputs(X0,bad)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_36])],[c_110]) ).
tcf(c_1922,plain,
( iPr_def_36
| iPr_def_32 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_110]) ).
tcf(c_1923,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_37
| ~ program(X0)
| ~ halts2(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_37])],[c_108]) ).
tcf(c_1924,plain,
! [X0: $i] :
( ~ iPr_def_38
| ~ program(X0)
| outputs(X0,good)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_38])],[c_108]) ).
tcf(c_1925,plain,
( iPr_def_38
| iPr_def_37 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_108]) ).
tcf(c_1926,plain,
! [X0: $i] :
( ~ iPr_def_39
| program(f4(X0))
| ~ program(X0)
| outputs(X0,good) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_39])],[c_104]) ).
tcf(c_1927,plain,
( iPr_def_39
| iPr_def_37 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_104]) ).
tcf(c_1963,plain,
( program(c2)
| program(f5(c1))
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_1964,plain,
( program(c3)
| program(f6(c1))
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_1966,plain,
! [X0: $i] :
( halts2(c1,X0)
| ~ iPr_def_32
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1908]) ).
tcf(c_1968,plain,
! [X0: $i] :
( ~ iPr_def_37
| ~ program(c1)
| ~ halts2(c1,X0) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_1970,plain,
( program(c2)
| program(f4(c1))
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ outputs(c1,good) ),
inference(instantiation,[status(thm)],[c_877]) ).
tcf(c_1975,plain,
( program(c3)
| ~ program(c1)
| ~ outputs(c1,good)
| ~ halts2(c1,f6(c1))
| ~ halts2(f6(c1),f6(c1)) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_1976,plain,
( program(c2)
| program(f4(c1))
| ~ program(c1)
| ~ outputs(c1,good)
| ~ halts2(f5(c1),f5(c1)) ),
inference(instantiation,[status(thm)],[c_924]) ).
tcf(c_1977,plain,
( program(c2)
| program(f4(c1))
| halts2(f5(c1),f5(c1))
| ~ program(c1)
| ~ outputs(c1,bad) ),
inference(instantiation,[status(thm)],[c_975]) ).
tcf(c_1992,plain,
! [X0: $i] :
( ~ iPr_def_37
| ~ program(f5(c1))
| ~ halts2(f5(c1),X0) ),
inference(instantiation,[status(thm)],[c_1923]) ).
tcf(c_2015,plain,
! [X0: $i] :
( halts2(f6(c1),X0)
| ~ iPr_def_32
| ~ program(f6(c1)) ),
inference(instantiation,[status(thm)],[c_1908]) ).
tcf(c_2041,plain,
! [X0: $i] :
( program(f2(c4))
| decides(c1,f4(c1),X0)
| ~ program(f4(c1)) ),
inference(instantiation,[status(thm)],[c_724]) ).
tcf(c_2064,plain,
! [X0: $i] :
( decides(c4,f2(c4),X0)
| ~ program(f2(c4)) ),
inference(instantiation,[status(thm)],[c_148]) ).
tcf(c_2076,plain,
( ~ iPr_def_30
| ~ program(c3)
| ~ halts2(c3,c3) ),
inference(instantiation,[status(thm)],[c_1902]) ).
tcf(c_2077,plain,
( halts2(c3,c3)
| ~ iPr_def_29
| ~ program(c3) ),
inference(instantiation,[status(thm)],[c_1900]) ).
tcf(c_2080,plain,
! [X0: $i] :
( halts2(c3,X0)
| ~ iPr_def_32
| ~ program(c3) ),
inference(instantiation,[status(thm)],[c_1908]) ).
tcf(c_2131,plain,
( program(c3)
| ~ program(c2)
| ~ outputs(c2,good)
| ~ halts2(c2,f6(c2))
| ~ halts2(f6(c2),f6(c2)) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_2140,plain,
( program(c3)
| program(f6(c2))
| ~ program(c2) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_2298,plain,
( program(f6(c1))
| ~ iPr_def_31
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1904]) ).
tcf(c_2299,plain,
( program(f6(c2))
| ~ iPr_def_31
| ~ program(c2) ),
inference(instantiation,[status(thm)],[c_1904]) ).
tcf(c_2301,plain,
( outputs(c1,bad)
| program(f4(c1))
| ~ iPr_def_33
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1909]) ).
tcf(c_2304,plain,
( ~ iPr_def_34
| ~ program(c1)
| ~ outputs(c1,good)
| ~ halts2(c1,f6(c1))
| ~ halts2(f6(c1),f6(c1)) ),
inference(instantiation,[status(thm)],[c_1911]) ).
tcf(c_2305,plain,
( ~ iPr_def_34
| ~ program(c2)
| ~ outputs(c2,good)
| ~ halts2(c2,f6(c2))
| ~ halts2(f6(c2),f6(c2)) ),
inference(instantiation,[status(thm)],[c_1911]) ).
tcf(c_2577,plain,
( program(f5(c1))
| ~ iPr_def_27
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1896]) ).
tcf(c_2696,plain,
( program(f4(c1))
| ~ iPr_def_24
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ outputs(c1,good) ),
inference(instantiation,[status(thm)],[c_1890]) ).
tcf(c_2703,plain,
( ~ iPr_def_37
| ~ program(f5(c1))
| ~ halts2(f5(c1),f5(c1)) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_2704,plain,
( program(f4(c1))
| halts2(f5(c1),f5(c1))
| ~ iPr_def_25
| ~ program(c1)
| ~ outputs(c1,bad) ),
inference(instantiation,[status(thm)],[c_1892]) ).
tcf(c_2739,plain,
( decides(c4,f2(c4),f1(c4))
| ~ program(f2(c4)) ),
inference(instantiation,[status(thm)],[c_2064]) ).
tcf(c_2808,plain,
program(c1),
inference(global_subsumption_just,[status(thm)],[c_735,c_717,c_735,c_2739]) ).
tcf(c_2814,plain,
! [X0: $i,X1: $i] :
( ~ program(X0)
| decides(c1,X0,X1) ),
inference(global_subsumption_just,[status(thm)],[c_724,c_706,c_724,c_2739]) ).
tcf(c_2815,plain,
! [X0: $i,X1: $i] :
( decides(c1,X0,X1)
| ~ program(X0) ),
inference(renaming,[status(thm)],[c_2814]) ).
tcf(c_2868,plain,
( program(c2)
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1117]) ).
tcf(c_2869,plain,
( program(c2)
| ~ outputs(c1,bad)
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2868,c_2808]) ).
tcf(c_2929,plain,
! [X0: $i] :
( ~ halts2(X0,f6(X0))
| ~ outputs(X0,good)
| ~ outputs(X0,bad)
| ~ program(X0) ),
inference(global_subsumption_just,[status(thm)],[c_143,c_143,c_1901,c_1903,c_1898,c_2077,c_2076]) ).
tcf(c_2930,plain,
! [X0: $i] :
( ~ program(X0)
| ~ outputs(X0,bad)
| ~ outputs(X0,good)
| ~ halts2(X0,f6(X0)) ),
inference(renaming,[status(thm)],[c_2929]) ).
tcf(c_3023,plain,
( program(c2)
| ~ outputs(c1,bad)
| ~ outputs(c1,good) ),
inference(global_subsumption_just,[status(thm)],[c_2869,c_717,c_735,c_1970,c_2739,c_2869]) ).
tcf(c_3098,plain,
( program(c2)
| ~ program(c1)
| ~ outputs(c1,good)
| ~ program(f4(c1))
| ~ halts2(f5(c1),f5(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1169]) ).
tcf(c_3099,plain,
( program(c2)
| ~ outputs(c1,good)
| ~ program(f4(c1))
| ~ halts2(f5(c1),f5(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3098,c_2808]) ).
tcf(c_3201,plain,
( halts2(f5(c1),f5(c1))
| ~ iPr_def_18
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ decides(c1,f4(c1),f3(c1)) ),
inference(instantiation,[status(thm)],[c_1878]) ).
tcf(c_3334,plain,
( program(c2)
| ~ outputs(c1,good)
| ~ halts2(f5(c1),f5(c1)) ),
inference(global_subsumption_just,[status(thm)],[c_3099,c_717,c_735,c_1976,c_2739,c_3099]) ).
tcf(c_3464,plain,
( program(c2)
| halts2(f5(c1),f5(c1))
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1215]) ).
tcf(c_3465,plain,
( program(c2)
| halts2(f5(c1),f5(c1))
| ~ outputs(c1,bad)
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3464,c_2808]) ).
tcf(c_3650,plain,
( program(c2)
| ~ iPr_def_10
| ~ outputs(c1,good)
| ~ program(f5(c1)) ),
inference(superposition,[status(thm)],[c_1865,c_3334]) ).
tcf(c_3692,plain,
( halts2(c1,f6(c1))
| ~ iPr_def_32
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1966]) ).
tcf(c_4184,plain,
( halts2(c2,f6(c2))
| ~ iPr_def_16
| ~ program(f6(c2)) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_4215,plain,
( program(c2)
| halts2(f5(c1),f5(c1))
| ~ outputs(c1,bad) ),
inference(global_subsumption_just,[status(thm)],[c_3465,c_717,c_735,c_1977,c_2739,c_3465]) ).
tcf(c_4277,plain,
( program(c2)
| ~ iPr_def_10
| ~ outputs(c1,good) ),
inference(global_subsumption_just,[status(thm)],[c_3650,c_717,c_735,c_1963,c_2739,c_3650]) ).
tcf(c_4299,plain,
( ~ iPr_def_16
| ~ program(c2)
| ~ outputs(c2,bad)
| ~ outputs(c2,good)
| ~ program(f6(c2)) ),
inference(superposition,[status(thm)],[c_1875,c_2930]) ).
tcf(c_4337,plain,
( program(c2)
| ~ iPr_def_32
| ~ outputs(c1,good)
| ~ program(f5(c1)) ),
inference(superposition,[status(thm)],[c_1908,c_3334]) ).
tcf(c_4433,plain,
( halts2(f5(c1),f5(c1))
| ~ iPr_def_11
| ~ program(c1)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1866]) ).
tcf(c_4434,plain,
( halts2(f5(c1),f5(c1))
| ~ iPr_def_11
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4433,c_2808]) ).
tcf(c_4466,plain,
! [X0: $i] :
( ~ iPr_def_37
| ~ iPr_def_32
| ~ program(X0) ),
inference(superposition,[status(thm)],[c_1908,c_1923]) ).
tcf(c_4468,plain,
! [X0: $i] :
( ~ iPr_def_37
| ~ iPr_def_16
| ~ program(c2)
| ~ program(X0) ),
inference(superposition,[status(thm)],[c_1875,c_1923]) ).
tcf(c_4470,plain,
( program(c2)
| ~ iPr_def_37
| ~ outputs(c1,bad)
| ~ program(f5(c1)) ),
inference(superposition,[status(thm)],[c_4215,c_1923]) ).
tcf(c_5096,plain,
( outputs(c1,good)
| program(f4(c1))
| ~ iPr_def_39
| ~ program(c1) ),
inference(instantiation,[status(thm)],[c_1926]) ).
tcf(c_5294,plain,
( halts2(c3,c3)
| ~ iPr_def_29
| ~ program(c3) ),
inference(equality_factoring,[status(thm)],[c_1900]) ).
tcf(c_6934,plain,
( program(c2)
| program(f4(c1))
| ~ iPr_def_39
| ~ iPr_def_10
| ~ program(c1) ),
inference(superposition,[status(thm)],[c_1926,c_4277]) ).
tcf(c_6935,plain,
( program(c2)
| program(f4(c1))
| ~ iPr_def_39
| ~ program(c1)
| ~ outputs(c1,bad) ),
inference(superposition,[status(thm)],[c_1926,c_3023]) ).
tcf(c_6936,plain,
( program(c2)
| program(f4(c1))
| ~ iPr_def_39
| ~ iPr_def_10 ),
inference(forward_subsumption_resolution,[status(thm)],[c_6934,c_2808]) ).
tcf(c_6941,plain,
( program(c2)
| program(f4(c1))
| ~ iPr_def_39
| ~ outputs(c1,bad) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6935,c_2808]) ).
tcf(c_7052,plain,
( ~ iPr_def_37
| ~ iPr_def_32 ),
inference(global_subsumption_just,[status(thm)],[c_4466,c_717,c_735,c_1966,c_1968,c_2739]) ).
tcf(c_7295,plain,
( program(c2)
| program(f4(c1))
| ~ iPr_def_39 ),
inference(global_subsumption_just,[status(thm)],[c_6936,c_717,c_735,c_1910,c_1963,c_2301,c_2739,c_4337,c_5096,c_6941]) ).
tcf(c_7297,plain,
( program(c2)
| program(f4(c1)) ),
inference(global_subsumption_just,[status(thm)],[c_7295,c_717,c_735,c_1910,c_1927,c_1963,c_2301,c_2739,c_4470,c_7052,c_7295]) ).
tcf(c_7309,plain,
( ~ iPr_def_37
| ~ iPr_def_11
| ~ program(f5(c1))
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_4434,c_1923]) ).
tcf(c_7425,plain,
( decides(c1,f4(c1),f3(c1))
| ~ program(f4(c1))
| ~ decides(c4,f2(c4),f1(c4)) ),
inference(instantiation,[status(thm)],[c_706]) ).
tcf(c_7541,plain,
! [X0: $i] :
( ~ iPr_def_32
| ~ iPr_def_30
| ~ program(X0)
| ~ halts2(c3,X0) ),
inference(superposition,[status(thm)],[c_1908,c_1902]) ).
tcf(c_7543,plain,
! [X0: $i] :
( ~ iPr_def_30
| ~ iPr_def_10
| ~ program(X0)
| ~ halts2(c3,X0) ),
inference(superposition,[status(thm)],[c_1865,c_1902]) ).
tcf(c_7549,plain,
( ~ iPr_def_30
| ~ iPr_def_29
| ~ program(c3)
| ~ halts2(c3,c3) ),
inference(superposition,[status(thm)],[c_5294,c_1902]) ).
tcf(c_7609,plain,
( halts2(f6(c2),f6(c2))
| ~ iPr_def_10
| ~ program(f6(c2)) ),
inference(instantiation,[status(thm)],[c_1865]) ).
tcf(c_7729,plain,
! [X0: $i] :
( ~ iPr_def_30
| ~ iPr_def_10
| ~ program(X0)
| ~ halts2(c3,X0) ),
inference(superposition,[status(thm)],[c_1865,c_1902]) ).
tcf(c_7834,plain,
( program(f4(c1))
| ~ iPr_def_22
| ~ program(c1)
| ~ outputs(c1,bad) ),
inference(instantiation,[status(thm)],[c_1886]) ).
tcf(c_7889,plain,
( outputs(c1,bad)
| ~ iPr_def_36
| ~ program(c1)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1921]) ).
tcf(c_7890,plain,
( outputs(c1,bad)
| ~ iPr_def_36
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7889,c_2808]) ).
tcf(c_7959,plain,
( outputs(c1,good)
| ~ iPr_def_38
| ~ program(c1)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1924]) ).
tcf(c_7960,plain,
( outputs(c1,good)
| ~ iPr_def_38
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_7959,c_2808]) ).
tcf(c_7972,plain,
( halts2(f6(c1),f6(c1))
| ~ iPr_def_32
| ~ program(f6(c1)) ),
inference(instantiation,[status(thm)],[c_2015]) ).
tcf(c_8028,plain,
( ~ iPr_def_16
| ~ iPr_def_12
| ~ program(c2) ),
inference(superposition,[status(thm)],[c_1875,c_1868]) ).
tcf(c_8114,plain,
( program(f2(c4))
| decides(c1,f4(c1),f3(c1))
| ~ program(f4(c1)) ),
inference(instantiation,[status(thm)],[c_2041]) ).
tcf(c_8481,plain,
( program(c2)
| outputs(c1,bad)
| ~ iPr_def_36 ),
inference(superposition,[status(thm)],[c_7297,c_7890]) ).
tcf(c_8704,plain,
( ~ iPr_def_14
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1871]) ).
tcf(c_8705,plain,
( ~ iPr_def_14
| ~ outputs(c1,bad)
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_8704,c_2808]) ).
tcf(c_9113,plain,
( program(c2)
| outputs(c1,bad) ),
inference(global_subsumption_just,[status(thm)],[c_8481,c_717,c_735,c_1922,c_1925,c_1963,c_2739,c_4337,c_7052,c_7297,c_7960,c_8481]) ).
tcf(c_9115,plain,
program(c2),
inference(global_subsumption_just,[status(thm)],[c_9113,c_717,c_735,c_1925,c_1963,c_2739,c_2869,c_4470,c_7297,c_7960,c_9113]) ).
tcf(c_9184,plain,
( ~ iPr_def_15
| ~ program(c1)
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1873]) ).
tcf(c_9185,plain,
( ~ iPr_def_15
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9184,c_2808]) ).
tcf(c_9259,plain,
! [X0: $i] :
( ~ iPr_def_37
| ~ iPr_def_16
| ~ program(X0) ),
inference(global_subsumption_just,[status(thm)],[c_4468,c_4468,c_9115]) ).
tcf(c_9268,plain,
( ~ iPr_def_37
| ~ iPr_def_16 ),
inference(superposition,[status(thm)],[c_2808,c_9259]) ).
tcf(c_9453,plain,
( ~ iPr_def_17
| ~ program(c1)
| ~ outputs(c1,bad)
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_1876]) ).
tcf(c_9454,plain,
( ~ iPr_def_17
| ~ outputs(c1,bad)
| ~ outputs(c1,good)
| ~ program(f4(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_9453,c_2808]) ).
tcf(c_9557,plain,
! [X0: $i] :
( ~ iPr_def_32
| ~ iPr_def_30
| ~ program(X0) ),
inference(global_subsumption_just,[status(thm)],[c_7541,c_717,c_735,c_1925,c_1927,c_1964,c_1975,c_2080,c_2739,c_3692,c_5096,c_7052,c_7541,c_7960,c_7972]) ).
tcf(c_9560,plain,
! [X0: $i] :
( ~ iPr_def_32
| ~ program(X0) ),
inference(global_subsumption_just,[status(thm)],[c_9557,c_717,c_735,c_1914,c_1919,c_1925,c_1927,c_2298,c_2304,c_2739,c_3692,c_5096,c_7052,c_7960,c_7972,c_9557]) ).
tcf(c_9567,plain,
~ iPr_def_32,
inference(superposition,[status(thm)],[c_2808,c_9560]) ).
tcf(c_9571,plain,
iPr_def_36,
inference(backward_subsumption_resolution,[status(thm)],[c_1922,c_9567]) ).
tcf(c_9572,plain,
iPr_def_33,
inference(backward_subsumption_resolution,[status(thm)],[c_1910,c_9567]) ).
tcf(c_9573,plain,
( outputs(c1,bad)
| ~ program(f4(c1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_7890,c_9571]) ).
tcf(c_9611,plain,
( ~ iPr_def_17
| ~ program(f4(c1)) ),
inference(global_subsumption_just,[status(thm)],[c_9454,c_717,c_735,c_1879,c_1897,c_1925,c_2577,c_2703,c_2739,c_3201,c_7425,c_7960,c_8114,c_9268,c_9454,c_9573]) ).
tcf(c_9644,plain,
outputs(c1,bad),
inference(global_subsumption_just,[status(thm)],[c_9573,c_717,c_735,c_2301,c_2739,c_7890,c_9572,c_9571]) ).
tcf(c_9653,plain,
~ iPr_def_37,
inference(global_subsumption_just,[status(thm)],[c_7309,c_1877,c_1893,c_1897,c_2577,c_2703,c_2704,c_2808,c_9268,c_9611,c_9644]) ).
tcf(c_9656,plain,
iPr_def_38,
inference(backward_subsumption_resolution,[status(thm)],[c_1925,c_9653]) ).
tcf(c_9661,plain,
( outputs(c1,good)
| ~ program(f4(c1)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_7960,c_9656]) ).
tcf(c_9663,plain,
! [X0: $i] :
( outputs(X0,good)
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1924,c_9656]) ).
tcf(c_9674,plain,
! [X0: $i] :
( ~ iPr_def_18
| ~ program(X0)
| halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1878,c_717,c_735,c_1877,c_1891,c_1893,c_1897,c_1906,c_1913,c_1914,c_1919,c_1925,c_1927,c_1867,c_1872,c_1887,c_1866,c_1963,c_2077,c_2140,c_2131,c_2299,c_2301,c_2305,c_2577,c_2696,c_2703,c_2704,c_2739,c_2869,c_4184,c_4299,c_4470,c_5096,c_7297,c_7549,c_7609,c_7834,c_7890,c_7960,c_8028,c_8705,c_9113,c_9268,c_9572,c_9571,c_9611]) ).
tcf(c_9675,plain,
! [X0: $i] :
( halts2(f5(X0),f5(X0))
| ~ iPr_def_18
| ~ program(X0)
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(renaming,[status(thm)],[c_9674]) ).
tcf(c_9685,plain,
( halts2(f5(c4),f5(c4))
| ~ iPr_def_18
| ~ program(c4)
| ~ program(f4(c4)) ),
inference(superposition,[status(thm)],[c_148,c_9675]) ).
tcf(c_9703,plain,
( ~ iPr_def_18
| ~ iPr_def_12
| ~ program(c4)
| ~ program(f5(c4))
| ~ program(f4(c4)) ),
inference(superposition,[status(thm)],[c_9685,c_1868]) ).
tcf(c_9789,plain,
outputs(c1,good),
inference(global_subsumption_just,[status(thm)],[c_9661,c_717,c_735,c_1877,c_1893,c_1897,c_1925,c_1927,c_2301,c_2577,c_2703,c_2704,c_2739,c_5096,c_7890,c_7960,c_9268,c_9572,c_9571,c_9611]) ).
tcf(c_9984,plain,
( ~ iPr_def_30
| ~ iPr_def_10
| ~ program(c3) ),
inference(superposition,[status(thm)],[c_1865,c_7729]) ).
tcf(c_10046,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_9703,c_717,c_735,c_1877,c_1891,c_1893,c_1897,c_1925,c_1927,c_1963,c_2301,c_2577,c_2696,c_2703,c_2704,c_2739,c_2869,c_4470,c_5096,c_7297,c_7890,c_7960,c_8028,c_9113,c_9268,c_9572,c_9571,c_9611]) ).
tcf(c_10048,plain,
( iPr_def_27
| outputs(c2,good) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1920,c_10046]) ).
tcf(c_10089,plain,
outputs(c2,good),
inference(global_subsumption_just,[status(thm)],[c_10048,c_717,c_735,c_1877,c_1891,c_1893,c_1897,c_1925,c_1927,c_1872,c_1887,c_1963,c_2301,c_2577,c_2696,c_2703,c_2704,c_2739,c_2869,c_4470,c_5096,c_7297,c_7834,c_7890,c_7960,c_8028,c_8705,c_9113,c_9268,c_9572,c_9571,c_9611]) ).
tcf(c_10091,plain,
! [X0: $i] :
( ~ iPr_def_19
| ~ program(X0)
| ~ halts2(f5(X0),f5(X0))
| ~ decides(X0,f4(X0),f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1880,c_717,c_735,c_1877,c_1891,c_1893,c_1897,c_1906,c_1913,c_1914,c_1919,c_1925,c_1927,c_1872,c_1874,c_1887,c_1873,c_1963,c_2077,c_2140,c_2131,c_2299,c_2301,c_2305,c_2577,c_2696,c_2703,c_2704,c_2739,c_2869,c_4184,c_4299,c_4470,c_5096,c_7297,c_7549,c_7609,c_7834,c_7890,c_7960,c_8028,c_8705,c_9113,c_9268,c_9572,c_9571,c_9611,c_9663]) ).
tcf(c_10103,plain,
( ~ iPr_def_19
| ~ program(c1)
| ~ program(f4(c1))
| ~ halts2(f5(c1),f5(c1)) ),
inference(superposition,[status(thm)],[c_2815,c_10091]) ).
tcf(c_10104,plain,
( ~ iPr_def_19
| ~ program(f4(c1))
| ~ halts2(f5(c1),f5(c1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_10103,c_2808]) ).
tcf(c_10143,plain,
( ~ iPr_def_30
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_7543,c_717,c_735,c_1877,c_1891,c_1906,c_1914,c_1919,c_1925,c_1963,c_2077,c_2140,c_2131,c_2299,c_2301,c_2305,c_2696,c_2739,c_2869,c_4184,c_4470,c_7297,c_7549,c_7609,c_7890,c_7960,c_9113,c_9572,c_9571,c_9611,c_9789,c_9984,c_10089]) ).
tcf(c_10145,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_10143,c_717,c_735,c_1877,c_1891,c_1906,c_1914,c_1919,c_1925,c_1963,c_2077,c_2140,c_2299,c_2301,c_2305,c_2696,c_2739,c_2869,c_4184,c_4470,c_7297,c_7549,c_7609,c_7890,c_7960,c_9113,c_9572,c_9571,c_9611,c_9789,c_10089,c_10143]) ).
tcf(c_10152,plain,
( iPr_def_23
| outputs(c2,bad) ),
inference(backward_subsumption_resolution,[status(thm)],[c_1889,c_10145]) ).
tcf(c_10202,plain,
~ program(f4(c1)),
inference(global_subsumption_just,[status(thm)],[c_10104,c_717,c_735,c_1877,c_1891,c_1893,c_1897,c_1906,c_1913,c_1914,c_1919,c_1925,c_1927,c_1872,c_1874,c_1887,c_1963,c_2077,c_2140,c_2131,c_2299,c_2301,c_2305,c_2577,c_2696,c_2703,c_2704,c_2739,c_2869,c_4184,c_4299,c_4470,c_5096,c_7297,c_7549,c_7609,c_7834,c_7890,c_7960,c_8028,c_8705,c_9113,c_9185,c_9268,c_9572,c_9571,c_9611]) ).
tcf(c_10212,plain,
iPr_def_23,
inference(global_subsumption_just,[status(thm)],[c_10152,c_717,c_735,c_1891,c_1906,c_1919,c_1925,c_1889,c_1963,c_2077,c_2140,c_2299,c_2301,c_2696,c_2739,c_2869,c_4299,c_4470,c_7297,c_7549,c_7890,c_7960,c_9113,c_9572,c_9571,c_9789,c_10089,c_10145,c_10202]) ).
tcf(c_10269,plain,
! [X0: $i] :
( ~ program(X0)
| program(f4(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_1888,c_1927,c_1926,c_1888,c_9653,c_10212]) ).
tcf(c_10270,plain,
! [X0: $i] :
( program(f4(X0))
| ~ program(X0) ),
inference(renaming,[status(thm)],[c_10269]) ).
tcf(c_10277,plain,
~ program(c1),
inference(superposition,[status(thm)],[c_10270,c_10202]) ).
tcf(c_10278,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_10277,c_2808]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COM003-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/10.60 % Computer : n006.cluster.edu
% 0.13/10.60 % Model : x86_64 x86_64
% 0.13/10.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.60 % Memory : 8046.5625MB
% 0.13/10.60 % OS : Linux 6.8.0-71-generic
% 0.13/10.60 % CPULimit : 300
% 0.13/10.60 % WCLimit : 300
% 0.13/10.60 % DateTime : Fri Sep 25 07:43:26 UTC 2026
% 0.13/10.60 % CPUTime :
% 0.13/10.60 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/10.64 Running first-order theorem proving
% 0.13/10.64 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/10.65
% 0.13/10.65 % ======== iProver multi-core TPTP/SMT =========
% 0.13/10.65
% 0.13/10.65 % Detected problem language: tptp
% 0.13/10.66 % Proving...
% 1.40/11.41 % SZS status Started for theBenchmark.p
% 1.40/11.41 % SZS status Unsatisfiable for theBenchmark.p
% 1.40/11.41
% 1.40/11.41 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 1.40/11.41
% 1.40/11.41 % ------ iProver source info
% 1.40/11.41
% 1.40/11.41 % git: date: 2026-07-19 20:42:38 +0200
% 1.40/11.41 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 1.40/11.41 % git: non_committed_changes: false
% 1.40/11.41
% 1.40/11.41 % ------ Parsing...% successful
% 1.40/11.41
% 1.40/11.41
% 1.40/11.41 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 1.40/11.41
% 1.40/11.41 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 1.40/11.41
% 1.40/11.41 % ------ Preprocessing... gs_s sp: 66 0s gs_e snvd_s sp: 0 0s snvd_e
% 1.40/11.41 % ------ Proving...
% 1.40/11.41 % ------ Problem Properties
% 1.40/11.41
% 1.40/11.41 %
% 1.40/11.41 % clauses 79
% 1.40/11.41 % conjectures 1
% 1.40/11.41 % EPR 41
% 1.40/11.41 % Horn 32
% 1.40/11.41 % unary 0
% 1.40/11.41 % binary 22
% 1.40/11.41 % lits 265
% 1.40/11.41 % lits eq 0
% 1.40/11.41 % fd_pure 0
% 1.40/11.41 % fd_pseudo 0
% 1.40/11.41 % fd_cond 0
% 1.40/11.41 % fd_pseudo_cond 0
% 1.40/11.41 % AC symbols 0
% 1.40/11.41
% 1.40/11.41 % ------ Schedule dynamic 5 is on
% 1.40/11.41
% 1.40/11.41 % ------ no equalities: superposition off
% 1.40/11.41
% 1.40/11.41 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 1.40/11.41
% 1.40/11.41
% 1.40/11.41 % ------
% 1.40/11.41 % Current options:
% 1.40/11.41 % ------
% 1.40/11.41
% 1.40/11.41
% 1.40/11.41 %
% 1.40/11.41
% 1.40/11.41 % ------ Proving...
% 1.40/11.41 %
% 1.40/11.41
% 1.40/11.41 % SZS status Unsatisfiable for theBenchmark.p
% 1.40/11.41
% 1.40/11.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 1.40/11.42
% 1.40/11.42
%------------------------------------------------------------------------------