%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN577-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n018.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:41:08 PM UTC 2026
% Result : Unsatisfiable 4.39s 1.54s
% Output : CNFRefutation 4.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 29
% Syntax : Number of formulae : 584 ( 64 unt; 7 def)
% Number of atoms : 2540 ( 7 equ)
% Maximal formula atoms : 10 ( 4 avg)
% Number of connectives : 2215 (1112 ~;1103 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 12 ( 10 usr; 8 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 12 con; 0-2 aty)
% Number of variables : 915 ( 0 sgn 915 !; 0 ?; 872 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : p2(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_1) ).
fof(f2,negated_conjecture,
p8(c14,c13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_2) ).
fof(f3,negated_conjecture,
p7(c11,c12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_3) ).
fof(f4,negated_conjecture,
p7(c13,c12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_4) ).
fof(f5,negated_conjecture,
p7(c9,c10),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_5) ).
fof(f6,negated_conjecture,
p8(c14,c11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_6) ).
fof(f7,negated_conjecture,
p2(f3(c12,c11),c15),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_7) ).
fof(f8,negated_conjecture,
p2(f4(c16,c14),c18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_8) ).
fof(f9,negated_conjecture,
p2(f4(c15,c14),c17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_9) ).
fof(f10,negated_conjecture,
p2(f3(c12,c13),c16),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_10) ).
fof(f11,negated_conjecture,
p2(f5(f6(c9),c19),c17),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_11) ).
fof(f12,negated_conjecture,
p2(f5(f6(c9),c20),c18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_12) ).
fof(f13,negated_conjecture,
! [X0,X1] :
( ~ p2(X0,X1)
| p2(f6(X0),f6(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_13) ).
fof(f14,negated_conjecture,
! [X2,X0,X1] :
( ~ p2(X2,X1)
| ~ p2(X2,X0)
| p2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_14) ).
fof(f15,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p2(X3,X0)
| ~ p8(X3,X2)
| ~ p2(X2,X1)
| p8(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p8_15) ).
fof(f16,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p2(X3,X0)
| ~ p7(X3,X2)
| ~ p2(X2,X1)
| p7(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_16) ).
fof(f17,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p2(X1,X3)
| ~ p2(X0,X2)
| p2(f3(X0,X1),f3(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_17) ).
fof(f18,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p2(X0,X2)
| ~ p2(X1,X3)
| p2(f5(X0,X1),f5(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_18) ).
fof(f19,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p2(X1,X3)
| ~ p2(X0,X2)
| p2(f4(X0,X1),f4(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_19) ).
fof(f20,negated_conjecture,
! [X2,X0,X1] :
( ~ p2(f4(X2,c14),f5(f6(X0),c20))
| ~ p2(f4(X1,c14),f5(f6(X0),c19))
| ~ p2(c16,X2)
| ~ p2(c15,X1)
| ~ p7(X0,c10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p7_20) ).
fof(f21,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p2(f4(X3,c14),f5(f6(X2),X6))
| ~ p2(f4(X4,c14),f5(f6(X2),X5))
| ~ p2(f3(c12,X0),X4)
| ~ p2(f3(c12,X1),X3)
| ~ p8(c14,X0)
| ~ p8(c14,X1)
| ~ p7(X1,c12)
| ~ p7(X0,c12)
| ~ p7(X2,c10)
| p2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_21) ).
fof(f22,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ p2(f4(X5,c14),f5(f6(X2),X1))
| ~ p2(f4(X6,c14),f5(f6(X2),X0))
| ~ p2(f3(c12,X3),X6)
| ~ p2(f3(c12,X4),X5)
| ~ p8(c14,X3)
| ~ p8(c14,X4)
| ~ p7(X4,c12)
| ~ p7(X3,c12)
| ~ p7(X2,c10)
| p2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_22) ).
tcf(c_71,negated_conjecture,
! [X0: $i] : p2(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_72,negated_conjecture,
p8(c14,c13),
inference(cnf_transformation,[],[f2]) ).
tcf(c_73,negated_conjecture,
p7(c11,c12),
inference(cnf_transformation,[],[f3]) ).
tcf(c_74,negated_conjecture,
p7(c13,c12),
inference(cnf_transformation,[],[f4]) ).
tcf(c_75,negated_conjecture,
p7(c9,c10),
inference(cnf_transformation,[],[f5]) ).
tcf(c_76,negated_conjecture,
p8(c14,c11),
inference(cnf_transformation,[],[f6]) ).
tcf(c_77,negated_conjecture,
p2(f3(c12,c11),c15),
inference(cnf_transformation,[],[f7]) ).
tcf(c_78,negated_conjecture,
p2(f4(c16,c14),c18),
inference(cnf_transformation,[],[f8]) ).
tcf(c_79,negated_conjecture,
p2(f4(c15,c14),c17),
inference(cnf_transformation,[],[f9]) ).
tcf(c_80,negated_conjecture,
p2(f3(c12,c13),c16),
inference(cnf_transformation,[],[f10]) ).
tcf(c_81,negated_conjecture,
p2(f5(f6(c9),c19),c17),
inference(cnf_transformation,[],[f11]) ).
tcf(c_82,negated_conjecture,
p2(f5(f6(c9),c20),c18),
inference(cnf_transformation,[],[f12]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f6(X0),f6(X1))
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_84,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X1,X2)
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_85,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,X1)
| ~ p8(X2,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_86,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,X1)
| ~ p7(X2,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_87,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f3(X0,X2),f3(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_88,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f5(X0,X2),f5(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_89,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X0,X2),f4(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_90,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ~ p7(X1,c10)
| ~ p2(c16,X2)
| ~ p2(c15,X0)
| ~ p2(f4(X2,c14),f5(f6(X1),c20))
| ~ p2(f4(X0,c14),f5(f6(X1),c19)) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_91,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p2(X5,X6)
| ~ p7(X6,c12)
| ~ p7(X5,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X6)
| ~ p8(c14,X5)
| ~ p2(f3(c12,X6),X0)
| ~ p2(f3(c12,X5),X3)
| ~ p2(f4(X3,c14),f5(f6(X1),X4))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_92,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p2(X2,X4)
| ~ p7(X6,c12)
| ~ p7(X5,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X6)
| ~ p8(c14,X5)
| ~ p2(f3(c12,X6),X3)
| ~ p2(f3(c12,X5),X0)
| ~ p2(f4(X3,c14),f5(f6(X1),X4))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_217,definition,
iPr_def_10 = f6(c9),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_218,definition,
iPr_def_11 = f5(iPr_def_10,c20),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_219,definition,
iPr_def_12 = f5(iPr_def_10,c19),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_220,definition,
iPr_def_13 = f3(c12,c13),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_221,definition,
iPr_def_14 = f4(c15,c14),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_222,definition,
iPr_def_15 = f4(c16,c14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_223,definition,
iPr_def_16 = f3(c12,c11),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_224,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p2(X2,X4)
| ~ p7(X6,c12)
| ~ p7(X5,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X6)
| ~ p8(c14,X5)
| ~ p2(f3(c12,X6),X3)
| ~ p2(f3(c12,X5),X0)
| ~ p2(f4(X3,c14),f5(f6(X1),X4))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_225,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p2(X5,X6)
| ~ p7(X6,c12)
| ~ p7(X5,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X6)
| ~ p8(c14,X5)
| ~ p2(f3(c12,X6),X0)
| ~ p2(f3(c12,X5),X3)
| ~ p2(f4(X3,c14),f5(f6(X1),X4))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_226,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( ~ p7(X1,c10)
| ~ p2(c16,X2)
| ~ p2(c15,X0)
| ~ p2(f4(X2,c14),f5(f6(X1),c20))
| ~ p2(f4(X0,c14),f5(f6(X1),c19)) ),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_227,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X0,X2),f4(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_89]) ).
tcf(c_228,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f5(X0,X2),f5(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_229,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f3(X0,X2),f3(X1,X3))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_87]) ).
tcf(c_230,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,X1)
| ~ p7(X2,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_231,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,X1)
| ~ p8(X2,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_85]) ).
tcf(c_232,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X1,X2)
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_233,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f6(X0),f6(X1))
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_234,negated_conjecture,
p2(iPr_def_11,c18),
inference(demodulation,[status(thm)],[c_82,c_217,c_218]) ).
tcf(c_235,negated_conjecture,
p2(iPr_def_12,c17),
inference(demodulation,[status(thm)],[c_81,c_219]) ).
tcf(c_236,negated_conjecture,
p2(iPr_def_13,c16),
inference(demodulation,[status(thm)],[c_80,c_220]) ).
tcf(c_237,negated_conjecture,
p2(iPr_def_14,c17),
inference(demodulation,[status(thm)],[c_79,c_221]) ).
tcf(c_238,negated_conjecture,
p2(iPr_def_15,c18),
inference(demodulation,[status(thm)],[c_78,c_222]) ).
tcf(c_239,negated_conjecture,
p2(iPr_def_16,c15),
inference(demodulation,[status(thm)],[c_77,c_223]) ).
tcf(c_240,negated_conjecture,
p8(c14,c11),
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_241,negated_conjecture,
p7(c9,c10),
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_242,negated_conjecture,
p7(c13,c12),
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_243,negated_conjecture,
p7(c11,c12),
inference(demodulation,[status(thm)],[c_73]) ).
tcf(c_244,negated_conjecture,
p8(c14,c13),
inference(demodulation,[status(thm)],[c_72]) ).
tcf(c_245,negated_conjecture,
! [X0: $i] : p2(X0,X0),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_638,plain,
! [X0: $i] :
( p2(iPr_def_10,f6(X0))
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_217,c_233]) ).
tcf(c_639,plain,
! [X0: $i] :
( p2(f6(X0),iPr_def_10)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_217,c_233]) ).
tcf(c_653,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f6(X2),X1)
| ~ p2(X0,X2)
| ~ p2(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_233,c_232]) ).
tcf(c_654,plain,
! [X0: $i] :
( p2(c18,X0)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_234,c_232]) ).
tcf(c_655,plain,
! [X0: $i] :
( p2(c17,X0)
| ~ p2(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_235,c_232]) ).
tcf(c_656,plain,
! [X0: $i] :
( p2(c16,X0)
| ~ p2(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_236,c_232]) ).
tcf(c_657,plain,
! [X0: $i] :
( p2(c17,X0)
| ~ p2(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_237,c_232]) ).
tcf(c_658,plain,
! [X0: $i] :
( p2(c18,X0)
| ~ p2(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_238,c_232]) ).
tcf(c_659,plain,
! [X0: $i] :
( p2(c15,X0)
| ~ p2(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_239,c_232]) ).
tcf(c_687,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_14,f4(X1,X0))
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_221,c_227]) ).
tcf(c_688,plain,
! [X0: $i,X1: $i] :
( p2(f4(X0,X1),iPr_def_14)
| ~ p2(X1,c14)
| ~ p2(X0,c15) ),
inference(superposition,[status(thm)],[c_221,c_227]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(f4(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p2(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_227,c_232]) ).
tcf(c_708,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_218,c_228]) ).
tcf(c_709,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_219,c_228]) ).
tcf(c_710,plain,
! [X0: $i,X1: $i] :
( p2(f5(X0,X1),iPr_def_11)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_218,c_228]) ).
tcf(c_711,plain,
! [X0: $i,X1: $i] :
( p2(f5(X0,X1),iPr_def_12)
| ~ p2(X1,c19)
| ~ p2(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_219,c_228]) ).
tcf(c_712,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(f5(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p2(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_228,c_232]) ).
tcf(c_739,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_13,f3(X1,X0))
| ~ p2(c12,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_220,c_229]) ).
tcf(c_740,plain,
! [X0: $i,X1: $i] :
( p2(f3(X0,X1),iPr_def_13)
| ~ p2(X1,c13)
| ~ p2(X0,c12) ),
inference(superposition,[status(thm)],[c_220,c_229]) ).
tcf(c_741,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(f3(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p2(f3(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_229,c_232]) ).
tcf(c_762,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(X1,X2)
| ~ p7(X0,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_245,c_230]) ).
tcf(c_763,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,f6(X2))
| ~ p2(X1,X2)
| ~ p2(X0,X3)
| ~ p7(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_233,c_230]) ).
tcf(c_764,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p7(X5,f3(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p7(X0,f3(X1,X2)) ),
inference(superposition,[status(thm)],[c_229,c_230]) ).
tcf(c_765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p7(X5,f5(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p7(X0,f5(X1,X2)) ),
inference(superposition,[status(thm)],[c_228,c_230]) ).
tcf(c_766,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p7(X5,f4(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p7(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_227,c_230]) ).
tcf(c_767,plain,
! [X0: $i,X1: $i] :
( p7(X1,c18)
| ~ p7(X0,iPr_def_11)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_234,c_230]) ).
tcf(c_768,plain,
! [X0: $i,X1: $i] :
( p7(X1,c17)
| ~ p7(X0,iPr_def_12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_235,c_230]) ).
tcf(c_769,plain,
! [X0: $i,X1: $i] :
( p7(X1,c16)
| ~ p7(X0,iPr_def_13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_236,c_230]) ).
tcf(c_770,plain,
! [X0: $i,X1: $i] :
( p7(X1,c17)
| ~ p7(X0,iPr_def_14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_237,c_230]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] :
( p7(X1,c18)
| ~ p7(X0,iPr_def_15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_238,c_230]) ).
tcf(c_772,plain,
! [X0: $i,X1: $i] :
( p7(X1,c15)
| ~ p7(X0,iPr_def_16)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_239,c_230]) ).
tcf(c_827,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(X1,X2)
| ~ p8(X0,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_245,c_231]) ).
tcf(c_828,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,f6(X2))
| ~ p2(X1,X2)
| ~ p2(X0,X3)
| ~ p8(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_233,c_231]) ).
tcf(c_829,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p8(X5,f3(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p8(X0,f3(X1,X2)) ),
inference(superposition,[status(thm)],[c_229,c_231]) ).
tcf(c_830,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p8(X5,f5(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p8(X0,f5(X1,X2)) ),
inference(superposition,[status(thm)],[c_228,c_231]) ).
tcf(c_831,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p8(X5,f4(X3,X4))
| ~ p2(X2,X4)
| ~ p2(X1,X3)
| ~ p2(X0,X5)
| ~ p8(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_227,c_231]) ).
tcf(c_832,plain,
! [X0: $i,X1: $i] :
( p8(X1,c18)
| ~ p8(X0,iPr_def_11)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_234,c_231]) ).
tcf(c_833,plain,
! [X0: $i,X1: $i] :
( p8(X1,c17)
| ~ p8(X0,iPr_def_12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_235,c_231]) ).
tcf(c_834,plain,
! [X0: $i,X1: $i] :
( p8(X1,c16)
| ~ p8(X0,iPr_def_13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_236,c_231]) ).
tcf(c_835,plain,
! [X0: $i,X1: $i] :
( p8(X1,c17)
| ~ p8(X0,iPr_def_14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_237,c_231]) ).
tcf(c_836,plain,
! [X0: $i,X1: $i] :
( p8(X1,c18)
| ~ p8(X0,iPr_def_15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_238,c_231]) ).
tcf(c_837,plain,
! [X0: $i,X1: $i] :
( p8(X1,c15)
| ~ p8(X0,iPr_def_16)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_239,c_231]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i] :
( ~ p2(c15,c15)
| ~ p7(X1,c10)
| ~ p2(c16,X0)
| ~ p2(iPr_def_14,f5(f6(X1),c19))
| ~ p2(f4(X0,c14),f5(f6(X1),c20)) ),
inference(superposition,[status(thm)],[c_221,c_226]) ).
tcf(c_906,plain,
! [X0: $i,X1: $i] :
( ~ p7(c9,c10)
| ~ p2(c16,X0)
| ~ p2(c15,X1)
| ~ p2(f4(X1,c14),f5(iPr_def_10,c19))
| ~ p2(f4(X0,c14),f5(f6(c9),c20)) ),
inference(superposition,[status(thm)],[c_217,c_226]) ).
tcf(c_907,plain,
! [X0: $i,X1: $i] :
( ~ p7(X1,c10)
| ~ p2(c16,X0)
| ~ p2(iPr_def_14,f5(f6(X1),c19))
| ~ p2(f4(X0,c14),f5(f6(X1),c20)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_905,c_245]) ).
tcf(c_912,plain,
! [X0: $i,X1: $i] :
( ~ p7(c9,c10)
| ~ p2(c16,X0)
| ~ p2(c15,X1)
| ~ p2(f4(X1,c14),iPr_def_12)
| ~ p2(f4(X0,c14),iPr_def_11) ),
inference(light_normalisation,[status(thm)],[c_906,c_217,c_218,c_219]) ).
tcf(c_913,plain,
! [X0: $i,X1: $i] :
( ~ p2(c16,X0)
| ~ p2(c15,X1)
| ~ p2(f4(X1,c14),iPr_def_12)
| ~ p2(f4(X0,c14),iPr_def_11) ),
inference(forward_subsumption_resolution,[status(thm)],[c_912,c_241]) ).
tcf(c_924,plain,
( p2(iPr_def_10,iPr_def_10)
| ~ p2(c9,c9) ),
inference(superposition,[status(thm)],[c_217,c_638]) ).
tcf(c_925,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(X1,f6(X2))
| ~ p8(X0,iPr_def_10)
| ~ p2(c9,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_638,c_231]) ).
tcf(c_926,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(X1,f6(X2))
| ~ p7(X0,iPr_def_10)
| ~ p2(c9,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_638,c_230]) ).
tcf(c_927,plain,
! [X0: $i,X1: $i] :
( p2(f6(X0),X1)
| ~ p2(iPr_def_10,X1)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_232]) ).
tcf(c_946,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_15,f4(X1,X0))
| ~ p2(c16,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_222,c_227]) ).
tcf(c_947,plain,
! [X0: $i,X1: $i] :
( p2(f4(X0,X1),iPr_def_15)
| ~ p2(X1,c14)
| ~ p2(X0,c16) ),
inference(superposition,[status(thm)],[c_222,c_227]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i] :
( ~ p2(c15,c16)
| ~ p7(X1,c10)
| ~ p2(c16,X0)
| ~ p2(iPr_def_15,f5(f6(X1),c19))
| ~ p2(f4(X0,c14),f5(f6(X1),c20)) ),
inference(superposition,[status(thm)],[c_222,c_226]) ).
tcf(c_967,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_16,f3(X1,X0))
| ~ p2(c12,X1)
| ~ p2(c11,X0) ),
inference(superposition,[status(thm)],[c_223,c_229]) ).
tcf(c_968,plain,
! [X0: $i,X1: $i] :
( p2(f3(X0,X1),iPr_def_16)
| ~ p2(X1,c11)
| ~ p2(X0,c12) ),
inference(superposition,[status(thm)],[c_223,c_229]) ).
tcf(c_1003,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X3,X2)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),c16)
| ~ p2(f3(c12,X4),X0)
| ~ p2(iPr_def_15,f5(f6(X1),X3))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(superposition,[status(thm)],[c_222,c_224]) ).
tcf(c_1004,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X3,X2)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),c15)
| ~ p2(f3(c12,X4),X0)
| ~ p2(iPr_def_14,f5(f6(X1),X3))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(superposition,[status(thm)],[c_221,c_224]) ).
tcf(c_1005,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X3,X1)
| ~ p7(c9,c10)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X0)
| ~ p2(f3(c12,X4),X2)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(f6(c9),X1)) ),
inference(superposition,[status(thm)],[c_217,c_224]) ).
tcf(c_1026,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X3,X1)
| ~ p7(c9,c10)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X0)
| ~ p2(f3(c12,X4),X2)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(iPr_def_10,X1)) ),
inference(light_normalisation,[status(thm)],[c_1005,c_217]) ).
tcf(c_1027,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X3,X1)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X0)
| ~ p2(f3(c12,X4),X2)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(iPr_def_10,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1026,c_241]) ).
tcf(c_1057,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X4,X5)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),c16)
| ~ p2(f3(c12,X4),X0)
| ~ p2(iPr_def_15,f5(f6(X1),X3))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(superposition,[status(thm)],[c_222,c_225]) ).
tcf(c_1058,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X4,X5)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p7(X1,c10)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),c15)
| ~ p2(f3(c12,X4),X0)
| ~ p2(iPr_def_14,f5(f6(X1),X3))
| ~ p2(f4(X0,c14),f5(f6(X1),X2)) ),
inference(superposition,[status(thm)],[c_221,c_225]) ).
tcf(c_1059,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X4,X5)
| ~ p7(c9,c10)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X2)
| ~ p2(f3(c12,X4),X0)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(f6(c9),X1)) ),
inference(superposition,[status(thm)],[c_217,c_225]) ).
tcf(c_1080,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X4,X5)
| ~ p7(c9,c10)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X2)
| ~ p2(f3(c12,X4),X0)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(iPr_def_10,X1)) ),
inference(light_normalisation,[status(thm)],[c_1059,c_217]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(X4,X5)
| ~ p7(X5,c12)
| ~ p7(X4,c12)
| ~ p8(c14,X5)
| ~ p8(c14,X4)
| ~ p2(f3(c12,X5),X2)
| ~ p2(f3(c12,X4),X0)
| ~ p2(f4(X2,c14),f5(iPr_def_10,X3))
| ~ p2(f4(X0,c14),f5(iPr_def_10,X1)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1080,c_241]) ).
tcf(c_1101,plain,
p2(c18,iPr_def_11),
inference(superposition,[status(thm)],[c_245,c_654]) ).
tcf(c_1102,plain,
p2(c18,c18),
inference(superposition,[status(thm)],[c_234,c_654]) ).
tcf(c_1103,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_11)
| ~ p8(X0,c18)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1101,c_231]) ).
tcf(c_1104,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_11)
| ~ p7(X0,c18)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1101,c_230]) ).
tcf(c_1105,plain,
! [X0: $i] :
( p2(iPr_def_11,X0)
| ~ p2(c18,X0) ),
inference(superposition,[status(thm)],[c_1101,c_232]) ).
tcf(c_1133,plain,
p2(c17,iPr_def_12),
inference(superposition,[status(thm)],[c_245,c_655]) ).
tcf(c_1134,plain,
p2(c17,c17),
inference(superposition,[status(thm)],[c_235,c_655]) ).
tcf(c_1135,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_12)
| ~ p8(X0,c17)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1133,c_231]) ).
tcf(c_1136,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_12)
| ~ p7(X0,c17)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1133,c_230]) ).
tcf(c_1137,plain,
! [X0: $i] :
( p2(iPr_def_12,X0)
| ~ p2(c17,X0) ),
inference(superposition,[status(thm)],[c_1133,c_232]) ).
tcf(c_1153,plain,
p2(c16,iPr_def_13),
inference(superposition,[status(thm)],[c_245,c_656]) ).
tcf(c_1154,plain,
p2(c16,c16),
inference(superposition,[status(thm)],[c_236,c_656]) ).
tcf(c_1166,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_13)
| ~ p8(X0,c16)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1153,c_231]) ).
tcf(c_1167,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_13)
| ~ p7(X0,c16)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1153,c_230]) ).
tcf(c_1168,plain,
! [X0: $i] :
( p2(iPr_def_13,X0)
| ~ p2(c16,X0) ),
inference(superposition,[status(thm)],[c_1153,c_232]) ).
tcf(c_1184,plain,
p2(c17,iPr_def_14),
inference(superposition,[status(thm)],[c_245,c_657]) ).
tcf(c_1186,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_14)
| ~ p8(X0,c17)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1184,c_231]) ).
tcf(c_1187,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_14)
| ~ p7(X0,c17)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1184,c_230]) ).
tcf(c_1188,plain,
! [X0: $i] :
( p2(iPr_def_14,X0)
| ~ p2(c17,X0) ),
inference(superposition,[status(thm)],[c_1184,c_232]) ).
tcf(c_1204,plain,
p2(c18,iPr_def_15),
inference(superposition,[status(thm)],[c_245,c_658]) ).
tcf(c_1206,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_15)
| ~ p8(X0,c18)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1204,c_231]) ).
tcf(c_1207,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_15)
| ~ p7(X0,c18)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1204,c_230]) ).
tcf(c_1208,plain,
! [X0: $i] :
( p2(iPr_def_15,X0)
| ~ p2(c18,X0) ),
inference(superposition,[status(thm)],[c_1204,c_232]) ).
tcf(c_1235,plain,
p2(c15,iPr_def_16),
inference(superposition,[status(thm)],[c_245,c_659]) ).
tcf(c_1236,plain,
p2(c15,c15),
inference(superposition,[status(thm)],[c_239,c_659]) ).
tcf(c_1237,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_16)
| ~ p8(X0,c15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1235,c_231]) ).
tcf(c_1238,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_16)
| ~ p7(X0,c15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1235,c_230]) ).
tcf(c_1239,plain,
! [X0: $i] :
( p2(iPr_def_16,X0)
| ~ p2(c15,X0) ),
inference(superposition,[status(thm)],[c_1235,c_232]) ).
tcf(c_1256,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(X2,iPr_def_10)
| ~ p2(X1,c9)
| ~ p2(X0,X2)
| ~ p8(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_639,c_231]) ).
tcf(c_1257,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(X2,iPr_def_10)
| ~ p2(X1,c9)
| ~ p2(X0,X2)
| ~ p7(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_639,c_230]) ).
tcf(c_1258,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_10,X1)
| ~ p2(X0,c9)
| ~ p2(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_639,c_232]) ).
tcf(c_1278,plain,
p2(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_1101,c_1105]) ).
tcf(c_1279,plain,
p2(iPr_def_11,iPr_def_15),
inference(superposition,[status(thm)],[c_1204,c_1105]) ).
tcf(c_1296,plain,
p2(iPr_def_12,iPr_def_12),
inference(superposition,[status(thm)],[c_1133,c_1137]) ).
tcf(c_1297,plain,
p2(iPr_def_12,iPr_def_14),
inference(superposition,[status(thm)],[c_1184,c_1137]) ).
tcf(c_1303,plain,
p2(iPr_def_13,iPr_def_13),
inference(superposition,[status(thm)],[c_1153,c_1168]) ).
tcf(c_1309,plain,
p2(iPr_def_14,iPr_def_12),
inference(superposition,[status(thm)],[c_1133,c_1188]) ).
tcf(c_1310,plain,
p2(iPr_def_14,iPr_def_14),
inference(superposition,[status(thm)],[c_1184,c_1188]) ).
tcf(c_1311,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_15)
| ~ p8(X0,iPr_def_11)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1279,c_231]) ).
tcf(c_1312,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_15)
| ~ p7(X0,iPr_def_11)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1279,c_230]) ).
tcf(c_1313,plain,
! [X0: $i] :
( p2(iPr_def_15,X0)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_1279,c_232]) ).
tcf(c_1334,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_14)
| ~ p8(X0,iPr_def_12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1297,c_231]) ).
tcf(c_1335,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_14)
| ~ p7(X0,iPr_def_12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1297,c_230]) ).
tcf(c_1336,plain,
! [X0: $i] :
( p2(iPr_def_14,X0)
| ~ p2(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_1297,c_232]) ).
tcf(c_1349,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_12)
| ~ p8(X0,iPr_def_14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1309,c_231]) ).
tcf(c_1350,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_12)
| ~ p7(X0,iPr_def_14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1309,c_230]) ).
tcf(c_1351,plain,
! [X0: $i] :
( p2(iPr_def_12,X0)
| ~ p2(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1309,c_232]) ).
tcf(c_1385,plain,
p2(iPr_def_15,iPr_def_11),
inference(superposition,[status(thm)],[c_1101,c_1208]) ).
tcf(c_1386,plain,
p2(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_1204,c_1208]) ).
tcf(c_1421,plain,
p2(iPr_def_16,iPr_def_16),
inference(superposition,[status(thm)],[c_1235,c_1239]) ).
tcf(c_1450,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(f6(X2),X1)
| ~ p2(X0,X2)
| ~ p7(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_233,c_762]) ).
tcf(c_1451,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p7(f3(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p7(f3(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_229,c_762]) ).
tcf(c_1452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p7(f5(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p7(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_228,c_762]) ).
tcf(c_1453,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p7(f4(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p7(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_227,c_762]) ).
tcf(c_1454,plain,
! [X0: $i] :
( p7(c18,X0)
| ~ p7(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_234,c_762]) ).
tcf(c_1455,plain,
! [X0: $i] :
( p7(c17,X0)
| ~ p7(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_235,c_762]) ).
tcf(c_1456,plain,
! [X0: $i] :
( p7(c16,X0)
| ~ p7(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_236,c_762]) ).
tcf(c_1457,plain,
! [X0: $i] :
( p7(c17,X0)
| ~ p7(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_237,c_762]) ).
tcf(c_1458,plain,
! [X0: $i] :
( p7(c18,X0)
| ~ p7(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_238,c_762]) ).
tcf(c_1459,plain,
! [X0: $i] :
( p7(c15,X0)
| ~ p7(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_239,c_762]) ).
tcf(c_1460,plain,
! [X0: $i,X1: $i] :
( p7(f6(X0),X1)
| ~ p7(iPr_def_10,X1)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_762]) ).
tcf(c_1461,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_10,X1)
| ~ p2(X0,c9)
| ~ p7(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_639,c_762]) ).
tcf(c_1462,plain,
! [X0: $i] :
( p7(iPr_def_11,X0)
| ~ p7(c18,X0) ),
inference(superposition,[status(thm)],[c_1101,c_762]) ).
tcf(c_1463,plain,
! [X0: $i] :
( p7(iPr_def_12,X0)
| ~ p7(c17,X0) ),
inference(superposition,[status(thm)],[c_1133,c_762]) ).
tcf(c_1464,plain,
! [X0: $i] :
( p7(iPr_def_13,X0)
| ~ p7(c16,X0) ),
inference(superposition,[status(thm)],[c_1153,c_762]) ).
tcf(c_1465,plain,
! [X0: $i] :
( p7(iPr_def_14,X0)
| ~ p7(c17,X0) ),
inference(superposition,[status(thm)],[c_1184,c_762]) ).
tcf(c_1466,plain,
! [X0: $i] :
( p7(iPr_def_15,X0)
| ~ p7(c18,X0) ),
inference(superposition,[status(thm)],[c_1204,c_762]) ).
tcf(c_1467,plain,
! [X0: $i] :
( p7(iPr_def_16,X0)
| ~ p7(c15,X0) ),
inference(superposition,[status(thm)],[c_1235,c_762]) ).
tcf(c_1468,plain,
! [X0: $i] :
( p7(iPr_def_15,X0)
| ~ p7(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_1279,c_762]) ).
tcf(c_1469,plain,
! [X0: $i] :
( p7(iPr_def_14,X0)
| ~ p7(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_1297,c_762]) ).
tcf(c_1470,plain,
! [X0: $i] :
( p7(iPr_def_12,X0)
| ~ p7(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1309,c_762]) ).
tcf(c_1587,plain,
! [X0: $i,X1: $i] :
( p2(f6(X1),f6(X0))
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_245,c_653]) ).
tcf(c_1588,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f6(X2),f6(X1))
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_233,c_653]) ).
tcf(c_1589,plain,
! [X0: $i,X1: $i] :
( p2(f6(X1),iPr_def_10)
| ~ p2(X0,c9)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_639,c_653]) ).
tcf(c_1615,plain,
! [X0: $i] :
( p2(iPr_def_10,f6(X0))
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_217,c_1587]) ).
tcf(c_1616,plain,
! [X0: $i] :
( p2(f6(X0),iPr_def_10)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_217,c_1587]) ).
tcf(c_1617,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(f6(X2),X1)
| ~ p2(X2,X0)
| ~ p7(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1587,c_762]) ).
tcf(c_1618,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,f6(X2))
| ~ p2(X2,X1)
| ~ p2(X0,X3)
| ~ p8(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_1587,c_231]) ).
tcf(c_1619,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,f6(X2))
| ~ p2(X2,X1)
| ~ p2(X0,X3)
| ~ p7(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_1587,c_230]) ).
tcf(c_1620,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f6(X2),X1)
| ~ p2(X2,X0)
| ~ p2(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1587,c_232]) ).
tcf(c_1621,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f6(X2),f6(X0))
| ~ p2(X1,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1587,c_653]) ).
tcf(c_1667,plain,
! [X0: $i] :
( p7(iPr_def_11,X0)
| ~ p7(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_1385,c_762]) ).
tcf(c_1668,plain,
! [X0: $i,X1: $i] :
( p8(X1,iPr_def_11)
| ~ p8(X0,iPr_def_15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1385,c_231]) ).
tcf(c_1669,plain,
! [X0: $i,X1: $i] :
( p7(X1,iPr_def_11)
| ~ p7(X0,iPr_def_15)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1385,c_230]) ).
tcf(c_1670,plain,
! [X0: $i] :
( p2(iPr_def_11,X0)
| ~ p2(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_1385,c_232]) ).
tcf(c_1713,plain,
! [X0: $i] :
( p7(X0,c18)
| ~ p7(X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_245,c_767]) ).
tcf(c_1714,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c18)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_233,c_767]) ).
tcf(c_1715,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_229,c_767]) ).
tcf(c_1716,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_228,c_767]) ).
tcf(c_1717,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_227,c_767]) ).
tcf(c_1718,plain,
( p7(c18,c18)
| ~ p7(iPr_def_11,iPr_def_11) ),
inference(superposition,[status(thm)],[c_234,c_767]) ).
tcf(c_1719,plain,
( p7(c17,c18)
| ~ p7(iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_235,c_767]) ).
tcf(c_1720,plain,
( p7(c16,c18)
| ~ p7(iPr_def_13,iPr_def_11) ),
inference(superposition,[status(thm)],[c_236,c_767]) ).
tcf(c_1721,plain,
( p7(c17,c18)
| ~ p7(iPr_def_14,iPr_def_11) ),
inference(superposition,[status(thm)],[c_237,c_767]) ).
tcf(c_1722,plain,
( p7(c18,c18)
| ~ p7(iPr_def_15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_238,c_767]) ).
tcf(c_1723,plain,
( p7(c15,c18)
| ~ p7(iPr_def_16,iPr_def_11) ),
inference(superposition,[status(thm)],[c_239,c_767]) ).
tcf(c_1724,plain,
! [X0: $i] :
( p7(f6(X0),c18)
| ~ p7(iPr_def_10,iPr_def_11)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_767]) ).
tcf(c_1725,plain,
! [X0: $i] :
( p7(iPr_def_10,c18)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_639,c_767]) ).
tcf(c_1726,plain,
( p7(iPr_def_11,c18)
| ~ p7(c18,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1101,c_767]) ).
tcf(c_1727,plain,
( p7(iPr_def_12,c18)
| ~ p7(c17,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1133,c_767]) ).
tcf(c_1728,plain,
( p7(iPr_def_13,c18)
| ~ p7(c16,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1153,c_767]) ).
tcf(c_1729,plain,
( p7(iPr_def_14,c18)
| ~ p7(c17,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1184,c_767]) ).
tcf(c_1730,plain,
( p7(iPr_def_15,c18)
| ~ p7(c18,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1204,c_767]) ).
tcf(c_1731,plain,
( p7(iPr_def_16,c18)
| ~ p7(c15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1235,c_767]) ).
tcf(c_1732,plain,
( p7(iPr_def_15,c18)
| ~ p7(iPr_def_11,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1279,c_767]) ).
tcf(c_1733,plain,
( p7(iPr_def_14,c18)
| ~ p7(iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1297,c_767]) ).
tcf(c_1734,plain,
( p7(iPr_def_12,c18)
| ~ p7(iPr_def_14,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1309,c_767]) ).
tcf(c_1735,plain,
( p7(iPr_def_11,c18)
| ~ p7(iPr_def_15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1385,c_767]) ).
tcf(c_1736,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c18)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_1587,c_767]) ).
tcf(c_1920,plain,
( p2(iPr_def_14,iPr_def_15)
| ~ p2(c15,c16)
| ~ p2(c14,c14) ),
inference(superposition,[status(thm)],[c_222,c_687]) ).
tcf(c_1921,plain,
( p2(iPr_def_14,iPr_def_14)
| ~ p2(c15,c15)
| ~ p2(c14,c14) ),
inference(superposition,[status(thm)],[c_221,c_687]) ).
tcf(c_1922,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c18)
| ~ p7(iPr_def_14,iPr_def_11)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_767]) ).
tcf(c_1923,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(f4(X1,X0),X2)
| ~ p7(iPr_def_14,X2)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_762]) ).
tcf(c_1924,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X1,f4(X3,X2))
| ~ p8(X0,iPr_def_14)
| ~ p2(c15,X3)
| ~ p2(c14,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_687,c_231]) ).
tcf(c_1925,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X1,f4(X3,X2))
| ~ p7(X0,iPr_def_14)
| ~ p2(c15,X3)
| ~ p2(c14,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_687,c_230]) ).
tcf(c_1926,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f4(X1,X0),X2)
| ~ p2(iPr_def_14,X2)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_232]) ).
tcf(c_1927,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f4(X1,X0))
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_1351]) ).
tcf(c_1928,plain,
! [X0: $i,X1: $i] :
( p2(c17,f4(X1,X0))
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_657]) ).
tcf(c_1929,plain,
( p2(iPr_def_14,iPr_def_15)
| ~ p2(c15,c16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1920,c_245]) ).
tcf(c_1999,plain,
! [X0: $i] :
( p7(f6(X0),c18)
| ~ p7(iPr_def_10,iPr_def_11)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_767]) ).
tcf(c_2000,plain,
! [X0: $i,X1: $i] :
( p7(f6(X0),X1)
| ~ p7(iPr_def_10,X1)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_762]) ).
tcf(c_2001,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(X1,f6(X2))
| ~ p8(X0,iPr_def_10)
| ~ p2(X2,c9)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1615,c_231]) ).
tcf(c_2002,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(X1,f6(X2))
| ~ p7(X0,iPr_def_10)
| ~ p2(X2,c9)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1615,c_230]) ).
tcf(c_2003,plain,
! [X0: $i,X1: $i] :
( p2(f6(X0),X1)
| ~ p2(iPr_def_10,X1)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_232]) ).
tcf(c_2099,plain,
! [X0: $i] :
( p7(iPr_def_10,c18)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_1616,c_767]) ).
tcf(c_2100,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_10,X1)
| ~ p2(c9,X0)
| ~ p7(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1616,c_762]) ).
tcf(c_2101,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(X2,iPr_def_10)
| ~ p2(c9,X1)
| ~ p2(X0,X2)
| ~ p8(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_1616,c_231]) ).
tcf(c_2102,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(X2,iPr_def_10)
| ~ p2(c9,X1)
| ~ p2(X0,X2)
| ~ p7(X0,f6(X1)) ),
inference(superposition,[status(thm)],[c_1616,c_230]) ).
tcf(c_2103,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_10,X1)
| ~ p2(c9,X0)
| ~ p2(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1616,c_232]) ).
tcf(c_2104,plain,
! [X0: $i,X1: $i] :
( p2(f6(X1),iPr_def_10)
| ~ p2(c9,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1616,c_653]) ).
tcf(c_2152,plain,
! [X0: $i] :
( p7(X0,c17)
| ~ p7(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_245,c_768]) ).
tcf(c_2153,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c17)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_233,c_768]) ).
tcf(c_2154,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_229,c_768]) ).
tcf(c_2155,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_228,c_768]) ).
tcf(c_2156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_227,c_768]) ).
tcf(c_2157,plain,
( p7(c18,c17)
| ~ p7(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_234,c_768]) ).
tcf(c_2158,plain,
( p7(c17,c17)
| ~ p7(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_235,c_768]) ).
tcf(c_2159,plain,
( p7(c16,c17)
| ~ p7(iPr_def_13,iPr_def_12) ),
inference(superposition,[status(thm)],[c_236,c_768]) ).
tcf(c_2160,plain,
( p7(c17,c17)
| ~ p7(iPr_def_14,iPr_def_12) ),
inference(superposition,[status(thm)],[c_237,c_768]) ).
tcf(c_2161,plain,
( p7(c18,c17)
| ~ p7(iPr_def_15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_238,c_768]) ).
tcf(c_2162,plain,
( p7(c15,c17)
| ~ p7(iPr_def_16,iPr_def_12) ),
inference(superposition,[status(thm)],[c_239,c_768]) ).
tcf(c_2163,plain,
! [X0: $i] :
( p7(f6(X0),c17)
| ~ p7(iPr_def_10,iPr_def_12)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_768]) ).
tcf(c_2164,plain,
! [X0: $i] :
( p7(f6(X0),c17)
| ~ p7(iPr_def_10,iPr_def_12)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_768]) ).
tcf(c_2165,plain,
! [X0: $i] :
( p7(iPr_def_10,c17)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_1616,c_768]) ).
tcf(c_2166,plain,
! [X0: $i] :
( p7(iPr_def_10,c17)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_639,c_768]) ).
tcf(c_2167,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c17)
| ~ p7(iPr_def_14,iPr_def_12)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_768]) ).
tcf(c_2168,plain,
( p7(iPr_def_11,c17)
| ~ p7(c18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1101,c_768]) ).
tcf(c_2169,plain,
( p7(iPr_def_12,c17)
| ~ p7(c17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1133,c_768]) ).
tcf(c_2170,plain,
( p7(iPr_def_13,c17)
| ~ p7(c16,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1153,c_768]) ).
tcf(c_2171,plain,
( p7(iPr_def_14,c17)
| ~ p7(c17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1184,c_768]) ).
tcf(c_2172,plain,
( p7(iPr_def_15,c17)
| ~ p7(c18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1204,c_768]) ).
tcf(c_2173,plain,
( p7(iPr_def_16,c17)
| ~ p7(c15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1235,c_768]) ).
tcf(c_2174,plain,
( p7(iPr_def_15,c17)
| ~ p7(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1279,c_768]) ).
tcf(c_2175,plain,
( p7(iPr_def_14,c17)
| ~ p7(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1297,c_768]) ).
tcf(c_2176,plain,
( p7(iPr_def_12,c17)
| ~ p7(iPr_def_14,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1309,c_768]) ).
tcf(c_2177,plain,
( p7(iPr_def_11,c17)
| ~ p7(iPr_def_15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1385,c_768]) ).
tcf(c_2178,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c17)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_1587,c_768]) ).
tcf(c_2333,plain,
( p2(iPr_def_15,iPr_def_14)
| ~ p2(c16,c15)
| ~ p2(c14,c14) ),
inference(superposition,[status(thm)],[c_222,c_688]) ).
tcf(c_2335,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c17)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_688,c_768]) ).
tcf(c_2336,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c18)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_688,c_767]) ).
tcf(c_2337,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(iPr_def_14,X2)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_688,c_762]) ).
tcf(c_2338,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,iPr_def_14)
| ~ p2(X2,c14)
| ~ p2(X1,c15)
| ~ p2(X0,X3)
| ~ p8(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_688,c_231]) ).
tcf(c_2339,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,iPr_def_14)
| ~ p2(X2,c14)
| ~ p2(X1,c15)
| ~ p2(X0,X3)
| ~ p7(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_688,c_230]) ).
tcf(c_2340,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(iPr_def_14,X2)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p2(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_688,c_232]) ).
tcf(c_2341,plain,
( p2(iPr_def_15,iPr_def_14)
| ~ p2(c16,c15) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2333,c_245]) ).
tcf(c_2399,plain,
! [X0: $i] :
( p7(X0,c16)
| ~ p7(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_245,c_769]) ).
tcf(c_2400,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c16)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_233,c_769]) ).
tcf(c_2401,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_229,c_769]) ).
tcf(c_2402,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_228,c_769]) ).
tcf(c_2403,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_227,c_769]) ).
tcf(c_2404,plain,
( p7(c18,c16)
| ~ p7(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_234,c_769]) ).
tcf(c_2405,plain,
( p7(c17,c16)
| ~ p7(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_235,c_769]) ).
tcf(c_2406,plain,
( p7(c16,c16)
| ~ p7(iPr_def_13,iPr_def_13) ),
inference(superposition,[status(thm)],[c_236,c_769]) ).
tcf(c_2407,plain,
( p7(c17,c16)
| ~ p7(iPr_def_14,iPr_def_13) ),
inference(superposition,[status(thm)],[c_237,c_769]) ).
tcf(c_2408,plain,
( p7(c18,c16)
| ~ p7(iPr_def_15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_238,c_769]) ).
tcf(c_2409,plain,
( p7(c15,c16)
| ~ p7(iPr_def_16,iPr_def_13) ),
inference(superposition,[status(thm)],[c_239,c_769]) ).
tcf(c_2410,plain,
! [X0: $i] :
( p7(f6(X0),c16)
| ~ p7(iPr_def_10,iPr_def_13)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_769]) ).
tcf(c_2411,plain,
! [X0: $i] :
( p7(f6(X0),c16)
| ~ p7(iPr_def_10,iPr_def_13)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_769]) ).
tcf(c_2412,plain,
! [X0: $i] :
( p7(iPr_def_10,c16)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1616,c_769]) ).
tcf(c_2413,plain,
! [X0: $i] :
( p7(iPr_def_10,c16)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_639,c_769]) ).
tcf(c_2414,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c16)
| ~ p7(iPr_def_14,iPr_def_13)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_769]) ).
tcf(c_2415,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c16)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_688,c_769]) ).
tcf(c_2416,plain,
( p7(iPr_def_11,c16)
| ~ p7(c18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1101,c_769]) ).
tcf(c_2417,plain,
( p7(iPr_def_12,c16)
| ~ p7(c17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1133,c_769]) ).
tcf(c_2418,plain,
( p7(iPr_def_13,c16)
| ~ p7(c16,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1153,c_769]) ).
tcf(c_2419,plain,
( p7(iPr_def_14,c16)
| ~ p7(c17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1184,c_769]) ).
tcf(c_2420,plain,
( p7(iPr_def_15,c16)
| ~ p7(c18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1204,c_769]) ).
tcf(c_2421,plain,
( p7(iPr_def_16,c16)
| ~ p7(c15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1235,c_769]) ).
tcf(c_2422,plain,
( p7(iPr_def_15,c16)
| ~ p7(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1279,c_769]) ).
tcf(c_2423,plain,
( p7(iPr_def_14,c16)
| ~ p7(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1297,c_769]) ).
tcf(c_2424,plain,
( p7(iPr_def_12,c16)
| ~ p7(iPr_def_14,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1309,c_769]) ).
tcf(c_2425,plain,
( p7(iPr_def_11,c16)
| ~ p7(iPr_def_15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1385,c_769]) ).
tcf(c_2426,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c16)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1587,c_769]) ).
tcf(c_2668,plain,
! [X0: $i] :
( p7(X0,c17)
| ~ p7(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_245,c_770]) ).
tcf(c_2669,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c17)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_233,c_770]) ).
tcf(c_2670,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_14) ),
inference(superposition,[status(thm)],[c_229,c_770]) ).
tcf(c_2671,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_14) ),
inference(superposition,[status(thm)],[c_228,c_770]) ).
tcf(c_2672,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_14) ),
inference(superposition,[status(thm)],[c_227,c_770]) ).
tcf(c_2673,plain,
( p7(c18,c17)
| ~ p7(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_234,c_770]) ).
tcf(c_2674,plain,
( p7(c17,c17)
| ~ p7(iPr_def_12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_235,c_770]) ).
tcf(c_2675,plain,
( p7(c16,c17)
| ~ p7(iPr_def_13,iPr_def_14) ),
inference(superposition,[status(thm)],[c_236,c_770]) ).
tcf(c_2676,plain,
( p7(c17,c17)
| ~ p7(iPr_def_14,iPr_def_14) ),
inference(superposition,[status(thm)],[c_237,c_770]) ).
tcf(c_2677,plain,
( p7(c18,c17)
| ~ p7(iPr_def_15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_238,c_770]) ).
tcf(c_2678,plain,
( p7(c15,c17)
| ~ p7(iPr_def_16,iPr_def_14) ),
inference(superposition,[status(thm)],[c_239,c_770]) ).
tcf(c_2679,plain,
! [X0: $i] :
( p7(f6(X0),c17)
| ~ p7(iPr_def_10,iPr_def_14)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_770]) ).
tcf(c_2680,plain,
! [X0: $i] :
( p7(f6(X0),c17)
| ~ p7(iPr_def_10,iPr_def_14)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_770]) ).
tcf(c_2681,plain,
! [X0: $i] :
( p7(iPr_def_10,c17)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1616,c_770]) ).
tcf(c_2682,plain,
! [X0: $i] :
( p7(iPr_def_10,c17)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_639,c_770]) ).
tcf(c_2683,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c17)
| ~ p7(iPr_def_14,iPr_def_14)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_770]) ).
tcf(c_2684,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c17)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_14) ),
inference(superposition,[status(thm)],[c_688,c_770]) ).
tcf(c_2685,plain,
( p7(iPr_def_11,c17)
| ~ p7(c18,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1101,c_770]) ).
tcf(c_2686,plain,
( p7(iPr_def_12,c17)
| ~ p7(c17,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1133,c_770]) ).
tcf(c_2687,plain,
( p7(iPr_def_13,c17)
| ~ p7(c16,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1153,c_770]) ).
tcf(c_2688,plain,
( p7(iPr_def_14,c17)
| ~ p7(c17,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1184,c_770]) ).
tcf(c_2689,plain,
( p7(iPr_def_15,c17)
| ~ p7(c18,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1204,c_770]) ).
tcf(c_2690,plain,
( p7(iPr_def_16,c17)
| ~ p7(c15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1235,c_770]) ).
tcf(c_2691,plain,
( p7(iPr_def_15,c17)
| ~ p7(iPr_def_11,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1279,c_770]) ).
tcf(c_2692,plain,
( p7(iPr_def_14,c17)
| ~ p7(iPr_def_12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1297,c_770]) ).
tcf(c_2693,plain,
( p7(iPr_def_12,c17)
| ~ p7(iPr_def_14,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1309,c_770]) ).
tcf(c_2694,plain,
( p7(iPr_def_11,c17)
| ~ p7(iPr_def_15,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1385,c_770]) ).
tcf(c_2695,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c17)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1587,c_770]) ).
tcf(c_2886,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X1,X3),f4(X0,X2))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_245,c_689]) ).
tcf(c_2887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p2(f4(X2,X5),f4(X1,X4))
| ~ p2(X3,X5)
| ~ p2(X3,X4)
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_227,c_689]) ).
tcf(c_2888,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X1,X3),iPr_def_14)
| ~ p2(X2,c14)
| ~ p2(X0,c15)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_688,c_689]) ).
tcf(c_2889,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f4(X1,X0),X2)
| ~ p2(iPr_def_15,X2)
| ~ p2(c16,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_222,c_689]) ).
tcf(c_2962,plain,
! [X0: $i] :
( p7(X0,c18)
| ~ p7(X0,iPr_def_15) ),
inference(superposition,[status(thm)],[c_245,c_771]) ).
tcf(c_2963,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c18)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_15) ),
inference(superposition,[status(thm)],[c_233,c_771]) ).
tcf(c_2964,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_15) ),
inference(superposition,[status(thm)],[c_229,c_771]) ).
tcf(c_2965,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_15) ),
inference(superposition,[status(thm)],[c_228,c_771]) ).
tcf(c_2966,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_15) ),
inference(superposition,[status(thm)],[c_227,c_771]) ).
tcf(c_2967,plain,
( p7(c18,c18)
| ~ p7(iPr_def_11,iPr_def_15) ),
inference(superposition,[status(thm)],[c_234,c_771]) ).
tcf(c_2968,plain,
( p7(c17,c18)
| ~ p7(iPr_def_12,iPr_def_15) ),
inference(superposition,[status(thm)],[c_235,c_771]) ).
tcf(c_2969,plain,
( p7(c16,c18)
| ~ p7(iPr_def_13,iPr_def_15) ),
inference(superposition,[status(thm)],[c_236,c_771]) ).
tcf(c_2970,plain,
( p7(c17,c18)
| ~ p7(iPr_def_14,iPr_def_15) ),
inference(superposition,[status(thm)],[c_237,c_771]) ).
tcf(c_2971,plain,
( p7(c18,c18)
| ~ p7(iPr_def_15,iPr_def_15) ),
inference(superposition,[status(thm)],[c_238,c_771]) ).
tcf(c_2972,plain,
( p7(c15,c18)
| ~ p7(iPr_def_16,iPr_def_15) ),
inference(superposition,[status(thm)],[c_239,c_771]) ).
tcf(c_2973,plain,
! [X0: $i] :
( p7(f6(X0),c18)
| ~ p7(iPr_def_10,iPr_def_15)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_771]) ).
tcf(c_2974,plain,
! [X0: $i] :
( p7(f6(X0),c18)
| ~ p7(iPr_def_10,iPr_def_15)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_771]) ).
tcf(c_2975,plain,
! [X0: $i] :
( p7(iPr_def_10,c18)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_15) ),
inference(superposition,[status(thm)],[c_1616,c_771]) ).
tcf(c_2976,plain,
! [X0: $i] :
( p7(iPr_def_10,c18)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_15) ),
inference(superposition,[status(thm)],[c_639,c_771]) ).
tcf(c_2977,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c18)
| ~ p7(iPr_def_14,iPr_def_15)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_771]) ).
tcf(c_2978,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c18)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_15) ),
inference(superposition,[status(thm)],[c_688,c_771]) ).
tcf(c_2979,plain,
( p7(iPr_def_11,c18)
| ~ p7(c18,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1101,c_771]) ).
tcf(c_2980,plain,
( p7(iPr_def_12,c18)
| ~ p7(c17,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1133,c_771]) ).
tcf(c_2981,plain,
( p7(iPr_def_13,c18)
| ~ p7(c16,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1153,c_771]) ).
tcf(c_2982,plain,
( p7(iPr_def_14,c18)
| ~ p7(c17,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1184,c_771]) ).
tcf(c_2983,plain,
( p7(iPr_def_15,c18)
| ~ p7(c18,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1204,c_771]) ).
tcf(c_2984,plain,
( p7(iPr_def_16,c18)
| ~ p7(c15,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1235,c_771]) ).
tcf(c_2985,plain,
( p7(iPr_def_15,c18)
| ~ p7(iPr_def_11,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1279,c_771]) ).
tcf(c_2986,plain,
( p7(iPr_def_14,c18)
| ~ p7(iPr_def_12,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1297,c_771]) ).
tcf(c_2987,plain,
( p7(iPr_def_12,c18)
| ~ p7(iPr_def_14,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1309,c_771]) ).
tcf(c_2988,plain,
( p7(iPr_def_11,c18)
| ~ p7(iPr_def_15,iPr_def_15) ),
inference(superposition,[status(thm)],[c_1385,c_771]) ).
tcf(c_2989,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c18)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_15) ),
inference(superposition,[status(thm)],[c_1587,c_771]) ).
tcf(c_3239,plain,
( p2(iPr_def_11,iPr_def_11)
| ~ p2(iPr_def_10,iPr_def_10)
| ~ p2(c20,c20) ),
inference(superposition,[status(thm)],[c_218,c_708]) ).
tcf(c_3240,plain,
( p2(iPr_def_11,iPr_def_12)
| ~ p2(iPr_def_10,iPr_def_10)
| ~ p2(c20,c19) ),
inference(superposition,[status(thm)],[c_219,c_708]) ).
tcf(c_3241,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c18)
| ~ p7(iPr_def_11,iPr_def_15)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_771]) ).
tcf(c_3242,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c17)
| ~ p7(iPr_def_11,iPr_def_14)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_770]) ).
tcf(c_3243,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c16)
| ~ p7(iPr_def_11,iPr_def_13)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_769]) ).
tcf(c_3244,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c17)
| ~ p7(iPr_def_11,iPr_def_12)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_768]) ).
tcf(c_3245,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c18)
| ~ p7(iPr_def_11,iPr_def_11)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_767]) ).
tcf(c_3246,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(f5(X1,X0),X2)
| ~ p7(iPr_def_11,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_762]) ).
tcf(c_3247,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X1,f5(X3,X2))
| ~ p8(X0,iPr_def_11)
| ~ p2(iPr_def_10,X3)
| ~ p2(c20,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_708,c_231]) ).
tcf(c_3248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X1,f5(X3,X2))
| ~ p7(X0,iPr_def_11)
| ~ p2(iPr_def_10,X3)
| ~ p2(c20,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_708,c_230]) ).
tcf(c_3249,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f5(X1,X0),X2)
| ~ p2(iPr_def_11,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_232]) ).
tcf(c_3250,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_15,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_1313]) ).
tcf(c_3251,plain,
! [X0: $i,X1: $i] :
( p2(c18,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_654]) ).
tcf(c_3252,plain,
( p2(iPr_def_11,iPr_def_12)
| ~ p2(c20,c19) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3240,c_245]) ).
tcf(c_3401,plain,
! [X0: $i] :
( p7(X0,c15)
| ~ p7(X0,iPr_def_16) ),
inference(superposition,[status(thm)],[c_245,c_772]) ).
tcf(c_3402,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c15)
| ~ p2(X0,X1)
| ~ p7(f6(X0),iPr_def_16) ),
inference(superposition,[status(thm)],[c_233,c_772]) ).
tcf(c_3403,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f3(X2,X3),c15)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f3(X0,X1),iPr_def_16) ),
inference(superposition,[status(thm)],[c_229,c_772]) ).
tcf(c_3404,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f5(X2,X3),c15)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f5(X0,X1),iPr_def_16) ),
inference(superposition,[status(thm)],[c_228,c_772]) ).
tcf(c_3405,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(f4(X2,X3),c15)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p7(f4(X0,X1),iPr_def_16) ),
inference(superposition,[status(thm)],[c_227,c_772]) ).
tcf(c_3406,plain,
( p7(c18,c15)
| ~ p7(iPr_def_11,iPr_def_16) ),
inference(superposition,[status(thm)],[c_234,c_772]) ).
tcf(c_3407,plain,
( p7(c17,c15)
| ~ p7(iPr_def_12,iPr_def_16) ),
inference(superposition,[status(thm)],[c_235,c_772]) ).
tcf(c_3408,plain,
( p7(c16,c15)
| ~ p7(iPr_def_13,iPr_def_16) ),
inference(superposition,[status(thm)],[c_236,c_772]) ).
tcf(c_3409,plain,
( p7(c17,c15)
| ~ p7(iPr_def_14,iPr_def_16) ),
inference(superposition,[status(thm)],[c_237,c_772]) ).
tcf(c_3410,plain,
( p7(c18,c15)
| ~ p7(iPr_def_15,iPr_def_16) ),
inference(superposition,[status(thm)],[c_238,c_772]) ).
tcf(c_3411,plain,
( p7(c15,c15)
| ~ p7(iPr_def_16,iPr_def_16) ),
inference(superposition,[status(thm)],[c_239,c_772]) ).
tcf(c_3412,plain,
! [X0: $i] :
( p7(f6(X0),c15)
| ~ p7(iPr_def_10,iPr_def_16)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_772]) ).
tcf(c_3413,plain,
! [X0: $i] :
( p7(f6(X0),c15)
| ~ p7(iPr_def_10,iPr_def_16)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_772]) ).
tcf(c_3414,plain,
! [X0: $i] :
( p7(iPr_def_10,c15)
| ~ p2(c9,X0)
| ~ p7(f6(X0),iPr_def_16) ),
inference(superposition,[status(thm)],[c_1616,c_772]) ).
tcf(c_3415,plain,
! [X0: $i] :
( p7(iPr_def_10,c15)
| ~ p2(X0,c9)
| ~ p7(f6(X0),iPr_def_16) ),
inference(superposition,[status(thm)],[c_639,c_772]) ).
tcf(c_3416,plain,
! [X0: $i,X1: $i] :
( p7(f4(X1,X0),c15)
| ~ p7(iPr_def_14,iPr_def_16)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_772]) ).
tcf(c_3417,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_14,c15)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p7(f4(X0,X1),iPr_def_16) ),
inference(superposition,[status(thm)],[c_688,c_772]) ).
tcf(c_3418,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c15)
| ~ p7(iPr_def_11,iPr_def_16)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_772]) ).
tcf(c_3419,plain,
( p7(iPr_def_11,c15)
| ~ p7(c18,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1101,c_772]) ).
tcf(c_3420,plain,
( p7(iPr_def_12,c15)
| ~ p7(c17,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1133,c_772]) ).
tcf(c_3421,plain,
( p7(iPr_def_13,c15)
| ~ p7(c16,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1153,c_772]) ).
tcf(c_3422,plain,
( p7(iPr_def_14,c15)
| ~ p7(c17,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1184,c_772]) ).
tcf(c_3423,plain,
( p7(iPr_def_15,c15)
| ~ p7(c18,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1204,c_772]) ).
tcf(c_3424,plain,
( p7(iPr_def_16,c15)
| ~ p7(c15,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1235,c_772]) ).
tcf(c_3425,plain,
( p7(iPr_def_15,c15)
| ~ p7(iPr_def_11,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1279,c_772]) ).
tcf(c_3426,plain,
( p7(iPr_def_14,c15)
| ~ p7(iPr_def_12,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1297,c_772]) ).
tcf(c_3427,plain,
( p7(iPr_def_12,c15)
| ~ p7(iPr_def_14,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1309,c_772]) ).
tcf(c_3428,plain,
( p7(iPr_def_11,c15)
| ~ p7(iPr_def_15,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1385,c_772]) ).
tcf(c_3429,plain,
! [X0: $i,X1: $i] :
( p7(f6(X1),c15)
| ~ p2(X1,X0)
| ~ p7(f6(X0),iPr_def_16) ),
inference(superposition,[status(thm)],[c_1587,c_772]) ).
tcf(c_3664,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(f6(X2),X1)
| ~ p2(X0,X2)
| ~ p8(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_233,c_827]) ).
tcf(c_3665,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p8(f3(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p8(f3(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_229,c_827]) ).
tcf(c_3666,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p8(f5(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p8(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_228,c_827]) ).
tcf(c_3667,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p8(f4(X3,X4),X2)
| ~ p2(X1,X4)
| ~ p2(X0,X3)
| ~ p8(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_227,c_827]) ).
tcf(c_3668,plain,
! [X0: $i] :
( p8(c18,X0)
| ~ p8(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_234,c_827]) ).
tcf(c_3669,plain,
! [X0: $i] :
( p8(c17,X0)
| ~ p8(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_235,c_827]) ).
tcf(c_3670,plain,
! [X0: $i] :
( p8(c16,X0)
| ~ p8(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_236,c_827]) ).
tcf(c_3671,plain,
! [X0: $i] :
( p8(c17,X0)
| ~ p8(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_237,c_827]) ).
tcf(c_3672,plain,
! [X0: $i] :
( p8(c18,X0)
| ~ p8(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_238,c_827]) ).
tcf(c_3673,plain,
! [X0: $i] :
( p8(c15,X0)
| ~ p8(iPr_def_16,X0) ),
inference(superposition,[status(thm)],[c_239,c_827]) ).
tcf(c_3674,plain,
! [X0: $i,X1: $i] :
( p8(f6(X0),X1)
| ~ p8(iPr_def_10,X1)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_827]) ).
tcf(c_3675,plain,
! [X0: $i,X1: $i] :
( p8(f6(X0),X1)
| ~ p8(iPr_def_10,X1)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_827]) ).
tcf(c_3676,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_10,X1)
| ~ p2(c9,X0)
| ~ p8(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1616,c_827]) ).
tcf(c_3677,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_10,X1)
| ~ p2(X0,c9)
| ~ p8(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_639,c_827]) ).
tcf(c_3678,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(f4(X1,X0),X2)
| ~ p8(iPr_def_14,X2)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_827]) ).
tcf(c_3679,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(iPr_def_14,X2)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p8(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_688,c_827]) ).
tcf(c_3680,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(f5(X1,X0),X2)
| ~ p8(iPr_def_11,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_827]) ).
tcf(c_3681,plain,
! [X0: $i] :
( p8(iPr_def_11,X0)
| ~ p8(c18,X0) ),
inference(superposition,[status(thm)],[c_1101,c_827]) ).
tcf(c_3682,plain,
! [X0: $i] :
( p8(iPr_def_12,X0)
| ~ p8(c17,X0) ),
inference(superposition,[status(thm)],[c_1133,c_827]) ).
tcf(c_3683,plain,
! [X0: $i] :
( p8(iPr_def_13,X0)
| ~ p8(c16,X0) ),
inference(superposition,[status(thm)],[c_1153,c_827]) ).
tcf(c_3684,plain,
! [X0: $i] :
( p8(iPr_def_14,X0)
| ~ p8(c17,X0) ),
inference(superposition,[status(thm)],[c_1184,c_827]) ).
tcf(c_3685,plain,
! [X0: $i] :
( p8(iPr_def_15,X0)
| ~ p8(c18,X0) ),
inference(superposition,[status(thm)],[c_1204,c_827]) ).
tcf(c_3686,plain,
! [X0: $i] :
( p8(iPr_def_16,X0)
| ~ p8(c15,X0) ),
inference(superposition,[status(thm)],[c_1235,c_827]) ).
tcf(c_3687,plain,
! [X0: $i] :
( p8(iPr_def_15,X0)
| ~ p8(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_1279,c_827]) ).
tcf(c_3688,plain,
! [X0: $i] :
( p8(iPr_def_14,X0)
| ~ p8(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_1297,c_827]) ).
tcf(c_3689,plain,
! [X0: $i] :
( p8(iPr_def_12,X0)
| ~ p8(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1309,c_827]) ).
tcf(c_3690,plain,
! [X0: $i] :
( p8(iPr_def_11,X0)
| ~ p8(iPr_def_15,X0) ),
inference(superposition,[status(thm)],[c_1385,c_827]) ).
tcf(c_3691,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(f6(X2),X1)
| ~ p2(X2,X0)
| ~ p8(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1587,c_827]) ).
tcf(c_3871,plain,
( p2(iPr_def_12,iPr_def_11)
| ~ p2(iPr_def_10,iPr_def_10)
| ~ p2(c19,c20) ),
inference(superposition,[status(thm)],[c_218,c_709]) ).
tcf(c_3872,plain,
( p2(iPr_def_12,iPr_def_12)
| ~ p2(iPr_def_10,iPr_def_10)
| ~ p2(c19,c19) ),
inference(superposition,[status(thm)],[c_219,c_709]) ).
tcf(c_3873,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(f5(X1,X0),X2)
| ~ p8(iPr_def_12,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_827]) ).
tcf(c_3874,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c15)
| ~ p7(iPr_def_12,iPr_def_16)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_772]) ).
tcf(c_3875,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c18)
| ~ p7(iPr_def_12,iPr_def_15)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_771]) ).
tcf(c_3876,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c17)
| ~ p7(iPr_def_12,iPr_def_14)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_770]) ).
tcf(c_3877,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c16)
| ~ p7(iPr_def_12,iPr_def_13)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_769]) ).
tcf(c_3878,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c17)
| ~ p7(iPr_def_12,iPr_def_12)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_768]) ).
tcf(c_3879,plain,
! [X0: $i,X1: $i] :
( p7(f5(X1,X0),c18)
| ~ p7(iPr_def_12,iPr_def_11)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_767]) ).
tcf(c_3880,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(f5(X1,X0),X2)
| ~ p7(iPr_def_12,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_762]) ).
tcf(c_3881,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X1,f5(X3,X2))
| ~ p8(X0,iPr_def_12)
| ~ p2(iPr_def_10,X3)
| ~ p2(c19,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_709,c_231]) ).
tcf(c_3882,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X1,f5(X3,X2))
| ~ p7(X0,iPr_def_12)
| ~ p2(iPr_def_10,X3)
| ~ p2(c19,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_709,c_230]) ).
tcf(c_3883,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f5(X1,X0),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_232]) ).
tcf(c_3884,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_14,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_1336]) ).
tcf(c_3885,plain,
! [X0: $i,X1: $i] :
( p2(c17,f5(X1,X0))
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_655]) ).
tcf(c_3886,plain,
( p2(iPr_def_12,iPr_def_11)
| ~ p2(c19,c20) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3871,c_245]) ).
tcf(c_4042,plain,
! [X0: $i] :
( p8(X0,c18)
| ~ p8(X0,iPr_def_11) ),
inference(superposition,[status(thm)],[c_245,c_832]) ).
tcf(c_4043,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c18)
| ~ p2(X0,X1)
| ~ p8(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_233,c_832]) ).
tcf(c_4044,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f3(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f3(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_229,c_832]) ).
tcf(c_4045,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f5(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f5(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_228,c_832]) ).
tcf(c_4046,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f4(X2,X3),c18)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f4(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_227,c_832]) ).
tcf(c_4047,plain,
( p8(c18,c18)
| ~ p8(iPr_def_11,iPr_def_11) ),
inference(superposition,[status(thm)],[c_234,c_832]) ).
tcf(c_4048,plain,
( p8(c17,c18)
| ~ p8(iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_235,c_832]) ).
tcf(c_4049,plain,
( p8(c16,c18)
| ~ p8(iPr_def_13,iPr_def_11) ),
inference(superposition,[status(thm)],[c_236,c_832]) ).
tcf(c_4050,plain,
( p8(c17,c18)
| ~ p8(iPr_def_14,iPr_def_11) ),
inference(superposition,[status(thm)],[c_237,c_832]) ).
tcf(c_4051,plain,
( p8(c18,c18)
| ~ p8(iPr_def_15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_238,c_832]) ).
tcf(c_4052,plain,
( p8(c15,c18)
| ~ p8(iPr_def_16,iPr_def_11) ),
inference(superposition,[status(thm)],[c_239,c_832]) ).
tcf(c_4053,plain,
! [X0: $i] :
( p8(f6(X0),c18)
| ~ p8(iPr_def_10,iPr_def_11)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_832]) ).
tcf(c_4054,plain,
! [X0: $i] :
( p8(f6(X0),c18)
| ~ p8(iPr_def_10,iPr_def_11)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_832]) ).
tcf(c_4055,plain,
! [X0: $i] :
( p8(iPr_def_10,c18)
| ~ p2(c9,X0)
| ~ p8(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_1616,c_832]) ).
tcf(c_4056,plain,
! [X0: $i] :
( p8(iPr_def_10,c18)
| ~ p2(X0,c9)
| ~ p8(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_639,c_832]) ).
tcf(c_4057,plain,
! [X0: $i,X1: $i] :
( p8(f4(X1,X0),c18)
| ~ p8(iPr_def_14,iPr_def_11)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_832]) ).
tcf(c_4058,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_14,c18)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p8(f4(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_688,c_832]) ).
tcf(c_4059,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c18)
| ~ p8(iPr_def_11,iPr_def_11)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_832]) ).
tcf(c_4060,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c18)
| ~ p8(iPr_def_12,iPr_def_11)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_832]) ).
tcf(c_4061,plain,
( p8(iPr_def_11,c18)
| ~ p8(c18,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1101,c_832]) ).
tcf(c_4062,plain,
( p8(iPr_def_12,c18)
| ~ p8(c17,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1133,c_832]) ).
tcf(c_4063,plain,
( p8(iPr_def_13,c18)
| ~ p8(c16,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1153,c_832]) ).
tcf(c_4064,plain,
( p8(iPr_def_14,c18)
| ~ p8(c17,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1184,c_832]) ).
tcf(c_4065,plain,
( p8(iPr_def_15,c18)
| ~ p8(c18,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1204,c_832]) ).
tcf(c_4066,plain,
( p8(iPr_def_16,c18)
| ~ p8(c15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1235,c_832]) ).
tcf(c_4067,plain,
( p8(iPr_def_15,c18)
| ~ p8(iPr_def_11,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1279,c_832]) ).
tcf(c_4068,plain,
( p8(iPr_def_14,c18)
| ~ p8(iPr_def_12,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1297,c_832]) ).
tcf(c_4069,plain,
( p8(iPr_def_12,c18)
| ~ p8(iPr_def_14,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1309,c_832]) ).
tcf(c_4070,plain,
( p8(iPr_def_11,c18)
| ~ p8(iPr_def_15,iPr_def_11) ),
inference(superposition,[status(thm)],[c_1385,c_832]) ).
tcf(c_4071,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c18)
| ~ p2(X1,X0)
| ~ p8(f6(X0),iPr_def_11) ),
inference(superposition,[status(thm)],[c_1587,c_832]) ).
tcf(c_4319,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_11,c18)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p8(f5(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_710,c_832]) ).
tcf(c_4320,plain,
! [X0: $i,X1: $i,X2: $i] :
( p8(iPr_def_11,X2)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p8(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_710,c_827]) ).
tcf(c_4321,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c15)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_16) ),
inference(superposition,[status(thm)],[c_710,c_772]) ).
tcf(c_4322,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c18)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_15) ),
inference(superposition,[status(thm)],[c_710,c_771]) ).
tcf(c_4323,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c17)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_14) ),
inference(superposition,[status(thm)],[c_710,c_770]) ).
tcf(c_4324,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c16)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_710,c_769]) ).
tcf(c_4325,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c17)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_710,c_768]) ).
tcf(c_4326,plain,
! [X0: $i,X1: $i] :
( p7(iPr_def_11,c18)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),iPr_def_11) ),
inference(superposition,[status(thm)],[c_710,c_767]) ).
tcf(c_4327,plain,
! [X0: $i,X1: $i,X2: $i] :
( p7(iPr_def_11,X2)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p7(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_710,c_762]) ).
tcf(c_4328,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(X3,iPr_def_11)
| ~ p2(X2,c20)
| ~ p2(X1,iPr_def_10)
| ~ p2(X0,X3)
| ~ p8(X0,f5(X1,X2)) ),
inference(superposition,[status(thm)],[c_710,c_231]) ).
tcf(c_4329,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p7(X3,iPr_def_11)
| ~ p2(X2,c20)
| ~ p2(X1,iPr_def_10)
| ~ p2(X0,X3)
| ~ p7(X0,f5(X1,X2)) ),
inference(superposition,[status(thm)],[c_710,c_230]) ).
tcf(c_4330,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(iPr_def_11,X2)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p2(f5(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_710,c_232]) ).
tcf(c_4460,plain,
! [X0: $i] :
( p8(X0,c17)
| ~ p8(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_245,c_833]) ).
tcf(c_4461,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c17)
| ~ p2(X0,X1)
| ~ p8(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_233,c_833]) ).
tcf(c_4462,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f3(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f3(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_229,c_833]) ).
tcf(c_4463,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f5(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f5(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_228,c_833]) ).
tcf(c_4464,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f4(X2,X3),c17)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f4(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_227,c_833]) ).
tcf(c_4465,plain,
( p8(c18,c17)
| ~ p8(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_234,c_833]) ).
tcf(c_4466,plain,
( p8(c17,c17)
| ~ p8(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_235,c_833]) ).
tcf(c_4467,plain,
( p8(c16,c17)
| ~ p8(iPr_def_13,iPr_def_12) ),
inference(superposition,[status(thm)],[c_236,c_833]) ).
tcf(c_4468,plain,
( p8(c17,c17)
| ~ p8(iPr_def_14,iPr_def_12) ),
inference(superposition,[status(thm)],[c_237,c_833]) ).
tcf(c_4469,plain,
( p8(c18,c17)
| ~ p8(iPr_def_15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_238,c_833]) ).
tcf(c_4470,plain,
( p8(c15,c17)
| ~ p8(iPr_def_16,iPr_def_12) ),
inference(superposition,[status(thm)],[c_239,c_833]) ).
tcf(c_4471,plain,
! [X0: $i] :
( p8(f6(X0),c17)
| ~ p8(iPr_def_10,iPr_def_12)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_833]) ).
tcf(c_4472,plain,
! [X0: $i] :
( p8(f6(X0),c17)
| ~ p8(iPr_def_10,iPr_def_12)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_833]) ).
tcf(c_4473,plain,
! [X0: $i] :
( p8(iPr_def_10,c17)
| ~ p2(c9,X0)
| ~ p8(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_1616,c_833]) ).
tcf(c_4474,plain,
! [X0: $i] :
( p8(iPr_def_10,c17)
| ~ p2(X0,c9)
| ~ p8(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_639,c_833]) ).
tcf(c_4475,plain,
! [X0: $i,X1: $i] :
( p8(f4(X1,X0),c17)
| ~ p8(iPr_def_14,iPr_def_12)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_833]) ).
tcf(c_4476,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_14,c17)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p8(f4(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_688,c_833]) ).
tcf(c_4477,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c17)
| ~ p8(iPr_def_11,iPr_def_12)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_833]) ).
tcf(c_4478,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c17)
| ~ p8(iPr_def_12,iPr_def_12)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_833]) ).
tcf(c_4479,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_11,c17)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p8(f5(X0,X1),iPr_def_12) ),
inference(superposition,[status(thm)],[c_710,c_833]) ).
tcf(c_4480,plain,
( p8(iPr_def_11,c17)
| ~ p8(c18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1101,c_833]) ).
tcf(c_4481,plain,
( p8(iPr_def_12,c17)
| ~ p8(c17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1133,c_833]) ).
tcf(c_4482,plain,
( p8(iPr_def_13,c17)
| ~ p8(c16,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1153,c_833]) ).
tcf(c_4483,plain,
( p8(iPr_def_14,c17)
| ~ p8(c17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1184,c_833]) ).
tcf(c_4484,plain,
( p8(iPr_def_15,c17)
| ~ p8(c18,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1204,c_833]) ).
tcf(c_4485,plain,
( p8(iPr_def_16,c17)
| ~ p8(c15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1235,c_833]) ).
tcf(c_4486,plain,
( p8(iPr_def_15,c17)
| ~ p8(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1279,c_833]) ).
tcf(c_4487,plain,
( p8(iPr_def_14,c17)
| ~ p8(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1297,c_833]) ).
tcf(c_4488,plain,
( p8(iPr_def_12,c17)
| ~ p8(iPr_def_14,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1309,c_833]) ).
tcf(c_4489,plain,
( p8(iPr_def_11,c17)
| ~ p8(iPr_def_15,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1385,c_833]) ).
tcf(c_4490,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c17)
| ~ p2(X1,X0)
| ~ p8(f6(X0),iPr_def_12) ),
inference(superposition,[status(thm)],[c_1587,c_833]) ).
tcf(c_4745,plain,
! [X0: $i] :
( p8(X0,c16)
| ~ p8(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_245,c_834]) ).
tcf(c_4746,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c16)
| ~ p2(X0,X1)
| ~ p8(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_233,c_834]) ).
tcf(c_4747,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f3(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f3(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_229,c_834]) ).
tcf(c_4748,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f5(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f5(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_228,c_834]) ).
tcf(c_4749,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p8(f4(X2,X3),c16)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p8(f4(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_227,c_834]) ).
tcf(c_4750,plain,
( p8(c18,c16)
| ~ p8(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_234,c_834]) ).
tcf(c_4751,plain,
( p8(c17,c16)
| ~ p8(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_235,c_834]) ).
tcf(c_4752,plain,
( p8(c16,c16)
| ~ p8(iPr_def_13,iPr_def_13) ),
inference(superposition,[status(thm)],[c_236,c_834]) ).
tcf(c_4753,plain,
( p8(c17,c16)
| ~ p8(iPr_def_14,iPr_def_13) ),
inference(superposition,[status(thm)],[c_237,c_834]) ).
tcf(c_4754,plain,
( p8(c18,c16)
| ~ p8(iPr_def_15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_238,c_834]) ).
tcf(c_4755,plain,
( p8(c15,c16)
| ~ p8(iPr_def_16,iPr_def_13) ),
inference(superposition,[status(thm)],[c_239,c_834]) ).
tcf(c_4756,plain,
! [X0: $i] :
( p8(f6(X0),c16)
| ~ p8(iPr_def_10,iPr_def_13)
| ~ p2(X0,c9) ),
inference(superposition,[status(thm)],[c_1615,c_834]) ).
tcf(c_4757,plain,
! [X0: $i] :
( p8(f6(X0),c16)
| ~ p8(iPr_def_10,iPr_def_13)
| ~ p2(c9,X0) ),
inference(superposition,[status(thm)],[c_638,c_834]) ).
tcf(c_4758,plain,
! [X0: $i] :
( p8(iPr_def_10,c16)
| ~ p2(c9,X0)
| ~ p8(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1616,c_834]) ).
tcf(c_4759,plain,
! [X0: $i] :
( p8(iPr_def_10,c16)
| ~ p2(X0,c9)
| ~ p8(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_639,c_834]) ).
tcf(c_4760,plain,
! [X0: $i,X1: $i] :
( p8(f4(X1,X0),c16)
| ~ p8(iPr_def_14,iPr_def_13)
| ~ p2(c15,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_687,c_834]) ).
tcf(c_4761,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_14,c16)
| ~ p2(X1,c14)
| ~ p2(X0,c15)
| ~ p8(f4(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_688,c_834]) ).
tcf(c_4762,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c16)
| ~ p8(iPr_def_11,iPr_def_13)
| ~ p2(iPr_def_10,X1)
| ~ p2(c20,X0) ),
inference(superposition,[status(thm)],[c_708,c_834]) ).
tcf(c_4763,plain,
! [X0: $i,X1: $i] :
( p8(f5(X1,X0),c16)
| ~ p8(iPr_def_12,iPr_def_13)
| ~ p2(iPr_def_10,X1)
| ~ p2(c19,X0) ),
inference(superposition,[status(thm)],[c_709,c_834]) ).
tcf(c_4764,plain,
! [X0: $i,X1: $i] :
( p8(iPr_def_11,c16)
| ~ p2(X1,c20)
| ~ p2(X0,iPr_def_10)
| ~ p8(f5(X0,X1),iPr_def_13) ),
inference(superposition,[status(thm)],[c_710,c_834]) ).
tcf(c_4765,plain,
( p8(iPr_def_11,c16)
| ~ p8(c18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1101,c_834]) ).
tcf(c_4766,plain,
( p8(iPr_def_12,c16)
| ~ p8(c17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1133,c_834]) ).
tcf(c_4767,plain,
( p8(iPr_def_13,c16)
| ~ p8(c16,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1153,c_834]) ).
tcf(c_4768,plain,
( p8(iPr_def_14,c16)
| ~ p8(c17,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1184,c_834]) ).
tcf(c_4769,plain,
( p8(iPr_def_15,c16)
| ~ p8(c18,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1204,c_834]) ).
tcf(c_4770,plain,
( p8(iPr_def_16,c16)
| ~ p8(c15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1235,c_834]) ).
tcf(c_4771,plain,
( p8(iPr_def_15,c16)
| ~ p8(iPr_def_11,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1279,c_834]) ).
tcf(c_4772,plain,
( p8(iPr_def_14,c16)
| ~ p8(iPr_def_12,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1297,c_834]) ).
tcf(c_4773,plain,
( p8(iPr_def_12,c16)
| ~ p8(iPr_def_14,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1309,c_834]) ).
tcf(c_4774,plain,
( p8(iPr_def_11,c16)
| ~ p8(iPr_def_15,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1385,c_834]) ).
tcf(c_4775,plain,
! [X0: $i,X1: $i] :
( p8(f6(X1),c16)
| ~ p2(X1,X0)
| ~ p8(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1587,c_834]) ).
tcf(c_5069,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_4775,c_4774,c_4773,c_4772,c_4771,c_4770,c_4769,c_4768,c_4767,c_4766,c_4765,c_4764,c_4763,c_4762,c_4761,c_4760,c_4759,c_4758,c_4757,c_4756,c_4755,c_4754,c_4753,c_4752,c_4751,c_4750,c_4749,c_4748,c_4747,c_4746,c_4745,c_4490,c_4489,c_4488,c_4487,c_4486,c_4485,c_4484,c_4483,c_4482,c_4481,c_4480,c_4479,c_4478,c_4477,c_4476,c_4475,c_4474,c_4473,c_4472,c_4471,c_4470,c_4469,c_4468,c_4467,c_4466,c_4465,c_4464,c_4463,c_4462,c_4461,c_4460,c_4330,c_4329,c_4328,c_4327,c_4326,c_4325,c_4324,c_4323,c_4322,c_4321,c_4320,c_4319,c_4071,c_4070,c_4069,c_4068,c_4067,c_4066,c_4065,c_4064,c_4063,c_4062,c_4061,c_4060,c_4059,c_4058,c_4057,c_4056,c_4055,c_4054,c_4053,c_4052,c_4051,c_4050,c_4049,c_4048,c_4047,c_4046,c_4045,c_4044,c_4043,c_4042,c_3886,c_3885,c_3884,c_3883,c_3882,c_3881,c_3880,c_3879,c_3878,c_3877,c_3876,c_3875,c_3874,c_3873,c_3872,c_3871,c_3691,c_3690,c_3689,c_3688,c_3687,c_3686,c_3685,c_3684,c_3683,c_3682,c_3681,c_3680,c_3679,c_3678,c_3677,c_3676,c_3675,c_3674,c_3673,c_3672,c_3671,c_3670,c_3669,c_3668,c_3667,c_3666,c_3665,c_3664,c_3429,c_3428,c_3427,c_3426,c_3425,c_3424,c_3423,c_3422,c_3421,c_3420,c_3419,c_3418,c_3417,c_3416,c_3415,c_3414,c_3413,c_3412,c_3411,c_3410,c_3409,c_3408,c_3407,c_3406,c_3405,c_3404,c_3403,c_3402,c_3401,c_3252,c_3251,c_3250,c_3249,c_3248,c_3247,c_3246,c_3245,c_3244,c_3243,c_3242,c_3241,c_3240,c_3239,c_2989,c_2988,c_2987,c_2986,c_2985,c_2984,c_2983,c_2982,c_2981,c_2980,c_2979,c_2978,c_2977,c_2976,c_2975,c_2974,c_2973,c_2972,c_2971,c_2970,c_2969,c_2968,c_2967,c_2966,c_2965,c_2964,c_2963,c_2962,c_2889,c_2888,c_2887,c_2886,c_2695,c_2694,c_2693,c_2692,c_2691,c_2690,c_2689,c_2688,c_2687,c_2686,c_2685,c_2684,c_2683,c_2682,c_2681,c_2680,c_2679,c_2678,c_2677,c_2676,c_2675,c_2674,c_2673,c_2672,c_2671,c_2670,c_2669,c_2668,c_2426,c_2425,c_2424,c_2423,c_2422,c_2421,c_2420,c_2419,c_2418,c_2417,c_2416,c_2415,c_2414,c_2413,c_2412,c_2411,c_2410,c_2409,c_2408,c_2407,c_2406,c_2405,c_2404,c_2403,c_2402,c_2401,c_2400,c_2399,c_2341,c_2340,c_2339,c_2338,c_2337,c_2336,c_2335,c_2333,c_2178,c_2177,c_2176,c_2175,c_2174,c_2173,c_2172,c_2171,c_2170,c_2169,c_2168,c_2167,c_2166,c_2165,c_2164,c_2163,c_2162,c_2161,c_2160,c_2159,c_2158,c_2157,c_2156,c_2155,c_2154,c_2153,c_2152,c_2104,c_2103,c_2102,c_2101,c_2100,c_2099,c_2003,c_2002,c_2001,c_2000,c_1999,c_1929,c_1928,c_1927,c_1926,c_1925,c_1924,c_1923,c_1922,c_1921,c_1920,c_1736,c_1735,c_1734,c_1733,c_1732,c_1731,c_1730,c_1729,c_1728,c_1727,c_1726,c_1725,c_1724,c_1723,c_1722,c_1721,c_1720,c_1719,c_1718,c_1717,c_1716,c_1715,c_1714,c_1713,c_1670,c_1669,c_1668,c_1667,c_1621,c_1620,c_1619,c_1618,c_1617,c_1616,c_1615,c_1589,c_1588,c_1587,c_1470,c_1469,c_1468,c_1467,c_1466,c_1465,c_1464,c_1463,c_1462,c_1461,c_1460,c_1459,c_1458,c_1457,c_1456,c_1455,c_1454,c_1453,c_1452,c_1451,c_1450,c_1421,c_1386,c_1385,c_1351,c_1350,c_1349,c_1336,c_1335,c_1334,c_1313,c_1312,c_1311,c_1310,c_1309,c_1303,c_1297,c_1296,c_1279,c_1278,c_1258,c_1257,c_1256,c_1239,c_1238,c_1237,c_1235,c_1208,c_1207,c_1206,c_1204,c_1188,c_1187,c_1186,c_1184,c_1168,c_1167,c_1166,c_1154,c_1153,c_1137,c_1136,c_1135,c_1134,c_1133,c_1105,c_1104,c_1103,c_1102,c_1101,c_1081,c_1080,c_1059,c_1058,c_1057,c_1027,c_1026,c_1005,c_1004,c_1003,c_968,c_967,c_948,c_947,c_946,c_927,c_926,c_925,c_924,c_913,c_912,c_907,c_906,c_905,c_1236,c_837,c_836,c_835,c_834,c_833,c_832,c_831,c_830,c_829,c_828,c_827,c_772,c_771,c_770,c_769,c_768,c_767,c_766,c_765,c_764,c_763,c_762,c_741,c_740,c_739,c_712,c_711,c_710,c_709,c_708,c_689,c_688,c_687,c_659,c_658,c_657,c_656,c_655,c_654,c_653,c_639,c_638,c_239,c_238,c_237,c_236,c_235,c_234,c_223,c_222,c_221,c_220,c_219,c_218,c_217,c_224,c_225,c_226,c_227,c_228,c_229,c_230,c_231,c_232,c_233,c_240,c_241,c_242,c_243,c_244,c_245]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN577-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.59 % Computer : n018.cluster.edu
% 0.10/0.59 % Model : x86_64 x86_64
% 0.10/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.59 % Memory : 8046.5625MB
% 0.10/0.59 % OS : Linux 6.8.0-71-generic
% 0.10/0.59 % CPULimit : 300
% 0.10/0.59 % WCLimit : 300
% 0.10/0.59 % DateTime : Fri Sep 25 01:48:51 UTC 2026
% 0.10/0.60 % CPUTime :
% 0.10/0.60 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.15/0.64 Running first-order theorem proving
% 0.15/0.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.15/0.65
% 0.15/0.65 % ======== iProver multi-core TPTP/SMT =========
% 0.15/0.65
% 0.15/0.65 % Detected problem language: tptp
% 0.15/0.66 % Proving...
% 4.39/1.54 % SZS status Started for theBenchmark.p
% 4.39/1.54 % SZS status Unsatisfiable for theBenchmark.p
% 4.39/1.54
% 4.39/1.54 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.39/1.54
% 4.39/1.54 % ------ iProver source info
% 4.39/1.54
% 4.39/1.54 % git: date: 2026-07-19 20:42:38 +0200
% 4.39/1.54 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.39/1.54 % git: non_committed_changes: false
% 4.39/1.54
% 4.39/1.54 % ------ Parsing...% successful
% 4.39/1.54
% 4.39/1.54
% 4.39/1.54 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.39/1.54
% 4.39/1.54 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 4.39/1.54
% 4.39/1.54 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 4.39/1.54
% 4.39/1.54 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 4.39/1.54 % ------ Proving...
% 4.39/1.54 % ------ Problem Properties
% 4.39/1.54
% 4.39/1.54 %
% 4.39/1.54 % clauses 29
% 4.39/1.54 % conjectures 22
% 4.39/1.54 % EPR 15
% 4.39/1.54 % Horn 29
% 4.39/1.54 % unary 19
% 4.39/1.54 % binary 1
% 4.39/1.54 % lits 66
% 4.39/1.54 % lits eq 7
% 4.39/1.54 % fd_pure 0
% 4.39/1.54 % fd_pseudo 0
% 4.39/1.54 % fd_cond 0
% 4.39/1.54 % fd_pseudo_cond 0
% 4.39/1.54 % AC symbols 0
% 4.39/1.54
% 4.39/1.54 % ------ Schedule dynamic 5 is on
% 4.39/1.54
% 4.39/1.54 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 4.39/1.54
% 4.39/1.54
% 4.39/1.54 % ------
% 4.39/1.54 % Current options:
% 4.39/1.54 % ------
% 4.39/1.54
% 4.39/1.54
% 4.39/1.54 %
% 4.39/1.54
% 4.39/1.54 % ------ Proving...
% 4.39/1.54 %
% 4.39/1.54
% 4.39/1.54 % SZS status Unsatisfiable for theBenchmark.p
% 4.39/1.54
% 4.39/1.54 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.39/1.55
% 4.39/1.55
%------------------------------------------------------------------------------