%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN067-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n020.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 03:39:04 PM UTC 2026
% Result : Unsatisfiable 2.27s 6.27s
% Output : CNFRefutation 2.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named f114ERROR: Could not build tree for root c_5160ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(f54,negated_conjecture,
( big_p(c3)
| ~ big_p(c4)
| big_p(c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_54) ).
fof(f55,negated_conjecture,
( big_r(c4,c3)
| ~ big_p(c4)
| big_p(c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_55) ).
fof(f60,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X3,X2)
| ~ big_r(c4,X3)
| ~ big_p(X2)
| ~ big_r(X1,X0)
| ~ big_r(c4,X1)
| ~ big_p(X0)
| big_p(c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_60) ).
fof(f66,negated_conjecture,
( big_p(c3)
| ~ big_p(c4)
| big_r(c2,c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_66) ).
fof(f67,negated_conjecture,
( big_r(c4,c3)
| ~ big_p(c4)
| big_r(c2,c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_67) ).
fof(f72,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ big_r(X3,X2)
| ~ big_r(c4,X3)
| ~ big_p(X2)
| ~ big_r(X1,X0)
| ~ big_r(c4,X1)
| ~ big_p(X0)
| big_r(c2,c1)
| ~ big_p(c2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_72) ).
fof(f78,negated_conjecture,
! [X0,X1] :
( big_p(c3)
| ~ big_p(c4)
| ~ big_r(X1,X0)
| ~ big_r(c2,X1)
| ~ big_p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_78) ).
fof(f79,negated_conjecture,
! [X0,X1] :
( big_r(c4,c3)
| ~ big_p(c4)
| ~ big_r(X1,X0)
| ~ big_r(c2,X1)
| ~ big_p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_79) ).
fof(f84,negated_conjecture,
! [X2,X3,X0,X1,X4,X5] :
( ~ big_r(X5,X4)
| ~ big_r(c4,X5)
| ~ big_p(X4)
| ~ big_r(X3,X2)
| ~ big_r(c4,X3)
| ~ big_p(X2)
| ~ big_r(X1,X0)
| ~ big_r(c2,X1)
| ~ big_p(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause_84) ).
tcf(c_133,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_p(f2(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_134,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f2(X1))
| big_r(X0,f3(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_135,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f2(X1))
| big_r(f3(X0),f4(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_136,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_p(f2(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_137,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(X0,f5(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_138,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_139,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_r(X0,f1(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_140,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f1(X1))
| big_r(X0,f3(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_141,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f1(X1))
| big_r(f3(X0),f4(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_142,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(X2,f1(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_143,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(X0,f5(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_144,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_145,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_r(f1(X0),f2(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_146,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f3(X1))
| big_r(f1(X0),f2(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_147,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(f1(X1),f2(X1))
| big_r(f3(X0),f4(X0))
| ~ big_p(a) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_148,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(f1(X2),f2(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_149,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f5(X0))
| big_r(f1(X2),f2(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_150,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X2),f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_153,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_154,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_p(f2(X0))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_155,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(X2,f5(X2))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_159,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f1(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_160,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(X0,f1(X0))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_161,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(X0,f1(X0))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_162,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X0,f1(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_163,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f4(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_164,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f3(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_165,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X0),f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(a)
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_166,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_167,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_168,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(f1(X0),f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(a)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_169,negated_conjecture,
big_p(a),
inference(cnf_transformation,[],[f121]) ).
tcf(c_186,negated_conjecture,
( big_p(c1)
| big_p(c3)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_187,negated_conjecture,
( big_p(c1)
| big_r(c4,c3)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_192,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(c1)
| ~ big_p(c2)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(c4,X2)
| ~ big_r(c4,X0)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_198,negated_conjecture,
( big_p(c3)
| big_r(c2,c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_199,negated_conjecture,
( big_r(c2,c1)
| big_r(c4,c3)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_204,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(c2,c1)
| ~ big_p(c2)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(c4,X2)
| ~ big_r(c4,X0)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_210,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(c3)
| ~ big_p(c4)
| ~ big_p(X1)
| ~ big_r(c2,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_211,negated_conjecture,
! [X0: $i,X1: $i] :
( big_r(c4,c3)
| ~ big_p(c4)
| ~ big_p(X1)
| ~ big_r(c2,X0)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_216,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ~ big_p(X5)
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(c2,X0)
| ~ big_r(c4,X4)
| ~ big_r(c4,X2)
| ~ big_r(X4,X5)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_272,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_p(f2(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_133,c_169,c_133]) ).
tcf(c_274,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_r(X0,f1(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_139,c_169,c_139]) ).
tcf(c_276,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f2(X1))
| big_r(X0,f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_134,c_169,c_134]) ).
tcf(c_282,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f4(X1))
| big_r(f1(X0),f2(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_145,c_169,c_145]) ).
tcf(c_284,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f1(X1))
| big_r(X0,f3(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_140,c_169,c_140]) ).
tcf(c_286,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_p(f2(X1))
| big_r(f3(X0),f4(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_135,c_169,c_135]) ).
tcf(c_296,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f3(X1))
| big_r(f1(X0),f2(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_146,c_169,c_146]) ).
tcf(c_298,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(X1,f1(X1))
| big_r(f3(X0),f4(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_141,c_169,c_141]) ).
tcf(c_300,negated_conjecture,
! [X0: $i,X1: $i] :
( big_p(X1)
| big_p(X0)
| big_r(f1(X1),f2(X1))
| big_r(f3(X0),f4(X0)) ),
inference(global_subsumption_just,[status(thm)],[c_147,c_169,c_147]) ).
tcf(c_308,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_p(f2(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_136,c_169,c_136]) ).
tcf(c_309,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_p(f2(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_308]) ).
tcf(c_318,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(X2,f1(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_142,c_169,c_142]) ).
tcf(c_319,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(X2,f1(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_318]) ).
tcf(c_320,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(X0,f5(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_137,c_169,c_137]) ).
tcf(c_321,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(X0,f5(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_320]) ).
tcf(c_322,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f4(X2))
| big_r(f1(X0),f2(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_163,c_169,c_163]) ).
tcf(c_323,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f4(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_322]) ).
tcf(c_326,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_153,c_169,c_153]) ).
tcf(c_327,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_326]) ).
tcf(c_328,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(f1(X2),f2(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_148,c_169,c_148]) ).
tcf(c_329,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f6(X0))
| big_r(f1(X2),f2(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_328]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(X0,f5(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_143,c_169,c_143]) ).
tcf(c_331,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(X0,f5(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_330]) ).
tcf(c_332,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_138,c_169,c_138]) ).
tcf(c_333,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_p(f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_332]) ).
tcf(c_334,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f3(X2))
| big_r(f1(X0),f2(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_164,c_169,c_164]) ).
tcf(c_335,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f3(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_334]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f1(X0))
| big_r(f3(X2),f4(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_159,c_169,c_159]) ).
tcf(c_337,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f1(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_336]) ).
tcf(c_338,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f5(X0))
| big_r(f1(X2),f2(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_149,c_169,c_149]) ).
tcf(c_339,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X0,f5(X0))
| big_r(f1(X2),f2(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_338]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(f5(X0),f6(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_144,c_169,c_144]) ).
tcf(c_341,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(X2,f1(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_340]) ).
tcf(c_342,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X0),f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_165,c_169,c_165]) ).
tcf(c_343,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X0),f2(X0))
| big_r(f3(X2),f4(X2))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_342]) ).
tcf(c_344,plain,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X2),f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_r(X0,X1)
| ~ big_p(X1) ),
inference(global_subsumption_just,[status(thm)],[c_150,c_169,c_150]) ).
tcf(c_345,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( big_p(X2)
| big_r(f1(X2),f2(X2))
| big_r(f5(X0),f6(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_344]) ).
tcf(c_346,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_p(f2(X0))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_154,c_169,c_154]) ).
tcf(c_347,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_p(f2(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_346]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(X0,f1(X0))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_160,c_169,c_160]) ).
tcf(c_355,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(X0,f1(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_354]) ).
tcf(c_356,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(X2,f5(X2))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_155,c_169,c_155]) ).
tcf(c_357,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(X2,f5(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_356]) ).
tcf(c_358,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(f1(X0),f2(X0))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_166,c_169,c_166]) ).
tcf(c_359,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f6(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_358]) ).
tcf(c_360,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(X0,f1(X0))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_161,c_169,c_161]) ).
tcf(c_361,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(X0,f1(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_360]) ).
tcf(c_362,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_156,c_169,c_156]) ).
tcf(c_363,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_p(f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_362]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(f1(X0),f2(X0))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_167,c_169,c_167]) ).
tcf(c_365,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X2,f5(X2))
| big_r(f1(X0),f2(X0))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_364]) ).
tcf(c_366,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X0,f1(X0))
| big_r(f5(X2),f6(X2))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_162,c_169,c_162]) ).
tcf(c_367,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(X0,f1(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_366]) ).
tcf(c_368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(f1(X0),f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_r(X0,X1)
| ~ big_r(X2,X3)
| ~ big_p(X1)
| ~ big_p(X3) ),
inference(global_subsumption_just,[status(thm)],[c_168,c_169,c_168]) ).
tcf(c_369,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( big_r(f1(X0),f2(X0))
| big_r(f5(X2),f6(X2))
| ~ big_p(X3)
| ~ big_p(X1)
| ~ big_r(X2,X3)
| ~ big_r(X0,X1) ),
inference(renaming,[status(thm)],[c_368]) ).
tcf(c_1526,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_10
| ~ big_p(X1)
| big_r(f5(X0),f6(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_369]) ).
tcf(c_1527,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ~ big_p(X1)
| big_r(f1(X0),f2(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_369]) ).
tcf(c_1528,negated_conjecture,
( iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_369]) ).
tcf(c_1529,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ~ big_p(X1)
| big_r(X0,f1(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_367]) ).
tcf(c_1530,negated_conjecture,
( iPr_def_12
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_367]) ).
tcf(c_1531,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ~ big_p(X1)
| big_r(X0,f5(X0))
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_365]) ).
tcf(c_1532,negated_conjecture,
( iPr_def_13
| iPr_def_11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_365]) ).
tcf(c_1533,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| big_p(f2(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_363]) ).
tcf(c_1534,negated_conjecture,
( iPr_def_14
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_363]) ).
tcf(c_1535,negated_conjecture,
( iPr_def_13
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_361]) ).
tcf(c_1536,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_15
| big_p(f6(X0))
| ~ big_p(X1)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_359]) ).
tcf(c_1537,negated_conjecture,
( iPr_def_15
| iPr_def_11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_359]) ).
tcf(c_1538,negated_conjecture,
( iPr_def_14
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_357]) ).
tcf(c_1539,negated_conjecture,
( iPr_def_15
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_355]) ).
tcf(c_1540,negated_conjecture,
( iPr_def_15
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_347]) ).
tcf(c_1541,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| big_p(X0)
| big_r(f1(X0),f2(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_345]) ).
tcf(c_1542,negated_conjecture,
( iPr_def_16
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_345]) ).
tcf(c_1543,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| big_p(X0)
| big_r(f3(X0),f4(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_343]) ).
tcf(c_1544,negated_conjecture,
( iPr_def_17
| iPr_def_11 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_343]) ).
tcf(c_1545,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| big_p(X0)
| big_r(X0,f1(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_341]) ).
tcf(c_1546,negated_conjecture,
( iPr_def_18
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_341]) ).
tcf(c_1547,negated_conjecture,
( iPr_def_16
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_339]) ).
tcf(c_1548,negated_conjecture,
( iPr_def_17
| iPr_def_12 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_337]) ).
tcf(c_1549,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| big_p(X0)
| big_r(X0,f3(X0)) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_335]) ).
tcf(c_1551,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| big_p(f2(X0))
| big_p(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_333]) ).
tcf(c_1552,negated_conjecture,
( iPr_def_20
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_333]) ).
tcf(c_1553,negated_conjecture,
( iPr_def_18
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_331]) ).
tcf(c_1554,negated_conjecture,
( iPr_def_16
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_329]) ).
tcf(c_1555,negated_conjecture,
( iPr_def_17
| iPr_def_14 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_327]) ).
tcf(c_1557,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| big_p(f4(X0))
| big_p(X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_323]) ).
tcf(c_1559,negated_conjecture,
( iPr_def_20
| iPr_def_13 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_321]) ).
tcf(c_1560,negated_conjecture,
( iPr_def_18
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_319]) ).
tcf(c_1563,negated_conjecture,
( iPr_def_20
| iPr_def_15 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_309]) ).
tcf(c_1565,negated_conjecture,
( iPr_def_17
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_300]) ).
tcf(c_1566,negated_conjecture,
( iPr_def_18
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_298]) ).
tcf(c_1567,negated_conjecture,
( iPr_def_19
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_296]) ).
tcf(c_1568,negated_conjecture,
( iPr_def_20
| iPr_def_17 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_286]) ).
tcf(c_1569,negated_conjecture,
( iPr_def_19
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_284]) ).
tcf(c_1570,negated_conjecture,
( iPr_def_21
| iPr_def_16 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_282]) ).
tcf(c_1571,negated_conjecture,
( iPr_def_20
| iPr_def_19 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_276]) ).
tcf(c_1572,negated_conjecture,
( iPr_def_21
| iPr_def_18 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_274]) ).
tcf(c_1573,negated_conjecture,
( iPr_def_21
| iPr_def_20 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_272]) ).
tcf(c_1574,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_22
| ~ big_p(X1)
| ~ big_r(c4,X0)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_216]) ).
tcf(c_1575,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_23
| ~ big_p(X1)
| ~ big_r(c2,X0)
| ~ big_r(X0,X1) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_216]) ).
tcf(c_1576,negated_conjecture,
( iPr_def_23
| iPr_def_22 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_216]) ).
tcf(c_1580,negated_conjecture,
( iPr_def_23
| big_r(c4,c3)
| ~ big_p(c4) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_211]) ).
tcf(c_1581,negated_conjecture,
( iPr_def_23
| big_p(c3)
| ~ big_p(c4) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_210]) ).
tcf(c_1582,negated_conjecture,
( iPr_def_22
| big_r(c2,c1)
| ~ big_p(c2) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_204]) ).
tcf(c_1586,negated_conjecture,
( iPr_def_22
| big_p(c1)
| ~ big_p(c2) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_192]) ).
tcf(c_1598,plain,
( big_p(c4)
| big_p(f2(c4))
| ~ iPr_def_20 ),
inference(instantiation,[status(thm)],[c_1551]) ).
tcf(c_1599,plain,
( big_p(c4)
| big_r(f1(c4),f2(c4))
| ~ iPr_def_16 ),
inference(instantiation,[status(thm)],[c_1541]) ).
tcf(c_1600,plain,
( big_p(c4)
| big_r(c4,f1(c4))
| ~ iPr_def_18 ),
inference(instantiation,[status(thm)],[c_1545]) ).
tcf(c_1607,plain,
! [X0: $i] :
( ~ iPr_def_22
| ~ big_p(X0)
| ~ big_r(c4,f1(c4))
| ~ big_r(f1(c4),X0) ),
inference(instantiation,[status(thm)],[c_1574]) ).
tcf(c_1618,plain,
( big_p(c4)
| big_r(f3(c4),f4(c4))
| ~ iPr_def_17 ),
inference(instantiation,[status(thm)],[c_1543]) ).
tcf(c_1619,plain,
( big_p(c4)
| big_r(c4,f3(c4))
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_1549]) ).
tcf(c_1620,plain,
( big_p(c4)
| big_p(f4(c4))
| ~ iPr_def_21 ),
inference(instantiation,[status(thm)],[c_1557]) ).
tcf(c_1663,plain,
! [X0: $i] :
( ~ iPr_def_22
| ~ big_p(X0)
| ~ big_r(c4,f3(c4))
| ~ big_r(f3(c4),X0) ),
inference(instantiation,[status(thm)],[c_1574]) ).
tcf(c_1707,plain,
( big_p(c2)
| big_p(f4(c2))
| ~ iPr_def_21 ),
inference(instantiation,[status(thm)],[c_1557]) ).
tcf(c_1708,plain,
( big_p(c2)
| big_r(c2,f3(c2))
| ~ iPr_def_19 ),
inference(instantiation,[status(thm)],[c_1549]) ).
tcf(c_1709,plain,
( big_p(c2)
| big_r(f3(c2),f4(c2))
| ~ iPr_def_17 ),
inference(instantiation,[status(thm)],[c_1543]) ).
tcf(c_1710,plain,
( big_p(c2)
| big_r(c2,f1(c2))
| ~ iPr_def_18 ),
inference(instantiation,[status(thm)],[c_1545]) ).
tcf(c_1711,plain,
( big_p(c2)
| big_r(f1(c2),f2(c2))
| ~ iPr_def_16 ),
inference(instantiation,[status(thm)],[c_1541]) ).
tcf(c_1712,plain,
( big_p(c2)
| big_p(f2(c2))
| ~ iPr_def_20 ),
inference(instantiation,[status(thm)],[c_1551]) ).
tcf(c_1839,plain,
! [X0: $i] :
( ~ iPr_def_23
| ~ big_p(X0)
| ~ big_r(c2,f1(c2))
| ~ big_r(f1(c2),X0) ),
inference(instantiation,[status(thm)],[c_1575]) ).
tcf(c_1907,plain,
( big_p(f6(c4))
| ~ iPr_def_15
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1536]) ).
tcf(c_1908,plain,
( big_r(c4,f5(c4))
| ~ iPr_def_13
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_1909,plain,
( big_r(f5(c4),f6(c4))
| ~ iPr_def_10
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1526]) ).
tcf(c_1910,plain,
( big_r(c4,f1(c4))
| ~ iPr_def_12
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1529]) ).
tcf(c_1911,plain,
( big_r(f1(c4),f2(c4))
| ~ iPr_def_11
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1527]) ).
tcf(c_1912,plain,
( big_p(f2(c4))
| ~ iPr_def_14
| ~ big_p(c3)
| ~ big_r(c4,c3) ),
inference(instantiation,[status(thm)],[c_1533]) ).
tcf(c_1965,plain,
( big_r(c2,f5(c2))
| ~ iPr_def_13
| ~ big_p(c1)
| ~ big_r(c2,c1) ),
inference(instantiation,[status(thm)],[c_1531]) ).
tcf(c_1969,plain,
( big_p(f2(c2))
| ~ iPr_def_14
| ~ big_p(c1)
| ~ big_r(c2,c1) ),
inference(instantiation,[status(thm)],[c_1533]) ).
tcf(c_2051,plain,
( ~ iPr_def_23
| ~ big_p(f2(c2))
| ~ big_r(c2,f1(c2))
| ~ big_r(f1(c2),f2(c2)) ),
inference(instantiation,[status(thm)],[c_1839]) ).
tcf(c_2119,plain,
! [X0: $i] :
( ~ iPr_def_23
| ~ big_p(X0)
| ~ big_r(c2,f5(c2))
| ~ big_r(f5(c2),X0) ),
inference(instantiation,[status(thm)],[c_1575]) ).
tcf(c_2449,plain,
( big_r(c4,c3)
| big_r(f5(c2),f6(c2))
| ~ iPr_def_10
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_199,c_1526]) ).
tcf(c_2450,plain,
( big_p(c3)
| big_r(f5(c2),f6(c2))
| ~ iPr_def_10
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_198,c_1526]) ).
tcf(c_2652,plain,
( big_p(c1)
| big_r(f1(c4),f2(c4))
| ~ iPr_def_11
| ~ big_p(c2)
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_187,c_1527]) ).
tcf(c_2653,plain,
( big_r(c4,c3)
| big_r(f1(c2),f2(c2))
| ~ iPr_def_11
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_199,c_1527]) ).
tcf(c_2654,plain,
( big_p(c3)
| big_r(f1(c2),f2(c2))
| ~ iPr_def_11
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_198,c_1527]) ).
tcf(c_2770,plain,
( iPr_def_23
| big_r(f1(c4),f2(c4))
| ~ iPr_def_11
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1527]) ).
tcf(c_2771,plain,
( iPr_def_23
| big_r(f5(c4),f6(c4))
| ~ iPr_def_10
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1526]) ).
tcf(c_2842,plain,
( iPr_def_22
| big_r(f1(c2),f2(c2))
| ~ iPr_def_11
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1527]) ).
tcf(c_2843,plain,
( iPr_def_22
| big_r(f5(c2),f6(c2))
| ~ iPr_def_10
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1526]) ).
tcf(c_3104,plain,
( ~ iPr_def_23
| ~ big_p(f6(c2))
| ~ big_r(c2,f5(c2))
| ~ big_r(f5(c2),f6(c2)) ),
inference(instantiation,[status(thm)],[c_2119]) ).
tcf(c_3141,plain,
( iPr_def_23
| big_p(f2(c4))
| ~ iPr_def_14
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1533]) ).
tcf(c_3143,plain,
( iPr_def_22
| big_p(f2(c2))
| ~ iPr_def_14
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1533]) ).
tcf(c_3346,plain,
( iPr_def_23
| big_r(c4,f1(c4))
| ~ iPr_def_12
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1529]) ).
tcf(c_3348,plain,
( iPr_def_22
| big_r(c2,f1(c2))
| ~ iPr_def_12
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1529]) ).
tcf(c_3349,plain,
( big_r(c4,c3)
| big_r(c2,f1(c2))
| ~ iPr_def_12
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_199,c_1529]) ).
tcf(c_3350,plain,
( big_p(c3)
| big_r(c2,f1(c2))
| ~ iPr_def_12
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_198,c_1529]) ).
tcf(c_3988,plain,
( iPr_def_23
| big_p(f6(c4))
| ~ iPr_def_15
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1536]) ).
tcf(c_3990,plain,
( iPr_def_22
| big_p(f6(c2))
| ~ iPr_def_15
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1536]) ).
tcf(c_3991,plain,
( big_r(c4,c3)
| big_p(f6(c2))
| ~ iPr_def_15
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_199,c_1536]) ).
tcf(c_3992,plain,
( big_p(c3)
| big_p(f6(c2))
| ~ iPr_def_15
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_198,c_1536]) ).
tcf(c_4166,plain,
( iPr_def_23
| big_p(f2(c4))
| ~ iPr_def_14
| ~ big_p(c4) ),
inference(global_subsumption_just,[status(thm)],[c_3141,c_1581,c_3141]) ).
tcf(c_4192,plain,
( iPr_def_22
| big_p(f2(c2))
| ~ big_p(c2) ),
inference(global_subsumption_just,[status(thm)],[c_3143,c_1534,c_1538,c_1540,c_1576,c_1586,c_1582,c_1969,c_1965,c_2843,c_3104,c_3990]) ).
tcf(c_4214,plain,
( iPr_def_23
| big_p(f6(c4))
| ~ iPr_def_15
| ~ big_p(c4) ),
inference(global_subsumption_just,[status(thm)],[c_3988,c_1581,c_3988]) ).
tcf(c_4252,plain,
( iPr_def_23
| big_r(c4,f5(c4))
| ~ iPr_def_13
| ~ big_p(c4)
| ~ big_p(c3) ),
inference(superposition,[status(thm)],[c_1580,c_1531]) ).
tcf(c_4254,plain,
( iPr_def_22
| big_r(c2,f5(c2))
| ~ iPr_def_13
| ~ big_p(c1)
| ~ big_p(c2) ),
inference(superposition,[status(thm)],[c_1582,c_1531]) ).
tcf(c_4255,plain,
( big_r(c4,c3)
| big_r(c2,f5(c2))
| ~ iPr_def_13
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_199,c_1531]) ).
tcf(c_4256,plain,
( big_p(c3)
| big_r(c2,f5(c2))
| ~ iPr_def_13
| ~ big_p(c1)
| ~ big_p(c2)
| ~ big_p(c4) ),
inference(superposition,[status(thm)],[c_198,c_1531]) ).
tcf(c_4394,plain,
! [X0: $i] :
( ~ iPr_def_23
| ~ big_p(X0)
| ~ big_r(c2,f3(c2))
| ~ big_r(f3(c2),X0) ),
inference(instantiation,[status(thm)],[c_1575]) ).
tcf(c_4452,plain,
( iPr_def_22
| big_p(f6(c2))
| ~ big_p(c2) ),
inference(global_subsumption_just,[status(thm)],[c_3990,c_1537,c_1539,c_1576,c_1586,c_2051,c_2842,c_3348,c_3990,c_4192]) ).
tcf(c_4469,plain,
! [X0: $i] :
( ~ iPr_def_22
| ~ big_p(X0)
| ~ big_r(c4,f5(c4))
| ~ big_r(f5(c4),X0) ),
inference(instantiation,[status(thm)],[c_1574]) ).
tcf(c_4535,plain,
( iPr_def_23
| big_r(c4,f1(c4))
| ~ iPr_def_12
| ~ big_p(c4) ),
inference(global_subsumption_just,[status(thm)],[c_3346,c_1581,c_3346]) ).
tcf(c_4657,plain,
( ~ iPr_def_23
| ~ big_p(f4(c2))
| ~ big_r(c2,f3(c2))
| ~ big_r(f3(c2),f4(c2)) ),
inference(instantiation,[status(thm)],[c_4394]) ).
tcf(c_4724,plain,
( iPr_def_22
| big_r(c2,f1(c2))
| ~ iPr_def_12
| ~ big_p(c1) ),
inference(global_subsumption_just,[status(thm)],[c_3348,c_1566,c_1567,c_1569,c_1570,c_1571,c_1572,c_1573,c_1576,c_1712,c_1711,c_1710,c_1709,c_1708,c_1707,c_2051,c_3348,c_4657]) ).
tcf(c_4726,plain,
( iPr_def_22
| big_r(c2,f1(c2))
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_4724,c_1566,c_1567,c_1569,c_1570,c_1571,c_1572,c_1573,c_1576,c_1586,c_1712,c_1711,c_1710,c_1709,c_1708,c_1707,c_2051,c_4657,c_4724]) ).
tcf(c_4739,plain,
( iPr_def_22
| big_p(f2(c2))
| ~ iPr_def_14
| ~ iPr_def_12
| ~ big_p(f1(c2)) ),
inference(superposition,[status(thm)],[c_4726,c_1533]) ).
tcf(c_4872,plain,
( ~ iPr_def_22
| ~ big_p(f2(c4))
| ~ big_r(c4,f1(c4))
| ~ big_r(f1(c4),f2(c4)) ),
inference(instantiation,[status(thm)],[c_1607]) ).
tcf(c_4881,plain,
( ~ iPr_def_22
| ~ big_p(f4(c4))
| ~ big_r(c4,f3(c4))
| ~ big_r(f3(c4),f4(c4)) ),
inference(instantiation,[status(thm)],[c_1663]) ).
tcf(c_4951,plain,
( ~ iPr_def_22
| ~ big_p(f6(c4))
| ~ big_r(c4,f5(c4))
| ~ big_r(f5(c4),f6(c4)) ),
inference(instantiation,[status(thm)],[c_4469]) ).
tcf(c_4997,plain,
( iPr_def_22
| big_p(f2(c2)) ),
inference(global_subsumption_just,[status(thm)],[c_4739,c_1567,c_1568,c_1569,c_1570,c_1571,c_1572,c_1573,c_1576,c_1712,c_1711,c_1710,c_1709,c_1708,c_1707,c_2051,c_4192,c_4657]) ).
tcf(c_5160,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_4997,c_4951,c_4881,c_4872,c_4726,c_4657,c_4535,c_4452,c_4255,c_4256,c_4252,c_4254,c_4214,c_4166,c_3991,c_3992,c_3349,c_3350,c_3104,c_2842,c_2843,c_2770,c_2771,c_2653,c_2652,c_2654,c_2449,c_2450,c_2051,c_1969,c_1907,c_1908,c_1909,c_1910,c_1911,c_1912,c_1707,c_1708,c_1709,c_1710,c_1711,c_1712,c_1620,c_1619,c_1618,c_1600,c_1599,c_1598,c_1580,c_1586,c_1581,c_1576,c_1573,c_1572,c_1571,c_1570,c_1569,c_1568,c_1567,c_1566,c_1565,c_1563,c_1560,c_1559,c_1555,c_1554,c_1553,c_1552,c_1548,c_1547,c_1546,c_1544,c_1542,c_1540,c_1539,c_1538,c_1537,c_1535,c_1534,c_1532,c_1530,c_1528,c_199,c_187,c_198,c_186]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN067-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/5.40 % Computer : n020.cluster.edu
% 0.12/5.40 % Model : x86_64 x86_64
% 0.12/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.40 % Memory : 8046.5625MB
% 0.12/5.40 % OS : Linux 6.8.0-71-generic
% 0.12/5.40 % CPULimit : 300
% 0.12/5.40 % WCLimit : 300
% 0.12/5.40 % DateTime : Fri Sep 25 00:03:40 UTC 2026
% 0.12/5.40 % CPUTime :
% 0.12/5.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/5.46 Running first-order theorem proving
% 0.12/5.47 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/5.48
% 0.12/5.48 % ======== iProver multi-core TPTP/SMT =========
% 0.12/5.48
% 0.12/5.49 % Detected problem language: tptp
% 0.12/5.50 % Proving...
% 2.27/6.27 % SZS status Started for theBenchmark.p
% 2.27/6.27 % SZS status Unsatisfiable for theBenchmark.p
% 2.27/6.27
% 2.27/6.27 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.27/6.27
% 2.27/6.27 % ------ iProver source info
% 2.27/6.27
% 2.27/6.27 % git: date: 2026-07-19 20:42:38 +0200
% 2.27/6.27 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.27/6.27 % git: non_committed_changes: false
% 2.27/6.27
% 2.27/6.27 % ------ Parsing...% successful
% 2.27/6.27
% 2.27/6.27
% 2.27/6.27 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.27/6.27
% 2.27/6.27 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.27/6.27
% 2.27/6.27 % ------ Preprocessing... gs_s sp: 93 0s gs_e snvd_s sp: 0 0s snvd_e
% 2.27/6.27 % ------ Proving...
% 2.27/6.27 % ------ Problem Properties
% 2.27/6.27
% 2.27/6.27 %
% 2.27/6.27 % clauses 69
% 2.27/6.27 % conjectures 69
% 2.27/6.27 % EPR 57
% 2.27/6.27 % Horn 9
% 2.27/6.27 % unary 1
% 2.27/6.27 % binary 37
% 2.27/6.27 % lits 186
% 2.27/6.27 % lits eq 0
% 2.27/6.27 % fd_pure 0
% 2.27/6.27 % fd_pseudo 0
% 2.27/6.27 % fd_cond 0
% 2.27/6.27 % fd_pseudo_cond 0
% 2.27/6.27 % AC symbols 0
% 2.27/6.27
% 2.27/6.27 % ------ Schedule dynamic 5 is on
% 2.27/6.27
% 2.27/6.27 % ------ no equalities: superposition off
% 2.27/6.27
% 2.27/6.27 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.27/6.27
% 2.27/6.27
% 2.27/6.27 % ------
% 2.27/6.27 % Current options:
% 2.27/6.27 % ------
% 2.27/6.27
% 2.27/6.27
% 2.27/6.27 %
% 2.27/6.27
% 2.27/6.27 % ------ Proving...
% 2.27/6.27 %
% 2.27/6.27
% 2.27/6.27 % SZS status Unsatisfiable for theBenchmark.p
% 2.27/6.27
% 2.27/6.27 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.27/6.28
% 2.27/6.28
%------------------------------------------------------------------------------