%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : SYN568-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 : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:41:06 PM UTC 2026
% Result : Unsatisfiable 2.44s 1.28s
% Output : CNFRefutation 2.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 29
% Syntax : Number of formulae : 677 ( 37 unt; 9 def)
% Number of atoms : 3422 ( 9 equ)
% Maximal formula atoms : 5 ( 5 avg)
% Number of connectives : 2875 (1434 ~;1441 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 15 ( 13 usr; 10 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 3 con; 0-2 aty)
% Number of variables : 1178 ( 0 sgn1178 !; 0 ?;1137 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [X0] : p2(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_1) ).
fof(f2,negated_conjecture,
! [X0] : p3(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_2) ).
fof(f3,negated_conjecture,
~ p11(f9(c13),f9(c14)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p11_3) ).
fof(f4,negated_conjecture,
! [X0] : p11(f5(f6(c12)),f9(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_4) ).
fof(f5,negated_conjecture,
! [X0,X1] :
( p11(X1,X0)
| p10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_5) ).
fof(f6,negated_conjecture,
! [X0,X1] :
( ~ p11(X1,X0)
| ~ p10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p10_6) ).
fof(f7,negated_conjecture,
~ p3(f6(f7(f8(c12))),f6(c12)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p3_7) ).
fof(f8,negated_conjecture,
! [X0,X1] :
( ~ p3(X0,X1)
| p3(f8(X0),f8(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_8) ).
fof(f9,negated_conjecture,
! [X0,X1] :
( ~ p3(X0,X1)
| p2(f5(X0),f5(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_9) ).
fof(f10,negated_conjecture,
! [X0,X1] :
( ~ p2(X0,X1)
| p2(f9(X0),f9(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_10) ).
fof(f11,negated_conjecture,
! [X0,X1] :
( ~ p3(X0,X1)
| p3(f6(X0),f6(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_11) ).
fof(f12,negated_conjecture,
! [X0,X1] :
( ~ p3(X0,X1)
| p3(f7(X0),f7(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_12) ).
fof(f13,negated_conjecture,
! [X2,X0,X1] :
( ~ p2(X2,X1)
| ~ p2(X2,X0)
| p2(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_13) ).
fof(f14,negated_conjecture,
! [X2,X0,X1] :
( ~ p3(X2,X1)
| ~ p3(X2,X0)
| p3(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_14) ).
fof(f15,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p10(X2,X3)
| ~ p2(X3,X1)
| ~ p2(X2,X0)
| p10(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p10_15) ).
fof(f16,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p11(X2,X3)
| ~ p2(X3,X1)
| ~ p2(X2,X0)
| p11(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_16) ).
fof(f17,negated_conjecture,
! [X2,X3,X0,X1] :
( ~ p3(X1,X3)
| ~ p2(X0,X2)
| p2(f4(X0,X1),f4(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p2_17) ).
fof(f18,negated_conjecture,
p11(f4(f9(c13),f6(f7(f8(c12)))),f4(f9(c14),f6(f7(f8(c12))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_18) ).
fof(f19,negated_conjecture,
! [X2,X0,X1] :
( ~ p11(f5(f6(c12)),X0)
| ~ p11(X0,X2)
| p11(f4(X0,X1),f4(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p11_19) ).
fof(f20,negated_conjecture,
! [X2,X0,X1] :
( ~ p11(f5(f6(c12)),X1)
| ~ p10(X1,X2)
| p10(f4(X1,X0),f4(X2,X0))
| p3(X0,f6(c12)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_20) ).
tcf(c_69,negated_conjecture,
! [X0: $i] : p2(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_70,negated_conjecture,
! [X0: $i] : p3(X0,X0),
inference(cnf_transformation,[],[f2]) ).
tcf(c_71,negated_conjecture,
~ p11(f9(c13),f9(c14)),
inference(cnf_transformation,[],[f3]) ).
tcf(c_72,negated_conjecture,
! [X0: $i] : p11(f5(f6(c12)),f9(X0)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_73,negated_conjecture,
! [X0: $i,X1: $i] :
( p10(X1,X0)
| p11(X0,X1) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_74,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ p10(X1,X0)
| ~ p11(X0,X1) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_75,negated_conjecture,
~ p3(f6(f7(f8(c12))),f6(c12)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_76,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f8(X0),f8(X1))
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_77,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f5(X0),f5(X1))
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_78,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f9(X0),f9(X1))
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_79,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f6(X0),f6(X1))
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_80,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f7(X0),f7(X1))
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_81,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X1,X2)
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_82,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p3(X1,X2)
| ~ p3(X0,X2)
| ~ p3(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X1,X3)
| ~ p10(X0,X2)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_84,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X1,X3)
| ~ p11(X0,X2)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_85,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X0,X2),f4(X1,X3))
| ~ p3(X2,X3)
| ~ p2(X0,X1) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_86,negated_conjecture,
p11(f4(f9(c13),f6(f7(f8(c12)))),f4(f9(c14),f6(f7(f8(c12))))),
inference(cnf_transformation,[],[f18]) ).
tcf(c_87,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p11(f4(X0,X2),f4(X1,X2))
| ~ p11(X0,X1)
| ~ p11(f5(f6(c12)),X0) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_88,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,f6(c12))
| p10(f4(X0,X2),f4(X1,X2))
| ~ p10(X0,X1)
| ~ p11(f5(f6(c12)),X0) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i] :
( p11(X0,X1)
| p10(X1,X0) ),
inference(prop_impl_just,[status(thm)],[c_73]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] :
( p10(X1,X0)
| p11(X0,X1) ),
inference(renaming,[status(thm)],[c_104]) ).
tcf(c_161,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p10(X2,X0)
| p11(f4(X0,X1),f4(X2,X1))
| ~ p11(f5(f6(c12)),X0) ),
inference(bin_hyper_res,[status(thm)],[c_87,c_105]) ).
tcf(c_251,definition,
iPr_def_10 = f6(c12),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_252,definition,
iPr_def_11 = f5(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_253,definition,
iPr_def_12 = f9(c13),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_254,definition,
iPr_def_13 = f8(c12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_255,definition,
iPr_def_14 = f7(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_256,definition,
iPr_def_15 = f6(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_257,definition,
iPr_def_16 = f4(iPr_def_12,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_258,definition,
iPr_def_17 = f9(c14),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_259,definition,
iPr_def_18 = f4(iPr_def_17,iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_260,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p10(X2,X0)
| p11(f4(X0,X1),f4(X2,X1))
| ~ p11(iPr_def_11,X0) ),
inference(demodulation,[status(thm)],[c_161,c_251,c_252]) ).
tcf(c_261,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,iPr_def_10)
| p10(f4(X0,X2),f4(X1,X2))
| ~ p11(iPr_def_11,X0)
| ~ p10(X0,X1) ),
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_262,negated_conjecture,
p11(iPr_def_16,iPr_def_18),
inference(demodulation,[status(thm)],[c_86,c_258,c_259,c_254,c_255,c_256,c_253,c_257]) ).
tcf(c_263,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(f4(X0,X2),f4(X1,X3))
| ~ p3(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_85]) ).
tcf(c_264,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X1,X3)
| ~ p11(X0,X2)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_265,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X1,X3)
| ~ p10(X0,X2)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_266,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p3(X1,X2)
| ~ p3(X0,X2)
| ~ p3(X0,X1) ),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_267,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p2(X1,X2)
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_81]) ).
tcf(c_268,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f7(X0),f7(X1))
| ~ p3(X0,X1) ),
inference(demodulation,[status(thm)],[c_80]) ).
tcf(c_269,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f6(X0),f6(X1))
| ~ p3(X0,X1) ),
inference(demodulation,[status(thm)],[c_79]) ).
tcf(c_270,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f9(X0),f9(X1))
| ~ p2(X0,X1) ),
inference(demodulation,[status(thm)],[c_78]) ).
tcf(c_271,negated_conjecture,
! [X0: $i,X1: $i] :
( p2(f5(X0),f5(X1))
| ~ p3(X0,X1) ),
inference(demodulation,[status(thm)],[c_77]) ).
tcf(c_272,negated_conjecture,
! [X0: $i,X1: $i] :
( p3(f8(X0),f8(X1))
| ~ p3(X0,X1) ),
inference(demodulation,[status(thm)],[c_76]) ).
tcf(c_273,negated_conjecture,
~ p3(iPr_def_15,iPr_def_10),
inference(demodulation,[status(thm)],[c_75]) ).
tcf(c_274,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ p10(X1,X0)
| ~ p11(X0,X1) ),
inference(demodulation,[status(thm)],[c_74]) ).
tcf(c_275,negated_conjecture,
! [X0: $i,X1: $i] :
( p10(X1,X0)
| p11(X0,X1) ),
inference(demodulation,[status(thm)],[c_73]) ).
tcf(c_276,negated_conjecture,
! [X0: $i] : p11(iPr_def_11,f9(X0)),
inference(demodulation,[status(thm)],[c_72]) ).
tcf(c_277,negated_conjecture,
~ p11(iPr_def_12,iPr_def_17),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_278,negated_conjecture,
! [X0: $i] : p3(X0,X0),
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_279,negated_conjecture,
! [X0: $i] : p2(X0,X0),
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_873,plain,
~ p10(iPr_def_18,iPr_def_16),
inference(superposition,[status(thm)],[c_262,c_274]) ).
tcf(c_874,plain,
! [X0: $i] : ~ p10(f9(X0),iPr_def_11),
inference(superposition,[status(thm)],[c_276,c_274]) ).
tcf(c_884,plain,
p11(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_253,c_276]) ).
tcf(c_885,plain,
~ p10(iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_884,c_274]) ).
tcf(c_892,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(X0))
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_255,c_268]) ).
tcf(c_893,plain,
! [X0: $i] :
( p3(f7(X0),iPr_def_14)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_255,c_268]) ).
tcf(c_904,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(X0))
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_251,c_269]) ).
tcf(c_905,plain,
! [X0: $i] :
( p3(f6(X0),iPr_def_10)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_251,c_269]) ).
tcf(c_916,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_253,c_270]) ).
tcf(c_917,plain,
! [X0: $i] :
( p2(f9(X0),iPr_def_12)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_253,c_270]) ).
tcf(c_928,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(X0))
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_252,c_271]) ).
tcf(c_929,plain,
! [X0: $i] :
( p2(f5(X0),iPr_def_11)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_252,c_271]) ).
tcf(c_940,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(X0))
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_254,c_272]) ).
tcf(c_941,plain,
! [X0: $i] :
( p3(f8(X0),iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_254,c_272]) ).
tcf(c_955,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(f8(X2),X1)
| ~ p3(X0,X2)
| ~ p3(f8(X0),X1) ),
inference(superposition,[status(thm)],[c_272,c_266]) ).
tcf(c_956,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(f6(X2),X1)
| ~ p3(X0,X2)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_269,c_266]) ).
tcf(c_957,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(f7(X2),X1)
| ~ p3(X0,X2)
| ~ p3(f7(X0),X1) ),
inference(superposition,[status(thm)],[c_268,c_266]) ).
tcf(c_974,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f5(X2),X1)
| ~ p3(X0,X2)
| ~ p2(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_271,c_267]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X2),X1)
| ~ p2(X0,X2)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_270,c_267]) ).
tcf(c_988,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p11(iPr_def_11,X2)
| ~ p10(f4(X0,X1),f4(X2,X1)) ),
inference(superposition,[status(thm)],[c_260,c_274]) ).
tcf(c_997,plain,
( p2(iPr_def_12,iPr_def_12)
| ~ p2(c13,c13) ),
inference(superposition,[status(thm)],[c_253,c_916]) ).
tcf(c_998,plain,
! [X0: $i,X1: $i] :
( p2(f9(X0),X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_267]) ).
tcf(c_1003,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(X0))
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_256,c_269]) ).
tcf(c_1004,plain,
! [X0: $i] :
( p3(f6(X0),iPr_def_15)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_256,c_269]) ).
tcf(c_1011,plain,
( p2(iPr_def_12,iPr_def_17)
| ~ p2(c13,c14) ),
inference(superposition,[status(thm)],[c_258,c_916]) ).
tcf(c_1012,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_258,c_270]) ).
tcf(c_1013,plain,
p11(iPr_def_11,iPr_def_17),
inference(superposition,[status(thm)],[c_258,c_276]) ).
tcf(c_1014,plain,
! [X0: $i] :
( p2(f9(X0),iPr_def_17)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_258,c_270]) ).
tcf(c_1023,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_10)
| p10(iPr_def_16,f4(X0,iPr_def_15))
| ~ p11(iPr_def_11,iPr_def_12)
| ~ p10(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_257,c_261]) ).
tcf(c_1024,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_10)
| p10(f4(X0,iPr_def_15),iPr_def_16)
| ~ p10(X0,iPr_def_12)
| ~ p11(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_257,c_261]) ).
tcf(c_1025,plain,
! [X0: $i] :
( p10(X0,iPr_def_12)
| p11(iPr_def_16,f4(X0,iPr_def_15))
| ~ p11(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_257,c_260]) ).
tcf(c_1026,plain,
! [X0: $i] :
( p10(iPr_def_12,X0)
| p11(f4(X0,iPr_def_15),iPr_def_16)
| ~ p11(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_257,c_260]) ).
tcf(c_1030,plain,
! [X0: $i] :
( p10(X0,iPr_def_12)
| p11(iPr_def_16,f4(X0,iPr_def_15)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1025,c_884]) ).
tcf(c_1033,plain,
! [X0: $i] :
( p10(f4(X0,iPr_def_15),iPr_def_16)
| ~ p10(X0,iPr_def_12)
| ~ p11(iPr_def_11,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1024,c_273]) ).
tcf(c_1037,plain,
! [X0: $i] :
( p10(iPr_def_16,f4(X0,iPr_def_15))
| ~ p10(iPr_def_12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1023,c_273,c_884]) ).
tcf(c_1044,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_10)
| p10(iPr_def_18,f4(X0,iPr_def_15))
| ~ p11(iPr_def_11,iPr_def_17)
| ~ p10(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_259,c_261]) ).
tcf(c_1045,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_10)
| p10(f4(X0,iPr_def_15),iPr_def_18)
| ~ p10(X0,iPr_def_17)
| ~ p11(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_259,c_261]) ).
tcf(c_1046,plain,
! [X0: $i] :
( p10(X0,iPr_def_17)
| p11(iPr_def_18,f4(X0,iPr_def_15))
| ~ p11(iPr_def_11,iPr_def_17) ),
inference(superposition,[status(thm)],[c_259,c_260]) ).
tcf(c_1047,plain,
! [X0: $i] :
( p10(iPr_def_17,X0)
| p11(f4(X0,iPr_def_15),iPr_def_18)
| ~ p11(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_259,c_260]) ).
tcf(c_1054,plain,
! [X0: $i] :
( p10(f4(X0,iPr_def_15),iPr_def_18)
| ~ p10(X0,iPr_def_17)
| ~ p11(iPr_def_11,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1045,c_273]) ).
tcf(c_1058,plain,
! [X0: $i] :
( p10(iPr_def_18,f4(X0,iPr_def_15))
| ~ p11(iPr_def_11,iPr_def_17)
| ~ p10(iPr_def_17,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1044,c_273]) ).
tcf(c_1066,plain,
~ p10(iPr_def_17,iPr_def_11),
inference(superposition,[status(thm)],[c_1013,c_274]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_16,f4(X0,X1))
| ~ p3(iPr_def_15,X1)
| ~ p2(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_257,c_263]) ).
tcf(c_1082,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_18,f4(X0,X1))
| ~ p3(iPr_def_15,X1)
| ~ p2(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_259,c_263]) ).
tcf(c_1083,plain,
! [X0: $i,X1: $i] :
( p2(f4(X0,X1),iPr_def_16)
| ~ p3(X1,iPr_def_15)
| ~ p2(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_257,c_263]) ).
tcf(c_1084,plain,
! [X0: $i,X1: $i] :
( p2(f4(X0,X1),iPr_def_18)
| ~ p3(X1,iPr_def_15)
| ~ p2(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_259,c_263]) ).
tcf(c_1085,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p2(f4(X3,X4),X2)
| ~ p3(X1,X4)
| ~ p2(X0,X3)
| ~ p2(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_263,c_267]) ).
tcf(c_1115,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X2,X1)
| ~ p11(X2,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_279,c_264]) ).
tcf(c_1116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(f5(X3),X2)
| ~ p3(X0,X3)
| ~ p2(X1,X2)
| ~ p11(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_271,c_264]) ).
tcf(c_1117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(f9(X2),X3)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_270,c_264]) ).
tcf(c_1118,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p11(f4(X3,X5),X4)
| ~ p3(X1,X5)
| ~ p2(X2,X4)
| ~ p2(X0,X3)
| ~ p11(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_263,c_264]) ).
tcf(c_1119,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),X1)
| ~ p11(iPr_def_12,X0)
| ~ p2(c13,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_916,c_264]) ).
tcf(c_1141,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_10)
| ~ p3(X0,iPr_def_15)
| ~ p3(X0,iPr_def_10) ),
inference(instantiation,[status(thm)],[c_266]) ).
tcf(c_1155,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X2,X1)
| ~ p10(X2,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_279,c_265]) ).
tcf(c_1156,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(f5(X3),X2)
| ~ p3(X0,X3)
| ~ p2(X1,X2)
| ~ p10(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_271,c_265]) ).
tcf(c_1157,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(f9(X2),X3)
| ~ p2(X1,X3)
| ~ p2(X0,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_270,c_265]) ).
tcf(c_1158,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p10(f4(X3,X5),X4)
| ~ p3(X1,X5)
| ~ p2(X2,X4)
| ~ p2(X0,X3)
| ~ p10(f4(X0,X1),X2) ),
inference(superposition,[status(thm)],[c_263,c_265]) ).
tcf(c_1159,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),X1)
| ~ p10(iPr_def_12,X0)
| ~ p2(c13,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_916,c_265]) ).
tcf(c_1194,plain,
( p3(iPr_def_14,iPr_def_14)
| ~ p3(iPr_def_13,iPr_def_13) ),
inference(superposition,[status(thm)],[c_255,c_892]) ).
tcf(c_1195,plain,
! [X0: $i,X1: $i] :
( p3(f7(X0),X1)
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_892,c_266]) ).
tcf(c_1209,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),X1) ),
inference(superposition,[status(thm)],[c_893,c_266]) ).
tcf(c_1218,plain,
( p3(iPr_def_10,iPr_def_10)
| ~ p3(c12,c12) ),
inference(superposition,[status(thm)],[c_251,c_904]) ).
tcf(c_1219,plain,
( p3(iPr_def_10,iPr_def_15)
| ~ p3(c12,iPr_def_14) ),
inference(superposition,[status(thm)],[c_256,c_904]) ).
tcf(c_1220,plain,
! [X0: $i,X1: $i] :
( p3(f6(X0),X1)
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_266]) ).
tcf(c_1232,plain,
( p3(iPr_def_15,iPr_def_10)
| ~ p3(iPr_def_14,c12) ),
inference(superposition,[status(thm)],[c_256,c_905]) ).
tcf(c_1233,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_905,c_266]) ).
tcf(c_1234,plain,
~ p3(iPr_def_14,c12),
inference(forward_subsumption_resolution,[status(thm)],[c_1232,c_273]) ).
tcf(c_1244,plain,
( p3(iPr_def_15,iPr_def_10)
| ~ p3(iPr_def_10,iPr_def_15)
| ~ p3(iPr_def_10,iPr_def_10) ),
inference(instantiation,[status(thm)],[c_1141]) ).
tcf(c_1245,plain,
p3(iPr_def_10,iPr_def_10),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_1254,plain,
( p2(iPr_def_17,iPr_def_12)
| ~ p2(c14,c13) ),
inference(superposition,[status(thm)],[c_258,c_917]) ).
tcf(c_1255,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_12,X2)
| ~ p2(X0,c13)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_917,c_265]) ).
tcf(c_1256,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(iPr_def_12,X2)
| ~ p2(X0,c13)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_917,c_264]) ).
tcf(c_1257,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(X0,c13)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_917,c_267]) ).
tcf(c_1274,plain,
~ p3(c12,iPr_def_14),
inference(global_subsumption_just,[status(thm)],[c_1219,c_273,c_1219,c_1244,c_1245]) ).
tcf(c_1284,plain,
( p2(iPr_def_11,iPr_def_11)
| ~ p3(iPr_def_10,iPr_def_10) ),
inference(superposition,[status(thm)],[c_252,c_928]) ).
tcf(c_1285,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f5(X2),X1)
| ~ p10(iPr_def_11,X0)
| ~ p3(iPr_def_10,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_928,c_265]) ).
tcf(c_1286,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f5(X2),X1)
| ~ p11(iPr_def_11,X0)
| ~ p3(iPr_def_10,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_928,c_264]) ).
tcf(c_1287,plain,
! [X0: $i,X1: $i] :
( p2(f5(X1),X0)
| ~ p3(iPr_def_10,X1)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_928,c_267]) ).
tcf(c_1307,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_11,X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(X1,X2)
| ~ p10(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_929,c_265]) ).
tcf(c_1308,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(iPr_def_11,X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(X1,X2)
| ~ p11(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_929,c_264]) ).
tcf(c_1309,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,X1)
| ~ p3(X0,iPr_def_10)
| ~ p2(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_929,c_267]) ).
tcf(c_1334,plain,
( p3(iPr_def_13,iPr_def_13)
| ~ p3(c12,c12) ),
inference(superposition,[status(thm)],[c_254,c_940]) ).
tcf(c_1335,plain,
! [X0: $i,X1: $i] :
( p3(f8(X0),X1)
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_266]) ).
tcf(c_1345,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),X1) ),
inference(superposition,[status(thm)],[c_941,c_266]) ).
tcf(c_1361,plain,
( p3(iPr_def_15,iPr_def_15)
| ~ p3(iPr_def_14,iPr_def_14) ),
inference(superposition,[status(thm)],[c_256,c_1003]) ).
tcf(c_1362,plain,
! [X0: $i,X1: $i] :
( p3(f6(X0),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1003,c_266]) ).
tcf(c_1372,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1004,c_266]) ).
tcf(c_1381,plain,
( p2(iPr_def_17,iPr_def_17)
| ~ p2(c14,c14) ),
inference(superposition,[status(thm)],[c_258,c_1012]) ).
tcf(c_1382,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),X1)
| ~ p10(iPr_def_17,X0)
| ~ p2(c14,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1012,c_265]) ).
tcf(c_1383,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),X1)
| ~ p11(iPr_def_17,X0)
| ~ p2(c14,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1012,c_264]) ).
tcf(c_1384,plain,
! [X0: $i,X1: $i] :
( p2(f9(X0),X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_267]) ).
tcf(c_1405,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_17,X2)
| ~ p2(X0,c14)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1014,c_265]) ).
tcf(c_1406,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(iPr_def_17,X2)
| ~ p2(X0,c14)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1014,c_264]) ).
tcf(c_1407,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(X0,c14)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1014,c_267]) ).
tcf(c_1432,plain,
( p10(iPr_def_16,iPr_def_16)
| ~ p10(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_257,c_1037]) ).
tcf(c_1433,plain,
( p10(iPr_def_16,iPr_def_18)
| ~ p10(iPr_def_12,iPr_def_17) ),
inference(superposition,[status(thm)],[c_259,c_1037]) ).
tcf(c_1445,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,f5(X2))
| ~ p3(X1,X2)
| ~ p11(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_271,c_1115]) ).
tcf(c_1446,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,f9(X2))
| ~ p2(X1,X2)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_270,c_1115]) ).
tcf(c_1447,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p11(X0,f4(X3,X4))
| ~ p3(X2,X4)
| ~ p2(X1,X3)
| ~ p11(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_263,c_1115]) ).
tcf(c_1448,plain,
! [X0: $i,X1: $i] :
( p11(X1,f9(X0))
| ~ p11(X1,iPr_def_12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_1115]) ).
tcf(c_1449,plain,
! [X0: $i,X1: $i] :
( p11(X0,iPr_def_12)
| ~ p2(X1,c13)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_917,c_1115]) ).
tcf(c_1450,plain,
! [X0: $i,X1: $i] :
( p11(X1,f5(X0))
| ~ p11(X1,iPr_def_11)
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_928,c_1115]) ).
tcf(c_1451,plain,
! [X0: $i,X1: $i] :
( p11(X0,iPr_def_11)
| ~ p3(X1,iPr_def_10)
| ~ p11(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_929,c_1115]) ).
tcf(c_1452,plain,
! [X0: $i,X1: $i] :
( p11(X1,f9(X0))
| ~ p11(X1,iPr_def_17)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_1115]) ).
tcf(c_1453,plain,
! [X0: $i,X1: $i] :
( p11(X0,iPr_def_17)
| ~ p2(X1,c14)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1014,c_1115]) ).
tcf(c_1511,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,f5(X2))
| ~ p3(X1,X2)
| ~ p10(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_271,c_1155]) ).
tcf(c_1512,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,f9(X2))
| ~ p2(X1,X2)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_270,c_1155]) ).
tcf(c_1513,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p10(X0,f4(X3,X4))
| ~ p3(X2,X4)
| ~ p2(X1,X3)
| ~ p10(X0,f4(X1,X2)) ),
inference(superposition,[status(thm)],[c_263,c_1155]) ).
tcf(c_1514,plain,
! [X0: $i,X1: $i] :
( p10(X1,f9(X0))
| ~ p10(X1,iPr_def_12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_1155]) ).
tcf(c_1515,plain,
! [X0: $i,X1: $i] :
( p10(X0,iPr_def_12)
| ~ p2(X1,c13)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_917,c_1155]) ).
tcf(c_1516,plain,
! [X0: $i,X1: $i] :
( p10(X1,f5(X0))
| ~ p10(X1,iPr_def_11)
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_928,c_1155]) ).
tcf(c_1517,plain,
! [X0: $i,X1: $i] :
( p10(X0,iPr_def_11)
| ~ p3(X1,iPr_def_10)
| ~ p10(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_929,c_1155]) ).
tcf(c_1518,plain,
! [X0: $i,X1: $i] :
( p10(X1,f9(X0))
| ~ p10(X1,iPr_def_17)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_1155]) ).
tcf(c_1519,plain,
! [X0: $i,X1: $i] :
( p10(X0,iPr_def_17)
| ~ p2(X1,c14)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1014,c_1155]) ).
tcf(c_1587,plain,
! [X0: $i] :
( p2(iPr_def_17,X0)
| ~ p2(c13,c14)
| ~ p2(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_258,c_998]) ).
tcf(c_1588,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_998,c_1155]) ).
tcf(c_1589,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_998,c_1115]) ).
tcf(c_1590,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p2(iPr_def_12,X3)
| ~ p2(c13,X0)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_998,c_265]) ).
tcf(c_1591,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p2(iPr_def_12,X3)
| ~ p2(c13,X0)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_998,c_264]) ).
tcf(c_1592,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_998,c_267]) ).
tcf(c_1640,plain,
( p10(iPr_def_12,iPr_def_12)
| p11(iPr_def_16,iPr_def_16)
| ~ p11(iPr_def_11,iPr_def_12) ),
inference(superposition,[status(thm)],[c_257,c_1026]) ).
tcf(c_1641,plain,
( p10(iPr_def_12,iPr_def_17)
| p11(iPr_def_18,iPr_def_16)
| ~ p11(iPr_def_11,iPr_def_17) ),
inference(superposition,[status(thm)],[c_259,c_1026]) ).
tcf(c_1642,plain,
! [X0: $i] :
( p10(iPr_def_12,X0)
| ~ p11(iPr_def_11,X0)
| ~ p10(iPr_def_16,f4(X0,iPr_def_15)) ),
inference(superposition,[status(thm)],[c_1026,c_274]) ).
tcf(c_1643,plain,
( p10(iPr_def_12,iPr_def_17)
| p11(iPr_def_18,iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1641,c_1013]) ).
tcf(c_1646,plain,
( p10(iPr_def_12,iPr_def_12)
| p11(iPr_def_16,iPr_def_16) ),
inference(forward_subsumption_resolution,[status(thm)],[c_1640,c_884]) ).
tcf(c_1669,plain,
! [X0: $i] :
( p10(X0,iPr_def_17)
| p11(iPr_def_18,f4(X0,iPr_def_15)) ),
inference(global_subsumption_just,[status(thm)],[c_1046,c_1013,c_1046]) ).
tcf(c_1677,plain,
( p10(iPr_def_17,iPr_def_17)
| p11(iPr_def_18,iPr_def_18) ),
inference(superposition,[status(thm)],[c_259,c_1669]) ).
tcf(c_1678,plain,
! [X0: $i] :
( p10(X0,iPr_def_17)
| ~ p10(f4(X0,iPr_def_15),iPr_def_18) ),
inference(superposition,[status(thm)],[c_1669,c_274]) ).
tcf(c_1690,plain,
! [X0: $i,X1: $i] :
( p2(f9(X1),f9(X0))
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_279,c_975]) ).
tcf(c_1691,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X2),f9(X1))
| ~ p2(X0,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_270,c_975]) ).
tcf(c_1692,plain,
! [X0: $i,X1: $i] :
( p2(f9(X1),iPr_def_12)
| ~ p2(X0,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_917,c_975]) ).
tcf(c_1693,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_998,c_975]) ).
tcf(c_1694,plain,
! [X0: $i,X1: $i] :
( p2(f9(X1),iPr_def_17)
| ~ p2(X0,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1014,c_975]) ).
tcf(c_1750,plain,
( p10(iPr_def_16,iPr_def_16)
| p11(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_275,c_1432]) ).
tcf(c_1751,plain,
( p10(iPr_def_16,iPr_def_16)
| p11(iPr_def_16,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1646,c_1432]) ).
tcf(c_1765,plain,
( p10(iPr_def_16,iPr_def_18)
| p11(iPr_def_17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_275,c_1433]) ).
tcf(c_1766,plain,
( p10(iPr_def_16,iPr_def_18)
| p11(iPr_def_18,iPr_def_16) ),
inference(superposition,[status(thm)],[c_1643,c_1433]) ).
tcf(c_1785,plain,
( p10(iPr_def_12,iPr_def_17)
| ~ p10(iPr_def_16,iPr_def_18) ),
inference(superposition,[status(thm)],[c_257,c_1678]) ).
tcf(c_1786,plain,
( p10(iPr_def_17,iPr_def_17)
| ~ p10(iPr_def_18,iPr_def_18) ),
inference(superposition,[status(thm)],[c_259,c_1678]) ).
tcf(c_1795,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_253,c_1690]) ).
tcf(c_1796,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_258,c_1690]) ).
tcf(c_1797,plain,
! [X0: $i] :
( p2(f9(X0),iPr_def_12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_253,c_1690]) ).
tcf(c_1798,plain,
! [X0: $i] :
( p2(f9(X0),iPr_def_17)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_258,c_1690]) ).
tcf(c_1799,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,f9(X2))
| ~ p2(X2,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1690,c_1155]) ).
tcf(c_1800,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,f9(X2))
| ~ p2(X2,X1)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1690,c_1115]) ).
tcf(c_1801,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(f9(X2),X3)
| ~ p2(X2,X0)
| ~ p2(X1,X3)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1690,c_265]) ).
tcf(c_1802,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(f9(X2),X3)
| ~ p2(X2,X0)
| ~ p2(X1,X3)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1690,c_264]) ).
tcf(c_1803,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X2),X1)
| ~ p2(X2,X0)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1690,c_267]) ).
tcf(c_1804,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X2),f9(X0))
| ~ p2(X1,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1690,c_975]) ).
tcf(c_1872,plain,
! [X0: $i] :
( p10(iPr_def_17,X0)
| ~ p11(iPr_def_11,X0)
| ~ p10(iPr_def_18,f4(X0,iPr_def_15)) ),
inference(superposition,[status(thm)],[c_1047,c_274]) ).
tcf(c_1884,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_14,X2)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),X1) ),
inference(superposition,[status(thm)],[c_1195,c_266]) ).
tcf(c_1895,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(X0))
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_278,c_1209]) ).
tcf(c_1896,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(X0,iPr_def_13)
| ~ p3(X0,X1) ),
inference(superposition,[status(thm)],[c_268,c_1209]) ).
tcf(c_1897,plain,
! [X0: $i] :
( p3(iPr_def_14,iPr_def_14)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_893,c_1209]) ).
tcf(c_1917,plain,
! [X0: $i,X1: $i] :
( p3(f7(X0),X1)
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1895,c_266]) ).
tcf(c_1929,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_10,X2)
| ~ p3(c12,X0)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1220,c_266]) ).
tcf(c_1950,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(X0))
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_278,c_1233]) ).
tcf(c_1951,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(X0,c12)
| ~ p3(X0,X1) ),
inference(superposition,[status(thm)],[c_269,c_1233]) ).
tcf(c_1952,plain,
! [X0: $i] :
( p3(iPr_def_10,iPr_def_10)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_905,c_1233]) ).
tcf(c_1954,plain,
! [X0: $i] :
( p3(iPr_def_10,iPr_def_15)
| ~ p3(X0,iPr_def_14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1004,c_1233]) ).
tcf(c_1991,plain,
( p10(iPr_def_12,iPr_def_17)
| p11(iPr_def_17,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1765,c_1785]) ).
tcf(c_2005,plain,
! [X0: $i] :
( p10(X0,iPr_def_12)
| ~ p10(f4(X0,iPr_def_15),iPr_def_16) ),
inference(superposition,[status(thm)],[c_1030,c_274]) ).
tcf(c_2014,plain,
( p2(iPr_def_12,iPr_def_17)
| ~ p2(c14,c13) ),
inference(superposition,[status(thm)],[c_258,c_1795]) ).
tcf(c_2015,plain,
! [X0: $i,X1: $i] :
( p10(X1,f9(X0))
| ~ p10(X1,iPr_def_12)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_1155]) ).
tcf(c_2016,plain,
! [X0: $i,X1: $i] :
( p11(X1,f9(X0))
| ~ p11(X1,iPr_def_12)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_1115]) ).
tcf(c_2017,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),X1)
| ~ p10(iPr_def_12,X0)
| ~ p2(X2,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1795,c_265]) ).
tcf(c_2018,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),X1)
| ~ p11(iPr_def_12,X0)
| ~ p2(X2,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1795,c_264]) ).
tcf(c_2019,plain,
! [X0: $i,X1: $i] :
( p2(f9(X0),X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_267]) ).
tcf(c_2085,plain,
( p2(iPr_def_17,iPr_def_12)
| ~ p2(c13,c14) ),
inference(superposition,[status(thm)],[c_253,c_1796]) ).
tcf(c_2087,plain,
! [X0: $i,X1: $i] :
( p10(X1,f9(X0))
| ~ p10(X1,iPr_def_17)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_1155]) ).
tcf(c_2088,plain,
! [X0: $i,X1: $i] :
( p11(X1,f9(X0))
| ~ p11(X1,iPr_def_17)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_1115]) ).
tcf(c_2089,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),X1)
| ~ p10(iPr_def_17,X0)
| ~ p2(X2,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1796,c_265]) ).
tcf(c_2090,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),X1)
| ~ p11(iPr_def_17,X0)
| ~ p2(X2,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1796,c_264]) ).
tcf(c_2091,plain,
! [X0: $i,X1: $i] :
( p2(f9(X0),X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_267]) ).
tcf(c_2131,plain,
! [X0: $i,X1: $i] :
( p3(f6(X0),X1)
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_266]) ).
tcf(c_2145,plain,
( p10(iPr_def_12,iPr_def_12)
| ~ p10(iPr_def_16,iPr_def_16) ),
inference(superposition,[status(thm)],[c_257,c_2005]) ).
tcf(c_2168,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(X0,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_270,c_1257]) ).
tcf(c_2169,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_12)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_917,c_1257]) ).
tcf(c_2171,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(X0,c14)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1014,c_1257]) ).
tcf(c_2172,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(X1,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1690,c_1257]) ).
tcf(c_2174,plain,
! [X0: $i] :
( p2(iPr_def_12,X0)
| ~ p2(c14,c13)
| ~ p2(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_258,c_1257]) ).
tcf(c_2196,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p3(iPr_def_10,X1)
| ~ p2(iPr_def_11,X2)
| ~ p10(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_1287,c_1155]) ).
tcf(c_2197,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p3(iPr_def_10,X1)
| ~ p2(iPr_def_11,X2)
| ~ p11(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_1287,c_1115]) ).
tcf(c_2198,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X3)
| ~ p2(X1,X2)
| ~ p10(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_1287,c_265]) ).
tcf(c_2199,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X3)
| ~ p2(X1,X2)
| ~ p11(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_1287,c_264]) ).
tcf(c_2200,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X2)
| ~ p2(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_1287,c_267]) ).
tcf(c_2248,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(X0))
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_279,c_1309]) ).
tcf(c_2249,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(X0,iPr_def_10)
| ~ p3(X0,X1) ),
inference(superposition,[status(thm)],[c_271,c_1309]) ).
tcf(c_2250,plain,
! [X0: $i] :
( p2(iPr_def_11,iPr_def_11)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_929,c_1309]) ).
tcf(c_2279,plain,
! [X0: $i,X1: $i] :
( p10(X1,f5(X0))
| ~ p10(X1,iPr_def_11)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2248,c_1155]) ).
tcf(c_2280,plain,
! [X0: $i,X1: $i] :
( p11(X1,f5(X0))
| ~ p11(X1,iPr_def_11)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2248,c_1115]) ).
tcf(c_2281,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f5(X2),X1)
| ~ p10(iPr_def_11,X0)
| ~ p3(X2,iPr_def_10)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_2248,c_265]) ).
tcf(c_2282,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f5(X2),X1)
| ~ p11(iPr_def_11,X0)
| ~ p3(X2,iPr_def_10)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_2248,c_264]) ).
tcf(c_2283,plain,
! [X0: $i,X1: $i] :
( p2(f5(X1),X0)
| ~ p3(X1,iPr_def_10)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_2248,c_267]) ).
tcf(c_2330,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_13,X2)
| ~ p3(c12,X0)
| ~ p3(f8(X0),X1) ),
inference(superposition,[status(thm)],[c_1335,c_266]) ).
tcf(c_2341,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(X0))
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_278,c_1345]) ).
tcf(c_2342,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(X0,c12)
| ~ p3(X0,X1) ),
inference(superposition,[status(thm)],[c_272,c_1345]) ).
tcf(c_2343,plain,
! [X0: $i] :
( p3(iPr_def_13,iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_941,c_1345]) ).
tcf(c_2365,plain,
! [X0: $i,X1: $i] :
( p11(f9(X0),X1)
| ~ p11(iPr_def_12,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_279,c_1119]) ).
tcf(c_2366,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),f5(X1))
| ~ p2(c13,X2)
| ~ p3(X0,X1)
| ~ p11(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_271,c_1119]) ).
tcf(c_2367,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),f9(X1))
| ~ p2(c13,X2)
| ~ p2(X0,X1)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_270,c_1119]) ).
tcf(c_2368,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p11(f9(X4),f4(X2,X3))
| ~ p2(c13,X4)
| ~ p3(X1,X3)
| ~ p2(X0,X2)
| ~ p11(iPr_def_12,f4(X0,X1)) ),
inference(superposition,[status(thm)],[c_263,c_1119]) ).
tcf(c_2369,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),f9(X0))
| ~ p11(iPr_def_12,iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_1119]) ).
tcf(c_2370,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),f9(X0))
| ~ p11(iPr_def_12,iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_1119]) ).
tcf(c_2371,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(X0,c13)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_917,c_1119]) ).
tcf(c_2372,plain,
! [X0: $i,X1: $i] :
( p11(f9(X0),f5(X1))
| ~ p11(iPr_def_12,iPr_def_11)
| ~ p3(X1,iPr_def_10)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_2248,c_1119]) ).
tcf(c_2373,plain,
! [X0: $i,X1: $i] :
( p11(f9(X0),f5(X1))
| ~ p11(iPr_def_12,iPr_def_11)
| ~ p3(iPr_def_10,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_928,c_1119]) ).
tcf(c_2374,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),iPr_def_11)
| ~ p3(X0,iPr_def_10)
| ~ p2(c13,X1)
| ~ p11(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_929,c_1119]) ).
tcf(c_2375,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p2(c13,X0)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_998,c_1119]) ).
tcf(c_2378,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),iPr_def_17)
| ~ p2(c13,X1)
| ~ p2(X0,c14)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1014,c_1119]) ).
tcf(c_2379,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X2)
| ~ p2(c13,X1)
| ~ p11(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_1287,c_1119]) ).
tcf(c_2380,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X2),f9(X1))
| ~ p2(c13,X2)
| ~ p2(X1,X0)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1690,c_1119]) ).
tcf(c_2496,plain,
( p10(iPr_def_12,iPr_def_12)
| p11(iPr_def_12,iPr_def_12) ),
inference(superposition,[status(thm)],[c_1750,c_2145]) ).
tcf(c_2505,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(c13,X0)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1797,c_1119]) ).
tcf(c_2506,plain,
! [X0: $i,X1: $i] :
( p10(X0,iPr_def_12)
| ~ p2(c13,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1797,c_1155]) ).
tcf(c_2507,plain,
! [X0: $i,X1: $i] :
( p11(X0,iPr_def_12)
| ~ p2(c13,X1)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1797,c_1115]) ).
tcf(c_2508,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1797,c_265]) ).
tcf(c_2509,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1797,c_264]) ).
tcf(c_2510,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(c13,X0)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1797,c_267]) ).
tcf(c_2511,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_12)
| ~ p2(c13,X0)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1797,c_1257]) ).
tcf(c_2512,plain,
! [X0: $i,X1: $i] :
( p2(f9(X1),iPr_def_12)
| ~ p2(c13,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1797,c_975]) ).
tcf(c_2579,plain,
! [X0: $i,X1: $i] :
( p11(f9(X1),iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(c13,X1)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1798,c_1119]) ).
tcf(c_2580,plain,
! [X0: $i,X1: $i] :
( p10(X0,iPr_def_17)
| ~ p2(c14,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1798,c_1155]) ).
tcf(c_2581,plain,
! [X0: $i,X1: $i] :
( p11(X0,iPr_def_17)
| ~ p2(c14,X1)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1798,c_1115]) ).
tcf(c_2582,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1798,c_265]) ).
tcf(c_2583,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1798,c_264]) ).
tcf(c_2584,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1798,c_267]) ).
tcf(c_2585,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1798,c_1257]) ).
tcf(c_2586,plain,
! [X0: $i,X1: $i] :
( p2(f9(X1),iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1798,c_975]) ).
tcf(c_2648,plain,
! [X0: $i,X1: $i] :
( p3(f8(X0),X1)
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_266]) ).
tcf(c_2658,plain,
! [X0: $i] :
( ~ p3(X0,c12)
| ~ p3(X0,iPr_def_14) ),
inference(global_subsumption_just,[status(thm)],[c_1954,c_273,c_1244,c_1245,c_1954]) ).
tcf(c_2659,plain,
! [X0: $i] :
( ~ p3(X0,iPr_def_14)
| ~ p3(X0,c12) ),
inference(renaming,[status(thm)],[c_2658]) ).
tcf(c_2665,plain,
! [X0: $i] :
( ~ p3(iPr_def_13,c12)
| ~ p3(c12,X0)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1335,c_2659]) ).
tcf(c_2666,plain,
! [X0: $i] :
( ~ p3(iPr_def_10,c12)
| ~ p3(c12,X0)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1220,c_2659]) ).
tcf(c_2696,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_15,X2)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_1362,c_266]) ).
tcf(c_2697,plain,
! [X0: $i] :
( ~ p3(iPr_def_15,c12)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1362,c_2659]) ).
tcf(c_2698,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1362,c_1233]) ).
tcf(c_2716,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(X0))
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_278,c_1372]) ).
tcf(c_2717,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(X0,iPr_def_14)
| ~ p3(X0,X1) ),
inference(superposition,[status(thm)],[c_269,c_1372]) ).
tcf(c_2720,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,X1)
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1220,c_1372]) ).
tcf(c_2721,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_15)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_1004,c_1372]) ).
tcf(c_2739,plain,
! [X0: $i,X1: $i] :
( p3(f6(X0),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2716,c_266]) ).
tcf(c_2751,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(c13,X1)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1384,c_1119]) ).
tcf(c_2752,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1384,c_1155]) ).
tcf(c_2753,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X1)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_1384,c_1115]) ).
tcf(c_2754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p2(iPr_def_17,X3)
| ~ p2(c14,X0)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1384,c_265]) ).
tcf(c_2755,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p2(iPr_def_17,X3)
| ~ p2(c14,X0)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1384,c_264]) ).
tcf(c_2756,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1384,c_267]) ).
tcf(c_2757,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1384,c_1257]) ).
tcf(c_2758,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1384,c_975]) ).
tcf(c_2834,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(X0,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_270,c_1407]) ).
tcf(c_2835,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(c13,X0)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1797,c_1407]) ).
tcf(c_2836,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(X0,c14)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_917,c_1407]) ).
tcf(c_2838,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(c13,X0)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_998,c_1407]) ).
tcf(c_2839,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1798,c_1407]) ).
tcf(c_2840,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_17)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1014,c_1407]) ).
tcf(c_2841,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(X1,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1690,c_1407]) ).
tcf(c_2881,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(f8(X1)))
| ~ p3(X0,X1)
| ~ p3(f8(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_272,c_1896]) ).
tcf(c_2882,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(f6(X1)))
| ~ p3(X0,X1)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_269,c_1896]) ).
tcf(c_2883,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(f7(X1)))
| ~ p3(X0,X1)
| ~ p3(f7(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_268,c_1896]) ).
tcf(c_2884,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_13)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1895,c_1896]) ).
tcf(c_2885,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_13)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_892,c_1896]) ).
tcf(c_2886,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(iPr_def_14))
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_893,c_1896]) ).
tcf(c_2887,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_1896]) ).
tcf(c_2888,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_13)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_1896]) ).
tcf(c_2889,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(iPr_def_10))
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_905,c_1896]) ).
tcf(c_2890,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_1896]) ).
tcf(c_2891,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_13)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_1896]) ).
tcf(c_2892,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(iPr_def_13))
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_941,c_1896]) ).
tcf(c_2893,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0)
| ~ p3(f8(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1335,c_1896]) ).
tcf(c_2894,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1362,c_1896]) ).
tcf(c_2895,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1220,c_1896]) ).
tcf(c_2896,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1195,c_1896]) ).
tcf(c_2897,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(X0)))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2716,c_1896]) ).
tcf(c_2898,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(X0)))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1003,c_1896]) ).
tcf(c_2899,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(iPr_def_15))
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1004,c_1896]) ).
tcf(c_2909,plain,
! [X0: $i] :
( p3(iPr_def_14,iPr_def_14)
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_2892,c_255]) ).
tcf(c_2910,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f8(X0)))
| ~ p3(c12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2891,c_278]) ).
tcf(c_2913,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f8(X0)))
| ~ p3(X0,c12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_2890,c_278]) ).
tcf(c_3029,plain,
( p3(iPr_def_14,f7(iPr_def_13))
| ~ p3(c12,c12) ),
inference(superposition,[status(thm)],[c_254,c_2910]) ).
tcf(c_3030,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_13)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_2910,c_1896]) ).
tcf(c_3031,plain,
! [X0: $i,X1: $i] :
( p3(f7(f8(X0)),X1)
| ~ p3(iPr_def_14,X1)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_2910,c_266]) ).
tcf(c_3032,plain,
( p3(iPr_def_14,iPr_def_14)
| ~ p3(c12,c12) ),
inference(light_normalisation,[status(thm)],[c_3029,c_255]) ).
tcf(c_3045,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2913,c_1896]) ).
tcf(c_3046,plain,
! [X0: $i,X1: $i] :
( p3(f7(f8(X0)),X1)
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2913,c_266]) ).
tcf(c_3065,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(f9(X3),X1)
| p11(X0,f9(X2))
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_275,c_1157]) ).
tcf(c_3087,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(c14,c13)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_2174]) ).
tcf(c_3088,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(c14,c13)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_2174]) ).
tcf(c_3104,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_1917,c_1896]) ).
tcf(c_3105,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_14,X2)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),X1) ),
inference(superposition,[status(thm)],[c_1917,c_266]) ).
tcf(c_3130,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(f8(X1)))
| ~ p3(X0,X1)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_272,c_1951]) ).
tcf(c_3131,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(f6(X1)))
| ~ p3(X0,X1)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_269,c_1951]) ).
tcf(c_3132,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(f7(X1)))
| ~ p3(X0,X1)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_268,c_1951]) ).
tcf(c_3135,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(iPr_def_14))
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_893,c_1951]) ).
tcf(c_3136,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(X0)))
| ~ p3(iPr_def_10,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_1951]) ).
tcf(c_3137,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(X0)))
| ~ p3(iPr_def_10,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_1951]) ).
tcf(c_3138,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(iPr_def_10))
| ~ p3(X0,c12)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_905,c_1951]) ).
tcf(c_3139,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f8(X0)))
| ~ p3(iPr_def_13,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_1951]) ).
tcf(c_3140,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f8(X0)))
| ~ p3(iPr_def_13,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_1951]) ).
tcf(c_3141,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(iPr_def_13))
| ~ p3(X0,c12)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_941,c_1951]) ).
tcf(c_3142,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_1335,c_1951]) ).
tcf(c_3143,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1362,c_1951]) ).
tcf(c_3144,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1220,c_1951]) ).
tcf(c_3145,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_1917,c_1951]) ).
tcf(c_3146,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_1195,c_1951]) ).
tcf(c_3147,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(X0)))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2716,c_1951]) ).
tcf(c_3148,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(X0)))
| ~ p3(iPr_def_15,c12)
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1003,c_1951]) ).
tcf(c_3149,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(iPr_def_15))
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1004,c_1951]) ).
tcf(c_3179,plain,
! [X0: $i] :
( p3(iPr_def_10,iPr_def_15)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),c12) ),
inference(light_normalisation,[status(thm)],[c_3135,c_256]) ).
tcf(c_3288,plain,
! [X0: $i] :
( p2(iPr_def_17,X0)
| ~ p2(c14,c13)
| ~ p2(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_258,c_2019]) ).
tcf(c_3289,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p2(X0,c13)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_2019,c_1119]) ).
tcf(c_3290,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(X1,c13)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_2019,c_1155]) ).
tcf(c_3291,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(X1,c13)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_2019,c_1115]) ).
tcf(c_3292,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p2(iPr_def_12,X3)
| ~ p2(X0,c13)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2019,c_265]) ).
tcf(c_3293,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p2(iPr_def_12,X3)
| ~ p2(X0,c13)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2019,c_264]) ).
tcf(c_3294,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p2(iPr_def_12,X2)
| ~ p2(X0,c13)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2019,c_267]) ).
tcf(c_3295,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(X0,c14)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_2019,c_1407]) ).
tcf(c_3297,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(X0,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_2019,c_975]) ).
tcf(c_3402,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_12,c13)
| ~ p2(X0,c13)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2019,c_2171]) ).
tcf(c_3403,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_17,c13)
| ~ p2(c14,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1384,c_2171]) ).
tcf(c_3404,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_12,c13)
| ~ p2(c13,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_998,c_2171]) ).
tcf(c_3405,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_11,c13)
| ~ p3(iPr_def_10,X0)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_1287,c_2171]) ).
tcf(c_3441,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_12,c13)
| ~ p2(X0,c13)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_2019,c_2585]) ).
tcf(c_3442,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_17,c13)
| ~ p2(c14,X0)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_1384,c_2585]) ).
tcf(c_3443,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_12,c13)
| ~ p2(c13,X0)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_998,c_2585]) ).
tcf(c_3444,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_11,c13)
| ~ p3(iPr_def_10,X0)
| ~ p2(c14,f5(X0)) ),
inference(superposition,[status(thm)],[c_1287,c_2585]) ).
tcf(c_3486,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_12,c13)
| ~ p2(X0,c13)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2019,c_2836]) ).
tcf(c_3487,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_17,c13)
| ~ p2(c14,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1384,c_2836]) ).
tcf(c_3488,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_12,c13)
| ~ p2(c13,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_998,c_2836]) ).
tcf(c_3489,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_11,c13)
| ~ p3(iPr_def_10,X0)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_1287,c_2836]) ).
tcf(c_3516,plain,
! [X0: $i] :
( p2(iPr_def_12,X0)
| ~ p2(c13,c14)
| ~ p2(iPr_def_17,X0) ),
inference(superposition,[status(thm)],[c_253,c_2091]) ).
tcf(c_3518,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c13,X1)
| ~ p2(X0,c14)
| ~ p11(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_2091,c_1119]) ).
tcf(c_3519,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(X1,c14)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_2091,c_1155]) ).
tcf(c_3520,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(X1,c14)
| ~ p11(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_2091,c_1115]) ).
tcf(c_3521,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p2(iPr_def_17,X3)
| ~ p2(X0,c14)
| ~ p2(X1,X2)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2091,c_265]) ).
tcf(c_3522,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p2(iPr_def_17,X3)
| ~ p2(X0,c14)
| ~ p2(X1,X2)
| ~ p11(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2091,c_264]) ).
tcf(c_3523,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p2(iPr_def_17,X2)
| ~ p2(X0,c14)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_2091,c_267]) ).
tcf(c_3524,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_17,c13)
| ~ p2(X0,c14)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2091,c_2836]) ).
tcf(c_3525,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_17,c13)
| ~ p2(X0,c14)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_2091,c_2585]) ).
tcf(c_3526,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_17,c13)
| ~ p2(X0,c14)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2091,c_2171]) ).
tcf(c_3528,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(X0,c14)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_2091,c_1257]) ).
tcf(c_3529,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(X0,c14)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_2091,c_975]) ).
tcf(c_3646,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_2131,c_1951]) ).
tcf(c_3647,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2131,c_1896]) ).
tcf(c_3648,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_10,X2)
| ~ p3(X0,c12)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_2131,c_266]) ).
tcf(c_3649,plain,
! [X0: $i] :
( ~ p3(iPr_def_10,c12)
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2131,c_2659]) ).
tcf(c_3686,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f5(X1)))
| ~ p3(X0,X1)
| ~ p2(f5(X0),c13) ),
inference(superposition,[status(thm)],[c_271,c_2168]) ).
tcf(c_3687,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f9(X1)))
| ~ p2(X0,X1)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_270,c_2168]) ).
tcf(c_3688,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(iPr_def_12,f9(f4(X2,X3)))
| ~ p3(X1,X3)
| ~ p2(X0,X2)
| ~ p2(f4(X0,X1),c13) ),
inference(superposition,[status(thm)],[c_263,c_2168]) ).
tcf(c_3689,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(iPr_def_12,c13)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_2168]) ).
tcf(c_3690,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(iPr_def_12,c13)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_2168]) ).
tcf(c_3691,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_12))
| ~ p2(c13,X0)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_1797,c_2168]) ).
tcf(c_3692,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_12))
| ~ p2(X0,c13)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_917,c_2168]) ).
tcf(c_3693,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(X0)))
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2248,c_2168]) ).
tcf(c_3694,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(X0)))
| ~ p2(iPr_def_11,c13)
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_928,c_2168]) ).
tcf(c_3695,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_11))
| ~ p3(X0,iPr_def_10)
| ~ p2(f5(X0),c13) ),
inference(superposition,[status(thm)],[c_929,c_2168]) ).
tcf(c_3696,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(X0,c14)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_2091,c_2168]) ).
tcf(c_3697,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(X0,c13)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_2019,c_2168]) ).
tcf(c_3698,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_1384,c_2168]) ).
tcf(c_3699,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(c13,X0)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_998,c_2168]) ).
tcf(c_3700,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(iPr_def_17,c13)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_2168]) ).
tcf(c_3701,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(iPr_def_17,c13)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_2168]) ).
tcf(c_3702,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_17))
| ~ p2(c14,X0)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_1798,c_2168]) ).
tcf(c_3703,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_17))
| ~ p2(X0,c14)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_1014,c_2168]) ).
tcf(c_3704,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X1)
| ~ p2(f5(X0),c13) ),
inference(superposition,[status(thm)],[c_1287,c_2168]) ).
tcf(c_3705,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f9(X1)))
| ~ p2(X1,X0)
| ~ p2(f9(X0),c13) ),
inference(superposition,[status(thm)],[c_1690,c_2168]) ).
tcf(c_3875,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(f8(X1)))
| ~ p3(X0,X1)
| ~ p3(f8(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_272,c_2249]) ).
tcf(c_3876,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(f6(X1)))
| ~ p3(X0,X1)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_269,c_2249]) ).
tcf(c_3877,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(f7(X1)))
| ~ p3(X0,X1)
| ~ p3(f7(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_268,c_2249]) ).
tcf(c_3878,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_10)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1895,c_2249]) ).
tcf(c_3879,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_10)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_892,c_2249]) ).
tcf(c_3880,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(iPr_def_14))
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_893,c_2249]) ).
tcf(c_3881,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_10)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_2249]) ).
tcf(c_3882,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_10)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_2249]) ).
tcf(c_3883,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(iPr_def_10))
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_905,c_2249]) ).
tcf(c_3884,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_10)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_2249]) ).
tcf(c_3885,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_10)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_2249]) ).
tcf(c_3886,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(iPr_def_13))
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_941,c_2249]) ).
tcf(c_3887,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0)
| ~ p3(f8(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1335,c_2249]) ).
tcf(c_3888,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_2131,c_2249]) ).
tcf(c_3889,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1362,c_2249]) ).
tcf(c_3890,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1220,c_2249]) ).
tcf(c_3891,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1917,c_2249]) ).
tcf(c_3892,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1195,c_2249]) ).
tcf(c_3895,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(iPr_def_15))
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_1004,c_2249]) ).
tcf(c_3896,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_10)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2913,c_2249]) ).
tcf(c_3897,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_10)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_2910,c_2249]) ).
tcf(c_3910,plain,
! [X0: $i] :
( p2(iPr_def_11,iPr_def_11)
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_10) ),
inference(light_normalisation,[status(thm)],[c_3883,c_252]) ).
tcf(c_3911,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f6(X0)))
| ~ p3(c12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3882,c_278]) ).
tcf(c_3914,plain,
! [X0: $i] :
( p2(iPr_def_11,f5(f6(X0)))
| ~ p3(X0,c12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_3881,c_278]) ).
tcf(c_4073,plain,
( p2(iPr_def_11,f5(iPr_def_10))
| ~ p3(c12,c12) ),
inference(superposition,[status(thm)],[c_251,c_3911]) ).
tcf(c_4075,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(f6(X0))))
| ~ p2(iPr_def_11,c13)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_3911,c_2168]) ).
tcf(c_4076,plain,
! [X0: $i,X1: $i] :
( p11(f9(X0),f5(f6(X1)))
| ~ p11(iPr_def_12,iPr_def_11)
| ~ p3(c12,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_3911,c_1119]) ).
tcf(c_4077,plain,
! [X0: $i,X1: $i] :
( p10(X1,f5(f6(X0)))
| ~ p10(X1,iPr_def_11)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_3911,c_1155]) ).
tcf(c_4078,plain,
! [X0: $i,X1: $i] :
( p11(X1,f5(f6(X0)))
| ~ p11(X1,iPr_def_11)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_3911,c_1115]) ).
tcf(c_4079,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f5(f6(X2)),X1)
| ~ p10(iPr_def_11,X0)
| ~ p3(c12,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_3911,c_265]) ).
tcf(c_4080,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f5(f6(X2)),X1)
| ~ p11(iPr_def_11,X0)
| ~ p3(c12,X2)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_3911,c_264]) ).
tcf(c_4081,plain,
! [X0: $i,X1: $i] :
( p2(f5(f6(X1)),X0)
| ~ p3(c12,X1)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_3911,c_267]) ).
tcf(c_4082,plain,
( p2(iPr_def_11,iPr_def_11)
| ~ p3(c12,c12) ),
inference(light_normalisation,[status(thm)],[c_4073,c_252]) ).
tcf(c_4133,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(f6(X0))))
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_3914,c_2168]) ).
tcf(c_4134,plain,
! [X0: $i,X1: $i] :
( p11(f9(X0),f5(f6(X1)))
| ~ p11(iPr_def_12,iPr_def_11)
| ~ p3(X1,c12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_3914,c_1119]) ).
tcf(c_4135,plain,
! [X0: $i,X1: $i] :
( p10(X1,f5(f6(X0)))
| ~ p10(X1,iPr_def_11)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_3914,c_1155]) ).
tcf(c_4136,plain,
! [X0: $i,X1: $i] :
( p11(X1,f5(f6(X0)))
| ~ p11(X1,iPr_def_11)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_3914,c_1115]) ).
tcf(c_4137,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f5(f6(X2)),X1)
| ~ p10(iPr_def_11,X0)
| ~ p3(X2,c12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_3914,c_265]) ).
tcf(c_4138,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f5(f6(X2)),X1)
| ~ p11(iPr_def_11,X0)
| ~ p3(X2,c12)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_3914,c_264]) ).
tcf(c_4139,plain,
! [X0: $i,X1: $i] :
( p2(f5(f6(X1)),X0)
| ~ p3(X1,c12)
| ~ p2(iPr_def_11,X0) ),
inference(superposition,[status(thm)],[c_3914,c_267]) ).
tcf(c_4206,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X1)
| ~ p2(f5(X0),c13) ),
inference(superposition,[status(thm)],[c_2283,c_2168]) ).
tcf(c_4207,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(f9(X1),X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X2)
| ~ p2(c13,X1)
| ~ p11(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_2283,c_1119]) ).
tcf(c_4208,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(X0,X2)
| ~ p3(X1,iPr_def_10)
| ~ p2(iPr_def_11,X2)
| ~ p10(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_2283,c_1155]) ).
tcf(c_4209,plain,
! [X0: $i,X1: $i,X2: $i] :
( p11(X0,X2)
| ~ p3(X1,iPr_def_10)
| ~ p2(iPr_def_11,X2)
| ~ p11(X0,f5(X1)) ),
inference(superposition,[status(thm)],[c_2283,c_1115]) ).
tcf(c_4210,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(X3,X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X3)
| ~ p2(X1,X2)
| ~ p10(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_2283,c_265]) ).
tcf(c_4211,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(X3,X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X3)
| ~ p2(X1,X2)
| ~ p11(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_2283,c_264]) ).
tcf(c_4212,plain,
! [X0: $i,X1: $i,X2: $i] :
( p2(X2,X1)
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X2)
| ~ p2(f5(X0),X1) ),
inference(superposition,[status(thm)],[c_2283,c_267]) ).
tcf(c_4213,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,iPr_def_10)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_2283,c_2836]) ).
tcf(c_4214,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,iPr_def_10)
| ~ p2(c14,f5(X0)) ),
inference(superposition,[status(thm)],[c_2283,c_2585]) ).
tcf(c_4215,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,iPr_def_10)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_2283,c_2171]) ).
tcf(c_4329,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(f8(X1)))
| ~ p3(X0,X1)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_272,c_2342]) ).
tcf(c_4330,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(f6(X1)))
| ~ p3(X0,X1)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_269,c_2342]) ).
tcf(c_4331,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(f7(X1)))
| ~ p3(X0,X1)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_268,c_2342]) ).
tcf(c_4334,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(iPr_def_14))
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_893,c_2342]) ).
tcf(c_4335,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(X0)))
| ~ p3(iPr_def_10,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_2342]) ).
tcf(c_4336,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(X0)))
| ~ p3(iPr_def_10,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_2342]) ).
tcf(c_4337,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(iPr_def_10))
| ~ p3(X0,c12)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_905,c_2342]) ).
tcf(c_4338,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f8(X0)))
| ~ p3(iPr_def_13,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_2342]) ).
tcf(c_4339,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f8(X0)))
| ~ p3(iPr_def_13,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_2342]) ).
tcf(c_4340,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(iPr_def_13))
| ~ p3(X0,c12)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_941,c_2342]) ).
tcf(c_4341,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_1335,c_2342]) ).
tcf(c_4342,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_2131,c_2342]) ).
tcf(c_4343,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1362,c_2342]) ).
tcf(c_4344,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1220,c_2342]) ).
tcf(c_4345,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_1917,c_2342]) ).
tcf(c_4346,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),c12) ),
inference(superposition,[status(thm)],[c_1195,c_2342]) ).
tcf(c_4347,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(X0)))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2716,c_2342]) ).
tcf(c_4348,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(X0)))
| ~ p3(iPr_def_15,c12)
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1003,c_2342]) ).
tcf(c_4349,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(iPr_def_15))
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_1004,c_2342]) ).
tcf(c_4506,plain,
! [X0: $i,X1: $i] :
( p10(f9(X0),X1)
| ~ p10(iPr_def_12,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_279,c_1159]) ).
tcf(c_4507,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),f5(X1))
| ~ p2(c13,X2)
| ~ p3(X0,X1)
| ~ p10(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_271,c_1159]) ).
tcf(c_4508,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),f9(X1))
| ~ p2(c13,X2)
| ~ p2(X0,X1)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_270,c_1159]) ).
tcf(c_4509,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p10(f9(X4),f4(X2,X3))
| ~ p2(c13,X4)
| ~ p3(X1,X3)
| ~ p2(X0,X2)
| ~ p10(iPr_def_12,f4(X0,X1)) ),
inference(superposition,[status(thm)],[c_263,c_1159]) ).
tcf(c_4510,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),f9(X0))
| ~ p10(iPr_def_12,iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_1159]) ).
tcf(c_4511,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),f9(X0))
| ~ p10(iPr_def_12,iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_1159]) ).
tcf(c_4512,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(c13,X0)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1797,c_1159]) ).
tcf(c_4513,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),iPr_def_12)
| ~ p2(c13,X1)
| ~ p2(X0,c13)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_917,c_1159]) ).
tcf(c_4516,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),iPr_def_11)
| ~ p3(X0,iPr_def_10)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_929,c_1159]) ).
tcf(c_4517,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c13,X1)
| ~ p2(X0,c14)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_2091,c_1159]) ).
tcf(c_4518,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p2(X0,c13)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_2019,c_1159]) ).
tcf(c_4519,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p2(iPr_def_17,X2)
| ~ p2(c14,X0)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1384,c_1159]) ).
tcf(c_4520,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p2(iPr_def_12,X2)
| ~ p2(c13,X1)
| ~ p2(c13,X0)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_998,c_1159]) ).
tcf(c_4521,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),f9(X0))
| ~ p10(iPr_def_12,iPr_def_17)
| ~ p2(c13,X1)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_1159]) ).
tcf(c_4522,plain,
! [X0: $i,X1: $i] :
( p10(f9(X0),f9(X1))
| ~ p10(iPr_def_12,iPr_def_17)
| ~ p2(c14,X1)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_1012,c_1159]) ).
tcf(c_4523,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1798,c_1159]) ).
tcf(c_4524,plain,
! [X0: $i,X1: $i] :
( p10(f9(X1),iPr_def_17)
| ~ p2(c13,X1)
| ~ p2(X0,c14)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1014,c_1159]) ).
tcf(c_4525,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X2)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_2283,c_1159]) ).
tcf(c_4526,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X1),X2)
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X2)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f5(X0)) ),
inference(superposition,[status(thm)],[c_1287,c_1159]) ).
tcf(c_4527,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(f9(X2),f9(X1))
| ~ p2(c13,X2)
| ~ p2(X1,X0)
| ~ p10(iPr_def_12,f9(X0)) ),
inference(superposition,[status(thm)],[c_1690,c_1159]) ).
tcf(c_4549,plain,
! [X0: $i,X1: $i] :
( ~ p3(X0,iPr_def_10)
| ~ p2(c13,X1)
| ~ p10(iPr_def_12,f5(X0)) ),
inference(forward_subsumption_resolution,[status(thm)],[c_4516,c_874]) ).
tcf(c_4723,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(c14,c13)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_3288]) ).
tcf(c_4724,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(c14,c13)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_3288]) ).
tcf(c_4752,plain,
! [X0: $i] :
( p11(iPr_def_17,X0)
| ~ p2(c13,c14)
| ~ p11(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_258,c_2365]) ).
tcf(c_4753,plain,
! [X0: $i,X1: $i] :
( ~ p11(iPr_def_12,X0)
| ~ p2(c13,X1)
| ~ p10(X0,f9(X1)) ),
inference(superposition,[status(thm)],[c_2365,c_274]) ).
tcf(c_4754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(f9(X1),X3)
| ~ p11(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_2365,c_1117]) ).
tcf(c_4792,plain,
! [X0: $i] :
( p11(X0,iPr_def_17)
| ~ p2(c13,c14)
| ~ p11(X0,iPr_def_12) ),
inference(superposition,[status(thm)],[c_258,c_1448]) ).
tcf(c_4793,plain,
! [X0: $i,X1: $i] :
( ~ p11(X1,iPr_def_12)
| ~ p2(c13,X0)
| ~ p10(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1448,c_274]) ).
tcf(c_4794,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p11(f9(X3),X1)
| ~ p2(c13,X0)
| ~ p2(X2,X3)
| ~ p11(f9(X2),iPr_def_12)
| ~ p2(f9(X0),X1) ),
inference(superposition,[status(thm)],[c_1448,c_1117]) ).
tcf(c_4825,plain,
! [X0: $i] :
( p11(X0,iPr_def_12)
| ~ p2(c14,c13)
| ~ p11(X0,iPr_def_17) ),
inference(superposition,[status(thm)],[c_258,c_1449]) ).
tcf(c_4843,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(c13,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_270,c_2510]) ).
tcf(c_4844,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_1797,c_2510]) ).
tcf(c_4846,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(c13,X0)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_2091,c_2510]) ).
tcf(c_4848,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,X1)
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_1384,c_2510]) ).
tcf(c_4850,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(c14,X0)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_1798,c_2510]) ).
tcf(c_4851,plain,
! [X0: $i] :
( p2(iPr_def_12,iPr_def_17)
| ~ p2(c13,X0)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1014,c_2510]) ).
tcf(c_4852,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X0))
| ~ p2(c13,X1)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1690,c_2510]) ).
tcf(c_4899,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(c14,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_270,c_2584]) ).
tcf(c_4900,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(c14,X0)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_1797,c_2584]) ).
tcf(c_4901,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(c14,X0)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_917,c_2584]) ).
tcf(c_4903,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(c14,X0)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_2019,c_2584]) ).
tcf(c_4905,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,X1)
| ~ p2(iPr_def_12,X1)
| ~ p2(c14,X0)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_998,c_2584]) ).
tcf(c_4906,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_17)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1798,c_2584]) ).
tcf(c_4908,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X0))
| ~ p2(c14,X1)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_1690,c_2584]) ).
tcf(c_4955,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_2648,c_2342]) ).
tcf(c_4956,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_2648,c_2249]) ).
tcf(c_4957,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),c12) ),
inference(superposition,[status(thm)],[c_2648,c_1951]) ).
tcf(c_4958,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2648,c_1896]) ).
tcf(c_4959,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_13,X2)
| ~ p3(X0,c12)
| ~ p3(f8(X0),X1) ),
inference(superposition,[status(thm)],[c_2648,c_266]) ).
tcf(c_4960,plain,
! [X0: $i] :
( ~ p3(iPr_def_13,c12)
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2648,c_2659]) ).
tcf(c_5010,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(f8(X1)))
| ~ p3(X0,X1)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_272,c_2717]) ).
tcf(c_5011,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(f6(X1)))
| ~ p3(X0,X1)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_269,c_2717]) ).
tcf(c_5012,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(f7(X1)))
| ~ p3(X0,X1)
| ~ p3(f7(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_268,c_2717]) ).
tcf(c_5013,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_14)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_1895,c_2717]) ).
tcf(c_5014,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(X0)))
| ~ p3(iPr_def_14,iPr_def_14)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_892,c_2717]) ).
tcf(c_5015,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(iPr_def_14))
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_893,c_2717]) ).
tcf(c_5016,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_1950,c_2717]) ).
tcf(c_5017,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(X0)))
| ~ p3(iPr_def_10,iPr_def_14)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_904,c_2717]) ).
tcf(c_5018,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(iPr_def_10))
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_905,c_2717]) ).
tcf(c_5019,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2341,c_2717]) ).
tcf(c_5020,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f8(X0)))
| ~ p3(iPr_def_13,iPr_def_14)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_940,c_2717]) ).
tcf(c_5021,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(iPr_def_13))
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_941,c_2717]) ).
tcf(c_5022,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(X0,c12)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2648,c_2717]) ).
tcf(c_5023,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_13,X1)
| ~ p3(c12,X0)
| ~ p3(f8(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1335,c_2717]) ).
tcf(c_5024,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(X0,c12)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2131,c_2717]) ).
tcf(c_5025,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_14,X0)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1362,c_2717]) ).
tcf(c_5026,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_10,X1)
| ~ p3(c12,X0)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1220,c_2717]) ).
tcf(c_5027,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1917,c_2717]) ).
tcf(c_5028,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_14,X1)
| ~ p3(iPr_def_13,X0)
| ~ p3(f7(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1195,c_2717]) ).
tcf(c_5029,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(X0)))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(X0,iPr_def_14) ),
inference(superposition,[status(thm)],[c_2716,c_2717]) ).
tcf(c_5030,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(X0)))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(iPr_def_14,X0) ),
inference(superposition,[status(thm)],[c_1003,c_2717]) ).
tcf(c_5031,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(iPr_def_15))
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_1004,c_2717]) ).
tcf(c_5032,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_2913,c_2717]) ).
tcf(c_5033,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(f8(X0))))
| ~ p3(iPr_def_14,iPr_def_14)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_2910,c_2717]) ).
tcf(c_5061,plain,
! [X0: $i] :
( p3(iPr_def_15,iPr_def_15)
| ~ p3(X0,iPr_def_13)
| ~ p3(f7(X0),iPr_def_14) ),
inference(light_normalisation,[status(thm)],[c_5015,c_256]) ).
tcf(c_5062,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(X0)))
| ~ p3(iPr_def_13,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5014,c_278]) ).
tcf(c_5065,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(X0)))
| ~ p3(X0,iPr_def_13) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5013,c_278]) ).
tcf(c_5068,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(f8(X0))))
| ~ p3(c12,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5033,c_278]) ).
tcf(c_5071,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f7(f8(X0))))
| ~ p3(X0,c12) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5032,c_278]) ).
tcf(c_5205,plain,
( p3(iPr_def_15,f6(iPr_def_14))
| ~ p3(iPr_def_13,iPr_def_13) ),
inference(superposition,[status(thm)],[c_255,c_5062]) ).
tcf(c_5206,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(f7(X0))))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_5062,c_2717]) ).
tcf(c_5207,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(f7(X0))))
| ~ p3(iPr_def_15,c12)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_5062,c_2342]) ).
tcf(c_5209,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(f7(X0))))
| ~ p3(iPr_def_15,c12)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_5062,c_1951]) ).
tcf(c_5210,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(f7(X0))))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_5062,c_1896]) ).
tcf(c_5211,plain,
! [X0: $i,X1: $i] :
( p3(f6(f7(X0)),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(iPr_def_13,X0) ),
inference(superposition,[status(thm)],[c_5062,c_266]) ).
tcf(c_5212,plain,
( p3(iPr_def_15,iPr_def_15)
| ~ p3(iPr_def_13,iPr_def_13) ),
inference(light_normalisation,[status(thm)],[c_5205,c_256]) ).
tcf(c_5242,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(f7(X0))))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5065,c_2717]) ).
tcf(c_5243,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(f7(X0))))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5065,c_2342]) ).
tcf(c_5245,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(f7(X0))))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5065,c_1951]) ).
tcf(c_5246,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(f7(X0))))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5065,c_1896]) ).
tcf(c_5247,plain,
! [X0: $i,X1: $i] :
( p3(f6(f7(X0)),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_13) ),
inference(superposition,[status(thm)],[c_5065,c_266]) ).
tcf(c_5292,plain,
( p3(iPr_def_15,f6(f7(iPr_def_13)))
| ~ p3(c12,c12) ),
inference(superposition,[status(thm)],[c_254,c_5068]) ).
tcf(c_5293,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_5068,c_2717]) ).
tcf(c_5294,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_5068,c_2342]) ).
tcf(c_5296,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,c12)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_5068,c_1951]) ).
tcf(c_5297,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_5068,c_1896]) ).
tcf(c_5298,plain,
! [X0: $i,X1: $i] :
( p3(f6(f7(f8(X0))),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_5068,c_266]) ).
tcf(c_5299,plain,
( p3(iPr_def_15,iPr_def_15)
| ~ p3(c12,c12) ),
inference(light_normalisation,[status(thm)],[c_5292,c_255,c_256]) ).
tcf(c_5332,plain,
! [X0: $i] :
( p3(iPr_def_15,f6(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,iPr_def_14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_5071,c_2717]) ).
tcf(c_5333,plain,
! [X0: $i] :
( p3(iPr_def_13,f8(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_5071,c_2342]) ).
tcf(c_5335,plain,
! [X0: $i] :
( p3(iPr_def_10,f6(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,c12)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_5071,c_1951]) ).
tcf(c_5336,plain,
! [X0: $i] :
( p3(iPr_def_14,f7(f6(f7(f8(X0)))))
| ~ p3(iPr_def_15,iPr_def_13)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_5071,c_1896]) ).
tcf(c_5337,plain,
! [X0: $i,X1: $i] :
( p3(f6(f7(f8(X0))),X1)
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_5071,c_266]) ).
tcf(c_5399,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_12,X1)
| p11(X0,f9(X2))
| ~ p2(X2,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_275,c_1255]) ).
tcf(c_5400,plain,
! [X0: $i,X1: $i] :
( p10(iPr_def_12,X1)
| ~ p2(c13,c13)
| ~ p10(iPr_def_12,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_253,c_1255]) ).
tcf(c_5401,plain,
! [X0: $i,X1: $i] :
( p10(iPr_def_12,X1)
| ~ p2(c14,c13)
| ~ p10(iPr_def_17,X0)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_258,c_1255]) ).
tcf(c_5406,plain,
! [X0: $i,X1: $i] :
( p10(iPr_def_12,X1)
| ~ p10(iPr_def_12,X0)
| ~ p2(X0,X1) ),
inference(forward_subsumption_resolution,[status(thm)],[c_5400,c_279]) ).
tcf(c_5431,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_15,f6(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2739,c_2717]) ).
tcf(c_5432,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_13,f8(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_2739,c_2342]) ).
tcf(c_5433,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_11,f5(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_10) ),
inference(superposition,[status(thm)],[c_2739,c_2249]) ).
tcf(c_5434,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_10,f6(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),c12) ),
inference(superposition,[status(thm)],[c_2739,c_1951]) ).
tcf(c_5435,plain,
! [X0: $i,X1: $i] :
( p3(iPr_def_14,f7(X1))
| ~ p3(iPr_def_15,X1)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_13) ),
inference(superposition,[status(thm)],[c_2739,c_1896]) ).
tcf(c_5436,plain,
! [X0: $i,X1: $i,X2: $i] :
( p3(X2,X1)
| ~ p3(iPr_def_15,X2)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),X1) ),
inference(superposition,[status(thm)],[c_2739,c_266]) ).
tcf(c_5437,plain,
! [X0: $i] :
( ~ p3(iPr_def_15,c12)
| ~ p3(X0,iPr_def_14)
| ~ p3(f6(X0),iPr_def_14) ),
inference(superposition,[status(thm)],[c_2739,c_2659]) ).
tcf(c_5481,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(f5(X1)))
| ~ p3(X0,X1)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_271,c_2834]) ).
tcf(c_5482,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(f9(X1)))
| ~ p2(X0,X1)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_270,c_2834]) ).
tcf(c_5483,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(iPr_def_17,f9(f4(X2,X3)))
| ~ p3(X1,X3)
| ~ p2(X0,X2)
| ~ p2(f4(X0,X1),c14) ),
inference(superposition,[status(thm)],[c_263,c_2834]) ).
tcf(c_5484,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f9(X0)))
| ~ p2(iPr_def_12,c14)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_2834]) ).
tcf(c_5485,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f9(X0)))
| ~ p2(iPr_def_12,c14)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_2834]) ).
tcf(c_5486,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(iPr_def_12))
| ~ p2(c13,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1797,c_2834]) ).
tcf(c_5487,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(iPr_def_12))
| ~ p2(X0,c13)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_917,c_2834]) ).
tcf(c_5488,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f5(X0)))
| ~ p2(iPr_def_11,c14)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2248,c_2834]) ).
tcf(c_5489,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f5(X0)))
| ~ p2(iPr_def_11,c14)
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_928,c_2834]) ).
tcf(c_5490,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(iPr_def_11))
| ~ p3(X0,iPr_def_10)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_929,c_2834]) ).
tcf(c_5491,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(X0,c14)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2091,c_2834]) ).
tcf(c_5492,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(X0,c13)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_2019,c_2834]) ).
tcf(c_5493,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1384,c_2834]) ).
tcf(c_5494,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(c13,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_998,c_2834]) ).
tcf(c_5495,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f9(X0)))
| ~ p2(iPr_def_17,c14)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_2834]) ).
tcf(c_5496,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f9(X0)))
| ~ p2(iPr_def_17,c14)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_2834]) ).
tcf(c_5497,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(iPr_def_17))
| ~ p2(c14,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1798,c_2834]) ).
tcf(c_5498,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(iPr_def_17))
| ~ p2(X0,c14)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1014,c_2834]) ).
tcf(c_5499,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X1)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_2283,c_2834]) ).
tcf(c_5500,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(X1))
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X1)
| ~ p2(f5(X0),c14) ),
inference(superposition,[status(thm)],[c_1287,c_2834]) ).
tcf(c_5501,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_17,f9(f9(X1)))
| ~ p2(X1,X0)
| ~ p2(f9(X0),c14) ),
inference(superposition,[status(thm)],[c_1690,c_2834]) ).
tcf(c_5502,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f5(f6(X0))))
| ~ p2(iPr_def_11,c14)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_3914,c_2834]) ).
tcf(c_5503,plain,
! [X0: $i] :
( p2(iPr_def_17,f9(f5(f6(X0))))
| ~ p2(iPr_def_11,c14)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_3911,c_2834]) ).
tcf(c_5724,plain,
! [X0: $i] :
( p10(iPr_def_17,X0)
| ~ p2(c13,c14)
| ~ p10(iPr_def_12,X0) ),
inference(superposition,[status(thm)],[c_258,c_4506]) ).
tcf(c_5726,plain,
! [X0: $i,X1: $i,X2: $i] :
( p10(iPr_def_12,X1)
| ~ p10(iPr_def_12,X0)
| ~ p2(c13,X2)
| ~ p2(X2,c13)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_4506,c_1255]) ).
tcf(c_5727,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p10(f9(X1),X3)
| ~ p10(iPr_def_12,X2)
| ~ p2(c13,X0)
| ~ p2(X2,X3)
| ~ p2(X0,X1) ),
inference(superposition,[status(thm)],[c_4506,c_1157]) ).
tcf(c_5783,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_17,c13)
| ~ p2(X0,c14)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_2091,c_4901]) ).
tcf(c_5784,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_12,c13)
| ~ p2(X0,c13)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_2019,c_4901]) ).
tcf(c_5785,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_17,c13)
| ~ p2(c14,X0)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_1384,c_4901]) ).
tcf(c_5786,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_12,c13)
| ~ p2(c13,X0)
| ~ p2(c14,f9(X0)) ),
inference(superposition,[status(thm)],[c_998,c_4901]) ).
tcf(c_5787,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_11,c13)
| ~ p3(X0,iPr_def_10)
| ~ p2(c14,f5(X0)) ),
inference(superposition,[status(thm)],[c_2283,c_4901]) ).
tcf(c_5788,plain,
! [X0: $i] :
( p2(iPr_def_17,iPr_def_12)
| ~ p2(iPr_def_11,c13)
| ~ p3(iPr_def_10,X0)
| ~ p2(c14,f5(X0)) ),
inference(superposition,[status(thm)],[c_1287,c_4901]) ).
tcf(c_5840,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f5(X1)))
| ~ p3(X0,X1)
| ~ p2(c13,f5(X0)) ),
inference(superposition,[status(thm)],[c_271,c_4843]) ).
tcf(c_5841,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f9(X1)))
| ~ p2(X0,X1)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_270,c_4843]) ).
tcf(c_5842,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p2(iPr_def_12,f9(f4(X2,X3)))
| ~ p3(X1,X3)
| ~ p2(X0,X2)
| ~ p2(c13,f4(X0,X1)) ),
inference(superposition,[status(thm)],[c_263,c_4843]) ).
tcf(c_5843,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(c13,iPr_def_12)
| ~ p2(X0,c13) ),
inference(superposition,[status(thm)],[c_1795,c_4843]) ).
tcf(c_5844,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(c13,iPr_def_12)
| ~ p2(c13,X0) ),
inference(superposition,[status(thm)],[c_916,c_4843]) ).
tcf(c_5845,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_12))
| ~ p2(c13,X0)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_1797,c_4843]) ).
tcf(c_5846,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_12))
| ~ p2(X0,c13)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_917,c_4843]) ).
tcf(c_5847,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(X0)))
| ~ p2(c13,iPr_def_11)
| ~ p3(X0,iPr_def_10) ),
inference(superposition,[status(thm)],[c_2248,c_4843]) ).
tcf(c_5848,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(X0)))
| ~ p2(c13,iPr_def_11)
| ~ p3(iPr_def_10,X0) ),
inference(superposition,[status(thm)],[c_928,c_4843]) ).
tcf(c_5849,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_11))
| ~ p3(X0,iPr_def_10)
| ~ p2(c13,f5(X0)) ),
inference(superposition,[status(thm)],[c_929,c_4843]) ).
tcf(c_5850,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(X0,c14)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_2091,c_4843]) ).
tcf(c_5851,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(X0,c13)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_2019,c_4843]) ).
tcf(c_5852,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_17,X1)
| ~ p2(c14,X0)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_1384,c_4843]) ).
tcf(c_5853,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p2(iPr_def_12,X1)
| ~ p2(c13,X0)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_998,c_4843]) ).
tcf(c_5854,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(c13,iPr_def_17)
| ~ p2(X0,c14) ),
inference(superposition,[status(thm)],[c_1796,c_4843]) ).
tcf(c_5855,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f9(X0)))
| ~ p2(c13,iPr_def_17)
| ~ p2(c14,X0) ),
inference(superposition,[status(thm)],[c_1012,c_4843]) ).
tcf(c_5856,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_17))
| ~ p2(c14,X0)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_1798,c_4843]) ).
tcf(c_5857,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(iPr_def_17))
| ~ p2(X0,c14)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_1014,c_4843]) ).
tcf(c_5858,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p3(X0,iPr_def_10)
| ~ p2(iPr_def_11,X1)
| ~ p2(c13,f5(X0)) ),
inference(superposition,[status(thm)],[c_2283,c_4843]) ).
tcf(c_5859,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(X1))
| ~ p3(iPr_def_10,X0)
| ~ p2(iPr_def_11,X1)
| ~ p2(c13,f5(X0)) ),
inference(superposition,[status(thm)],[c_1287,c_4843]) ).
tcf(c_5860,plain,
! [X0: $i,X1: $i] :
( p2(iPr_def_12,f9(f9(X1)))
| ~ p2(X1,X0)
| ~ p2(c13,f9(X0)) ),
inference(superposition,[status(thm)],[c_1690,c_4843]) ).
tcf(c_5861,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(f6(X0))))
| ~ p2(c13,iPr_def_11)
| ~ p3(X0,c12) ),
inference(superposition,[status(thm)],[c_3914,c_4843]) ).
tcf(c_5862,plain,
! [X0: $i] :
( p2(iPr_def_12,f9(f5(f6(X0))))
| ~ p2(c13,iPr_def_11)
| ~ p3(c12,X0) ),
inference(superposition,[status(thm)],[c_3911,c_4843]) ).
tcf(c_6063,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_5862,c_5861,c_5860,c_5859,c_5858,c_5857,c_5856,c_5855,c_5854,c_5853,c_5852,c_5851,c_5850,c_5849,c_5848,c_5847,c_5846,c_5845,c_5844,c_5843,c_5842,c_5841,c_5840,c_5788,c_5787,c_5786,c_5785,c_5784,c_5783,c_5727,c_5726,c_5724,c_5503,c_5502,c_5501,c_5500,c_5499,c_5498,c_5497,c_5496,c_5495,c_5494,c_5493,c_5492,c_5491,c_5490,c_5489,c_5488,c_5487,c_5486,c_5485,c_5484,c_5483,c_5482,c_5481,c_5437,c_5436,c_5435,c_5434,c_5433,c_5432,c_5431,c_5406,c_5401,c_5400,c_5399,c_5337,c_5336,c_5335,c_5333,c_5332,c_5299,c_5298,c_5297,c_5296,c_5294,c_5293,c_5292,c_5247,c_5246,c_5245,c_5243,c_5242,c_5212,c_5211,c_5210,c_5209,c_5207,c_5206,c_5205,c_5071,c_5068,c_5065,c_5062,c_5061,c_5033,c_5032,c_5031,c_5030,c_5029,c_5028,c_5027,c_5026,c_5025,c_5024,c_5023,c_5022,c_5021,c_5020,c_5019,c_5018,c_5017,c_5016,c_5015,c_5014,c_5013,c_5012,c_5011,c_5010,c_4960,c_4959,c_4958,c_4957,c_4956,c_4955,c_4908,c_4906,c_4905,c_4903,c_4901,c_4900,c_4899,c_4852,c_4851,c_4850,c_4848,c_4846,c_4844,c_4843,c_4825,c_4794,c_4793,c_4792,c_4754,c_4753,c_4752,c_4724,c_4723,c_4549,c_4527,c_4526,c_4525,c_4524,c_4523,c_4522,c_4521,c_4520,c_4519,c_4518,c_4517,c_4516,c_4513,c_4512,c_4511,c_4510,c_4509,c_4508,c_4507,c_4506,c_4349,c_4348,c_4347,c_4346,c_4345,c_4344,c_4343,c_4342,c_4341,c_4340,c_4339,c_4338,c_4337,c_4336,c_4335,c_4334,c_4331,c_4330,c_4329,c_4215,c_4214,c_4213,c_4212,c_4211,c_4210,c_4209,c_4208,c_4207,c_4206,c_4139,c_4138,c_4137,c_4136,c_4135,c_4134,c_4133,c_4082,c_4081,c_4080,c_4079,c_4078,c_4077,c_4076,c_4075,c_4073,c_3914,c_3911,c_3910,c_3897,c_3896,c_3895,c_3892,c_3891,c_3890,c_3889,c_3888,c_3887,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_3705,c_3704,c_3703,c_3702,c_3701,c_3700,c_3699,c_3698,c_3697,c_3696,c_3695,c_3694,c_3693,c_3692,c_3691,c_3690,c_3689,c_3688,c_3687,c_3686,c_3649,c_3648,c_3647,c_3646,c_3529,c_3528,c_3526,c_3525,c_3524,c_3523,c_3522,c_3521,c_3520,c_3519,c_3518,c_3516,c_3489,c_3488,c_3487,c_3486,c_3444,c_3443,c_3442,c_3441,c_3405,c_3404,c_3403,c_3402,c_3297,c_3295,c_3294,c_3293,c_3292,c_3291,c_3290,c_3289,c_3288,c_3179,c_3149,c_3148,c_3147,c_3146,c_3145,c_3144,c_3143,c_3142,c_3141,c_3140,c_3139,c_3138,c_3137,c_3136,c_3135,c_3132,c_3131,c_3130,c_3105,c_3104,c_3088,c_3087,c_3065,c_3046,c_3045,c_3032,c_3031,c_3030,c_3029,c_2913,c_2910,c_2909,c_2899,c_2898,c_2897,c_2896,c_2895,c_2894,c_2893,c_2892,c_2891,c_2890,c_2889,c_2888,c_2887,c_2886,c_2885,c_2884,c_2883,c_2882,c_2881,c_2841,c_2840,c_2839,c_2838,c_2836,c_2835,c_2834,c_2758,c_2757,c_2756,c_2755,c_2754,c_2753,c_2752,c_2751,c_2739,c_2721,c_2720,c_2717,c_2716,c_2698,c_2697,c_2696,c_2666,c_2665,c_2659,c_2648,c_2586,c_2585,c_2584,c_2583,c_2582,c_2581,c_2580,c_2579,c_2512,c_2511,c_2510,c_2509,c_2508,c_2507,c_2506,c_2505,c_2496,c_2380,c_2379,c_2378,c_2375,c_2374,c_2373,c_2372,c_2371,c_2370,c_2369,c_2368,c_2367,c_2366,c_2365,c_2343,c_2342,c_2341,c_2330,c_2283,c_2282,c_2281,c_2280,c_2279,c_2250,c_2249,c_2248,c_2200,c_2199,c_2198,c_2197,c_2196,c_2174,c_2172,c_2171,c_2169,c_2168,c_2145,c_2131,c_2091,c_2090,c_2089,c_2088,c_2087,c_2085,c_2019,c_2018,c_2017,c_2016,c_2015,c_2014,c_2005,c_1991,c_1954,c_1952,c_1951,c_1950,c_1929,c_1917,c_1897,c_1896,c_1895,c_1884,c_1872,c_1804,c_1803,c_1802,c_1801,c_1800,c_1799,c_1798,c_1797,c_1796,c_1795,c_1786,c_1785,c_1766,c_1765,c_1751,c_1750,c_1694,c_1693,c_1692,c_1691,c_1690,c_1678,c_1677,c_1669,c_1646,c_1643,c_1642,c_1641,c_1640,c_1592,c_1591,c_1590,c_1589,c_1588,c_1587,c_1519,c_1518,c_1517,c_1516,c_1515,c_1514,c_1513,c_1512,c_1511,c_1453,c_1452,c_1451,c_1450,c_1449,c_1448,c_1447,c_1446,c_1445,c_1433,c_1432,c_1407,c_1406,c_1405,c_1384,c_1383,c_1382,c_1381,c_1372,c_1362,c_1361,c_1345,c_1335,c_1334,c_1309,c_1308,c_1307,c_1287,c_1286,c_1285,c_1284,c_1274,c_1257,c_1256,c_1255,c_1254,c_1234,c_1233,c_1232,c_1220,c_1219,c_1218,c_1209,c_1195,c_1194,c_1159,c_1158,c_1157,c_1156,c_1155,c_1119,c_1118,c_1117,c_1116,c_1115,c_1085,c_1084,c_1083,c_1082,c_1081,c_1066,c_1058,c_1054,c_1047,c_1046,c_1045,c_1044,c_1037,c_1033,c_1030,c_1026,c_1025,c_1024,c_1023,c_1014,c_1013,c_1012,c_1011,c_1004,c_1003,c_998,c_997,c_988,c_975,c_974,c_957,c_956,c_955,c_941,c_940,c_929,c_928,c_917,c_916,c_905,c_904,c_893,c_892,c_885,c_884,c_874,c_873,c_277,c_276,c_273,c_262,c_261,c_260,c_259,c_258,c_257,c_256,c_255,c_254,c_253,c_252,c_251,c_263,c_264,c_265,c_266,c_267,c_268,c_269,c_270,c_271,c_272,c_274,c_275,c_278,c_279]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN568-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.08/0.36 % Computer : n009.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 01:44:29 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.40 Running first-order theorem proving
% 0.13/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.42
% 0.13/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.42
% 0.13/0.42 % Detected problem language: tptp
% 0.13/0.43 % Proving...
% 2.44/1.28 % SZS status Started for theBenchmark.p
% 2.44/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 2.44/1.28
% 2.44/1.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.44/1.28
% 2.44/1.28 % ------ iProver source info
% 2.44/1.28
% 2.44/1.28 % git: date: 2026-07-19 20:42:38 +0200
% 2.44/1.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.44/1.28 % git: non_committed_changes: false
% 2.44/1.28
% 2.44/1.28 % ------ Parsing...% successful
% 2.44/1.28
% 2.44/1.28
% 2.44/1.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 2.44/1.28
% 2.44/1.28 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.44/1.28
% 2.44/1.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 2.44/1.28
% 2.44/1.28 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 2.44/1.28 % ------ Proving...
% 2.44/1.28 % ------ Problem Properties
% 2.44/1.28
% 2.44/1.28 %
% 2.44/1.28 % clauses 29
% 2.44/1.28 % conjectures 20
% 2.44/1.28 % EPR 11
% 2.44/1.28 % Horn 26
% 2.44/1.28 % unary 15
% 2.44/1.28 % binary 7
% 2.44/1.28 % lits 53
% 2.44/1.28 % lits eq 9
% 2.44/1.28 % fd_pure 0
% 2.44/1.28 % fd_pseudo 0
% 2.44/1.28 % fd_cond 0
% 2.44/1.28 % fd_pseudo_cond 0
% 2.44/1.28 % AC symbols 0
% 2.44/1.28
% 2.44/1.28 % ------ Schedule dynamic 5 is on
% 2.44/1.28
% 2.44/1.28 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 2.44/1.28
% 2.44/1.28
% 2.44/1.28 % ------
% 2.44/1.28 % Current options:
% 2.44/1.28 % ------
% 2.44/1.28
% 2.44/1.28
% 2.44/1.28 %
% 2.44/1.28
% 2.44/1.28 % ------ Proving...
% 2.44/1.28 %
% 2.44/1.28
% 2.44/1.28 % SZS status Unsatisfiable for theBenchmark.p
% 2.44/1.28
% 2.44/1.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.44/1.29
% 2.44/1.29
%------------------------------------------------------------------------------