%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL666+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 02:07:51 PM UTC 2026
% Result : Theorem 4.03s 1.74s
% Output : CNFRefutation 4.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 43
% Syntax : Number of formulae : 950 ( 5 unt; 41 def)
% Number of atoms : 5181 ( 0 equ)
% Maximal formula atoms : 241 ( 5 avg)
% Number of connectives : 7236 (3037 ~;3179 |;1020 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 85 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 85 ( 84 usr; 11 prp; 0-2 aty)
% Number of functors : 49 ( 49 usr; 1 con; 0-1 aty)
% Number of variables : 1238 ( 0 sgn 980 !; 258 ?; 330 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ( ( p101(X0)
| ! [X1] :
( p102(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p103(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p104(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p105(X1)
| ~ r1(X0,X1) ) )
& ( p201(X0)
| p202(X0)
| ! [X1] :
( p203(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p204(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p205(X1)
| ~ r1(X0,X1) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X1] :
( p304(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p305(X1)
| ~ r1(X0,X1) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X1] :
( p405(X1)
| ~ r1(X0,X1) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) ) )
| ~ ! [X1] :
( ~ ( ( p101(X1)
& p201(X1) )
| ( p101(X1)
& p301(X1) )
| ( p101(X1)
& p401(X1) )
| ( p101(X1)
& p501(X1) )
| ( p101(X1)
& p601(X1) )
| ( p201(X1)
& p301(X1) )
| ( p201(X1)
& p401(X1) )
| ( p201(X1)
& p501(X1) )
| ( p201(X1)
& p601(X1) )
| ( p301(X1)
& p401(X1) )
| ( p301(X1)
& p501(X1) )
| ( p301(X1)
& p601(X1) )
| ( p401(X1)
& p501(X1) )
| ( p401(X1)
& p601(X1) )
| ( p501(X1)
& p601(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p202(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p302(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p402(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p502(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p602(X1) )
| ( p202(X1)
& p302(X1) )
| ( p202(X1)
& p402(X1) )
| ( p202(X1)
& p502(X1) )
| ( p202(X1)
& p602(X1) )
| ( p302(X1)
& p402(X1) )
| ( p302(X1)
& p502(X1) )
| ( p302(X1)
& p602(X1) )
| ( p402(X1)
& p502(X1) )
| ( p402(X1)
& p602(X1) )
| ( p502(X1)
& p602(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p203(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p303(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p403(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p503(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p603(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p303(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p403(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p503(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p603(X1) )
| ( p303(X1)
& p403(X1) )
| ( p303(X1)
& p503(X1) )
| ( p303(X1)
& p603(X1) )
| ( p403(X1)
& p503(X1) )
| ( p403(X1)
& p603(X1) )
| ( p503(X1)
& p603(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p204(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p304(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p304(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( p404(X1)
& p504(X1) )
| ( p404(X1)
& p604(X1) )
| ( p504(X1)
& p604(X1) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p205(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p305(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p305(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p405(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p405(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( p505(X1)
& p605(X1) ) )
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ( ( p101(X0)
| ! [X1] :
( p102(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p103(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p104(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p105(X1)
| ~ r1(X0,X1) ) )
& ( p201(X0)
| p202(X0)
| ! [X1] :
( p203(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p204(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p205(X1)
| ~ r1(X0,X1) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X1] :
( p304(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( p305(X1)
| ~ r1(X0,X1) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X1] :
( p405(X1)
| ~ r1(X0,X1) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) ) )
| ~ ! [X1] :
( ~ ( ( p101(X1)
& p201(X1) )
| ( p101(X1)
& p301(X1) )
| ( p101(X1)
& p401(X1) )
| ( p101(X1)
& p501(X1) )
| ( p101(X1)
& p601(X1) )
| ( p201(X1)
& p301(X1) )
| ( p201(X1)
& p401(X1) )
| ( p201(X1)
& p501(X1) )
| ( p201(X1)
& p601(X1) )
| ( p301(X1)
& p401(X1) )
| ( p301(X1)
& p501(X1) )
| ( p301(X1)
& p601(X1) )
| ( p401(X1)
& p501(X1) )
| ( p401(X1)
& p601(X1) )
| ( p501(X1)
& p601(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p202(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p302(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p402(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p502(X1) )
| ( ! [X0] :
( p102(X0)
| ~ r1(X1,X0) )
& p602(X1) )
| ( p202(X1)
& p302(X1) )
| ( p202(X1)
& p402(X1) )
| ( p202(X1)
& p502(X1) )
| ( p202(X1)
& p602(X1) )
| ( p302(X1)
& p402(X1) )
| ( p302(X1)
& p502(X1) )
| ( p302(X1)
& p602(X1) )
| ( p402(X1)
& p502(X1) )
| ( p402(X1)
& p602(X1) )
| ( p502(X1)
& p602(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p203(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p303(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p403(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p503(X1) )
| ( ! [X0] :
( p103(X0)
| ~ r1(X1,X0) )
& p603(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p303(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p403(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p503(X1) )
| ( ! [X0] :
( p203(X0)
| ~ r1(X1,X0) )
& p603(X1) )
| ( p303(X1)
& p403(X1) )
| ( p303(X1)
& p503(X1) )
| ( p303(X1)
& p603(X1) )
| ( p403(X1)
& p503(X1) )
| ( p403(X1)
& p603(X1) )
| ( p503(X1)
& p603(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p204(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p304(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p104(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p304(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p204(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p404(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p504(X1) )
| ( ! [X0] :
( p304(X0)
| ~ r1(X1,X0) )
& p604(X1) )
| ( p404(X1)
& p504(X1) )
| ( p404(X1)
& p604(X1) )
| ( p504(X1)
& p604(X1) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p205(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p305(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p105(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p305(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p205(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& ! [X0] :
( p405(X0)
| ~ r1(X1,X0) ) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p305(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( ! [X0] :
( p405(X0)
| ~ r1(X1,X0) )
& p505(X1) )
| ( ! [X0] :
( p405(X0)
| ~ r1(X1,X0) )
& p605(X1) )
| ( p505(X1)
& p605(X1) ) )
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ( ( p101(X0)
| ! [X61] :
( p102(X61)
| ~ r1(X0,X61) )
| ! [X60] :
( p103(X60)
| ~ r1(X0,X60) )
| ! [X59] :
( p104(X59)
| ~ r1(X0,X59) )
| ! [X58] :
( p105(X58)
| ~ r1(X0,X58) ) )
& ( p201(X0)
| p202(X0)
| ! [X57] :
( p203(X57)
| ~ r1(X0,X57) )
| ! [X56] :
( p204(X56)
| ~ r1(X0,X56) )
| ! [X55] :
( p205(X55)
| ~ r1(X0,X55) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X54] :
( p304(X54)
| ~ r1(X0,X54) )
| ! [X53] :
( p305(X53)
| ~ r1(X0,X53) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X52] :
( p405(X52)
| ~ r1(X0,X52) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) ) )
| ~ ! [X1] :
( ~ ( ( p101(X1)
& p201(X1) )
| ( p101(X1)
& p301(X1) )
| ( p101(X1)
& p401(X1) )
| ( p101(X1)
& p501(X1) )
| ( p101(X1)
& p601(X1) )
| ( p201(X1)
& p301(X1) )
| ( p201(X1)
& p401(X1) )
| ( p201(X1)
& p501(X1) )
| ( p201(X1)
& p601(X1) )
| ( p301(X1)
& p401(X1) )
| ( p301(X1)
& p501(X1) )
| ( p301(X1)
& p601(X1) )
| ( p401(X1)
& p501(X1) )
| ( p401(X1)
& p601(X1) )
| ( p501(X1)
& p601(X1) )
| ( ! [X51] :
( p102(X51)
| ~ r1(X1,X51) )
& p202(X1) )
| ( ! [X50] :
( p102(X50)
| ~ r1(X1,X50) )
& p302(X1) )
| ( ! [X49] :
( p102(X49)
| ~ r1(X1,X49) )
& p402(X1) )
| ( ! [X48] :
( p102(X48)
| ~ r1(X1,X48) )
& p502(X1) )
| ( ! [X47] :
( p102(X47)
| ~ r1(X1,X47) )
& p602(X1) )
| ( p202(X1)
& p302(X1) )
| ( p202(X1)
& p402(X1) )
| ( p202(X1)
& p502(X1) )
| ( p202(X1)
& p602(X1) )
| ( p302(X1)
& p402(X1) )
| ( p302(X1)
& p502(X1) )
| ( p302(X1)
& p602(X1) )
| ( p402(X1)
& p502(X1) )
| ( p402(X1)
& p602(X1) )
| ( p502(X1)
& p602(X1) )
| ( ! [X46] :
( p103(X46)
| ~ r1(X1,X46) )
& ! [X45] :
( p203(X45)
| ~ r1(X1,X45) ) )
| ( ! [X44] :
( p103(X44)
| ~ r1(X1,X44) )
& p303(X1) )
| ( ! [X43] :
( p103(X43)
| ~ r1(X1,X43) )
& p403(X1) )
| ( ! [X42] :
( p103(X42)
| ~ r1(X1,X42) )
& p503(X1) )
| ( ! [X41] :
( p103(X41)
| ~ r1(X1,X41) )
& p603(X1) )
| ( ! [X40] :
( p203(X40)
| ~ r1(X1,X40) )
& p303(X1) )
| ( ! [X39] :
( p203(X39)
| ~ r1(X1,X39) )
& p403(X1) )
| ( ! [X38] :
( p203(X38)
| ~ r1(X1,X38) )
& p503(X1) )
| ( ! [X37] :
( p203(X37)
| ~ r1(X1,X37) )
& p603(X1) )
| ( p303(X1)
& p403(X1) )
| ( p303(X1)
& p503(X1) )
| ( p303(X1)
& p603(X1) )
| ( p403(X1)
& p503(X1) )
| ( p403(X1)
& p603(X1) )
| ( p503(X1)
& p603(X1) )
| ( ! [X36] :
( p104(X36)
| ~ r1(X1,X36) )
& ! [X35] :
( p204(X35)
| ~ r1(X1,X35) ) )
| ( ! [X34] :
( p104(X34)
| ~ r1(X1,X34) )
& ! [X33] :
( p304(X33)
| ~ r1(X1,X33) ) )
| ( ! [X32] :
( p104(X32)
| ~ r1(X1,X32) )
& p404(X1) )
| ( ! [X31] :
( p104(X31)
| ~ r1(X1,X31) )
& p504(X1) )
| ( ! [X30] :
( p104(X30)
| ~ r1(X1,X30) )
& p604(X1) )
| ( ! [X29] :
( p204(X29)
| ~ r1(X1,X29) )
& ! [X28] :
( p304(X28)
| ~ r1(X1,X28) ) )
| ( ! [X27] :
( p204(X27)
| ~ r1(X1,X27) )
& p404(X1) )
| ( ! [X26] :
( p204(X26)
| ~ r1(X1,X26) )
& p504(X1) )
| ( ! [X25] :
( p204(X25)
| ~ r1(X1,X25) )
& p604(X1) )
| ( ! [X24] :
( p304(X24)
| ~ r1(X1,X24) )
& p404(X1) )
| ( ! [X23] :
( p304(X23)
| ~ r1(X1,X23) )
& p504(X1) )
| ( ! [X22] :
( p304(X22)
| ~ r1(X1,X22) )
& p604(X1) )
| ( p404(X1)
& p504(X1) )
| ( p404(X1)
& p604(X1) )
| ( p504(X1)
& p604(X1) )
| ( ! [X21] :
( p105(X21)
| ~ r1(X1,X21) )
& ! [X20] :
( p205(X20)
| ~ r1(X1,X20) ) )
| ( ! [X19] :
( p105(X19)
| ~ r1(X1,X19) )
& ! [X18] :
( p305(X18)
| ~ r1(X1,X18) ) )
| ( ! [X17] :
( p105(X17)
| ~ r1(X1,X17) )
& ! [X16] :
( p405(X16)
| ~ r1(X1,X16) ) )
| ( ! [X15] :
( p105(X15)
| ~ r1(X1,X15) )
& p505(X1) )
| ( ! [X14] :
( p105(X14)
| ~ r1(X1,X14) )
& p605(X1) )
| ( ! [X13] :
( p205(X13)
| ~ r1(X1,X13) )
& ! [X12] :
( p305(X12)
| ~ r1(X1,X12) ) )
| ( ! [X11] :
( p205(X11)
| ~ r1(X1,X11) )
& ! [X10] :
( p405(X10)
| ~ r1(X1,X10) ) )
| ( ! [X9] :
( p205(X9)
| ~ r1(X1,X9) )
& p505(X1) )
| ( ! [X8] :
( p205(X8)
| ~ r1(X1,X8) )
& p605(X1) )
| ( ! [X7] :
( p305(X7)
| ~ r1(X1,X7) )
& ! [X6] :
( p405(X6)
| ~ r1(X1,X6) ) )
| ( ! [X5] :
( p305(X5)
| ~ r1(X1,X5) )
& p505(X1) )
| ( ! [X4] :
( p305(X4)
| ~ r1(X1,X4) )
& p605(X1) )
| ( ! [X3] :
( p405(X3)
| ~ r1(X1,X3) )
& p505(X1) )
| ( ! [X2] :
( p405(X2)
| ~ r1(X1,X2) )
& p605(X1) )
| ( p505(X1)
& p605(X1) ) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ( ( p101(X0)
| ! [X61] :
( p102(X61)
| ~ r1(X0,X61) )
| ! [X60] :
( p103(X60)
| ~ r1(X0,X60) )
| ! [X59] :
( p104(X59)
| ~ r1(X0,X59) )
| ! [X58] :
( p105(X58)
| ~ r1(X0,X58) ) )
& ( p201(X0)
| p202(X0)
| ! [X57] :
( p203(X57)
| ~ r1(X0,X57) )
| ! [X56] :
( p204(X56)
| ~ r1(X0,X56) )
| ! [X55] :
( p205(X55)
| ~ r1(X0,X55) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X54] :
( p304(X54)
| ~ r1(X0,X54) )
| ! [X53] :
( p305(X53)
| ~ r1(X0,X53) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X52] :
( p405(X52)
| ~ r1(X0,X52) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) ) )
| ~ ! [X1] :
( ~ ( ( p101(X1)
& p201(X1) )
| ( p101(X1)
& p301(X1) )
| ( p101(X1)
& p401(X1) )
| ( p101(X1)
& p501(X1) )
| ( p101(X1)
& p601(X1) )
| ( p201(X1)
& p301(X1) )
| ( p201(X1)
& p401(X1) )
| ( p201(X1)
& p501(X1) )
| ( p201(X1)
& p601(X1) )
| ( p301(X1)
& p401(X1) )
| ( p301(X1)
& p501(X1) )
| ( p301(X1)
& p601(X1) )
| ( p401(X1)
& p501(X1) )
| ( p401(X1)
& p601(X1) )
| ( p501(X1)
& p601(X1) )
| ( ! [X51] :
( p102(X51)
| ~ r1(X1,X51) )
& p202(X1) )
| ( ! [X50] :
( p102(X50)
| ~ r1(X1,X50) )
& p302(X1) )
| ( ! [X49] :
( p102(X49)
| ~ r1(X1,X49) )
& p402(X1) )
| ( ! [X48] :
( p102(X48)
| ~ r1(X1,X48) )
& p502(X1) )
| ( ! [X47] :
( p102(X47)
| ~ r1(X1,X47) )
& p602(X1) )
| ( p202(X1)
& p302(X1) )
| ( p202(X1)
& p402(X1) )
| ( p202(X1)
& p502(X1) )
| ( p202(X1)
& p602(X1) )
| ( p302(X1)
& p402(X1) )
| ( p302(X1)
& p502(X1) )
| ( p302(X1)
& p602(X1) )
| ( p402(X1)
& p502(X1) )
| ( p402(X1)
& p602(X1) )
| ( p502(X1)
& p602(X1) )
| ( ! [X46] :
( p103(X46)
| ~ r1(X1,X46) )
& ! [X45] :
( p203(X45)
| ~ r1(X1,X45) ) )
| ( ! [X44] :
( p103(X44)
| ~ r1(X1,X44) )
& p303(X1) )
| ( ! [X43] :
( p103(X43)
| ~ r1(X1,X43) )
& p403(X1) )
| ( ! [X42] :
( p103(X42)
| ~ r1(X1,X42) )
& p503(X1) )
| ( ! [X41] :
( p103(X41)
| ~ r1(X1,X41) )
& p603(X1) )
| ( ! [X40] :
( p203(X40)
| ~ r1(X1,X40) )
& p303(X1) )
| ( ! [X39] :
( p203(X39)
| ~ r1(X1,X39) )
& p403(X1) )
| ( ! [X38] :
( p203(X38)
| ~ r1(X1,X38) )
& p503(X1) )
| ( ! [X37] :
( p203(X37)
| ~ r1(X1,X37) )
& p603(X1) )
| ( p303(X1)
& p403(X1) )
| ( p303(X1)
& p503(X1) )
| ( p303(X1)
& p603(X1) )
| ( p403(X1)
& p503(X1) )
| ( p403(X1)
& p603(X1) )
| ( p503(X1)
& p603(X1) )
| ( ! [X36] :
( p104(X36)
| ~ r1(X1,X36) )
& ! [X35] :
( p204(X35)
| ~ r1(X1,X35) ) )
| ( ! [X34] :
( p104(X34)
| ~ r1(X1,X34) )
& ! [X33] :
( p304(X33)
| ~ r1(X1,X33) ) )
| ( ! [X32] :
( p104(X32)
| ~ r1(X1,X32) )
& p404(X1) )
| ( ! [X31] :
( p104(X31)
| ~ r1(X1,X31) )
& p504(X1) )
| ( ! [X30] :
( p104(X30)
| ~ r1(X1,X30) )
& p604(X1) )
| ( ! [X29] :
( p204(X29)
| ~ r1(X1,X29) )
& ! [X28] :
( p304(X28)
| ~ r1(X1,X28) ) )
| ( ! [X27] :
( p204(X27)
| ~ r1(X1,X27) )
& p404(X1) )
| ( ! [X26] :
( p204(X26)
| ~ r1(X1,X26) )
& p504(X1) )
| ( ! [X25] :
( p204(X25)
| ~ r1(X1,X25) )
& p604(X1) )
| ( ! [X24] :
( p304(X24)
| ~ r1(X1,X24) )
& p404(X1) )
| ( ! [X23] :
( p304(X23)
| ~ r1(X1,X23) )
& p504(X1) )
| ( ! [X22] :
( p304(X22)
| ~ r1(X1,X22) )
& p604(X1) )
| ( p404(X1)
& p504(X1) )
| ( p404(X1)
& p604(X1) )
| ( p504(X1)
& p604(X1) )
| ( ! [X21] :
( p105(X21)
| ~ r1(X1,X21) )
& ! [X20] :
( p205(X20)
| ~ r1(X1,X20) ) )
| ( ! [X19] :
( p105(X19)
| ~ r1(X1,X19) )
& ! [X18] :
( p305(X18)
| ~ r1(X1,X18) ) )
| ( ! [X17] :
( p105(X17)
| ~ r1(X1,X17) )
& ! [X16] :
( p405(X16)
| ~ r1(X1,X16) ) )
| ( ! [X15] :
( p105(X15)
| ~ r1(X1,X15) )
& p505(X1) )
| ( ! [X14] :
( p105(X14)
| ~ r1(X1,X14) )
& p605(X1) )
| ( ! [X13] :
( p205(X13)
| ~ r1(X1,X13) )
& ! [X12] :
( p305(X12)
| ~ r1(X1,X12) ) )
| ( ! [X11] :
( p205(X11)
| ~ r1(X1,X11) )
& ! [X10] :
( p405(X10)
| ~ r1(X1,X10) ) )
| ( ! [X9] :
( p205(X9)
| ~ r1(X1,X9) )
& p505(X1) )
| ( ! [X8] :
( p205(X8)
| ~ r1(X1,X8) )
& p605(X1) )
| ( ! [X7] :
( p305(X7)
| ~ r1(X1,X7) )
& ! [X6] :
( p405(X6)
| ~ r1(X1,X6) ) )
| ( ! [X5] :
( p305(X5)
| ~ r1(X1,X5) )
& p505(X1) )
| ( ! [X4] :
( p305(X4)
| ~ r1(X1,X4) )
& p605(X1) )
| ( ! [X3] :
( p405(X3)
| ~ r1(X1,X3) )
& p505(X1) )
| ( ! [X2] :
( p405(X2)
| ~ r1(X1,X2) )
& p605(X1) )
| ( p505(X1)
& p605(X1) ) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ( p101(X0)
| ! [X61] :
( p102(X61)
| ~ r1(X0,X61) )
| ! [X60] :
( p103(X60)
| ~ r1(X0,X60) )
| ! [X59] :
( p104(X59)
| ~ r1(X0,X59) )
| ! [X58] :
( p105(X58)
| ~ r1(X0,X58) ) )
& ( p201(X0)
| p202(X0)
| ! [X57] :
( p203(X57)
| ~ r1(X0,X57) )
| ! [X56] :
( p204(X56)
| ~ r1(X0,X56) )
| ! [X55] :
( p205(X55)
| ~ r1(X0,X55) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X54] :
( p304(X54)
| ~ r1(X0,X54) )
| ! [X53] :
( p305(X53)
| ~ r1(X0,X53) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X52] :
( p405(X52)
| ~ r1(X0,X52) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) )
& ! [X1] :
( ( ( ~ p101(X1)
| ~ p201(X1) )
& ( ~ p101(X1)
| ~ p301(X1) )
& ( ~ p101(X1)
| ~ p401(X1) )
& ( ~ p101(X1)
| ~ p501(X1) )
& ( ~ p101(X1)
| ~ p601(X1) )
& ( ~ p201(X1)
| ~ p301(X1) )
& ( ~ p201(X1)
| ~ p401(X1) )
& ( ~ p201(X1)
| ~ p501(X1) )
& ( ~ p201(X1)
| ~ p601(X1) )
& ( ~ p301(X1)
| ~ p401(X1) )
& ( ~ p301(X1)
| ~ p501(X1) )
& ( ~ p301(X1)
| ~ p601(X1) )
& ( ~ p401(X1)
| ~ p501(X1) )
& ( ~ p401(X1)
| ~ p601(X1) )
& ( ~ p501(X1)
| ~ p601(X1) )
& ( ? [X51] :
( ~ p102(X51)
& r1(X1,X51) )
| ~ p202(X1) )
& ( ? [X50] :
( ~ p102(X50)
& r1(X1,X50) )
| ~ p302(X1) )
& ( ? [X49] :
( ~ p102(X49)
& r1(X1,X49) )
| ~ p402(X1) )
& ( ? [X48] :
( ~ p102(X48)
& r1(X1,X48) )
| ~ p502(X1) )
& ( ? [X47] :
( ~ p102(X47)
& r1(X1,X47) )
| ~ p602(X1) )
& ( ~ p202(X1)
| ~ p302(X1) )
& ( ~ p202(X1)
| ~ p402(X1) )
& ( ~ p202(X1)
| ~ p502(X1) )
& ( ~ p202(X1)
| ~ p602(X1) )
& ( ~ p302(X1)
| ~ p402(X1) )
& ( ~ p302(X1)
| ~ p502(X1) )
& ( ~ p302(X1)
| ~ p602(X1) )
& ( ~ p402(X1)
| ~ p502(X1) )
& ( ~ p402(X1)
| ~ p602(X1) )
& ( ~ p502(X1)
| ~ p602(X1) )
& ( ? [X46] :
( ~ p103(X46)
& r1(X1,X46) )
| ? [X45] :
( ~ p203(X45)
& r1(X1,X45) ) )
& ( ? [X44] :
( ~ p103(X44)
& r1(X1,X44) )
| ~ p303(X1) )
& ( ? [X43] :
( ~ p103(X43)
& r1(X1,X43) )
| ~ p403(X1) )
& ( ? [X42] :
( ~ p103(X42)
& r1(X1,X42) )
| ~ p503(X1) )
& ( ? [X41] :
( ~ p103(X41)
& r1(X1,X41) )
| ~ p603(X1) )
& ( ? [X40] :
( ~ p203(X40)
& r1(X1,X40) )
| ~ p303(X1) )
& ( ? [X39] :
( ~ p203(X39)
& r1(X1,X39) )
| ~ p403(X1) )
& ( ? [X38] :
( ~ p203(X38)
& r1(X1,X38) )
| ~ p503(X1) )
& ( ? [X37] :
( ~ p203(X37)
& r1(X1,X37) )
| ~ p603(X1) )
& ( ~ p303(X1)
| ~ p403(X1) )
& ( ~ p303(X1)
| ~ p503(X1) )
& ( ~ p303(X1)
| ~ p603(X1) )
& ( ~ p403(X1)
| ~ p503(X1) )
& ( ~ p403(X1)
| ~ p603(X1) )
& ( ~ p503(X1)
| ~ p603(X1) )
& ( ? [X36] :
( ~ p104(X36)
& r1(X1,X36) )
| ? [X35] :
( ~ p204(X35)
& r1(X1,X35) ) )
& ( ? [X34] :
( ~ p104(X34)
& r1(X1,X34) )
| ? [X33] :
( ~ p304(X33)
& r1(X1,X33) ) )
& ( ? [X32] :
( ~ p104(X32)
& r1(X1,X32) )
| ~ p404(X1) )
& ( ? [X31] :
( ~ p104(X31)
& r1(X1,X31) )
| ~ p504(X1) )
& ( ? [X30] :
( ~ p104(X30)
& r1(X1,X30) )
| ~ p604(X1) )
& ( ? [X29] :
( ~ p204(X29)
& r1(X1,X29) )
| ? [X28] :
( ~ p304(X28)
& r1(X1,X28) ) )
& ( ? [X27] :
( ~ p204(X27)
& r1(X1,X27) )
| ~ p404(X1) )
& ( ? [X26] :
( ~ p204(X26)
& r1(X1,X26) )
| ~ p504(X1) )
& ( ? [X25] :
( ~ p204(X25)
& r1(X1,X25) )
| ~ p604(X1) )
& ( ? [X24] :
( ~ p304(X24)
& r1(X1,X24) )
| ~ p404(X1) )
& ( ? [X23] :
( ~ p304(X23)
& r1(X1,X23) )
| ~ p504(X1) )
& ( ? [X22] :
( ~ p304(X22)
& r1(X1,X22) )
| ~ p604(X1) )
& ( ~ p404(X1)
| ~ p504(X1) )
& ( ~ p404(X1)
| ~ p604(X1) )
& ( ~ p504(X1)
| ~ p604(X1) )
& ( ? [X21] :
( ~ p105(X21)
& r1(X1,X21) )
| ? [X20] :
( ~ p205(X20)
& r1(X1,X20) ) )
& ( ? [X19] :
( ~ p105(X19)
& r1(X1,X19) )
| ? [X18] :
( ~ p305(X18)
& r1(X1,X18) ) )
& ( ? [X17] :
( ~ p105(X17)
& r1(X1,X17) )
| ? [X16] :
( ~ p405(X16)
& r1(X1,X16) ) )
& ( ? [X15] :
( ~ p105(X15)
& r1(X1,X15) )
| ~ p505(X1) )
& ( ? [X14] :
( ~ p105(X14)
& r1(X1,X14) )
| ~ p605(X1) )
& ( ? [X13] :
( ~ p205(X13)
& r1(X1,X13) )
| ? [X12] :
( ~ p305(X12)
& r1(X1,X12) ) )
& ( ? [X11] :
( ~ p205(X11)
& r1(X1,X11) )
| ? [X10] :
( ~ p405(X10)
& r1(X1,X10) ) )
& ( ? [X9] :
( ~ p205(X9)
& r1(X1,X9) )
| ~ p505(X1) )
& ( ? [X8] :
( ~ p205(X8)
& r1(X1,X8) )
| ~ p605(X1) )
& ( ? [X7] :
( ~ p305(X7)
& r1(X1,X7) )
| ? [X6] :
( ~ p405(X6)
& r1(X1,X6) ) )
& ( ? [X5] :
( ~ p305(X5)
& r1(X1,X5) )
| ~ p505(X1) )
& ( ? [X4] :
( ~ p305(X4)
& r1(X1,X4) )
| ~ p605(X1) )
& ( ? [X3] :
( ~ p405(X3)
& r1(X1,X3) )
| ~ p505(X1) )
& ( ? [X2] :
( ~ p405(X2)
& r1(X1,X2) )
| ~ p605(X1) )
& ( ~ p505(X1)
| ~ p605(X1) ) )
| ~ r1(X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ( p101(X0)
| ! [X61] :
( p102(X61)
| ~ r1(X0,X61) )
| ! [X60] :
( p103(X60)
| ~ r1(X0,X60) )
| ! [X59] :
( p104(X59)
| ~ r1(X0,X59) )
| ! [X58] :
( p105(X58)
| ~ r1(X0,X58) ) )
& ( p201(X0)
| p202(X0)
| ! [X57] :
( p203(X57)
| ~ r1(X0,X57) )
| ! [X56] :
( p204(X56)
| ~ r1(X0,X56) )
| ! [X55] :
( p205(X55)
| ~ r1(X0,X55) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X54] :
( p304(X54)
| ~ r1(X0,X54) )
| ! [X53] :
( p305(X53)
| ~ r1(X0,X53) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X52] :
( p405(X52)
| ~ r1(X0,X52) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) )
& ! [X1] :
( ( ( ~ p101(X1)
| ~ p201(X1) )
& ( ~ p101(X1)
| ~ p301(X1) )
& ( ~ p101(X1)
| ~ p401(X1) )
& ( ~ p101(X1)
| ~ p501(X1) )
& ( ~ p101(X1)
| ~ p601(X1) )
& ( ~ p201(X1)
| ~ p301(X1) )
& ( ~ p201(X1)
| ~ p401(X1) )
& ( ~ p201(X1)
| ~ p501(X1) )
& ( ~ p201(X1)
| ~ p601(X1) )
& ( ~ p301(X1)
| ~ p401(X1) )
& ( ~ p301(X1)
| ~ p501(X1) )
& ( ~ p301(X1)
| ~ p601(X1) )
& ( ~ p401(X1)
| ~ p501(X1) )
& ( ~ p401(X1)
| ~ p601(X1) )
& ( ~ p501(X1)
| ~ p601(X1) )
& ( ? [X51] :
( ~ p102(X51)
& r1(X1,X51) )
| ~ p202(X1) )
& ( ? [X50] :
( ~ p102(X50)
& r1(X1,X50) )
| ~ p302(X1) )
& ( ? [X49] :
( ~ p102(X49)
& r1(X1,X49) )
| ~ p402(X1) )
& ( ? [X48] :
( ~ p102(X48)
& r1(X1,X48) )
| ~ p502(X1) )
& ( ? [X47] :
( ~ p102(X47)
& r1(X1,X47) )
| ~ p602(X1) )
& ( ~ p202(X1)
| ~ p302(X1) )
& ( ~ p202(X1)
| ~ p402(X1) )
& ( ~ p202(X1)
| ~ p502(X1) )
& ( ~ p202(X1)
| ~ p602(X1) )
& ( ~ p302(X1)
| ~ p402(X1) )
& ( ~ p302(X1)
| ~ p502(X1) )
& ( ~ p302(X1)
| ~ p602(X1) )
& ( ~ p402(X1)
| ~ p502(X1) )
& ( ~ p402(X1)
| ~ p602(X1) )
& ( ~ p502(X1)
| ~ p602(X1) )
& ( ? [X46] :
( ~ p103(X46)
& r1(X1,X46) )
| ? [X45] :
( ~ p203(X45)
& r1(X1,X45) ) )
& ( ? [X44] :
( ~ p103(X44)
& r1(X1,X44) )
| ~ p303(X1) )
& ( ? [X43] :
( ~ p103(X43)
& r1(X1,X43) )
| ~ p403(X1) )
& ( ? [X42] :
( ~ p103(X42)
& r1(X1,X42) )
| ~ p503(X1) )
& ( ? [X41] :
( ~ p103(X41)
& r1(X1,X41) )
| ~ p603(X1) )
& ( ? [X40] :
( ~ p203(X40)
& r1(X1,X40) )
| ~ p303(X1) )
& ( ? [X39] :
( ~ p203(X39)
& r1(X1,X39) )
| ~ p403(X1) )
& ( ? [X38] :
( ~ p203(X38)
& r1(X1,X38) )
| ~ p503(X1) )
& ( ? [X37] :
( ~ p203(X37)
& r1(X1,X37) )
| ~ p603(X1) )
& ( ~ p303(X1)
| ~ p403(X1) )
& ( ~ p303(X1)
| ~ p503(X1) )
& ( ~ p303(X1)
| ~ p603(X1) )
& ( ~ p403(X1)
| ~ p503(X1) )
& ( ~ p403(X1)
| ~ p603(X1) )
& ( ~ p503(X1)
| ~ p603(X1) )
& ( ? [X36] :
( ~ p104(X36)
& r1(X1,X36) )
| ? [X35] :
( ~ p204(X35)
& r1(X1,X35) ) )
& ( ? [X34] :
( ~ p104(X34)
& r1(X1,X34) )
| ? [X33] :
( ~ p304(X33)
& r1(X1,X33) ) )
& ( ? [X32] :
( ~ p104(X32)
& r1(X1,X32) )
| ~ p404(X1) )
& ( ? [X31] :
( ~ p104(X31)
& r1(X1,X31) )
| ~ p504(X1) )
& ( ? [X30] :
( ~ p104(X30)
& r1(X1,X30) )
| ~ p604(X1) )
& ( ? [X29] :
( ~ p204(X29)
& r1(X1,X29) )
| ? [X28] :
( ~ p304(X28)
& r1(X1,X28) ) )
& ( ? [X27] :
( ~ p204(X27)
& r1(X1,X27) )
| ~ p404(X1) )
& ( ? [X26] :
( ~ p204(X26)
& r1(X1,X26) )
| ~ p504(X1) )
& ( ? [X25] :
( ~ p204(X25)
& r1(X1,X25) )
| ~ p604(X1) )
& ( ? [X24] :
( ~ p304(X24)
& r1(X1,X24) )
| ~ p404(X1) )
& ( ? [X23] :
( ~ p304(X23)
& r1(X1,X23) )
| ~ p504(X1) )
& ( ? [X22] :
( ~ p304(X22)
& r1(X1,X22) )
| ~ p604(X1) )
& ( ~ p404(X1)
| ~ p504(X1) )
& ( ~ p404(X1)
| ~ p604(X1) )
& ( ~ p504(X1)
| ~ p604(X1) )
& ( ? [X21] :
( ~ p105(X21)
& r1(X1,X21) )
| ? [X20] :
( ~ p205(X20)
& r1(X1,X20) ) )
& ( ? [X19] :
( ~ p105(X19)
& r1(X1,X19) )
| ? [X18] :
( ~ p305(X18)
& r1(X1,X18) ) )
& ( ? [X17] :
( ~ p105(X17)
& r1(X1,X17) )
| ? [X16] :
( ~ p405(X16)
& r1(X1,X16) ) )
& ( ? [X15] :
( ~ p105(X15)
& r1(X1,X15) )
| ~ p505(X1) )
& ( ? [X14] :
( ~ p105(X14)
& r1(X1,X14) )
| ~ p605(X1) )
& ( ? [X13] :
( ~ p205(X13)
& r1(X1,X13) )
| ? [X12] :
( ~ p305(X12)
& r1(X1,X12) ) )
& ( ? [X11] :
( ~ p205(X11)
& r1(X1,X11) )
| ? [X10] :
( ~ p405(X10)
& r1(X1,X10) ) )
& ( ? [X9] :
( ~ p205(X9)
& r1(X1,X9) )
| ~ p505(X1) )
& ( ? [X8] :
( ~ p205(X8)
& r1(X1,X8) )
| ~ p605(X1) )
& ( ? [X7] :
( ~ p305(X7)
& r1(X1,X7) )
| ? [X6] :
( ~ p405(X6)
& r1(X1,X6) ) )
& ( ? [X5] :
( ~ p305(X5)
& r1(X1,X5) )
| ~ p505(X1) )
& ( ? [X4] :
( ~ p305(X4)
& r1(X1,X4) )
| ~ p605(X1) )
& ( ? [X3] :
( ~ p405(X3)
& r1(X1,X3) )
| ~ p505(X1) )
& ( ? [X2] :
( ~ p405(X2)
& r1(X1,X2) )
| ~ p605(X1) )
& ( ~ p505(X1)
| ~ p605(X1) ) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f6]) ).
fof(f50,plain,
! [X1] :
( ~ sP40(X1)
| ( ( ~ p101(X1)
| ~ p201(X1) )
& ( ~ p101(X1)
| ~ p301(X1) )
& ( ~ p101(X1)
| ~ p401(X1) )
& ( ~ p101(X1)
| ~ p501(X1) )
& ( ~ p101(X1)
| ~ p601(X1) )
& ( ~ p201(X1)
| ~ p301(X1) )
& ( ~ p201(X1)
| ~ p401(X1) )
& ( ~ p201(X1)
| ~ p501(X1) )
& ( ~ p201(X1)
| ~ p601(X1) )
& ( ~ p301(X1)
| ~ p401(X1) )
& ( ~ p301(X1)
| ~ p501(X1) )
& ( ~ p301(X1)
| ~ p601(X1) )
& ( ~ p401(X1)
| ~ p501(X1) )
& ( ~ p401(X1)
| ~ p601(X1) )
& ( ~ p501(X1)
| ~ p601(X1) )
& sP10(X1)
& sP11(X1)
& sP12(X1)
& sP13(X1)
& sP14(X1)
& ( ~ p202(X1)
| ~ p302(X1) )
& ( ~ p202(X1)
| ~ p402(X1) )
& ( ~ p202(X1)
| ~ p502(X1) )
& ( ~ p202(X1)
| ~ p602(X1) )
& ( ~ p302(X1)
| ~ p402(X1) )
& ( ~ p302(X1)
| ~ p502(X1) )
& ( ~ p302(X1)
| ~ p602(X1) )
& ( ~ p402(X1)
| ~ p502(X1) )
& ( ~ p402(X1)
| ~ p602(X1) )
& ( ~ p502(X1)
| ~ p602(X1) )
& sP0(X1)
& sP15(X1)
& sP16(X1)
& sP17(X1)
& sP18(X1)
& sP19(X1)
& sP20(X1)
& sP21(X1)
& sP22(X1)
& ( ~ p303(X1)
| ~ p403(X1) )
& ( ~ p303(X1)
| ~ p503(X1) )
& ( ~ p303(X1)
| ~ p603(X1) )
& ( ~ p403(X1)
| ~ p503(X1) )
& ( ~ p403(X1)
| ~ p603(X1) )
& ( ~ p503(X1)
| ~ p603(X1) )
& sP1(X1)
& sP2(X1)
& sP23(X1)
& sP24(X1)
& sP25(X1)
& sP3(X1)
& sP26(X1)
& sP27(X1)
& sP28(X1)
& sP29(X1)
& sP30(X1)
& sP31(X1)
& ( ~ p404(X1)
| ~ p504(X1) )
& ( ~ p404(X1)
| ~ p604(X1) )
& ( ~ p504(X1)
| ~ p604(X1) )
& sP4(X1)
& sP5(X1)
& sP6(X1)
& sP32(X1)
& sP33(X1)
& sP7(X1)
& sP8(X1)
& sP34(X1)
& sP35(X1)
& sP9(X1)
& sP36(X1)
& sP37(X1)
& sP38(X1)
& sP39(X1)
& ( ~ p505(X1)
| ~ p605(X1) ) ) ),
inference(nnf_transformation,[],[f48]) ).
fof(f51,plain,
! [X0] :
( ~ sP40(X0)
| ( ( ~ p101(X0)
| ~ p201(X0) )
& ( ~ p101(X0)
| ~ p301(X0) )
& ( ~ p101(X0)
| ~ p401(X0) )
& ( ~ p101(X0)
| ~ p501(X0) )
& ( ~ p101(X0)
| ~ p601(X0) )
& ( ~ p201(X0)
| ~ p301(X0) )
& ( ~ p201(X0)
| ~ p401(X0) )
& ( ~ p201(X0)
| ~ p501(X0) )
& ( ~ p201(X0)
| ~ p601(X0) )
& ( ~ p301(X0)
| ~ p401(X0) )
& ( ~ p301(X0)
| ~ p501(X0) )
& ( ~ p301(X0)
| ~ p601(X0) )
& ( ~ p401(X0)
| ~ p501(X0) )
& ( ~ p401(X0)
| ~ p601(X0) )
& ( ~ p501(X0)
| ~ p601(X0) )
& sP10(X0)
& sP11(X0)
& sP12(X0)
& sP13(X0)
& sP14(X0)
& ( ~ p202(X0)
| ~ p302(X0) )
& ( ~ p202(X0)
| ~ p402(X0) )
& ( ~ p202(X0)
| ~ p502(X0) )
& ( ~ p202(X0)
| ~ p602(X0) )
& ( ~ p302(X0)
| ~ p402(X0) )
& ( ~ p302(X0)
| ~ p502(X0) )
& ( ~ p302(X0)
| ~ p602(X0) )
& ( ~ p402(X0)
| ~ p502(X0) )
& ( ~ p402(X0)
| ~ p602(X0) )
& ( ~ p502(X0)
| ~ p602(X0) )
& sP0(X0)
& sP15(X0)
& sP16(X0)
& sP17(X0)
& sP18(X0)
& sP19(X0)
& sP20(X0)
& sP21(X0)
& sP22(X0)
& ( ~ p303(X0)
| ~ p403(X0) )
& ( ~ p303(X0)
| ~ p503(X0) )
& ( ~ p303(X0)
| ~ p603(X0) )
& ( ~ p403(X0)
| ~ p503(X0) )
& ( ~ p403(X0)
| ~ p603(X0) )
& ( ~ p503(X0)
| ~ p603(X0) )
& sP1(X0)
& sP2(X0)
& sP23(X0)
& sP24(X0)
& sP25(X0)
& sP3(X0)
& sP26(X0)
& sP27(X0)
& sP28(X0)
& sP29(X0)
& sP30(X0)
& sP31(X0)
& ( ~ p404(X0)
| ~ p504(X0) )
& ( ~ p404(X0)
| ~ p604(X0) )
& ( ~ p504(X0)
| ~ p604(X0) )
& sP4(X0)
& sP5(X0)
& sP6(X0)
& sP32(X0)
& sP33(X0)
& sP7(X0)
& sP8(X0)
& sP34(X0)
& sP35(X0)
& sP9(X0)
& sP36(X0)
& sP37(X0)
& sP38(X0)
& sP39(X0)
& ( ~ p505(X0)
| ~ p605(X0) ) ) ),
inference(rectify,[],[f50]) ).
fof(f52,plain,
! [X1] :
( ~ sP39(X1)
| ? [X2] :
( ~ p405(X2)
& r1(X1,X2) )
| ~ p605(X1) ),
inference(nnf_transformation,[],[f47]) ).
fof(f53,plain,
! [X0] :
( ~ sP39(X0)
| ? [X1] :
( ~ p405(X1)
& r1(X0,X1) )
| ~ p605(X0) ),
inference(rectify,[],[f52]) ).
fof(f54,plain,
! [X0] :
( ~ sP39(X0)
| ( ~ p405(sK41(X0))
& r1(X0,sK41(X0)) )
| ~ p605(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X1,sK41(X0))],[f53]) ).
fof(f55,plain,
! [X1] :
( ~ sP38(X1)
| ? [X3] :
( ~ p405(X3)
& r1(X1,X3) )
| ~ p505(X1) ),
inference(nnf_transformation,[],[f46]) ).
fof(f56,plain,
! [X0] :
( ~ sP38(X0)
| ? [X1] :
( ~ p405(X1)
& r1(X0,X1) )
| ~ p505(X0) ),
inference(rectify,[],[f55]) ).
fof(f57,plain,
! [X0] :
( ~ sP38(X0)
| ( ~ p405(sK42(X0))
& r1(X0,sK42(X0)) )
| ~ p505(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X1,sK42(X0))],[f56]) ).
fof(f58,plain,
! [X1] :
( ~ sP37(X1)
| ? [X4] :
( ~ p305(X4)
& r1(X1,X4) )
| ~ p605(X1) ),
inference(nnf_transformation,[],[f45]) ).
fof(f59,plain,
! [X0] :
( ~ sP37(X0)
| ? [X1] :
( ~ p305(X1)
& r1(X0,X1) )
| ~ p605(X0) ),
inference(rectify,[],[f58]) ).
fof(f60,plain,
! [X0] :
( ~ sP37(X0)
| ( ~ p305(sK43(X0))
& r1(X0,sK43(X0)) )
| ~ p605(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X1,sK43(X0))],[f59]) ).
fof(f61,plain,
! [X1] :
( ~ sP36(X1)
| ? [X5] :
( ~ p305(X5)
& r1(X1,X5) )
| ~ p505(X1) ),
inference(nnf_transformation,[],[f44]) ).
fof(f62,plain,
! [X0] :
( ~ sP36(X0)
| ? [X1] :
( ~ p305(X1)
& r1(X0,X1) )
| ~ p505(X0) ),
inference(rectify,[],[f61]) ).
fof(f63,plain,
! [X0] :
( ~ sP36(X0)
| ( ~ p305(sK44(X0))
& r1(X0,sK44(X0)) )
| ~ p505(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X1,sK44(X0))],[f62]) ).
fof(f64,plain,
! [X1] :
( ~ sP35(X1)
| ? [X8] :
( ~ p205(X8)
& r1(X1,X8) )
| ~ p605(X1) ),
inference(nnf_transformation,[],[f43]) ).
fof(f65,plain,
! [X0] :
( ~ sP35(X0)
| ? [X1] :
( ~ p205(X1)
& r1(X0,X1) )
| ~ p605(X0) ),
inference(rectify,[],[f64]) ).
fof(f66,plain,
! [X0] :
( ~ sP35(X0)
| ( ~ p205(sK45(X0))
& r1(X0,sK45(X0)) )
| ~ p605(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X1,sK45(X0))],[f65]) ).
fof(f67,plain,
! [X1] :
( ~ sP34(X1)
| ? [X9] :
( ~ p205(X9)
& r1(X1,X9) )
| ~ p505(X1) ),
inference(nnf_transformation,[],[f42]) ).
fof(f68,plain,
! [X0] :
( ~ sP34(X0)
| ? [X1] :
( ~ p205(X1)
& r1(X0,X1) )
| ~ p505(X0) ),
inference(rectify,[],[f67]) ).
fof(f69,plain,
! [X0] :
( ~ sP34(X0)
| ( ~ p205(sK46(X0))
& r1(X0,sK46(X0)) )
| ~ p505(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X1,sK46(X0))],[f68]) ).
fof(f70,plain,
! [X1] :
( ~ sP33(X1)
| ? [X14] :
( ~ p105(X14)
& r1(X1,X14) )
| ~ p605(X1) ),
inference(nnf_transformation,[],[f41]) ).
fof(f71,plain,
! [X0] :
( ~ sP33(X0)
| ? [X1] :
( ~ p105(X1)
& r1(X0,X1) )
| ~ p605(X0) ),
inference(rectify,[],[f70]) ).
fof(f72,plain,
! [X0] :
( ~ sP33(X0)
| ( ~ p105(sK47(X0))
& r1(X0,sK47(X0)) )
| ~ p605(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(X1,sK47(X0))],[f71]) ).
fof(f73,plain,
! [X1] :
( ~ sP32(X1)
| ? [X15] :
( ~ p105(X15)
& r1(X1,X15) )
| ~ p505(X1) ),
inference(nnf_transformation,[],[f40]) ).
fof(f74,plain,
! [X0] :
( ~ sP32(X0)
| ? [X1] :
( ~ p105(X1)
& r1(X0,X1) )
| ~ p505(X0) ),
inference(rectify,[],[f73]) ).
fof(f75,plain,
! [X0] :
( ~ sP32(X0)
| ( ~ p105(sK48(X0))
& r1(X0,sK48(X0)) )
| ~ p505(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(X1,sK48(X0))],[f74]) ).
fof(f76,plain,
! [X1] :
( ~ sP31(X1)
| ? [X22] :
( ~ p304(X22)
& r1(X1,X22) )
| ~ p604(X1) ),
inference(nnf_transformation,[],[f39]) ).
fof(f77,plain,
! [X0] :
( ~ sP31(X0)
| ? [X1] :
( ~ p304(X1)
& r1(X0,X1) )
| ~ p604(X0) ),
inference(rectify,[],[f76]) ).
fof(f78,plain,
! [X0] :
( ~ sP31(X0)
| ( ~ p304(sK49(X0))
& r1(X0,sK49(X0)) )
| ~ p604(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(X1,sK49(X0))],[f77]) ).
fof(f79,plain,
! [X1] :
( ~ sP30(X1)
| ? [X23] :
( ~ p304(X23)
& r1(X1,X23) )
| ~ p504(X1) ),
inference(nnf_transformation,[],[f38]) ).
fof(f80,plain,
! [X0] :
( ~ sP30(X0)
| ? [X1] :
( ~ p304(X1)
& r1(X0,X1) )
| ~ p504(X0) ),
inference(rectify,[],[f79]) ).
fof(f81,plain,
! [X0] :
( ~ sP30(X0)
| ( ~ p304(sK50(X0))
& r1(X0,sK50(X0)) )
| ~ p504(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(X1,sK50(X0))],[f80]) ).
fof(f82,plain,
! [X1] :
( ~ sP29(X1)
| ? [X24] :
( ~ p304(X24)
& r1(X1,X24) )
| ~ p404(X1) ),
inference(nnf_transformation,[],[f37]) ).
fof(f83,plain,
! [X0] :
( ~ sP29(X0)
| ? [X1] :
( ~ p304(X1)
& r1(X0,X1) )
| ~ p404(X0) ),
inference(rectify,[],[f82]) ).
fof(f84,plain,
! [X0] :
( ~ sP29(X0)
| ( ~ p304(sK51(X0))
& r1(X0,sK51(X0)) )
| ~ p404(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X1,sK51(X0))],[f83]) ).
fof(f85,plain,
! [X1] :
( ~ sP28(X1)
| ? [X25] :
( ~ p204(X25)
& r1(X1,X25) )
| ~ p604(X1) ),
inference(nnf_transformation,[],[f36]) ).
fof(f86,plain,
! [X0] :
( ~ sP28(X0)
| ? [X1] :
( ~ p204(X1)
& r1(X0,X1) )
| ~ p604(X0) ),
inference(rectify,[],[f85]) ).
fof(f87,plain,
! [X0] :
( ~ sP28(X0)
| ( ~ p204(sK52(X0))
& r1(X0,sK52(X0)) )
| ~ p604(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(X1,sK52(X0))],[f86]) ).
fof(f88,plain,
! [X1] :
( ~ sP27(X1)
| ? [X26] :
( ~ p204(X26)
& r1(X1,X26) )
| ~ p504(X1) ),
inference(nnf_transformation,[],[f35]) ).
fof(f89,plain,
! [X0] :
( ~ sP27(X0)
| ? [X1] :
( ~ p204(X1)
& r1(X0,X1) )
| ~ p504(X0) ),
inference(rectify,[],[f88]) ).
fof(f90,plain,
! [X0] :
( ~ sP27(X0)
| ( ~ p204(sK53(X0))
& r1(X0,sK53(X0)) )
| ~ p504(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X1,sK53(X0))],[f89]) ).
fof(f91,plain,
! [X1] :
( ~ sP26(X1)
| ? [X27] :
( ~ p204(X27)
& r1(X1,X27) )
| ~ p404(X1) ),
inference(nnf_transformation,[],[f34]) ).
fof(f92,plain,
! [X0] :
( ~ sP26(X0)
| ? [X1] :
( ~ p204(X1)
& r1(X0,X1) )
| ~ p404(X0) ),
inference(rectify,[],[f91]) ).
fof(f93,plain,
! [X0] :
( ~ sP26(X0)
| ( ~ p204(sK54(X0))
& r1(X0,sK54(X0)) )
| ~ p404(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X1,sK54(X0))],[f92]) ).
fof(f94,plain,
! [X1] :
( ~ sP25(X1)
| ? [X30] :
( ~ p104(X30)
& r1(X1,X30) )
| ~ p604(X1) ),
inference(nnf_transformation,[],[f33]) ).
fof(f95,plain,
! [X0] :
( ~ sP25(X0)
| ? [X1] :
( ~ p104(X1)
& r1(X0,X1) )
| ~ p604(X0) ),
inference(rectify,[],[f94]) ).
fof(f96,plain,
! [X0] :
( ~ sP25(X0)
| ( ~ p104(sK55(X0))
& r1(X0,sK55(X0)) )
| ~ p604(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(X1,sK55(X0))],[f95]) ).
fof(f97,plain,
! [X1] :
( ~ sP24(X1)
| ? [X31] :
( ~ p104(X31)
& r1(X1,X31) )
| ~ p504(X1) ),
inference(nnf_transformation,[],[f32]) ).
fof(f98,plain,
! [X0] :
( ~ sP24(X0)
| ? [X1] :
( ~ p104(X1)
& r1(X0,X1) )
| ~ p504(X0) ),
inference(rectify,[],[f97]) ).
fof(f99,plain,
! [X0] :
( ~ sP24(X0)
| ( ~ p104(sK56(X0))
& r1(X0,sK56(X0)) )
| ~ p504(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X1,sK56(X0))],[f98]) ).
fof(f100,plain,
! [X1] :
( ~ sP23(X1)
| ? [X32] :
( ~ p104(X32)
& r1(X1,X32) )
| ~ p404(X1) ),
inference(nnf_transformation,[],[f31]) ).
fof(f101,plain,
! [X0] :
( ~ sP23(X0)
| ? [X1] :
( ~ p104(X1)
& r1(X0,X1) )
| ~ p404(X0) ),
inference(rectify,[],[f100]) ).
fof(f102,plain,
! [X0] :
( ~ sP23(X0)
| ( ~ p104(sK57(X0))
& r1(X0,sK57(X0)) )
| ~ p404(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(X1,sK57(X0))],[f101]) ).
fof(f103,plain,
! [X1] :
( ~ sP22(X1)
| ? [X37] :
( ~ p203(X37)
& r1(X1,X37) )
| ~ p603(X1) ),
inference(nnf_transformation,[],[f30]) ).
fof(f104,plain,
! [X0] :
( ~ sP22(X0)
| ? [X1] :
( ~ p203(X1)
& r1(X0,X1) )
| ~ p603(X0) ),
inference(rectify,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ~ sP22(X0)
| ( ~ p203(sK58(X0))
& r1(X0,sK58(X0)) )
| ~ p603(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X1,sK58(X0))],[f104]) ).
fof(f106,plain,
! [X1] :
( ~ sP21(X1)
| ? [X38] :
( ~ p203(X38)
& r1(X1,X38) )
| ~ p503(X1) ),
inference(nnf_transformation,[],[f29]) ).
fof(f107,plain,
! [X0] :
( ~ sP21(X0)
| ? [X1] :
( ~ p203(X1)
& r1(X0,X1) )
| ~ p503(X0) ),
inference(rectify,[],[f106]) ).
fof(f108,plain,
! [X0] :
( ~ sP21(X0)
| ( ~ p203(sK59(X0))
& r1(X0,sK59(X0)) )
| ~ p503(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X1,sK59(X0))],[f107]) ).
fof(f109,plain,
! [X1] :
( ~ sP20(X1)
| ? [X39] :
( ~ p203(X39)
& r1(X1,X39) )
| ~ p403(X1) ),
inference(nnf_transformation,[],[f28]) ).
fof(f110,plain,
! [X0] :
( ~ sP20(X0)
| ? [X1] :
( ~ p203(X1)
& r1(X0,X1) )
| ~ p403(X0) ),
inference(rectify,[],[f109]) ).
fof(f111,plain,
! [X0] :
( ~ sP20(X0)
| ( ~ p203(sK60(X0))
& r1(X0,sK60(X0)) )
| ~ p403(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f110]) ).
fof(f112,plain,
! [X1] :
( ~ sP19(X1)
| ? [X40] :
( ~ p203(X40)
& r1(X1,X40) )
| ~ p303(X1) ),
inference(nnf_transformation,[],[f27]) ).
fof(f113,plain,
! [X0] :
( ~ sP19(X0)
| ? [X1] :
( ~ p203(X1)
& r1(X0,X1) )
| ~ p303(X0) ),
inference(rectify,[],[f112]) ).
fof(f114,plain,
! [X0] :
( ~ sP19(X0)
| ( ~ p203(sK61(X0))
& r1(X0,sK61(X0)) )
| ~ p303(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(X1,sK61(X0))],[f113]) ).
fof(f115,plain,
! [X1] :
( ~ sP18(X1)
| ? [X41] :
( ~ p103(X41)
& r1(X1,X41) )
| ~ p603(X1) ),
inference(nnf_transformation,[],[f26]) ).
fof(f116,plain,
! [X0] :
( ~ sP18(X0)
| ? [X1] :
( ~ p103(X1)
& r1(X0,X1) )
| ~ p603(X0) ),
inference(rectify,[],[f115]) ).
fof(f117,plain,
! [X0] :
( ~ sP18(X0)
| ( ~ p103(sK62(X0))
& r1(X0,sK62(X0)) )
| ~ p603(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X1,sK62(X0))],[f116]) ).
fof(f118,plain,
! [X1] :
( ~ sP17(X1)
| ? [X42] :
( ~ p103(X42)
& r1(X1,X42) )
| ~ p503(X1) ),
inference(nnf_transformation,[],[f25]) ).
fof(f119,plain,
! [X0] :
( ~ sP17(X0)
| ? [X1] :
( ~ p103(X1)
& r1(X0,X1) )
| ~ p503(X0) ),
inference(rectify,[],[f118]) ).
fof(f120,plain,
! [X0] :
( ~ sP17(X0)
| ( ~ p103(sK63(X0))
& r1(X0,sK63(X0)) )
| ~ p503(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X1,sK63(X0))],[f119]) ).
fof(f121,plain,
! [X1] :
( ~ sP16(X1)
| ? [X43] :
( ~ p103(X43)
& r1(X1,X43) )
| ~ p403(X1) ),
inference(nnf_transformation,[],[f24]) ).
fof(f122,plain,
! [X0] :
( ~ sP16(X0)
| ? [X1] :
( ~ p103(X1)
& r1(X0,X1) )
| ~ p403(X0) ),
inference(rectify,[],[f121]) ).
fof(f123,plain,
! [X0] :
( ~ sP16(X0)
| ( ~ p103(sK64(X0))
& r1(X0,sK64(X0)) )
| ~ p403(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(X1,sK64(X0))],[f122]) ).
fof(f124,plain,
! [X1] :
( ~ sP15(X1)
| ? [X44] :
( ~ p103(X44)
& r1(X1,X44) )
| ~ p303(X1) ),
inference(nnf_transformation,[],[f23]) ).
fof(f125,plain,
! [X0] :
( ~ sP15(X0)
| ? [X1] :
( ~ p103(X1)
& r1(X0,X1) )
| ~ p303(X0) ),
inference(rectify,[],[f124]) ).
fof(f126,plain,
! [X0] :
( ~ sP15(X0)
| ( ~ p103(sK65(X0))
& r1(X0,sK65(X0)) )
| ~ p303(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(X1,sK65(X0))],[f125]) ).
fof(f127,plain,
! [X1] :
( ~ sP14(X1)
| ? [X47] :
( ~ p102(X47)
& r1(X1,X47) )
| ~ p602(X1) ),
inference(nnf_transformation,[],[f22]) ).
fof(f128,plain,
! [X0] :
( ~ sP14(X0)
| ? [X1] :
( ~ p102(X1)
& r1(X0,X1) )
| ~ p602(X0) ),
inference(rectify,[],[f127]) ).
fof(f129,plain,
! [X0] :
( ~ sP14(X0)
| ( ~ p102(sK66(X0))
& r1(X0,sK66(X0)) )
| ~ p602(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(X1,sK66(X0))],[f128]) ).
fof(f130,plain,
! [X1] :
( ~ sP13(X1)
| ? [X48] :
( ~ p102(X48)
& r1(X1,X48) )
| ~ p502(X1) ),
inference(nnf_transformation,[],[f21]) ).
fof(f131,plain,
! [X0] :
( ~ sP13(X0)
| ? [X1] :
( ~ p102(X1)
& r1(X0,X1) )
| ~ p502(X0) ),
inference(rectify,[],[f130]) ).
fof(f132,plain,
! [X0] :
( ~ sP13(X0)
| ( ~ p102(sK67(X0))
& r1(X0,sK67(X0)) )
| ~ p502(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(X1,sK67(X0))],[f131]) ).
fof(f133,plain,
! [X1] :
( ~ sP12(X1)
| ? [X49] :
( ~ p102(X49)
& r1(X1,X49) )
| ~ p402(X1) ),
inference(nnf_transformation,[],[f20]) ).
fof(f134,plain,
! [X0] :
( ~ sP12(X0)
| ? [X1] :
( ~ p102(X1)
& r1(X0,X1) )
| ~ p402(X0) ),
inference(rectify,[],[f133]) ).
fof(f135,plain,
! [X0] :
( ~ sP12(X0)
| ( ~ p102(sK68(X0))
& r1(X0,sK68(X0)) )
| ~ p402(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X1,sK68(X0))],[f134]) ).
fof(f136,plain,
! [X1] :
( ~ sP11(X1)
| ? [X50] :
( ~ p102(X50)
& r1(X1,X50) )
| ~ p302(X1) ),
inference(nnf_transformation,[],[f19]) ).
fof(f137,plain,
! [X0] :
( ~ sP11(X0)
| ? [X1] :
( ~ p102(X1)
& r1(X0,X1) )
| ~ p302(X0) ),
inference(rectify,[],[f136]) ).
fof(f138,plain,
! [X0] :
( ~ sP11(X0)
| ( ~ p102(sK69(X0))
& r1(X0,sK69(X0)) )
| ~ p302(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(X1,sK69(X0))],[f137]) ).
fof(f139,plain,
! [X1] :
( ~ sP10(X1)
| ? [X51] :
( ~ p102(X51)
& r1(X1,X51) )
| ~ p202(X1) ),
inference(nnf_transformation,[],[f18]) ).
fof(f140,plain,
! [X0] :
( ~ sP10(X0)
| ? [X1] :
( ~ p102(X1)
& r1(X0,X1) )
| ~ p202(X0) ),
inference(rectify,[],[f139]) ).
fof(f141,plain,
! [X0] :
( ~ sP10(X0)
| ( ~ p102(sK70(X0))
& r1(X0,sK70(X0)) )
| ~ p202(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(X1,sK70(X0))],[f140]) ).
fof(f142,plain,
! [X1] :
( ~ sP9(X1)
| ? [X7] :
( ~ p305(X7)
& r1(X1,X7) )
| ? [X6] :
( ~ p405(X6)
& r1(X1,X6) ) ),
inference(nnf_transformation,[],[f17]) ).
fof(f143,plain,
! [X0] :
( ~ sP9(X0)
| ? [X2] :
( ~ p305(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p405(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f142]) ).
fof(f144,plain,
! [X0] :
( ~ sP9(X0)
| ( ~ p305(sK72(X0))
& r1(X0,sK72(X0)) )
| ( ~ p405(sK71(X0))
& r1(X0,sK71(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72]),skolemize(X1,sK71(X0)),skolemize(X2,sK72(X0))],[f143]) ).
fof(f145,plain,
! [X1] :
( ~ sP8(X1)
| ? [X11] :
( ~ p205(X11)
& r1(X1,X11) )
| ? [X10] :
( ~ p405(X10)
& r1(X1,X10) ) ),
inference(nnf_transformation,[],[f16]) ).
fof(f146,plain,
! [X0] :
( ~ sP8(X0)
| ? [X2] :
( ~ p205(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p405(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f145]) ).
fof(f147,plain,
! [X0] :
( ~ sP8(X0)
| ( ~ p205(sK74(X0))
& r1(X0,sK74(X0)) )
| ( ~ p405(sK73(X0))
& r1(X0,sK73(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73,sK74]),skolemize(X1,sK73(X0)),skolemize(X2,sK74(X0))],[f146]) ).
fof(f148,plain,
! [X1] :
( ~ sP7(X1)
| ? [X13] :
( ~ p205(X13)
& r1(X1,X13) )
| ? [X12] :
( ~ p305(X12)
& r1(X1,X12) ) ),
inference(nnf_transformation,[],[f15]) ).
fof(f149,plain,
! [X0] :
( ~ sP7(X0)
| ? [X2] :
( ~ p205(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p305(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f148]) ).
fof(f150,plain,
! [X0] :
( ~ sP7(X0)
| ( ~ p205(sK76(X0))
& r1(X0,sK76(X0)) )
| ( ~ p305(sK75(X0))
& r1(X0,sK75(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76]),skolemize(X1,sK75(X0)),skolemize(X2,sK76(X0))],[f149]) ).
fof(f151,plain,
! [X1] :
( ~ sP6(X1)
| ? [X17] :
( ~ p105(X17)
& r1(X1,X17) )
| ? [X16] :
( ~ p405(X16)
& r1(X1,X16) ) ),
inference(nnf_transformation,[],[f14]) ).
fof(f152,plain,
! [X0] :
( ~ sP6(X0)
| ? [X2] :
( ~ p105(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p405(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f151]) ).
fof(f153,plain,
! [X0] :
( ~ sP6(X0)
| ( ~ p105(sK78(X0))
& r1(X0,sK78(X0)) )
| ( ~ p405(sK77(X0))
& r1(X0,sK77(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77,sK78]),skolemize(X1,sK77(X0)),skolemize(X2,sK78(X0))],[f152]) ).
fof(f154,plain,
! [X1] :
( ~ sP5(X1)
| ? [X19] :
( ~ p105(X19)
& r1(X1,X19) )
| ? [X18] :
( ~ p305(X18)
& r1(X1,X18) ) ),
inference(nnf_transformation,[],[f13]) ).
fof(f155,plain,
! [X0] :
( ~ sP5(X0)
| ? [X2] :
( ~ p105(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p305(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f154]) ).
fof(f156,plain,
! [X0] :
( ~ sP5(X0)
| ( ~ p105(sK80(X0))
& r1(X0,sK80(X0)) )
| ( ~ p305(sK79(X0))
& r1(X0,sK79(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK79,sK80]),skolemize(X1,sK79(X0)),skolemize(X2,sK80(X0))],[f155]) ).
fof(f157,plain,
! [X1] :
( ~ sP4(X1)
| ? [X21] :
( ~ p105(X21)
& r1(X1,X21) )
| ? [X20] :
( ~ p205(X20)
& r1(X1,X20) ) ),
inference(nnf_transformation,[],[f12]) ).
fof(f158,plain,
! [X0] :
( ~ sP4(X0)
| ? [X2] :
( ~ p105(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p205(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f157]) ).
fof(f159,plain,
! [X0] :
( ~ sP4(X0)
| ( ~ p105(sK82(X0))
& r1(X0,sK82(X0)) )
| ( ~ p205(sK81(X0))
& r1(X0,sK81(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81,sK82]),skolemize(X1,sK81(X0)),skolemize(X2,sK82(X0))],[f158]) ).
fof(f160,plain,
! [X1] :
( ~ sP3(X1)
| ? [X29] :
( ~ p204(X29)
& r1(X1,X29) )
| ? [X28] :
( ~ p304(X28)
& r1(X1,X28) ) ),
inference(nnf_transformation,[],[f11]) ).
fof(f161,plain,
! [X0] :
( ~ sP3(X0)
| ? [X2] :
( ~ p204(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p304(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f160]) ).
fof(f162,plain,
! [X0] :
( ~ sP3(X0)
| ( ~ p204(sK84(X0))
& r1(X0,sK84(X0)) )
| ( ~ p304(sK83(X0))
& r1(X0,sK83(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83,sK84]),skolemize(X1,sK83(X0)),skolemize(X2,sK84(X0))],[f161]) ).
fof(f163,plain,
! [X1] :
( ~ sP2(X1)
| ? [X34] :
( ~ p104(X34)
& r1(X1,X34) )
| ? [X33] :
( ~ p304(X33)
& r1(X1,X33) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f164,plain,
! [X0] :
( ~ sP2(X0)
| ? [X2] :
( ~ p104(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p304(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f163]) ).
fof(f165,plain,
! [X0] :
( ~ sP2(X0)
| ( ~ p104(sK86(X0))
& r1(X0,sK86(X0)) )
| ( ~ p304(sK85(X0))
& r1(X0,sK85(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK85,sK86]),skolemize(X1,sK85(X0)),skolemize(X2,sK86(X0))],[f164]) ).
fof(f166,plain,
! [X1] :
( ~ sP1(X1)
| ? [X36] :
( ~ p104(X36)
& r1(X1,X36) )
| ? [X35] :
( ~ p204(X35)
& r1(X1,X35) ) ),
inference(nnf_transformation,[],[f9]) ).
fof(f167,plain,
! [X0] :
( ~ sP1(X0)
| ? [X2] :
( ~ p104(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p204(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f166]) ).
fof(f168,plain,
! [X0] :
( ~ sP1(X0)
| ( ~ p104(sK88(X0))
& r1(X0,sK88(X0)) )
| ( ~ p204(sK87(X0))
& r1(X0,sK87(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88]),skolemize(X1,sK87(X0)),skolemize(X2,sK88(X0))],[f167]) ).
fof(f172,plain,
? [X0] :
( ( p101(X0)
| ! [X11] :
( p102(X11)
| ~ r1(X0,X11) )
| ! [X10] :
( p103(X10)
| ~ r1(X0,X10) )
| ! [X9] :
( p104(X9)
| ~ r1(X0,X9) )
| ! [X8] :
( p105(X8)
| ~ r1(X0,X8) ) )
& ( p201(X0)
| p202(X0)
| ! [X7] :
( p203(X7)
| ~ r1(X0,X7) )
| ! [X6] :
( p204(X6)
| ~ r1(X0,X6) )
| ! [X5] :
( p205(X5)
| ~ r1(X0,X5) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X4] :
( p304(X4)
| ~ r1(X0,X4) )
| ! [X3] :
( p305(X3)
| ~ r1(X0,X3) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X2] :
( p405(X2)
| ~ r1(X0,X2) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) )
& ! [X1] :
( sP40(X1)
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f49]) ).
fof(f173,plain,
( ( p101(sK91)
| ! [X11] :
( p102(X11)
| ~ r1(sK91,X11) )
| ! [X10] :
( p103(X10)
| ~ r1(sK91,X10) )
| ! [X9] :
( p104(X9)
| ~ r1(sK91,X9) )
| ! [X8] :
( p105(X8)
| ~ r1(sK91,X8) ) )
& ( p201(sK91)
| p202(sK91)
| ! [X7] :
( p203(X7)
| ~ r1(sK91,X7) )
| ! [X6] :
( p204(X6)
| ~ r1(sK91,X6) )
| ! [X5] :
( p205(X5)
| ~ r1(sK91,X5) ) )
& ( p301(sK91)
| p302(sK91)
| p303(sK91)
| ! [X4] :
( p304(X4)
| ~ r1(sK91,X4) )
| ! [X3] :
( p305(X3)
| ~ r1(sK91,X3) ) )
& ( p401(sK91)
| p402(sK91)
| p403(sK91)
| p404(sK91)
| ! [X2] :
( p405(X2)
| ~ r1(sK91,X2) ) )
& ( p501(sK91)
| p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91) )
& ( p601(sK91)
| p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91) )
& ! [X1] :
( sP40(X1)
| ~ r1(sK91,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91]),skolemize(X0,sK91)],[f172]) ).
fof(f174,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f175,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p201(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f176,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p301(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f177,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f178,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f179,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f180,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p301(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f181,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f182,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f183,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f184,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f185,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f186,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f187,plain,
! [X0] :
( ~ sP40(X0)
| ~ p401(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f188,plain,
! [X0] :
( ~ sP40(X0)
| ~ p401(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f189,plain,
! [X0] :
( ~ sP40(X0)
| ~ p501(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f190,plain,
! [X0] :
( ~ sP40(X0)
| sP10(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f191,plain,
! [X0] :
( ~ sP40(X0)
| sP11(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f192,plain,
! [X0] :
( ~ sP40(X0)
| sP12(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f193,plain,
! [X0] :
( ~ sP40(X0)
| sP13(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f194,plain,
! [X0] :
( ~ sP40(X0)
| sP14(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f195,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p302(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f196,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p402(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f197,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f198,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f199,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p402(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f200,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f201,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f202,plain,
! [X0] :
( ~ sP40(X0)
| ~ p402(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f203,plain,
! [X0] :
( ~ sP40(X0)
| ~ p402(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f204,plain,
! [X0] :
( ~ sP40(X0)
| ~ p502(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f205,plain,
! [X0] :
( ~ sP40(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f206,plain,
! [X0] :
( ~ sP40(X0)
| sP15(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f207,plain,
! [X0] :
( ~ sP40(X0)
| sP16(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f208,plain,
! [X0] :
( ~ sP40(X0)
| sP17(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f209,plain,
! [X0] :
( ~ sP40(X0)
| sP18(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f210,plain,
! [X0] :
( ~ sP40(X0)
| sP19(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f211,plain,
! [X0] :
( ~ sP40(X0)
| sP20(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f212,plain,
! [X0] :
( ~ sP40(X0)
| sP21(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f213,plain,
! [X0] :
( ~ sP40(X0)
| sP22(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f214,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p403(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f215,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f216,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f217,plain,
! [X0] :
( ~ sP40(X0)
| ~ p403(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f218,plain,
! [X0] :
( ~ sP40(X0)
| ~ p403(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f219,plain,
! [X0] :
( ~ sP40(X0)
| ~ p503(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f220,plain,
! [X0] :
( ~ sP40(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f221,plain,
! [X0] :
( ~ sP40(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f222,plain,
! [X0] :
( ~ sP40(X0)
| sP23(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f223,plain,
! [X0] :
( ~ sP40(X0)
| sP24(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f224,plain,
! [X0] :
( ~ sP40(X0)
| sP25(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f225,plain,
! [X0] :
( ~ sP40(X0)
| sP3(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f226,plain,
! [X0] :
( ~ sP40(X0)
| sP26(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f227,plain,
! [X0] :
( ~ sP40(X0)
| sP27(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f228,plain,
! [X0] :
( ~ sP40(X0)
| sP28(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f229,plain,
! [X0] :
( ~ sP40(X0)
| sP29(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f230,plain,
! [X0] :
( ~ sP40(X0)
| sP30(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f231,plain,
! [X0] :
( ~ sP40(X0)
| sP31(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f232,plain,
! [X0] :
( ~ sP40(X0)
| ~ p404(X0)
| ~ p504(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f233,plain,
! [X0] :
( ~ sP40(X0)
| ~ p404(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f234,plain,
! [X0] :
( ~ sP40(X0)
| ~ p504(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f235,plain,
! [X0] :
( ~ sP40(X0)
| sP4(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f236,plain,
! [X0] :
( ~ sP40(X0)
| sP5(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f237,plain,
! [X0] :
( ~ sP40(X0)
| sP6(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f238,plain,
! [X0] :
( ~ sP40(X0)
| sP32(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f239,plain,
! [X0] :
( ~ sP40(X0)
| sP33(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f240,plain,
! [X0] :
( ~ sP40(X0)
| sP7(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f241,plain,
! [X0] :
( ~ sP40(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f242,plain,
! [X0] :
( ~ sP40(X0)
| sP34(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f243,plain,
! [X0] :
( ~ sP40(X0)
| sP35(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f244,plain,
! [X0] :
( ~ sP40(X0)
| sP9(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f245,plain,
! [X0] :
( ~ sP40(X0)
| sP36(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f246,plain,
! [X0] :
( ~ sP40(X0)
| sP37(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f247,plain,
! [X0] :
( ~ sP40(X0)
| sP38(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f248,plain,
! [X0] :
( ~ sP40(X0)
| sP39(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f249,plain,
! [X0] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f51]) ).
fof(f250,plain,
! [X0] :
( ~ sP39(X0)
| ~ p405(sK41(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f251,plain,
! [X0] :
( ~ sP39(X0)
| r1(X0,sK41(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f54]) ).
fof(f252,plain,
! [X0] :
( ~ sP38(X0)
| ~ p405(sK42(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f253,plain,
! [X0] :
( ~ sP38(X0)
| r1(X0,sK42(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f57]) ).
fof(f254,plain,
! [X0] :
( ~ sP37(X0)
| ~ p305(sK43(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f255,plain,
! [X0] :
( ~ sP37(X0)
| r1(X0,sK43(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f60]) ).
fof(f256,plain,
! [X0] :
( ~ sP36(X0)
| ~ p305(sK44(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f257,plain,
! [X0] :
( ~ sP36(X0)
| r1(X0,sK44(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f63]) ).
fof(f258,plain,
! [X0] :
( ~ sP35(X0)
| ~ p205(sK45(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f66]) ).
fof(f259,plain,
! [X0] :
( ~ sP35(X0)
| r1(X0,sK45(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f66]) ).
fof(f260,plain,
! [X0] :
( ~ sP34(X0)
| ~ p205(sK46(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f261,plain,
! [X0] :
( ~ sP34(X0)
| r1(X0,sK46(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f69]) ).
fof(f262,plain,
! [X0] :
( ~ sP33(X0)
| ~ p105(sK47(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f263,plain,
! [X0] :
( ~ sP33(X0)
| r1(X0,sK47(X0))
| ~ p605(X0) ),
inference(cnf_transformation,[],[f72]) ).
fof(f264,plain,
! [X0] :
( ~ sP32(X0)
| ~ p105(sK48(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f265,plain,
! [X0] :
( ~ sP32(X0)
| r1(X0,sK48(X0))
| ~ p505(X0) ),
inference(cnf_transformation,[],[f75]) ).
fof(f266,plain,
! [X0] :
( ~ sP31(X0)
| ~ p304(sK49(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f267,plain,
! [X0] :
( ~ sP31(X0)
| r1(X0,sK49(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f78]) ).
fof(f268,plain,
! [X0] :
( ~ sP30(X0)
| ~ p304(sK50(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f269,plain,
! [X0] :
( ~ sP30(X0)
| r1(X0,sK50(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f81]) ).
fof(f270,plain,
! [X0] :
( ~ sP29(X0)
| ~ p304(sK51(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f271,plain,
! [X0] :
( ~ sP29(X0)
| r1(X0,sK51(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f84]) ).
fof(f272,plain,
! [X0] :
( ~ sP28(X0)
| ~ p204(sK52(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f273,plain,
! [X0] :
( ~ sP28(X0)
| r1(X0,sK52(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f87]) ).
fof(f274,plain,
! [X0] :
( ~ sP27(X0)
| ~ p204(sK53(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f90]) ).
fof(f275,plain,
! [X0] :
( ~ sP27(X0)
| r1(X0,sK53(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f90]) ).
fof(f276,plain,
! [X0] :
( ~ sP26(X0)
| ~ p204(sK54(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f277,plain,
! [X0] :
( ~ sP26(X0)
| r1(X0,sK54(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f93]) ).
fof(f278,plain,
! [X0] :
( ~ sP25(X0)
| ~ p104(sK55(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f96]) ).
fof(f279,plain,
! [X0] :
( ~ sP25(X0)
| r1(X0,sK55(X0))
| ~ p604(X0) ),
inference(cnf_transformation,[],[f96]) ).
fof(f280,plain,
! [X0] :
( ~ sP24(X0)
| ~ p104(sK56(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f281,plain,
! [X0] :
( ~ sP24(X0)
| r1(X0,sK56(X0))
| ~ p504(X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f282,plain,
! [X0] :
( ~ sP23(X0)
| ~ p104(sK57(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f283,plain,
! [X0] :
( ~ sP23(X0)
| r1(X0,sK57(X0))
| ~ p404(X0) ),
inference(cnf_transformation,[],[f102]) ).
fof(f284,plain,
! [X0] :
( ~ sP22(X0)
| ~ p203(sK58(X0))
| ~ p603(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f285,plain,
! [X0] :
( ~ sP22(X0)
| r1(X0,sK58(X0))
| ~ p603(X0) ),
inference(cnf_transformation,[],[f105]) ).
fof(f286,plain,
! [X0] :
( ~ sP21(X0)
| ~ p203(sK59(X0))
| ~ p503(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f287,plain,
! [X0] :
( ~ sP21(X0)
| r1(X0,sK59(X0))
| ~ p503(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f288,plain,
! [X0] :
( ~ sP20(X0)
| ~ p203(sK60(X0))
| ~ p403(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f289,plain,
! [X0] :
( ~ sP20(X0)
| r1(X0,sK60(X0))
| ~ p403(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f290,plain,
! [X0] :
( ~ sP19(X0)
| ~ p203(sK61(X0))
| ~ p303(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f291,plain,
! [X0] :
( ~ sP19(X0)
| r1(X0,sK61(X0))
| ~ p303(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f292,plain,
! [X0] :
( ~ sP18(X0)
| ~ p103(sK62(X0))
| ~ p603(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f293,plain,
! [X0] :
( ~ sP18(X0)
| r1(X0,sK62(X0))
| ~ p603(X0) ),
inference(cnf_transformation,[],[f117]) ).
fof(f294,plain,
! [X0] :
( ~ sP17(X0)
| ~ p103(sK63(X0))
| ~ p503(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f295,plain,
! [X0] :
( ~ sP17(X0)
| r1(X0,sK63(X0))
| ~ p503(X0) ),
inference(cnf_transformation,[],[f120]) ).
fof(f296,plain,
! [X0] :
( ~ sP16(X0)
| ~ p103(sK64(X0))
| ~ p403(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f297,plain,
! [X0] :
( ~ sP16(X0)
| r1(X0,sK64(X0))
| ~ p403(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f298,plain,
! [X0] :
( ~ sP15(X0)
| ~ p103(sK65(X0))
| ~ p303(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f299,plain,
! [X0] :
( ~ sP15(X0)
| r1(X0,sK65(X0))
| ~ p303(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f300,plain,
! [X0] :
( ~ sP14(X0)
| ~ p102(sK66(X0))
| ~ p602(X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f301,plain,
! [X0] :
( ~ sP14(X0)
| r1(X0,sK66(X0))
| ~ p602(X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f302,plain,
! [X0] :
( ~ sP13(X0)
| ~ p102(sK67(X0))
| ~ p502(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f303,plain,
! [X0] :
( ~ sP13(X0)
| r1(X0,sK67(X0))
| ~ p502(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f304,plain,
! [X0] :
( ~ sP12(X0)
| ~ p102(sK68(X0))
| ~ p402(X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f305,plain,
! [X0] :
( ~ sP12(X0)
| r1(X0,sK68(X0))
| ~ p402(X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f306,plain,
! [X0] :
( ~ sP11(X0)
| ~ p102(sK69(X0))
| ~ p302(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f307,plain,
! [X0] :
( ~ sP11(X0)
| r1(X0,sK69(X0))
| ~ p302(X0) ),
inference(cnf_transformation,[],[f138]) ).
fof(f308,plain,
! [X0] :
( ~ sP10(X0)
| ~ p102(sK70(X0))
| ~ p202(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f309,plain,
! [X0] :
( ~ sP10(X0)
| r1(X0,sK70(X0))
| ~ p202(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f310,plain,
! [X0] :
( ~ sP9(X0)
| ~ p305(sK72(X0))
| ~ p405(sK71(X0)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f311,plain,
! [X0] :
( ~ sP9(X0)
| r1(X0,sK72(X0))
| ~ p405(sK71(X0)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f312,plain,
! [X0] :
( ~ sP9(X0)
| ~ p305(sK72(X0))
| r1(X0,sK71(X0)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f313,plain,
! [X0] :
( ~ sP9(X0)
| r1(X0,sK72(X0))
| r1(X0,sK71(X0)) ),
inference(cnf_transformation,[],[f144]) ).
fof(f314,plain,
! [X0] :
( ~ sP8(X0)
| ~ p205(sK74(X0))
| ~ p405(sK73(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f315,plain,
! [X0] :
( ~ sP8(X0)
| r1(X0,sK74(X0))
| ~ p405(sK73(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f316,plain,
! [X0] :
( ~ sP8(X0)
| ~ p205(sK74(X0))
| r1(X0,sK73(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f317,plain,
! [X0] :
( ~ sP8(X0)
| r1(X0,sK74(X0))
| r1(X0,sK73(X0)) ),
inference(cnf_transformation,[],[f147]) ).
fof(f318,plain,
! [X0] :
( ~ sP7(X0)
| ~ p205(sK76(X0))
| ~ p305(sK75(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f319,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK76(X0))
| ~ p305(sK75(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f320,plain,
! [X0] :
( ~ sP7(X0)
| ~ p205(sK76(X0))
| r1(X0,sK75(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f321,plain,
! [X0] :
( ~ sP7(X0)
| r1(X0,sK76(X0))
| r1(X0,sK75(X0)) ),
inference(cnf_transformation,[],[f150]) ).
fof(f322,plain,
! [X0] :
( ~ sP6(X0)
| ~ p105(sK78(X0))
| ~ p405(sK77(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f323,plain,
! [X0] :
( ~ sP6(X0)
| r1(X0,sK78(X0))
| ~ p405(sK77(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f324,plain,
! [X0] :
( ~ sP6(X0)
| ~ p105(sK78(X0))
| r1(X0,sK77(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f325,plain,
! [X0] :
( ~ sP6(X0)
| r1(X0,sK78(X0))
| r1(X0,sK77(X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f326,plain,
! [X0] :
( ~ sP5(X0)
| ~ p105(sK80(X0))
| ~ p305(sK79(X0)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f327,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK80(X0))
| ~ p305(sK79(X0)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f328,plain,
! [X0] :
( ~ sP5(X0)
| ~ p105(sK80(X0))
| r1(X0,sK79(X0)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f329,plain,
! [X0] :
( ~ sP5(X0)
| r1(X0,sK80(X0))
| r1(X0,sK79(X0)) ),
inference(cnf_transformation,[],[f156]) ).
fof(f330,plain,
! [X0] :
( ~ sP4(X0)
| ~ p105(sK82(X0))
| ~ p205(sK81(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f331,plain,
! [X0] :
( ~ sP4(X0)
| r1(X0,sK82(X0))
| ~ p205(sK81(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f332,plain,
! [X0] :
( ~ sP4(X0)
| ~ p105(sK82(X0))
| r1(X0,sK81(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f333,plain,
! [X0] :
( ~ sP4(X0)
| r1(X0,sK82(X0))
| r1(X0,sK81(X0)) ),
inference(cnf_transformation,[],[f159]) ).
fof(f334,plain,
! [X0] :
( ~ sP3(X0)
| ~ p204(sK84(X0))
| ~ p304(sK83(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f335,plain,
! [X0] :
( ~ sP3(X0)
| r1(X0,sK84(X0))
| ~ p304(sK83(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f336,plain,
! [X0] :
( ~ sP3(X0)
| ~ p204(sK84(X0))
| r1(X0,sK83(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f337,plain,
! [X0] :
( ~ sP3(X0)
| r1(X0,sK84(X0))
| r1(X0,sK83(X0)) ),
inference(cnf_transformation,[],[f162]) ).
fof(f338,plain,
! [X0] :
( ~ sP2(X0)
| ~ p104(sK86(X0))
| ~ p304(sK85(X0)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f339,plain,
! [X0] :
( ~ sP2(X0)
| r1(X0,sK86(X0))
| ~ p304(sK85(X0)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f340,plain,
! [X0] :
( ~ sP2(X0)
| ~ p104(sK86(X0))
| r1(X0,sK85(X0)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f341,plain,
! [X0] :
( ~ sP2(X0)
| r1(X0,sK86(X0))
| r1(X0,sK85(X0)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f342,plain,
! [X0] :
( ~ sP1(X0)
| ~ p104(sK88(X0))
| ~ p204(sK87(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f343,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK88(X0))
| ~ p204(sK87(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f344,plain,
! [X0] :
( ~ sP1(X0)
| ~ p104(sK88(X0))
| r1(X0,sK87(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f345,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK88(X0))
| r1(X0,sK87(X0)) ),
inference(cnf_transformation,[],[f168]) ).
fof(f350,plain,
! [X10,X11,X8,X9] :
( p101(sK91)
| p102(X11)
| ~ r1(sK91,X11)
| p103(X10)
| ~ r1(sK91,X10)
| p104(X9)
| ~ r1(sK91,X9)
| p105(X8)
| ~ r1(sK91,X8) ),
inference(cnf_transformation,[],[f173]) ).
fof(f351,plain,
! [X6,X7,X5] :
( p201(sK91)
| p202(sK91)
| p203(X7)
| ~ r1(sK91,X7)
| p204(X6)
| ~ r1(sK91,X6)
| p205(X5)
| ~ r1(sK91,X5) ),
inference(cnf_transformation,[],[f173]) ).
fof(f352,plain,
! [X3,X4] :
( p301(sK91)
| p302(sK91)
| p303(sK91)
| p304(X4)
| ~ r1(sK91,X4)
| p305(X3)
| ~ r1(sK91,X3) ),
inference(cnf_transformation,[],[f173]) ).
fof(f353,plain,
! [X2] :
( p401(sK91)
| p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X2)
| ~ r1(sK91,X2) ),
inference(cnf_transformation,[],[f173]) ).
fof(f354,plain,
( p501(sK91)
| p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91) ),
inference(cnf_transformation,[],[f173]) ).
fof(f355,plain,
( p601(sK91)
| p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91) ),
inference(cnf_transformation,[],[f173]) ).
fof(f356,plain,
! [X1] :
( sP40(X1)
| ~ r1(sK91,X1) ),
inference(cnf_transformation,[],[f173]) ).
tcf(c_49,plain,
! [X0: $i] : r1(X0,X0),
inference(cnf_transformation,[],[f174]) ).
tcf(c_50,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f249]) ).
tcf(c_51,plain,
! [X0: $i] :
( sP39(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f248]) ).
tcf(c_52,plain,
! [X0: $i] :
( sP38(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f247]) ).
tcf(c_53,plain,
! [X0: $i] :
( sP37(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f246]) ).
tcf(c_54,plain,
! [X0: $i] :
( sP36(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f245]) ).
tcf(c_55,plain,
! [X0: $i] :
( sP9(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f244]) ).
tcf(c_56,plain,
! [X0: $i] :
( sP35(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f243]) ).
tcf(c_57,plain,
! [X0: $i] :
( sP34(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f242]) ).
tcf(c_58,plain,
! [X0: $i] :
( sP8(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f241]) ).
tcf(c_59,plain,
! [X0: $i] :
( sP7(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f240]) ).
tcf(c_60,plain,
! [X0: $i] :
( sP33(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f239]) ).
tcf(c_61,plain,
! [X0: $i] :
( sP32(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f238]) ).
tcf(c_62,plain,
! [X0: $i] :
( sP6(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f237]) ).
tcf(c_63,plain,
! [X0: $i] :
( sP5(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f236]) ).
tcf(c_64,plain,
! [X0: $i] :
( sP4(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f235]) ).
tcf(c_65,plain,
! [X0: $i] :
( ~ p504(X0)
| ~ p604(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f234]) ).
tcf(c_66,plain,
! [X0: $i] :
( ~ p404(X0)
| ~ p604(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f233]) ).
tcf(c_67,plain,
! [X0: $i] :
( ~ p404(X0)
| ~ p504(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f232]) ).
tcf(c_68,plain,
! [X0: $i] :
( sP31(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f231]) ).
tcf(c_69,plain,
! [X0: $i] :
( sP30(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f230]) ).
tcf(c_70,plain,
! [X0: $i] :
( sP29(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f229]) ).
tcf(c_71,plain,
! [X0: $i] :
( sP28(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f228]) ).
tcf(c_72,plain,
! [X0: $i] :
( sP27(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f227]) ).
tcf(c_73,plain,
! [X0: $i] :
( sP26(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f226]) ).
tcf(c_74,plain,
! [X0: $i] :
( sP3(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f225]) ).
tcf(c_75,plain,
! [X0: $i] :
( sP25(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f224]) ).
tcf(c_76,plain,
! [X0: $i] :
( sP24(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f223]) ).
tcf(c_77,plain,
! [X0: $i] :
( sP23(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f222]) ).
tcf(c_78,plain,
! [X0: $i] :
( sP2(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f221]) ).
tcf(c_79,plain,
! [X0: $i] :
( sP1(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f220]) ).
tcf(c_80,plain,
! [X0: $i] :
( ~ p503(X0)
| ~ p603(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f219]) ).
tcf(c_81,plain,
! [X0: $i] :
( ~ p403(X0)
| ~ p603(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f218]) ).
tcf(c_82,plain,
! [X0: $i] :
( ~ p403(X0)
| ~ p503(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f217]) ).
tcf(c_83,plain,
! [X0: $i] :
( ~ p303(X0)
| ~ p603(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f216]) ).
tcf(c_84,plain,
! [X0: $i] :
( ~ p303(X0)
| ~ p503(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f215]) ).
tcf(c_85,plain,
! [X0: $i] :
( ~ p303(X0)
| ~ p403(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f214]) ).
tcf(c_86,plain,
! [X0: $i] :
( sP22(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f213]) ).
tcf(c_87,plain,
! [X0: $i] :
( sP21(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f212]) ).
tcf(c_88,plain,
! [X0: $i] :
( sP20(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f211]) ).
tcf(c_89,plain,
! [X0: $i] :
( sP19(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_90,plain,
! [X0: $i] :
( sP18(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f209]) ).
tcf(c_91,plain,
! [X0: $i] :
( sP17(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f208]) ).
tcf(c_92,plain,
! [X0: $i] :
( sP16(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f207]) ).
tcf(c_93,plain,
! [X0: $i] :
( sP15(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f206]) ).
tcf(c_94,plain,
! [X0: $i] :
( sP0(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f205]) ).
tcf(c_95,plain,
! [X0: $i] :
( ~ p502(X0)
| ~ p602(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f204]) ).
tcf(c_96,plain,
! [X0: $i] :
( ~ p402(X0)
| ~ p602(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f203]) ).
tcf(c_97,plain,
! [X0: $i] :
( ~ p402(X0)
| ~ p502(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_98,plain,
! [X0: $i] :
( ~ p302(X0)
| ~ p602(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_99,plain,
! [X0: $i] :
( ~ p302(X0)
| ~ p502(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f200]) ).
tcf(c_100,plain,
! [X0: $i] :
( ~ p302(X0)
| ~ p402(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f199]) ).
tcf(c_101,plain,
! [X0: $i] :
( ~ p202(X0)
| ~ p602(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f198]) ).
tcf(c_102,plain,
! [X0: $i] :
( ~ p202(X0)
| ~ p502(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f197]) ).
tcf(c_103,plain,
! [X0: $i] :
( ~ p202(X0)
| ~ p402(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f196]) ).
tcf(c_104,plain,
! [X0: $i] :
( ~ p202(X0)
| ~ p302(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f195]) ).
tcf(c_105,plain,
! [X0: $i] :
( sP14(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f194]) ).
tcf(c_106,plain,
! [X0: $i] :
( sP13(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f193]) ).
tcf(c_107,plain,
! [X0: $i] :
( sP12(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f192]) ).
tcf(c_108,plain,
! [X0: $i] :
( sP11(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f191]) ).
tcf(c_109,plain,
! [X0: $i] :
( sP10(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f190]) ).
tcf(c_110,plain,
! [X0: $i] :
( ~ p501(X0)
| ~ p601(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f189]) ).
tcf(c_111,plain,
! [X0: $i] :
( ~ p401(X0)
| ~ p601(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f188]) ).
tcf(c_112,plain,
! [X0: $i] :
( ~ p401(X0)
| ~ p501(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f187]) ).
tcf(c_113,plain,
! [X0: $i] :
( ~ p301(X0)
| ~ p601(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f186]) ).
tcf(c_114,plain,
! [X0: $i] :
( ~ p301(X0)
| ~ p501(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f185]) ).
tcf(c_115,plain,
! [X0: $i] :
( ~ p301(X0)
| ~ p401(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f184]) ).
tcf(c_116,plain,
! [X0: $i] :
( ~ p201(X0)
| ~ p601(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f183]) ).
tcf(c_117,plain,
! [X0: $i] :
( ~ p201(X0)
| ~ p501(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f182]) ).
tcf(c_118,plain,
! [X0: $i] :
( ~ p201(X0)
| ~ p401(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f181]) ).
tcf(c_119,plain,
! [X0: $i] :
( ~ p201(X0)
| ~ p301(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f180]) ).
tcf(c_120,plain,
! [X0: $i] :
( ~ p101(X0)
| ~ p601(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f179]) ).
tcf(c_121,plain,
! [X0: $i] :
( ~ p101(X0)
| ~ p501(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f178]) ).
tcf(c_122,plain,
! [X0: $i] :
( ~ p101(X0)
| ~ p401(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f177]) ).
tcf(c_123,plain,
! [X0: $i] :
( ~ p101(X0)
| ~ p301(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f176]) ).
tcf(c_124,plain,
! [X0: $i] :
( ~ p101(X0)
| ~ p201(X0)
| ~ sP40(X0) ),
inference(cnf_transformation,[],[f175]) ).
tcf(c_125,plain,
! [X0: $i] :
( r1(X0,sK41(X0))
| ~ sP39(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f251]) ).
tcf(c_126,plain,
! [X0: $i] :
( ~ sP39(X0)
| ~ p605(X0)
| ~ p405(sK41(X0)) ),
inference(cnf_transformation,[],[f250]) ).
tcf(c_127,plain,
! [X0: $i] :
( r1(X0,sK42(X0))
| ~ sP38(X0)
| ~ p505(X0) ),
inference(cnf_transformation,[],[f253]) ).
tcf(c_128,plain,
! [X0: $i] :
( ~ sP38(X0)
| ~ p505(X0)
| ~ p405(sK42(X0)) ),
inference(cnf_transformation,[],[f252]) ).
tcf(c_129,plain,
! [X0: $i] :
( r1(X0,sK43(X0))
| ~ sP37(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f255]) ).
tcf(c_130,plain,
! [X0: $i] :
( ~ sP37(X0)
| ~ p605(X0)
| ~ p305(sK43(X0)) ),
inference(cnf_transformation,[],[f254]) ).
tcf(c_131,plain,
! [X0: $i] :
( r1(X0,sK44(X0))
| ~ sP36(X0)
| ~ p505(X0) ),
inference(cnf_transformation,[],[f257]) ).
tcf(c_132,plain,
! [X0: $i] :
( ~ sP36(X0)
| ~ p505(X0)
| ~ p305(sK44(X0)) ),
inference(cnf_transformation,[],[f256]) ).
tcf(c_133,plain,
! [X0: $i] :
( r1(X0,sK45(X0))
| ~ sP35(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f259]) ).
tcf(c_134,plain,
! [X0: $i] :
( ~ sP35(X0)
| ~ p605(X0)
| ~ p205(sK45(X0)) ),
inference(cnf_transformation,[],[f258]) ).
tcf(c_135,plain,
! [X0: $i] :
( r1(X0,sK46(X0))
| ~ sP34(X0)
| ~ p505(X0) ),
inference(cnf_transformation,[],[f261]) ).
tcf(c_136,plain,
! [X0: $i] :
( ~ sP34(X0)
| ~ p505(X0)
| ~ p205(sK46(X0)) ),
inference(cnf_transformation,[],[f260]) ).
tcf(c_137,plain,
! [X0: $i] :
( r1(X0,sK47(X0))
| ~ sP33(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f263]) ).
tcf(c_138,plain,
! [X0: $i] :
( ~ sP33(X0)
| ~ p605(X0)
| ~ p105(sK47(X0)) ),
inference(cnf_transformation,[],[f262]) ).
tcf(c_139,plain,
! [X0: $i] :
( r1(X0,sK48(X0))
| ~ sP32(X0)
| ~ p505(X0) ),
inference(cnf_transformation,[],[f265]) ).
tcf(c_140,plain,
! [X0: $i] :
( ~ sP32(X0)
| ~ p505(X0)
| ~ p105(sK48(X0)) ),
inference(cnf_transformation,[],[f264]) ).
tcf(c_141,plain,
! [X0: $i] :
( r1(X0,sK49(X0))
| ~ sP31(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f267]) ).
tcf(c_142,plain,
! [X0: $i] :
( ~ sP31(X0)
| ~ p604(X0)
| ~ p304(sK49(X0)) ),
inference(cnf_transformation,[],[f266]) ).
tcf(c_143,plain,
! [X0: $i] :
( r1(X0,sK50(X0))
| ~ sP30(X0)
| ~ p504(X0) ),
inference(cnf_transformation,[],[f269]) ).
tcf(c_144,plain,
! [X0: $i] :
( ~ sP30(X0)
| ~ p504(X0)
| ~ p304(sK50(X0)) ),
inference(cnf_transformation,[],[f268]) ).
tcf(c_145,plain,
! [X0: $i] :
( r1(X0,sK51(X0))
| ~ sP29(X0)
| ~ p404(X0) ),
inference(cnf_transformation,[],[f271]) ).
tcf(c_146,plain,
! [X0: $i] :
( ~ sP29(X0)
| ~ p404(X0)
| ~ p304(sK51(X0)) ),
inference(cnf_transformation,[],[f270]) ).
tcf(c_147,plain,
! [X0: $i] :
( r1(X0,sK52(X0))
| ~ sP28(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f273]) ).
tcf(c_148,plain,
! [X0: $i] :
( ~ sP28(X0)
| ~ p604(X0)
| ~ p204(sK52(X0)) ),
inference(cnf_transformation,[],[f272]) ).
tcf(c_149,plain,
! [X0: $i] :
( r1(X0,sK53(X0))
| ~ sP27(X0)
| ~ p504(X0) ),
inference(cnf_transformation,[],[f275]) ).
tcf(c_150,plain,
! [X0: $i] :
( ~ sP27(X0)
| ~ p504(X0)
| ~ p204(sK53(X0)) ),
inference(cnf_transformation,[],[f274]) ).
tcf(c_151,plain,
! [X0: $i] :
( r1(X0,sK54(X0))
| ~ sP26(X0)
| ~ p404(X0) ),
inference(cnf_transformation,[],[f277]) ).
tcf(c_152,plain,
! [X0: $i] :
( ~ sP26(X0)
| ~ p404(X0)
| ~ p204(sK54(X0)) ),
inference(cnf_transformation,[],[f276]) ).
tcf(c_153,plain,
! [X0: $i] :
( r1(X0,sK55(X0))
| ~ sP25(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f279]) ).
tcf(c_154,plain,
! [X0: $i] :
( ~ sP25(X0)
| ~ p604(X0)
| ~ p104(sK55(X0)) ),
inference(cnf_transformation,[],[f278]) ).
tcf(c_155,plain,
! [X0: $i] :
( r1(X0,sK56(X0))
| ~ sP24(X0)
| ~ p504(X0) ),
inference(cnf_transformation,[],[f281]) ).
tcf(c_156,plain,
! [X0: $i] :
( ~ sP24(X0)
| ~ p504(X0)
| ~ p104(sK56(X0)) ),
inference(cnf_transformation,[],[f280]) ).
tcf(c_157,plain,
! [X0: $i] :
( r1(X0,sK57(X0))
| ~ sP23(X0)
| ~ p404(X0) ),
inference(cnf_transformation,[],[f283]) ).
tcf(c_158,plain,
! [X0: $i] :
( ~ sP23(X0)
| ~ p404(X0)
| ~ p104(sK57(X0)) ),
inference(cnf_transformation,[],[f282]) ).
tcf(c_159,plain,
! [X0: $i] :
( r1(X0,sK58(X0))
| ~ sP22(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f285]) ).
tcf(c_160,plain,
! [X0: $i] :
( ~ sP22(X0)
| ~ p603(X0)
| ~ p203(sK58(X0)) ),
inference(cnf_transformation,[],[f284]) ).
tcf(c_161,plain,
! [X0: $i] :
( r1(X0,sK59(X0))
| ~ sP21(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f287]) ).
tcf(c_162,plain,
! [X0: $i] :
( ~ sP21(X0)
| ~ p503(X0)
| ~ p203(sK59(X0)) ),
inference(cnf_transformation,[],[f286]) ).
tcf(c_163,plain,
! [X0: $i] :
( r1(X0,sK60(X0))
| ~ sP20(X0)
| ~ p403(X0) ),
inference(cnf_transformation,[],[f289]) ).
tcf(c_164,plain,
! [X0: $i] :
( ~ sP20(X0)
| ~ p403(X0)
| ~ p203(sK60(X0)) ),
inference(cnf_transformation,[],[f288]) ).
tcf(c_165,plain,
! [X0: $i] :
( r1(X0,sK61(X0))
| ~ sP19(X0)
| ~ p303(X0) ),
inference(cnf_transformation,[],[f291]) ).
tcf(c_166,plain,
! [X0: $i] :
( ~ sP19(X0)
| ~ p303(X0)
| ~ p203(sK61(X0)) ),
inference(cnf_transformation,[],[f290]) ).
tcf(c_167,plain,
! [X0: $i] :
( r1(X0,sK62(X0))
| ~ sP18(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_168,plain,
! [X0: $i] :
( ~ sP18(X0)
| ~ p603(X0)
| ~ p103(sK62(X0)) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_169,plain,
! [X0: $i] :
( r1(X0,sK63(X0))
| ~ sP17(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f295]) ).
tcf(c_170,plain,
! [X0: $i] :
( ~ sP17(X0)
| ~ p503(X0)
| ~ p103(sK63(X0)) ),
inference(cnf_transformation,[],[f294]) ).
tcf(c_171,plain,
! [X0: $i] :
( r1(X0,sK64(X0))
| ~ sP16(X0)
| ~ p403(X0) ),
inference(cnf_transformation,[],[f297]) ).
tcf(c_172,plain,
! [X0: $i] :
( ~ sP16(X0)
| ~ p403(X0)
| ~ p103(sK64(X0)) ),
inference(cnf_transformation,[],[f296]) ).
tcf(c_173,plain,
! [X0: $i] :
( r1(X0,sK65(X0))
| ~ sP15(X0)
| ~ p303(X0) ),
inference(cnf_transformation,[],[f299]) ).
tcf(c_174,plain,
! [X0: $i] :
( ~ sP15(X0)
| ~ p303(X0)
| ~ p103(sK65(X0)) ),
inference(cnf_transformation,[],[f298]) ).
tcf(c_175,plain,
! [X0: $i] :
( r1(X0,sK66(X0))
| ~ sP14(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f301]) ).
tcf(c_176,plain,
! [X0: $i] :
( ~ sP14(X0)
| ~ p602(X0)
| ~ p102(sK66(X0)) ),
inference(cnf_transformation,[],[f300]) ).
tcf(c_177,plain,
! [X0: $i] :
( r1(X0,sK67(X0))
| ~ sP13(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f303]) ).
tcf(c_178,plain,
! [X0: $i] :
( ~ sP13(X0)
| ~ p502(X0)
| ~ p102(sK67(X0)) ),
inference(cnf_transformation,[],[f302]) ).
tcf(c_179,plain,
! [X0: $i] :
( r1(X0,sK68(X0))
| ~ sP12(X0)
| ~ p402(X0) ),
inference(cnf_transformation,[],[f305]) ).
tcf(c_180,plain,
! [X0: $i] :
( ~ sP12(X0)
| ~ p402(X0)
| ~ p102(sK68(X0)) ),
inference(cnf_transformation,[],[f304]) ).
tcf(c_181,plain,
! [X0: $i] :
( r1(X0,sK69(X0))
| ~ sP11(X0)
| ~ p302(X0) ),
inference(cnf_transformation,[],[f307]) ).
tcf(c_182,plain,
! [X0: $i] :
( ~ sP11(X0)
| ~ p302(X0)
| ~ p102(sK69(X0)) ),
inference(cnf_transformation,[],[f306]) ).
tcf(c_183,plain,
! [X0: $i] :
( r1(X0,sK70(X0))
| ~ sP10(X0)
| ~ p202(X0) ),
inference(cnf_transformation,[],[f309]) ).
tcf(c_184,plain,
! [X0: $i] :
( ~ sP10(X0)
| ~ p202(X0)
| ~ p102(sK70(X0)) ),
inference(cnf_transformation,[],[f308]) ).
tcf(c_185,plain,
! [X0: $i] :
( r1(X0,sK72(X0))
| r1(X0,sK71(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f313]) ).
tcf(c_186,plain,
! [X0: $i] :
( r1(X0,sK71(X0))
| ~ sP9(X0)
| ~ p305(sK72(X0)) ),
inference(cnf_transformation,[],[f312]) ).
tcf(c_187,plain,
! [X0: $i] :
( r1(X0,sK72(X0))
| ~ sP9(X0)
| ~ p405(sK71(X0)) ),
inference(cnf_transformation,[],[f311]) ).
tcf(c_188,plain,
! [X0: $i] :
( ~ sP9(X0)
| ~ p305(sK72(X0))
| ~ p405(sK71(X0)) ),
inference(cnf_transformation,[],[f310]) ).
tcf(c_189,plain,
! [X0: $i] :
( r1(X0,sK74(X0))
| r1(X0,sK73(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f317]) ).
tcf(c_190,plain,
! [X0: $i] :
( r1(X0,sK73(X0))
| ~ sP8(X0)
| ~ p205(sK74(X0)) ),
inference(cnf_transformation,[],[f316]) ).
tcf(c_191,plain,
! [X0: $i] :
( r1(X0,sK74(X0))
| ~ sP8(X0)
| ~ p405(sK73(X0)) ),
inference(cnf_transformation,[],[f315]) ).
tcf(c_192,plain,
! [X0: $i] :
( ~ sP8(X0)
| ~ p205(sK74(X0))
| ~ p405(sK73(X0)) ),
inference(cnf_transformation,[],[f314]) ).
tcf(c_193,plain,
! [X0: $i] :
( r1(X0,sK76(X0))
| r1(X0,sK75(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f321]) ).
tcf(c_194,plain,
! [X0: $i] :
( r1(X0,sK75(X0))
| ~ sP7(X0)
| ~ p205(sK76(X0)) ),
inference(cnf_transformation,[],[f320]) ).
tcf(c_195,plain,
! [X0: $i] :
( r1(X0,sK76(X0))
| ~ sP7(X0)
| ~ p305(sK75(X0)) ),
inference(cnf_transformation,[],[f319]) ).
tcf(c_196,plain,
! [X0: $i] :
( ~ sP7(X0)
| ~ p205(sK76(X0))
| ~ p305(sK75(X0)) ),
inference(cnf_transformation,[],[f318]) ).
tcf(c_197,plain,
! [X0: $i] :
( r1(X0,sK78(X0))
| r1(X0,sK77(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f325]) ).
tcf(c_198,plain,
! [X0: $i] :
( r1(X0,sK77(X0))
| ~ sP6(X0)
| ~ p105(sK78(X0)) ),
inference(cnf_transformation,[],[f324]) ).
tcf(c_199,plain,
! [X0: $i] :
( r1(X0,sK78(X0))
| ~ sP6(X0)
| ~ p405(sK77(X0)) ),
inference(cnf_transformation,[],[f323]) ).
tcf(c_200,plain,
! [X0: $i] :
( ~ sP6(X0)
| ~ p105(sK78(X0))
| ~ p405(sK77(X0)) ),
inference(cnf_transformation,[],[f322]) ).
tcf(c_201,plain,
! [X0: $i] :
( r1(X0,sK80(X0))
| r1(X0,sK79(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f329]) ).
tcf(c_202,plain,
! [X0: $i] :
( r1(X0,sK79(X0))
| ~ sP5(X0)
| ~ p105(sK80(X0)) ),
inference(cnf_transformation,[],[f328]) ).
tcf(c_203,plain,
! [X0: $i] :
( r1(X0,sK80(X0))
| ~ sP5(X0)
| ~ p305(sK79(X0)) ),
inference(cnf_transformation,[],[f327]) ).
tcf(c_204,plain,
! [X0: $i] :
( ~ sP5(X0)
| ~ p105(sK80(X0))
| ~ p305(sK79(X0)) ),
inference(cnf_transformation,[],[f326]) ).
tcf(c_205,plain,
! [X0: $i] :
( r1(X0,sK82(X0))
| r1(X0,sK81(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f333]) ).
tcf(c_206,plain,
! [X0: $i] :
( r1(X0,sK81(X0))
| ~ sP4(X0)
| ~ p105(sK82(X0)) ),
inference(cnf_transformation,[],[f332]) ).
tcf(c_207,plain,
! [X0: $i] :
( r1(X0,sK82(X0))
| ~ sP4(X0)
| ~ p205(sK81(X0)) ),
inference(cnf_transformation,[],[f331]) ).
tcf(c_208,plain,
! [X0: $i] :
( ~ sP4(X0)
| ~ p105(sK82(X0))
| ~ p205(sK81(X0)) ),
inference(cnf_transformation,[],[f330]) ).
tcf(c_209,plain,
! [X0: $i] :
( r1(X0,sK84(X0))
| r1(X0,sK83(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f337]) ).
tcf(c_210,plain,
! [X0: $i] :
( r1(X0,sK83(X0))
| ~ sP3(X0)
| ~ p204(sK84(X0)) ),
inference(cnf_transformation,[],[f336]) ).
tcf(c_211,plain,
! [X0: $i] :
( r1(X0,sK84(X0))
| ~ sP3(X0)
| ~ p304(sK83(X0)) ),
inference(cnf_transformation,[],[f335]) ).
tcf(c_212,plain,
! [X0: $i] :
( ~ sP3(X0)
| ~ p204(sK84(X0))
| ~ p304(sK83(X0)) ),
inference(cnf_transformation,[],[f334]) ).
tcf(c_213,plain,
! [X0: $i] :
( r1(X0,sK86(X0))
| r1(X0,sK85(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f341]) ).
tcf(c_214,plain,
! [X0: $i] :
( r1(X0,sK85(X0))
| ~ sP2(X0)
| ~ p104(sK86(X0)) ),
inference(cnf_transformation,[],[f340]) ).
tcf(c_215,plain,
! [X0: $i] :
( r1(X0,sK86(X0))
| ~ sP2(X0)
| ~ p304(sK85(X0)) ),
inference(cnf_transformation,[],[f339]) ).
tcf(c_216,plain,
! [X0: $i] :
( ~ sP2(X0)
| ~ p104(sK86(X0))
| ~ p304(sK85(X0)) ),
inference(cnf_transformation,[],[f338]) ).
tcf(c_217,plain,
! [X0: $i] :
( r1(X0,sK88(X0))
| r1(X0,sK87(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f345]) ).
tcf(c_218,plain,
! [X0: $i] :
( r1(X0,sK87(X0))
| ~ sP1(X0)
| ~ p104(sK88(X0)) ),
inference(cnf_transformation,[],[f344]) ).
tcf(c_219,plain,
! [X0: $i] :
( r1(X0,sK88(X0))
| ~ sP1(X0)
| ~ p204(sK87(X0)) ),
inference(cnf_transformation,[],[f343]) ).
tcf(c_220,plain,
! [X0: $i] :
( ~ sP1(X0)
| ~ p104(sK88(X0))
| ~ p204(sK87(X0)) ),
inference(cnf_transformation,[],[f342]) ).
tcf(c_225,negated_conjecture,
! [X0: $i] :
( sP40(X0)
| ~ r1(sK91,X0) ),
inference(cnf_transformation,[],[f356]) ).
tcf(c_226,negated_conjecture,
( p601(sK91)
| p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91) ),
inference(cnf_transformation,[],[f355]) ).
tcf(c_227,negated_conjecture,
( p501(sK91)
| p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91) ),
inference(cnf_transformation,[],[f354]) ).
tcf(c_228,negated_conjecture,
! [X0: $i] :
( p401(sK91)
| p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ r1(sK91,X0) ),
inference(cnf_transformation,[],[f353]) ).
tcf(c_229,negated_conjecture,
! [X0: $i,X1: $i] :
( p301(sK91)
| p302(sK91)
| p303(sK91)
| p304(X1)
| p305(X0)
| ~ r1(sK91,X1)
| ~ r1(sK91,X0) ),
inference(cnf_transformation,[],[f352]) ).
tcf(c_230,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] :
( p201(sK91)
| p202(sK91)
| p203(X2)
| p204(X1)
| p205(X0)
| ~ r1(sK91,X2)
| ~ r1(sK91,X1)
| ~ r1(sK91,X0) ),
inference(cnf_transformation,[],[f351]) ).
tcf(c_231,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p101(sK91)
| p102(X3)
| p103(X2)
| p104(X1)
| p105(X0)
| ~ r1(sK91,X3)
| ~ r1(sK91,X2)
| ~ r1(sK91,X1)
| ~ r1(sK91,X0) ),
inference(cnf_transformation,[],[f350]) ).
tcf(c_232,plain,
r1(sK91,sK91),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_233,plain,
( sP10(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_109]) ).
tcf(c_234,plain,
( sP11(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_108]) ).
tcf(c_235,plain,
( sP12(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_107]) ).
tcf(c_236,plain,
( sP13(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_106]) ).
tcf(c_237,plain,
( sP14(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_105]) ).
tcf(c_238,plain,
( sP0(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_239,plain,
( sP15(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_240,plain,
( sP16(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_92]) ).
tcf(c_241,plain,
( sP17(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_91]) ).
tcf(c_242,plain,
( sP18(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_90]) ).
tcf(c_243,plain,
( sP19(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_89]) ).
tcf(c_244,plain,
( sP20(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_88]) ).
tcf(c_245,plain,
( sP21(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_87]) ).
tcf(c_246,plain,
( sP22(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_86]) ).
tcf(c_247,plain,
( sP1(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_79]) ).
tcf(c_248,plain,
( sP2(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_78]) ).
tcf(c_249,plain,
( sP23(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_77]) ).
tcf(c_250,plain,
( sP24(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_76]) ).
tcf(c_251,plain,
( sP25(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_75]) ).
tcf(c_252,plain,
( sP3(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_74]) ).
tcf(c_253,plain,
( sP26(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_73]) ).
tcf(c_254,plain,
( sP27(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_72]) ).
tcf(c_255,plain,
( sP28(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_71]) ).
tcf(c_256,plain,
( sP29(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_70]) ).
tcf(c_257,plain,
( sP30(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_258,plain,
( sP31(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_259,plain,
( sP4(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_64]) ).
tcf(c_260,plain,
( sP5(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_63]) ).
tcf(c_261,plain,
( sP6(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_62]) ).
tcf(c_262,plain,
( sP32(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_263,plain,
( sP33(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_264,plain,
( sP7(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_265,plain,
( sP8(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_266,plain,
( sP34(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_267,plain,
( sP35(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_56]) ).
tcf(c_268,plain,
( sP9(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_269,plain,
( sP36(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_270,plain,
( sP37(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_271,plain,
( sP38(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_52]) ).
tcf(c_272,plain,
( sP39(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_273,plain,
( sP40(sK91)
| ~ r1(sK91,sK91) ),
inference(instantiation,[status(thm)],[c_225]) ).
tcf(c_275,plain,
( ~ p101(sK91)
| ~ p301(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_276,plain,
( ~ p101(sK91)
| ~ p401(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_277,plain,
( ~ p101(sK91)
| ~ p501(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_278,plain,
( ~ p101(sK91)
| ~ p601(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_280,plain,
( ~ p201(sK91)
| ~ p401(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_118]) ).
tcf(c_281,plain,
( ~ p201(sK91)
| ~ p501(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_117]) ).
tcf(c_282,plain,
( ~ p201(sK91)
| ~ p601(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_116]) ).
tcf(c_284,plain,
( ~ p301(sK91)
| ~ p501(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_285,plain,
( ~ p301(sK91)
| ~ p601(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_286,plain,
( ~ p401(sK91)
| ~ p501(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_287,plain,
( ~ p401(sK91)
| ~ p601(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_288,plain,
( ~ p501(sK91)
| ~ p601(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_289,plain,
( ~ p202(sK91)
| ~ p302(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_290,plain,
( ~ p202(sK91)
| ~ p402(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_291,plain,
( ~ p202(sK91)
| ~ p502(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_292,plain,
( ~ p202(sK91)
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_293,plain,
( ~ p302(sK91)
| ~ p402(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_294,plain,
( ~ p302(sK91)
| ~ p502(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_295,plain,
( ~ p302(sK91)
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_296,plain,
( ~ p402(sK91)
| ~ p502(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_297,plain,
( ~ p402(sK91)
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_298,plain,
( ~ p502(sK91)
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_299,plain,
( ~ p303(sK91)
| ~ p403(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_85]) ).
tcf(c_300,plain,
( ~ p303(sK91)
| ~ p503(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_84]) ).
tcf(c_301,plain,
( ~ p303(sK91)
| ~ p603(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_83]) ).
tcf(c_302,plain,
( ~ p403(sK91)
| ~ p503(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_82]) ).
tcf(c_303,plain,
( ~ p403(sK91)
| ~ p603(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_81]) ).
tcf(c_304,plain,
( ~ p503(sK91)
| ~ p603(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_80]) ).
tcf(c_305,plain,
( ~ p404(sK91)
| ~ p504(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_306,plain,
( ~ p404(sK91)
| ~ p604(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_307,plain,
( ~ p504(sK91)
| ~ p604(sK91)
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_308,plain,
( ~ sP40(sK91)
| ~ p505(sK91)
| ~ p605(sK91) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_310,plain,
( r1(sK91,sK70(sK91))
| ~ sP10(sK91)
| ~ p202(sK91) ),
inference(instantiation,[status(thm)],[c_183]) ).
tcf(c_311,plain,
( ~ sP11(sK91)
| ~ p302(sK91)
| ~ p102(sK69(sK91)) ),
inference(instantiation,[status(thm)],[c_182]) ).
tcf(c_312,plain,
( r1(sK91,sK69(sK91))
| ~ sP11(sK91)
| ~ p302(sK91) ),
inference(instantiation,[status(thm)],[c_181]) ).
tcf(c_314,plain,
( r1(sK91,sK68(sK91))
| ~ sP12(sK91)
| ~ p402(sK91) ),
inference(instantiation,[status(thm)],[c_179]) ).
tcf(c_315,plain,
( ~ sP13(sK91)
| ~ p502(sK91)
| ~ p102(sK67(sK91)) ),
inference(instantiation,[status(thm)],[c_178]) ).
tcf(c_316,plain,
( r1(sK91,sK67(sK91))
| ~ sP13(sK91)
| ~ p502(sK91) ),
inference(instantiation,[status(thm)],[c_177]) ).
tcf(c_317,plain,
( ~ sP14(sK91)
| ~ p602(sK91)
| ~ p102(sK66(sK91)) ),
inference(instantiation,[status(thm)],[c_176]) ).
tcf(c_318,plain,
( r1(sK91,sK66(sK91))
| ~ sP14(sK91)
| ~ p602(sK91) ),
inference(instantiation,[status(thm)],[c_175]) ).
tcf(c_320,plain,
( r1(sK91,sK65(sK91))
| ~ sP15(sK91)
| ~ p303(sK91) ),
inference(instantiation,[status(thm)],[c_173]) ).
tcf(c_322,plain,
( r1(sK91,sK64(sK91))
| ~ sP16(sK91)
| ~ p403(sK91) ),
inference(instantiation,[status(thm)],[c_171]) ).
tcf(c_324,plain,
( r1(sK91,sK63(sK91))
| ~ sP17(sK91)
| ~ p503(sK91) ),
inference(instantiation,[status(thm)],[c_169]) ).
tcf(c_326,plain,
( r1(sK91,sK62(sK91))
| ~ sP18(sK91)
| ~ p603(sK91) ),
inference(instantiation,[status(thm)],[c_167]) ).
tcf(c_328,plain,
( r1(sK91,sK61(sK91))
| ~ sP19(sK91)
| ~ p303(sK91) ),
inference(instantiation,[status(thm)],[c_165]) ).
tcf(c_330,plain,
( r1(sK91,sK60(sK91))
| ~ sP20(sK91)
| ~ p403(sK91) ),
inference(instantiation,[status(thm)],[c_163]) ).
tcf(c_332,plain,
( r1(sK91,sK59(sK91))
| ~ sP21(sK91)
| ~ p503(sK91) ),
inference(instantiation,[status(thm)],[c_161]) ).
tcf(c_334,plain,
( r1(sK91,sK58(sK91))
| ~ sP22(sK91)
| ~ p603(sK91) ),
inference(instantiation,[status(thm)],[c_159]) ).
tcf(c_335,plain,
( ~ sP23(sK91)
| ~ p404(sK91)
| ~ p104(sK57(sK91)) ),
inference(instantiation,[status(thm)],[c_158]) ).
tcf(c_336,plain,
( r1(sK91,sK57(sK91))
| ~ sP23(sK91)
| ~ p404(sK91) ),
inference(instantiation,[status(thm)],[c_157]) ).
tcf(c_337,plain,
( ~ sP24(sK91)
| ~ p504(sK91)
| ~ p104(sK56(sK91)) ),
inference(instantiation,[status(thm)],[c_156]) ).
tcf(c_338,plain,
( r1(sK91,sK56(sK91))
| ~ sP24(sK91)
| ~ p504(sK91) ),
inference(instantiation,[status(thm)],[c_155]) ).
tcf(c_340,plain,
( r1(sK91,sK55(sK91))
| ~ sP25(sK91)
| ~ p604(sK91) ),
inference(instantiation,[status(thm)],[c_153]) ).
tcf(c_342,plain,
( r1(sK91,sK54(sK91))
| ~ sP26(sK91)
| ~ p404(sK91) ),
inference(instantiation,[status(thm)],[c_151]) ).
tcf(c_344,plain,
( r1(sK91,sK53(sK91))
| ~ sP27(sK91)
| ~ p504(sK91) ),
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_346,plain,
( r1(sK91,sK52(sK91))
| ~ sP28(sK91)
| ~ p604(sK91) ),
inference(instantiation,[status(thm)],[c_147]) ).
tcf(c_348,plain,
( r1(sK91,sK51(sK91))
| ~ sP29(sK91)
| ~ p404(sK91) ),
inference(instantiation,[status(thm)],[c_145]) ).
tcf(c_350,plain,
( r1(sK91,sK50(sK91))
| ~ sP30(sK91)
| ~ p504(sK91) ),
inference(instantiation,[status(thm)],[c_143]) ).
tcf(c_352,plain,
( r1(sK91,sK49(sK91))
| ~ sP31(sK91)
| ~ p604(sK91) ),
inference(instantiation,[status(thm)],[c_141]) ).
tcf(c_354,plain,
( r1(sK91,sK48(sK91))
| ~ sP32(sK91)
| ~ p505(sK91) ),
inference(instantiation,[status(thm)],[c_139]) ).
tcf(c_356,plain,
( r1(sK91,sK47(sK91))
| ~ sP33(sK91)
| ~ p605(sK91) ),
inference(instantiation,[status(thm)],[c_137]) ).
tcf(c_358,plain,
( r1(sK91,sK46(sK91))
| ~ sP34(sK91)
| ~ p505(sK91) ),
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_360,plain,
( r1(sK91,sK45(sK91))
| ~ sP35(sK91)
| ~ p605(sK91) ),
inference(instantiation,[status(thm)],[c_133]) ).
tcf(c_362,plain,
( r1(sK91,sK44(sK91))
| ~ sP36(sK91)
| ~ p505(sK91) ),
inference(instantiation,[status(thm)],[c_131]) ).
tcf(c_364,plain,
( r1(sK91,sK43(sK91))
| ~ sP37(sK91)
| ~ p605(sK91) ),
inference(instantiation,[status(thm)],[c_129]) ).
tcf(c_366,plain,
( r1(sK91,sK42(sK91))
| ~ sP38(sK91)
| ~ p505(sK91) ),
inference(instantiation,[status(thm)],[c_127]) ).
tcf(c_368,plain,
( r1(sK91,sK41(sK91))
| ~ sP39(sK91)
| ~ p605(sK91) ),
inference(instantiation,[status(thm)],[c_125]) ).
tcf(c_374,plain,
( r1(sK91,sK88(sK91))
| ~ sP1(sK91)
| ~ p204(sK87(sK91)) ),
inference(instantiation,[status(thm)],[c_219]) ).
tcf(c_378,plain,
( r1(sK91,sK86(sK91))
| ~ sP2(sK91)
| ~ p304(sK85(sK91)) ),
inference(instantiation,[status(thm)],[c_215]) ).
tcf(c_383,plain,
( r1(sK91,sK83(sK91))
| ~ sP3(sK91)
| ~ p204(sK84(sK91)) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_384,plain,
( r1(sK91,sK84(sK91))
| r1(sK91,sK83(sK91))
| ~ sP3(sK91) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_386,plain,
( r1(sK91,sK82(sK91))
| ~ sP4(sK91)
| ~ p205(sK81(sK91)) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_390,plain,
( r1(sK91,sK80(sK91))
| ~ sP5(sK91)
| ~ p305(sK79(sK91)) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_394,plain,
( r1(sK91,sK78(sK91))
| ~ sP6(sK91)
| ~ p405(sK77(sK91)) ),
inference(instantiation,[status(thm)],[c_199]) ).
tcf(c_398,plain,
( r1(sK91,sK76(sK91))
| ~ sP7(sK91)
| ~ p305(sK75(sK91)) ),
inference(instantiation,[status(thm)],[c_195]) ).
tcf(c_402,plain,
( r1(sK91,sK74(sK91))
| ~ sP8(sK91)
| ~ p405(sK73(sK91)) ),
inference(instantiation,[status(thm)],[c_191]) ).
tcf(c_406,plain,
( r1(sK91,sK72(sK91))
| ~ sP9(sK91)
| ~ p405(sK71(sK91)) ),
inference(instantiation,[status(thm)],[c_187]) ).
tcf(c_1469,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p605(X0)
| ~ p405(sK41(X0)) ),
inference(resolution,[status(thm)],[c_51,c_126]) ).
tcf(c_1497,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p405(sK42(X0)) ),
inference(resolution,[status(thm)],[c_52,c_128]) ).
tcf(c_1525,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p605(X0)
| ~ p305(sK43(X0)) ),
inference(resolution,[status(thm)],[c_53,c_130]) ).
tcf(c_1553,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p305(sK44(X0)) ),
inference(resolution,[status(thm)],[c_54,c_132]) ).
tcf(c_1581,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p605(X0)
| ~ p205(sK45(X0)) ),
inference(resolution,[status(thm)],[c_56,c_134]) ).
tcf(c_1609,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p205(sK46(X0)) ),
inference(resolution,[status(thm)],[c_57,c_136]) ).
tcf(c_1637,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p605(X0)
| ~ p105(sK47(X0)) ),
inference(resolution,[status(thm)],[c_60,c_138]) ).
tcf(c_1665,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p105(sK48(X0)) ),
inference(resolution,[status(thm)],[c_61,c_140]) ).
tcf(c_1693,plain,
! [X0: $i] :
( ~ p604(X0)
| ~ sP40(X0)
| ~ p304(sK49(X0)) ),
inference(resolution,[status(thm)],[c_68,c_142]) ).
tcf(c_1721,plain,
! [X0: $i] :
( ~ p504(X0)
| ~ sP40(X0)
| ~ p304(sK50(X0)) ),
inference(resolution,[status(thm)],[c_69,c_144]) ).
tcf(c_1749,plain,
! [X0: $i] :
( ~ p404(X0)
| ~ sP40(X0)
| ~ p304(sK51(X0)) ),
inference(resolution,[status(thm)],[c_70,c_146]) ).
tcf(c_1777,plain,
! [X0: $i] :
( ~ p604(X0)
| ~ sP40(X0)
| ~ p204(sK52(X0)) ),
inference(resolution,[status(thm)],[c_71,c_148]) ).
tcf(c_1805,plain,
! [X0: $i] :
( ~ p504(X0)
| ~ sP40(X0)
| ~ p204(sK53(X0)) ),
inference(resolution,[status(thm)],[c_72,c_150]) ).
tcf(c_1833,plain,
! [X0: $i] :
( ~ p404(X0)
| ~ sP40(X0)
| ~ p204(sK54(X0)) ),
inference(resolution,[status(thm)],[c_73,c_152]) ).
tcf(c_1861,plain,
! [X0: $i] :
( ~ p604(X0)
| ~ sP40(X0)
| ~ p104(sK55(X0)) ),
inference(resolution,[status(thm)],[c_75,c_154]) ).
tcf(c_1889,plain,
! [X0: $i] :
( ~ p504(X0)
| ~ sP40(X0)
| ~ p104(sK56(X0)) ),
inference(resolution,[status(thm)],[c_76,c_156]) ).
tcf(c_1917,plain,
! [X0: $i] :
( ~ p404(X0)
| ~ sP40(X0)
| ~ p104(sK57(X0)) ),
inference(resolution,[status(thm)],[c_77,c_158]) ).
tcf(c_1945,plain,
! [X0: $i] :
( ~ p603(X0)
| ~ sP40(X0)
| ~ p203(sK58(X0)) ),
inference(resolution,[status(thm)],[c_86,c_160]) ).
tcf(c_1973,plain,
! [X0: $i] :
( ~ p503(X0)
| ~ sP40(X0)
| ~ p203(sK59(X0)) ),
inference(resolution,[status(thm)],[c_87,c_162]) ).
tcf(c_2001,plain,
! [X0: $i] :
( ~ p403(X0)
| ~ sP40(X0)
| ~ p203(sK60(X0)) ),
inference(resolution,[status(thm)],[c_88,c_164]) ).
tcf(c_2029,plain,
! [X0: $i] :
( ~ p303(X0)
| ~ sP40(X0)
| ~ p203(sK61(X0)) ),
inference(resolution,[status(thm)],[c_89,c_166]) ).
tcf(c_2057,plain,
! [X0: $i] :
( ~ p603(X0)
| ~ sP40(X0)
| ~ p103(sK62(X0)) ),
inference(resolution,[status(thm)],[c_90,c_168]) ).
tcf(c_2085,plain,
! [X0: $i] :
( ~ p503(X0)
| ~ sP40(X0)
| ~ p103(sK63(X0)) ),
inference(resolution,[status(thm)],[c_91,c_170]) ).
tcf(c_2113,plain,
! [X0: $i] :
( ~ p403(X0)
| ~ sP40(X0)
| ~ p103(sK64(X0)) ),
inference(resolution,[status(thm)],[c_92,c_172]) ).
tcf(c_2141,plain,
! [X0: $i] :
( ~ p303(X0)
| ~ sP40(X0)
| ~ p103(sK65(X0)) ),
inference(resolution,[status(thm)],[c_93,c_174]) ).
tcf(c_2169,plain,
! [X0: $i] :
( ~ p602(X0)
| ~ sP40(X0)
| ~ p102(sK66(X0)) ),
inference(resolution,[status(thm)],[c_105,c_176]) ).
tcf(c_2197,plain,
! [X0: $i] :
( ~ p502(X0)
| ~ sP40(X0)
| ~ p102(sK67(X0)) ),
inference(resolution,[status(thm)],[c_106,c_178]) ).
tcf(c_2225,plain,
! [X0: $i] :
( ~ p402(X0)
| ~ sP40(X0)
| ~ p102(sK68(X0)) ),
inference(resolution,[status(thm)],[c_107,c_180]) ).
tcf(c_2253,plain,
! [X0: $i] :
( ~ p302(X0)
| ~ sP40(X0)
| ~ p102(sK69(X0)) ),
inference(resolution,[status(thm)],[c_108,c_182]) ).
tcf(c_2281,plain,
! [X0: $i] :
( ~ p202(X0)
| ~ sP40(X0)
| ~ p102(sK70(X0)) ),
inference(resolution,[status(thm)],[c_109,c_184]) ).
tcf(c_2309,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p305(sK72(X0))
| ~ p405(sK71(X0)) ),
inference(resolution,[status(thm)],[c_55,c_188]) ).
tcf(c_2331,plain,
! [X0: $i] :
( r1(X0,sK71(X0))
| ~ sP40(X0)
| ~ p305(sK72(X0)) ),
inference(resolution,[status(thm)],[c_55,c_186]) ).
tcf(c_2332,plain,
( r1(sK91,sK71(sK91))
| ~ sP40(sK91)
| ~ p305(sK72(sK91)) ),
inference(instantiation,[status(thm)],[c_2331]) ).
tcf(c_2342,plain,
! [X0: $i] :
( r1(X0,sK72(X0))
| r1(X0,sK71(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_55,c_185]) ).
tcf(c_2343,plain,
( r1(sK91,sK72(sK91))
| r1(sK91,sK71(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2342]) ).
tcf(c_2365,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p205(sK74(X0))
| ~ p405(sK73(X0)) ),
inference(resolution,[status(thm)],[c_58,c_192]) ).
tcf(c_2387,plain,
! [X0: $i] :
( r1(X0,sK73(X0))
| ~ sP40(X0)
| ~ p205(sK74(X0)) ),
inference(resolution,[status(thm)],[c_58,c_190]) ).
tcf(c_2388,plain,
( r1(sK91,sK73(sK91))
| ~ sP40(sK91)
| ~ p205(sK74(sK91)) ),
inference(instantiation,[status(thm)],[c_2387]) ).
tcf(c_2398,plain,
! [X0: $i] :
( r1(X0,sK74(X0))
| r1(X0,sK73(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_58,c_189]) ).
tcf(c_2399,plain,
( r1(sK91,sK74(sK91))
| r1(sK91,sK73(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2398]) ).
tcf(c_2421,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p205(sK76(X0))
| ~ p305(sK75(X0)) ),
inference(resolution,[status(thm)],[c_59,c_196]) ).
tcf(c_2443,plain,
! [X0: $i] :
( r1(X0,sK75(X0))
| ~ sP40(X0)
| ~ p205(sK76(X0)) ),
inference(resolution,[status(thm)],[c_59,c_194]) ).
tcf(c_2444,plain,
( r1(sK91,sK75(sK91))
| ~ sP40(sK91)
| ~ p205(sK76(sK91)) ),
inference(instantiation,[status(thm)],[c_2443]) ).
tcf(c_2454,plain,
! [X0: $i] :
( r1(X0,sK76(X0))
| r1(X0,sK75(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_59,c_193]) ).
tcf(c_2455,plain,
( r1(sK91,sK76(sK91))
| r1(sK91,sK75(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2454]) ).
tcf(c_2477,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p105(sK78(X0))
| ~ p405(sK77(X0)) ),
inference(resolution,[status(thm)],[c_62,c_200]) ).
tcf(c_2499,plain,
! [X0: $i] :
( r1(X0,sK77(X0))
| ~ sP40(X0)
| ~ p105(sK78(X0)) ),
inference(resolution,[status(thm)],[c_62,c_198]) ).
tcf(c_2500,plain,
( r1(sK91,sK77(sK91))
| ~ sP40(sK91)
| ~ p105(sK78(sK91)) ),
inference(instantiation,[status(thm)],[c_2499]) ).
tcf(c_2510,plain,
! [X0: $i] :
( r1(X0,sK78(X0))
| r1(X0,sK77(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_62,c_197]) ).
tcf(c_2511,plain,
( r1(sK91,sK78(sK91))
| r1(sK91,sK77(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2510]) ).
tcf(c_2533,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p105(sK80(X0))
| ~ p305(sK79(X0)) ),
inference(resolution,[status(thm)],[c_63,c_204]) ).
tcf(c_2555,plain,
! [X0: $i] :
( r1(X0,sK79(X0))
| ~ sP40(X0)
| ~ p105(sK80(X0)) ),
inference(resolution,[status(thm)],[c_63,c_202]) ).
tcf(c_2556,plain,
( r1(sK91,sK79(sK91))
| ~ sP40(sK91)
| ~ p105(sK80(sK91)) ),
inference(instantiation,[status(thm)],[c_2555]) ).
tcf(c_2566,plain,
! [X0: $i] :
( r1(X0,sK80(X0))
| r1(X0,sK79(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_63,c_201]) ).
tcf(c_2567,plain,
( r1(sK91,sK80(sK91))
| r1(sK91,sK79(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2566]) ).
tcf(c_2589,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p105(sK82(X0))
| ~ p205(sK81(X0)) ),
inference(resolution,[status(thm)],[c_64,c_208]) ).
tcf(c_2611,plain,
! [X0: $i] :
( r1(X0,sK81(X0))
| ~ sP40(X0)
| ~ p105(sK82(X0)) ),
inference(resolution,[status(thm)],[c_64,c_206]) ).
tcf(c_2612,plain,
( r1(sK91,sK81(sK91))
| ~ sP40(sK91)
| ~ p105(sK82(sK91)) ),
inference(instantiation,[status(thm)],[c_2611]) ).
tcf(c_2622,plain,
! [X0: $i] :
( r1(X0,sK82(X0))
| r1(X0,sK81(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_64,c_205]) ).
tcf(c_2623,plain,
( r1(sK91,sK82(sK91))
| r1(sK91,sK81(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2622]) ).
tcf(c_2645,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p204(sK84(X0))
| ~ p304(sK83(X0)) ),
inference(resolution,[status(thm)],[c_74,c_212]) ).
tcf(c_2656,plain,
! [X0: $i] :
( r1(X0,sK84(X0))
| ~ sP40(X0)
| ~ p304(sK83(X0)) ),
inference(resolution,[status(thm)],[c_74,c_211]) ).
tcf(c_2657,plain,
( r1(sK91,sK84(sK91))
| ~ sP40(sK91)
| ~ p304(sK83(sK91)) ),
inference(instantiation,[status(thm)],[c_2656]) ).
tcf(c_2701,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p104(sK86(X0))
| ~ p304(sK85(X0)) ),
inference(resolution,[status(thm)],[c_78,c_216]) ).
tcf(c_2723,plain,
! [X0: $i] :
( r1(X0,sK85(X0))
| ~ sP40(X0)
| ~ p104(sK86(X0)) ),
inference(resolution,[status(thm)],[c_78,c_214]) ).
tcf(c_2724,plain,
( r1(sK91,sK85(sK91))
| ~ sP40(sK91)
| ~ p104(sK86(sK91)) ),
inference(instantiation,[status(thm)],[c_2723]) ).
tcf(c_2734,plain,
! [X0: $i] :
( r1(X0,sK86(X0))
| r1(X0,sK85(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_78,c_213]) ).
tcf(c_2735,plain,
( r1(sK91,sK86(sK91))
| r1(sK91,sK85(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2734]) ).
tcf(c_2757,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p104(sK88(X0))
| ~ p204(sK87(X0)) ),
inference(resolution,[status(thm)],[c_79,c_220]) ).
tcf(c_2779,plain,
! [X0: $i] :
( r1(X0,sK87(X0))
| ~ sP40(X0)
| ~ p104(sK88(X0)) ),
inference(resolution,[status(thm)],[c_79,c_218]) ).
tcf(c_2780,plain,
( r1(sK91,sK87(sK91))
| ~ sP40(sK91)
| ~ p104(sK88(sK91)) ),
inference(instantiation,[status(thm)],[c_2779]) ).
tcf(c_2790,plain,
! [X0: $i] :
( r1(X0,sK88(X0))
| r1(X0,sK87(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_79,c_217]) ).
tcf(c_2791,plain,
( r1(sK91,sK88(sK91))
| r1(sK91,sK87(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2790]) ).
tcf(c_2869,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p101(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_120,c_226]) ).
tcf(c_2870,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p101(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_2869,c_232,c_273,c_278,c_226]) ).
tcf(c_2887,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p201(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_116,c_226]) ).
tcf(c_2888,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p201(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_2887,c_232,c_273,c_282,c_226]) ).
tcf(c_2905,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p301(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_113,c_226]) ).
tcf(c_2906,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p301(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_2905,c_232,c_273,c_285,c_226]) ).
tcf(c_2923,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p401(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_111,c_226]) ).
tcf(c_2924,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p401(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_2923,c_232,c_273,c_287,c_226]) ).
tcf(c_2941,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p501(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_110,c_226]) ).
tcf(c_2942,plain,
( p602(sK91)
| p603(sK91)
| p604(sK91)
| p605(sK91)
| ~ p501(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_2941,c_232,c_273,c_288,c_226]) ).
tcf(c_2984,plain,
( p502(sK91)
| p602(sK91)
| p503(sK91)
| p603(sK91)
| p504(sK91)
| p604(sK91)
| p505(sK91)
| p605(sK91) ),
inference(resolution,[status(thm)],[c_227,c_2942]) ).
tcf(c_3009,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p101(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_121,c_227]) ).
tcf(c_3010,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p101(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_3009,c_232,c_273,c_277,c_227]) ).
tcf(c_3027,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p201(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_117,c_227]) ).
tcf(c_3028,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p201(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_3027,c_232,c_273,c_281,c_227]) ).
tcf(c_3045,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p301(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_114,c_227]) ).
tcf(c_3046,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p301(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_3045,c_232,c_273,c_284,c_227]) ).
tcf(c_3063,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p401(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_112,c_227]) ).
tcf(c_3064,plain,
( p502(sK91)
| p503(sK91)
| p504(sK91)
| p505(sK91)
| ~ p401(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_3063,c_232,c_273,c_286,c_227]) ).
tcf(c_3109,plain,
! [X0: $i] :
( p402(sK91)
| p502(sK91)
| p403(sK91)
| p503(sK91)
| p404(sK91)
| p504(sK91)
| p505(sK91)
| p405(X0)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_228,c_3064]) ).
tcf(c_3138,plain,
! [X0: $i] :
( p402(sK91)
| p602(sK91)
| p403(sK91)
| p603(sK91)
| p404(sK91)
| p604(sK91)
| p605(sK91)
| p405(X0)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_228,c_2924]) ).
tcf(c_3167,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p101(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_122,c_228]) ).
tcf(c_3169,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p101(sK91)
| ~ r1(sK91,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3167,c_232,c_273,c_276,c_228]) ).
tcf(c_3190,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p201(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_118,c_228]) ).
tcf(c_3192,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p201(sK91)
| ~ r1(sK91,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3190,c_232,c_273,c_280,c_228]) ).
tcf(c_3213,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p301(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_115,c_228]) ).
tcf(c_3215,plain,
! [X0: $i] :
( p402(sK91)
| p403(sK91)
| p404(sK91)
| p405(X0)
| ~ p301(sK91)
| ~ r1(sK91,X0) ),
inference(global_subsumption_just,[status(thm)],[c_3213,c_232,c_273,c_3213]) ).
tcf(c_5955,plain,
! [X0: $i] :
( ~ iPr_def_10
| p405(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_3215]) ).
tcf(c_5956,plain,
( iPr_def_10
| p402(sK91)
| p403(sK91)
| p404(sK91)
| ~ p301(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3215]) ).
tcf(c_5957,plain,
( iPr_def_10
| p402(sK91)
| p403(sK91)
| p404(sK91)
| ~ p201(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3192]) ).
tcf(c_5958,plain,
( iPr_def_10
| p402(sK91)
| p403(sK91)
| p404(sK91)
| ~ p101(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3169]) ).
tcf(c_5959,plain,
( iPr_def_10
| p402(sK91)
| p602(sK91)
| p403(sK91)
| p603(sK91)
| p404(sK91)
| p604(sK91)
| p605(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3138]) ).
tcf(c_5960,plain,
( iPr_def_10
| p402(sK91)
| p502(sK91)
| p403(sK91)
| p503(sK91)
| p404(sK91)
| p504(sK91)
| p505(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3109]) ).
tcf(c_5961,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| p103(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_231]) ).
tcf(c_5962,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| p104(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_231]) ).
tcf(c_5963,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| p102(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_231]) ).
tcf(c_5964,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| p105(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_231]) ).
tcf(c_5965,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| p101(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_231]) ).
tcf(c_5966,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| p204(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_230]) ).
tcf(c_5967,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| p203(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_230]) ).
tcf(c_5968,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| p205(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_230]) ).
tcf(c_5969,negated_conjecture,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| p201(sK91)
| p202(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_230]) ).
tcf(c_5970,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| p304(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_229]) ).
tcf(c_5971,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| p305(X0)
| ~ r1(sK91,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_229]) ).
tcf(c_5972,negated_conjecture,
( iPr_def_19
| iPr_def_18
| p301(sK91)
| p302(sK91)
| p303(sK91) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_229]) ).
tcf(c_5989,plain,
! [X0: $i] :
( ~ p505(X0)
| ~ p605(X0)
| ~ r1(sK91,X0) ),
inference(resolution,[status(thm)],[c_50,c_225]) ).
tcf(c_6064,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| p202(sK91)
| ~ p301(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_119,c_5969]) ).
tcf(c_6065,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| p202(sK91)
| ~ p301(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6064,c_232,c_273,c_6064]) ).
tcf(c_6070,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p301(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_123,c_5965]) ).
tcf(c_6071,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p301(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6070,c_232,c_273,c_275,c_5965]) ).
tcf(c_6076,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p201(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_124,c_5965]) ).
tcf(c_6077,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p201(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6076,c_232,c_273,c_6076]) ).
tcf(c_6082,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ sP40(X0)
| ~ p605(X0)
| ~ r1(sK91,sK41(X0)) ),
inference(resolution,[status(thm)],[c_1469,c_5955]) ).
tcf(c_6083,plain,
( ~ iPr_def_10
| ~ sP40(sK91)
| ~ p605(sK91)
| ~ r1(sK91,sK41(sK91)) ),
inference(instantiation,[status(thm)],[c_6082]) ).
tcf(c_6090,plain,
! [X0: $i] :
( ~ iPr_def_10
| ~ sP40(X0)
| ~ p505(X0)
| ~ r1(sK91,sK42(X0)) ),
inference(resolution,[status(thm)],[c_1497,c_5955]) ).
tcf(c_6091,plain,
( ~ iPr_def_10
| ~ sP40(sK91)
| ~ p505(sK91)
| ~ r1(sK91,sK42(sK91)) ),
inference(instantiation,[status(thm)],[c_6090]) ).
tcf(c_6108,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| p202(sK91) ),
inference(resolution,[status(thm)],[c_6077,c_5969]) ).
tcf(c_6166,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ sP40(X0)
| ~ p605(X0)
| ~ r1(sK91,sK47(X0)) ),
inference(resolution,[status(thm)],[c_5964,c_1637]) ).
tcf(c_6167,plain,
( ~ iPr_def_14
| ~ sP40(sK91)
| ~ p605(sK91)
| ~ r1(sK91,sK47(sK91)) ),
inference(instantiation,[status(thm)],[c_6166]) ).
tcf(c_6168,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ sP40(X0)
| ~ p505(X0)
| ~ r1(sK91,sK48(X0)) ),
inference(resolution,[status(thm)],[c_5964,c_1665]) ).
tcf(c_6169,plain,
( ~ iPr_def_14
| ~ sP40(sK91)
| ~ p505(sK91)
| ~ r1(sK91,sK48(sK91)) ),
inference(instantiation,[status(thm)],[c_6168]) ).
tcf(c_6197,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ p604(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK55(X0)) ),
inference(resolution,[status(thm)],[c_1861,c_5962]) ).
tcf(c_6198,plain,
( ~ iPr_def_12
| ~ p604(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK55(sK91)) ),
inference(instantiation,[status(thm)],[c_6197]) ).
tcf(c_6205,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ p504(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK56(X0)) ),
inference(resolution,[status(thm)],[c_1889,c_5962]) ).
tcf(c_6206,plain,
( ~ iPr_def_12
| ~ p504(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK56(sK91)) ),
inference(instantiation,[status(thm)],[c_6205]) ).
tcf(c_6213,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ p404(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK57(X0)) ),
inference(resolution,[status(thm)],[c_1917,c_5962]) ).
tcf(c_6214,plain,
( ~ iPr_def_12
| ~ p404(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK57(sK91)) ),
inference(instantiation,[status(thm)],[c_6213]) ).
tcf(c_6224,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ p604(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK52(X0)) ),
inference(resolution,[status(thm)],[c_5966,c_1777]) ).
tcf(c_6225,plain,
( ~ iPr_def_15
| ~ p604(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK52(sK91)) ),
inference(instantiation,[status(thm)],[c_6224]) ).
tcf(c_6226,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ p504(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK53(X0)) ),
inference(resolution,[status(thm)],[c_5966,c_1805]) ).
tcf(c_6227,plain,
( ~ iPr_def_15
| ~ p504(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK53(sK91)) ),
inference(instantiation,[status(thm)],[c_6226]) ).
tcf(c_6228,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ p404(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK54(X0)) ),
inference(resolution,[status(thm)],[c_5966,c_1833]) ).
tcf(c_6229,plain,
( ~ iPr_def_15
| ~ p404(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK54(sK91)) ),
inference(instantiation,[status(thm)],[c_6228]) ).
tcf(c_6233,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ p603(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK58(X0)) ),
inference(resolution,[status(thm)],[c_5967,c_1945]) ).
tcf(c_6234,plain,
( ~ iPr_def_16
| ~ p603(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK58(sK91)) ),
inference(instantiation,[status(thm)],[c_6233]) ).
tcf(c_6238,plain,
! [X0: $i] :
( ~ iPr_def_17
| ~ sP40(X0)
| ~ p605(X0)
| ~ r1(sK91,sK45(X0)) ),
inference(resolution,[status(thm)],[c_5968,c_1581]) ).
tcf(c_6239,plain,
( ~ iPr_def_17
| ~ sP40(sK91)
| ~ p605(sK91)
| ~ r1(sK91,sK45(sK91)) ),
inference(instantiation,[status(thm)],[c_6238]) ).
tcf(c_6240,plain,
! [X0: $i] :
( ~ iPr_def_17
| ~ sP40(X0)
| ~ p505(X0)
| ~ r1(sK91,sK46(X0)) ),
inference(resolution,[status(thm)],[c_5968,c_1609]) ).
tcf(c_6241,plain,
( ~ iPr_def_17
| ~ sP40(sK91)
| ~ p505(sK91)
| ~ r1(sK91,sK46(sK91)) ),
inference(instantiation,[status(thm)],[c_6240]) ).
tcf(c_6248,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ p503(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK59(X0)) ),
inference(resolution,[status(thm)],[c_1973,c_5967]) ).
tcf(c_6249,plain,
( ~ iPr_def_16
| ~ p503(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK59(sK91)) ),
inference(instantiation,[status(thm)],[c_6248]) ).
tcf(c_6256,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ p403(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK60(X0)) ),
inference(resolution,[status(thm)],[c_2001,c_5967]) ).
tcf(c_6257,plain,
( ~ iPr_def_16
| ~ p403(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK60(sK91)) ),
inference(instantiation,[status(thm)],[c_6256]) ).
tcf(c_6264,plain,
! [X0: $i] :
( ~ iPr_def_16
| ~ p303(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK61(X0)) ),
inference(resolution,[status(thm)],[c_2029,c_5967]) ).
tcf(c_6265,plain,
( ~ iPr_def_16
| ~ p303(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK61(sK91)) ),
inference(instantiation,[status(thm)],[c_6264]) ).
tcf(c_6272,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ p603(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK62(X0)) ),
inference(resolution,[status(thm)],[c_2057,c_5961]) ).
tcf(c_6273,plain,
( ~ iPr_def_11
| ~ p603(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK62(sK91)) ),
inference(instantiation,[status(thm)],[c_6272]) ).
tcf(c_6280,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ p503(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK63(X0)) ),
inference(resolution,[status(thm)],[c_2085,c_5961]) ).
tcf(c_6281,plain,
( ~ iPr_def_11
| ~ p503(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK63(sK91)) ),
inference(instantiation,[status(thm)],[c_6280]) ).
tcf(c_6288,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ p403(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK64(X0)) ),
inference(resolution,[status(thm)],[c_2113,c_5961]) ).
tcf(c_6289,plain,
( ~ iPr_def_11
| ~ p403(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK64(sK91)) ),
inference(instantiation,[status(thm)],[c_6288]) ).
tcf(c_6296,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ p303(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK65(X0)) ),
inference(resolution,[status(thm)],[c_2141,c_5961]) ).
tcf(c_6297,plain,
( ~ iPr_def_11
| ~ p303(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK65(sK91)) ),
inference(instantiation,[status(thm)],[c_6296]) ).
tcf(c_6304,plain,
! [X0: $i] :
( ~ iPr_def_18
| ~ p604(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK49(X0)) ),
inference(resolution,[status(thm)],[c_5970,c_1693]) ).
tcf(c_6305,plain,
( ~ iPr_def_18
| ~ p604(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK49(sK91)) ),
inference(instantiation,[status(thm)],[c_6304]) ).
tcf(c_6306,plain,
! [X0: $i] :
( ~ iPr_def_18
| ~ p504(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK50(X0)) ),
inference(resolution,[status(thm)],[c_5970,c_1721]) ).
tcf(c_6307,plain,
( ~ iPr_def_18
| ~ p504(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK50(sK91)) ),
inference(instantiation,[status(thm)],[c_6306]) ).
tcf(c_6308,plain,
! [X0: $i] :
( ~ iPr_def_18
| ~ p404(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK51(X0)) ),
inference(resolution,[status(thm)],[c_5970,c_1749]) ).
tcf(c_6309,plain,
( ~ iPr_def_18
| ~ p404(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK51(sK91)) ),
inference(instantiation,[status(thm)],[c_6308]) ).
tcf(c_6313,plain,
! [X0: $i] :
( ~ iPr_def_19
| ~ sP40(X0)
| ~ p605(X0)
| ~ r1(sK91,sK43(X0)) ),
inference(resolution,[status(thm)],[c_5971,c_1525]) ).
tcf(c_6314,plain,
( ~ iPr_def_19
| ~ sP40(sK91)
| ~ p605(sK91)
| ~ r1(sK91,sK43(sK91)) ),
inference(instantiation,[status(thm)],[c_6313]) ).
tcf(c_6315,plain,
! [X0: $i] :
( ~ iPr_def_19
| ~ sP40(X0)
| ~ p505(X0)
| ~ r1(sK91,sK44(X0)) ),
inference(resolution,[status(thm)],[c_5971,c_1553]) ).
tcf(c_6316,plain,
( ~ iPr_def_19
| ~ sP40(sK91)
| ~ p505(sK91)
| ~ r1(sK91,sK44(sK91)) ),
inference(instantiation,[status(thm)],[c_6315]) ).
tcf(c_6322,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| p302(sK91)
| p303(sK91) ),
inference(resolution,[status(thm)],[c_5972,c_6071]) ).
tcf(c_6326,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p602(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK66(X0)) ),
inference(resolution,[status(thm)],[c_2169,c_5963]) ).
tcf(c_6327,plain,
( ~ iPr_def_13
| ~ p602(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK66(sK91)) ),
inference(instantiation,[status(thm)],[c_6326]) ).
tcf(c_6334,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p502(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK67(X0)) ),
inference(resolution,[status(thm)],[c_2197,c_5963]) ).
tcf(c_6335,plain,
( ~ iPr_def_13
| ~ p502(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK67(sK91)) ),
inference(instantiation,[status(thm)],[c_6334]) ).
tcf(c_6342,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p402(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK68(X0)) ),
inference(resolution,[status(thm)],[c_2225,c_5963]) ).
tcf(c_6343,plain,
( ~ iPr_def_13
| ~ p402(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK68(sK91)) ),
inference(instantiation,[status(thm)],[c_6342]) ).
tcf(c_6350,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p302(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK69(X0)) ),
inference(resolution,[status(thm)],[c_2253,c_5963]) ).
tcf(c_6351,plain,
( ~ iPr_def_13
| ~ p302(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK69(sK91)) ),
inference(instantiation,[status(thm)],[c_6350]) ).
tcf(c_6358,plain,
! [X0: $i] :
( ~ iPr_def_13
| ~ p202(X0)
| ~ sP40(X0)
| ~ r1(sK91,sK70(X0)) ),
inference(resolution,[status(thm)],[c_2281,c_5963]) ).
tcf(c_6359,plain,
( ~ iPr_def_13
| ~ p202(sK91)
| ~ sP40(sK91)
| ~ r1(sK91,sK70(sK91)) ),
inference(instantiation,[status(thm)],[c_6358]) ).
tcf(c_6366,plain,
! [X0: $i] :
( ~ iPr_def_19
| ~ sP40(X0)
| ~ p405(sK71(X0))
| ~ r1(sK91,sK72(X0)) ),
inference(resolution,[status(thm)],[c_2309,c_5971]) ).
tcf(c_6367,plain,
( ~ iPr_def_19
| ~ sP40(sK91)
| ~ p405(sK71(sK91))
| ~ r1(sK91,sK72(sK91)) ),
inference(instantiation,[status(thm)],[c_6366]) ).
tcf(c_6380,plain,
! [X0: $i] :
( ~ iPr_def_17
| ~ sP40(X0)
| ~ p405(sK73(X0))
| ~ r1(sK91,sK74(X0)) ),
inference(resolution,[status(thm)],[c_2365,c_5968]) ).
tcf(c_6381,plain,
( ~ iPr_def_17
| ~ sP40(sK91)
| ~ p405(sK73(sK91))
| ~ r1(sK91,sK74(sK91)) ),
inference(instantiation,[status(thm)],[c_6380]) ).
tcf(c_6388,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p402(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6065,c_103]) ).
tcf(c_6389,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p502(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6065,c_102]) ).
tcf(c_6390,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6065,c_101]) ).
tcf(c_6391,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p602(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6390,c_232,c_273,c_292,c_6064]) ).
tcf(c_6393,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p502(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6389,c_232,c_273,c_291,c_6064]) ).
tcf(c_6395,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p301(sK91)
| ~ p402(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6388,c_232,c_273,c_6388]) ).
tcf(c_6407,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p302(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6108,c_104]) ).
tcf(c_6408,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p402(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6108,c_103]) ).
tcf(c_6409,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p502(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6108,c_102]) ).
tcf(c_6410,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ~ p602(sK91)
| ~ sP40(sK91) ),
inference(resolution,[status(thm)],[c_6108,c_101]) ).
tcf(c_6411,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| ~ p602(sK91)
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_6410,c_232,c_237,c_273,c_292,c_318,c_5969,c_6077,c_6327]) ).
tcf(c_6412,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_12
| iPr_def_11
| ~ p602(sK91) ),
inference(renaming,[status(thm)],[c_6411]) ).
tcf(c_6413,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| ~ p502(sK91)
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_6409,c_232,c_236,c_273,c_291,c_316,c_5969,c_6077,c_6335]) ).
tcf(c_6414,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_12
| iPr_def_11
| ~ p502(sK91) ),
inference(renaming,[status(thm)],[c_6413]) ).
tcf(c_6415,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| ~ p402(sK91)
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_6408,c_232,c_235,c_273,c_290,c_314,c_5969,c_6077,c_6343]) ).
tcf(c_6416,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_12
| iPr_def_11
| ~ p402(sK91) ),
inference(renaming,[status(thm)],[c_6415]) ).
tcf(c_6417,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| ~ p302(sK91)
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_6407,c_232,c_234,c_273,c_289,c_312,c_5969,c_6077,c_6351]) ).
tcf(c_6418,plain,
( iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_12
| iPr_def_11
| ~ p302(sK91) ),
inference(renaming,[status(thm)],[c_6417]) ).
tcf(c_6424,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p302(sK91)
| p303(sK91)
| ~ p602(sK91) ),
inference(resolution,[status(thm)],[c_6391,c_5972]) ).
tcf(c_6425,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p602(sK91)
| p303(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6424,c_232,c_273,c_292,c_295,c_5972,c_6064]) ).
tcf(c_6426,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p303(sK91)
| ~ p602(sK91) ),
inference(renaming,[status(thm)],[c_6425]) ).
tcf(c_6439,plain,
! [X0: $i] :
( ~ iPr_def_17
| ~ sP40(X0)
| ~ p305(sK75(X0))
| ~ r1(sK91,sK76(X0)) ),
inference(resolution,[status(thm)],[c_2421,c_5968]) ).
tcf(c_6440,plain,
( ~ iPr_def_17
| ~ sP40(sK91)
| ~ p305(sK75(sK91))
| ~ r1(sK91,sK76(sK91)) ),
inference(instantiation,[status(thm)],[c_6439]) ).
tcf(c_6453,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ sP40(X0)
| ~ p405(sK77(X0))
| ~ r1(sK91,sK78(X0)) ),
inference(resolution,[status(thm)],[c_2477,c_5964]) ).
tcf(c_6454,plain,
( ~ iPr_def_14
| ~ sP40(sK91)
| ~ p405(sK77(sK91))
| ~ r1(sK91,sK78(sK91)) ),
inference(instantiation,[status(thm)],[c_6453]) ).
tcf(c_6467,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ sP40(X0)
| ~ p305(sK79(X0))
| ~ r1(sK91,sK80(X0)) ),
inference(resolution,[status(thm)],[c_2533,c_5964]) ).
tcf(c_6468,plain,
( ~ iPr_def_14
| ~ sP40(sK91)
| ~ p305(sK79(sK91))
| ~ r1(sK91,sK80(sK91)) ),
inference(instantiation,[status(thm)],[c_6467]) ).
tcf(c_6483,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p302(sK91)
| p303(sK91)
| ~ p502(sK91) ),
inference(resolution,[status(thm)],[c_6393,c_5972]) ).
tcf(c_6484,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p502(sK91)
| p303(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6483,c_232,c_273,c_291,c_294,c_5972,c_6064]) ).
tcf(c_6485,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p303(sK91)
| ~ p502(sK91) ),
inference(renaming,[status(thm)],[c_6484]) ).
tcf(c_6491,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p302(sK91)
| p303(sK91)
| ~ p402(sK91) ),
inference(resolution,[status(thm)],[c_6395,c_5972]) ).
tcf(c_6492,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| ~ p402(sK91)
| p303(sK91) ),
inference(global_subsumption_just,[status(thm)],[c_6491,c_232,c_273,c_293,c_6491]) ).
tcf(c_6493,plain,
( iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| p303(sK91)
| ~ p402(sK91) ),
inference(renaming,[status(thm)],[c_6492]) ).
tcf(c_6503,plain,
! [X0: $i] :
( ~ iPr_def_14
| ~ sP40(X0)
| ~ p205(sK81(X0))
| ~ r1(sK91,sK82(X0)) ),
inference(resolution,[status(thm)],[c_2589,c_5964]) ).
tcf(c_6504,plain,
( ~ iPr_def_14
| ~ sP40(sK91)
| ~ p205(sK81(sK91))
| ~ r1(sK91,sK82(sK91)) ),
inference(instantiation,[status(thm)],[c_6503]) ).
tcf(c_6517,plain,
! [X0: $i] :
( ~ iPr_def_15
| ~ sP40(X0)
| ~ p304(sK83(X0))
| ~ r1(sK91,sK84(X0)) ),
inference(resolution,[status(thm)],[c_2645,c_5966]) ).
tcf(c_6518,plain,
( ~ iPr_def_15
| ~ sP40(sK91)
| ~ p304(sK83(sK91))
| ~ r1(sK91,sK84(sK91)) ),
inference(instantiation,[status(thm)],[c_6517]) ).
tcf(c_6531,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ sP40(X0)
| ~ p304(sK85(X0))
| ~ r1(sK91,sK86(X0)) ),
inference(resolution,[status(thm)],[c_2701,c_5962]) ).
tcf(c_6532,plain,
( ~ iPr_def_12
| ~ sP40(sK91)
| ~ p304(sK85(sK91))
| ~ r1(sK91,sK86(sK91)) ),
inference(instantiation,[status(thm)],[c_6531]) ).
tcf(c_6545,plain,
! [X0: $i] :
( ~ iPr_def_12
| ~ sP40(X0)
| ~ p204(sK87(X0))
| ~ r1(sK91,sK88(X0)) ),
inference(resolution,[status(thm)],[c_2757,c_5962]) ).
tcf(c_6546,plain,
( ~ iPr_def_12
| ~ sP40(sK91)
| ~ p204(sK87(sK91))
| ~ r1(sK91,sK88(sK91)) ),
inference(instantiation,[status(thm)],[c_6545]) ).
tcf(c_6582,plain,
! [X0: $i] :
( p103(sK90(X0))
| ~ iPr_def_11
| ~ r1(sK91,sK90(X0)) ),
inference(instantiation,[status(thm)],[c_5961]) ).
tcf(c_6583,plain,
( p103(sK90(sK91))
| ~ iPr_def_11
| ~ r1(sK91,sK90(sK91)) ),
inference(instantiation,[status(thm)],[c_6582]) ).
tcf(c_6596,plain,
( ~ p505(sK91)
| ~ p605(sK91) ),
inference(resolution,[status(thm)],[c_5989,c_49]) ).
tcf(c_6778,plain,
! [X0: $i] :
( p203(sK89(X0))
| ~ iPr_def_16
| ~ r1(sK91,sK89(X0)) ),
inference(instantiation,[status(thm)],[c_5967]) ).
tcf(c_6779,plain,
( p203(sK89(sK91))
| ~ iPr_def_16
| ~ r1(sK91,sK89(sK91)) ),
inference(instantiation,[status(thm)],[c_6778]) ).
tcf(c_6782,plain,
! [X0: $i] :
( p204(sK84(X0))
| ~ iPr_def_15
| ~ r1(sK91,sK84(X0)) ),
inference(instantiation,[status(thm)],[c_5966]) ).
tcf(c_6783,plain,
( p204(sK84(sK91))
| ~ iPr_def_15
| ~ r1(sK91,sK84(sK91)) ),
inference(instantiation,[status(thm)],[c_6782]) ).
tcf(c_6786,plain,
! [X0: $i] :
( p304(sK83(X0))
| ~ iPr_def_18
| ~ r1(sK91,sK83(X0)) ),
inference(instantiation,[status(thm)],[c_5970]) ).
tcf(c_6787,plain,
( p304(sK83(sK91))
| ~ iPr_def_18
| ~ r1(sK91,sK83(sK91)) ),
inference(instantiation,[status(thm)],[c_6786]) ).
tcf(c_6792,plain,
! [X0: $i] :
( p305(sK72(X0))
| ~ iPr_def_19
| ~ r1(sK91,sK72(X0)) ),
inference(instantiation,[status(thm)],[c_5971]) ).
tcf(c_6793,plain,
( p305(sK72(sK91))
| ~ iPr_def_19
| ~ r1(sK91,sK72(sK91)) ),
inference(instantiation,[status(thm)],[c_6792]) ).
tcf(c_6798,plain,
! [X0: $i] :
( p405(sK71(X0))
| ~ iPr_def_10
| ~ r1(sK91,sK71(X0)) ),
inference(instantiation,[status(thm)],[c_5955]) ).
tcf(c_6799,plain,
( p405(sK71(sK91))
| ~ iPr_def_10
| ~ r1(sK91,sK71(sK91)) ),
inference(instantiation,[status(thm)],[c_6798]) ).
tcf(c_6808,plain,
! [X0: $i] :
( p105(sK78(X0))
| ~ iPr_def_14
| ~ r1(sK91,sK78(X0)) ),
inference(instantiation,[status(thm)],[c_5964]) ).
tcf(c_6809,plain,
( p105(sK78(sK91))
| ~ iPr_def_14
| ~ r1(sK91,sK78(sK91)) ),
inference(instantiation,[status(thm)],[c_6808]) ).
tcf(c_6810,plain,
! [X0: $i] :
( p105(sK80(X0))
| ~ iPr_def_14
| ~ r1(sK91,sK80(X0)) ),
inference(instantiation,[status(thm)],[c_5964]) ).
tcf(c_6811,plain,
( p105(sK80(sK91))
| ~ iPr_def_14
| ~ r1(sK91,sK80(sK91)) ),
inference(instantiation,[status(thm)],[c_6810]) ).
tcf(c_6812,plain,
! [X0: $i] :
( p105(sK82(X0))
| ~ iPr_def_14
| ~ r1(sK91,sK82(X0)) ),
inference(instantiation,[status(thm)],[c_5964]) ).
tcf(c_6813,plain,
( p105(sK82(sK91))
| ~ iPr_def_14
| ~ r1(sK91,sK82(sK91)) ),
inference(instantiation,[status(thm)],[c_6812]) ).
tcf(c_6814,plain,
! [X0: $i] :
( p405(sK77(X0))
| ~ iPr_def_10
| ~ r1(sK91,sK77(X0)) ),
inference(instantiation,[status(thm)],[c_5955]) ).
tcf(c_6815,plain,
( p405(sK77(sK91))
| ~ iPr_def_10
| ~ r1(sK91,sK77(sK91)) ),
inference(instantiation,[status(thm)],[c_6814]) ).
tcf(c_6816,plain,
! [X0: $i] :
( p305(sK79(X0))
| ~ iPr_def_19
| ~ r1(sK91,sK79(X0)) ),
inference(instantiation,[status(thm)],[c_5971]) ).
tcf(c_6817,plain,
( p305(sK79(sK91))
| ~ iPr_def_19
| ~ r1(sK91,sK79(sK91)) ),
inference(instantiation,[status(thm)],[c_6816]) ).
tcf(c_6818,plain,
! [X0: $i] :
( p104(sK56(X0))
| ~ iPr_def_12
| ~ r1(sK91,sK56(X0)) ),
inference(instantiation,[status(thm)],[c_5962]) ).
tcf(c_6819,plain,
( p104(sK56(sK91))
| ~ iPr_def_12
| ~ r1(sK91,sK56(sK91)) ),
inference(instantiation,[status(thm)],[c_6818]) ).
tcf(c_6820,plain,
! [X0: $i] :
( p104(sK86(X0))
| ~ iPr_def_12
| ~ r1(sK91,sK86(X0)) ),
inference(instantiation,[status(thm)],[c_5962]) ).
tcf(c_6821,plain,
( p104(sK86(sK91))
| ~ iPr_def_12
| ~ r1(sK91,sK86(sK91)) ),
inference(instantiation,[status(thm)],[c_6820]) ).
tcf(c_6822,plain,
! [X0: $i] :
( p104(sK88(X0))
| ~ iPr_def_12
| ~ r1(sK91,sK88(X0)) ),
inference(instantiation,[status(thm)],[c_5962]) ).
tcf(c_6823,plain,
( p104(sK88(sK91))
| ~ iPr_def_12
| ~ r1(sK91,sK88(sK91)) ),
inference(instantiation,[status(thm)],[c_6822]) ).
tcf(c_6824,plain,
! [X0: $i] :
( p204(sK87(X0))
| ~ iPr_def_15
| ~ r1(sK91,sK87(X0)) ),
inference(instantiation,[status(thm)],[c_5966]) ).
tcf(c_6825,plain,
( p204(sK87(sK91))
| ~ iPr_def_15
| ~ r1(sK91,sK87(sK91)) ),
inference(instantiation,[status(thm)],[c_6824]) ).
tcf(c_6826,plain,
! [X0: $i] :
( p304(sK85(X0))
| ~ iPr_def_18
| ~ r1(sK91,sK85(X0)) ),
inference(instantiation,[status(thm)],[c_5970]) ).
tcf(c_6827,plain,
( p304(sK85(sK91))
| ~ iPr_def_18
| ~ r1(sK91,sK85(sK91)) ),
inference(instantiation,[status(thm)],[c_6826]) ).
tcf(c_6832,plain,
! [X0: $i] :
( p205(sK74(X0))
| ~ iPr_def_17
| ~ r1(sK91,sK74(X0)) ),
inference(instantiation,[status(thm)],[c_5968]) ).
tcf(c_6833,plain,
( p205(sK74(sK91))
| ~ iPr_def_17
| ~ r1(sK91,sK74(sK91)) ),
inference(instantiation,[status(thm)],[c_6832]) ).
tcf(c_6834,plain,
! [X0: $i] :
( p205(sK76(X0))
| ~ iPr_def_17
| ~ r1(sK91,sK76(X0)) ),
inference(instantiation,[status(thm)],[c_5968]) ).
tcf(c_6835,plain,
( p205(sK76(sK91))
| ~ iPr_def_17
| ~ r1(sK91,sK76(sK91)) ),
inference(instantiation,[status(thm)],[c_6834]) ).
tcf(c_6836,plain,
! [X0: $i] :
( p205(sK81(X0))
| ~ iPr_def_17
| ~ r1(sK91,sK81(X0)) ),
inference(instantiation,[status(thm)],[c_5968]) ).
tcf(c_6837,plain,
( p205(sK81(sK91))
| ~ iPr_def_17
| ~ r1(sK91,sK81(sK91)) ),
inference(instantiation,[status(thm)],[c_6836]) ).
tcf(c_6842,plain,
! [X0: $i] :
( p104(sK57(X0))
| ~ iPr_def_12
| ~ r1(sK91,sK57(X0)) ),
inference(instantiation,[status(thm)],[c_5962]) ).
tcf(c_6843,plain,
( p104(sK57(sK91))
| ~ iPr_def_12
| ~ r1(sK91,sK57(sK91)) ),
inference(instantiation,[status(thm)],[c_6842]) ).
tcf(c_6844,plain,
! [X0: $i] :
( p102(sK66(X0))
| ~ iPr_def_13
| ~ r1(sK91,sK66(X0)) ),
inference(instantiation,[status(thm)],[c_5963]) ).
tcf(c_6845,plain,
( p102(sK66(sK91))
| ~ iPr_def_13
| ~ r1(sK91,sK66(sK91)) ),
inference(instantiation,[status(thm)],[c_6844]) ).
tcf(c_6846,plain,
! [X0: $i] :
( p102(sK67(X0))
| ~ iPr_def_13
| ~ r1(sK91,sK67(X0)) ),
inference(instantiation,[status(thm)],[c_5963]) ).
tcf(c_6847,plain,
( p102(sK67(sK91))
| ~ iPr_def_13
| ~ r1(sK91,sK67(sK91)) ),
inference(instantiation,[status(thm)],[c_6846]) ).
tcf(c_6848,plain,
! [X0: $i] :
( p102(sK69(X0))
| ~ iPr_def_13
| ~ r1(sK91,sK69(X0)) ),
inference(instantiation,[status(thm)],[c_5963]) ).
tcf(c_6849,plain,
( p102(sK69(sK91))
| ~ iPr_def_13
| ~ r1(sK91,sK69(sK91)) ),
inference(instantiation,[status(thm)],[c_6848]) ).
tcf(c_6850,plain,
! [X0: $i] :
( p405(sK73(X0))
| ~ iPr_def_10
| ~ r1(sK91,sK73(X0)) ),
inference(instantiation,[status(thm)],[c_5955]) ).
tcf(c_6851,plain,
( p405(sK73(sK91))
| ~ iPr_def_10
| ~ r1(sK91,sK73(sK91)) ),
inference(instantiation,[status(thm)],[c_6850]) ).
tcf(c_6852,plain,
! [X0: $i] :
( p305(sK75(X0))
| ~ iPr_def_19
| ~ r1(sK91,sK75(X0)) ),
inference(instantiation,[status(thm)],[c_5971]) ).
tcf(c_6853,plain,
( p305(sK75(sK91))
| ~ iPr_def_19
| ~ r1(sK91,sK75(sK91)) ),
inference(instantiation,[status(thm)],[c_6852]) ).
fof(f8,definition,
! [X1] :
( ~ sP0(X1)
| ? [X46] :
( ~ p103(X46)
& r1(X1,X46) )
| ? [X45] :
( ~ p203(X45)
& r1(X1,X45) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X1] :
( ~ sP1(X1)
| ? [X36] :
( ~ p104(X36)
& r1(X1,X36) )
| ? [X35] :
( ~ p204(X35)
& r1(X1,X35) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X1] :
( ~ sP2(X1)
| ? [X34] :
( ~ p104(X34)
& r1(X1,X34) )
| ? [X33] :
( ~ p304(X33)
& r1(X1,X33) ) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X1] :
( ~ sP3(X1)
| ? [X29] :
( ~ p204(X29)
& r1(X1,X29) )
| ? [X28] :
( ~ p304(X28)
& r1(X1,X28) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X1] :
( ~ sP4(X1)
| ? [X21] :
( ~ p105(X21)
& r1(X1,X21) )
| ? [X20] :
( ~ p205(X20)
& r1(X1,X20) ) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X1] :
( ~ sP5(X1)
| ? [X19] :
( ~ p105(X19)
& r1(X1,X19) )
| ? [X18] :
( ~ p305(X18)
& r1(X1,X18) ) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X1] :
( ~ sP6(X1)
| ? [X17] :
( ~ p105(X17)
& r1(X1,X17) )
| ? [X16] :
( ~ p405(X16)
& r1(X1,X16) ) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X1] :
( ~ sP7(X1)
| ? [X13] :
( ~ p205(X13)
& r1(X1,X13) )
| ? [X12] :
( ~ p305(X12)
& r1(X1,X12) ) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X1] :
( ~ sP8(X1)
| ? [X11] :
( ~ p205(X11)
& r1(X1,X11) )
| ? [X10] :
( ~ p405(X10)
& r1(X1,X10) ) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X1] :
( ~ sP9(X1)
| ? [X7] :
( ~ p305(X7)
& r1(X1,X7) )
| ? [X6] :
( ~ p405(X6)
& r1(X1,X6) ) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X1] :
( ~ sP10(X1)
| ? [X51] :
( ~ p102(X51)
& r1(X1,X51) )
| ~ p202(X1) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X1] :
( ~ sP11(X1)
| ? [X50] :
( ~ p102(X50)
& r1(X1,X50) )
| ~ p302(X1) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X1] :
( ~ sP12(X1)
| ? [X49] :
( ~ p102(X49)
& r1(X1,X49) )
| ~ p402(X1) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X1] :
( ~ sP13(X1)
| ? [X48] :
( ~ p102(X48)
& r1(X1,X48) )
| ~ p502(X1) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X1] :
( ~ sP14(X1)
| ? [X47] :
( ~ p102(X47)
& r1(X1,X47) )
| ~ p602(X1) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X1] :
( ~ sP15(X1)
| ? [X44] :
( ~ p103(X44)
& r1(X1,X44) )
| ~ p303(X1) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X1] :
( ~ sP16(X1)
| ? [X43] :
( ~ p103(X43)
& r1(X1,X43) )
| ~ p403(X1) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X1] :
( ~ sP17(X1)
| ? [X42] :
( ~ p103(X42)
& r1(X1,X42) )
| ~ p503(X1) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X1] :
( ~ sP18(X1)
| ? [X41] :
( ~ p103(X41)
& r1(X1,X41) )
| ~ p603(X1) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X1] :
( ~ sP19(X1)
| ? [X40] :
( ~ p203(X40)
& r1(X1,X40) )
| ~ p303(X1) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X1] :
( ~ sP20(X1)
| ? [X39] :
( ~ p203(X39)
& r1(X1,X39) )
| ~ p403(X1) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X1] :
( ~ sP21(X1)
| ? [X38] :
( ~ p203(X38)
& r1(X1,X38) )
| ~ p503(X1) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X1] :
( ~ sP22(X1)
| ? [X37] :
( ~ p203(X37)
& r1(X1,X37) )
| ~ p603(X1) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X1] :
( ~ sP23(X1)
| ? [X32] :
( ~ p104(X32)
& r1(X1,X32) )
| ~ p404(X1) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X1] :
( ~ sP24(X1)
| ? [X31] :
( ~ p104(X31)
& r1(X1,X31) )
| ~ p504(X1) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X1] :
( ~ sP25(X1)
| ? [X30] :
( ~ p104(X30)
& r1(X1,X30) )
| ~ p604(X1) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X1] :
( ~ sP26(X1)
| ? [X27] :
( ~ p204(X27)
& r1(X1,X27) )
| ~ p404(X1) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X1] :
( ~ sP27(X1)
| ? [X26] :
( ~ p204(X26)
& r1(X1,X26) )
| ~ p504(X1) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X1] :
( ~ sP28(X1)
| ? [X25] :
( ~ p204(X25)
& r1(X1,X25) )
| ~ p604(X1) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X1] :
( ~ sP29(X1)
| ? [X24] :
( ~ p304(X24)
& r1(X1,X24) )
| ~ p404(X1) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X1] :
( ~ sP30(X1)
| ? [X23] :
( ~ p304(X23)
& r1(X1,X23) )
| ~ p504(X1) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X1] :
( ~ sP31(X1)
| ? [X22] :
( ~ p304(X22)
& r1(X1,X22) )
| ~ p604(X1) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X1] :
( ~ sP32(X1)
| ? [X15] :
( ~ p105(X15)
& r1(X1,X15) )
| ~ p505(X1) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X1] :
( ~ sP33(X1)
| ? [X14] :
( ~ p105(X14)
& r1(X1,X14) )
| ~ p605(X1) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X1] :
( ~ sP34(X1)
| ? [X9] :
( ~ p205(X9)
& r1(X1,X9) )
| ~ p505(X1) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f43,definition,
! [X1] :
( ~ sP35(X1)
| ? [X8] :
( ~ p205(X8)
& r1(X1,X8) )
| ~ p605(X1) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f44,definition,
! [X1] :
( ~ sP36(X1)
| ? [X5] :
( ~ p305(X5)
& r1(X1,X5) )
| ~ p505(X1) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f45,definition,
! [X1] :
( ~ sP37(X1)
| ? [X4] :
( ~ p305(X4)
& r1(X1,X4) )
| ~ p605(X1) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f46,definition,
! [X1] :
( ~ sP38(X1)
| ? [X3] :
( ~ p405(X3)
& r1(X1,X3) )
| ~ p505(X1) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f47,definition,
! [X1] :
( ~ sP39(X1)
| ? [X2] :
( ~ p405(X2)
& r1(X1,X2) )
| ~ p605(X1) ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f48,definition,
! [X1] :
( ~ sP40(X1)
| ( ( ~ p101(X1)
| ~ p201(X1) )
& ( ~ p101(X1)
| ~ p301(X1) )
& ( ~ p101(X1)
| ~ p401(X1) )
& ( ~ p101(X1)
| ~ p501(X1) )
& ( ~ p101(X1)
| ~ p601(X1) )
& ( ~ p201(X1)
| ~ p301(X1) )
& ( ~ p201(X1)
| ~ p401(X1) )
& ( ~ p201(X1)
| ~ p501(X1) )
& ( ~ p201(X1)
| ~ p601(X1) )
& ( ~ p301(X1)
| ~ p401(X1) )
& ( ~ p301(X1)
| ~ p501(X1) )
& ( ~ p301(X1)
| ~ p601(X1) )
& ( ~ p401(X1)
| ~ p501(X1) )
& ( ~ p401(X1)
| ~ p601(X1) )
& ( ~ p501(X1)
| ~ p601(X1) )
& sP10(X1)
& sP11(X1)
& sP12(X1)
& sP13(X1)
& sP14(X1)
& ( ~ p202(X1)
| ~ p302(X1) )
& ( ~ p202(X1)
| ~ p402(X1) )
& ( ~ p202(X1)
| ~ p502(X1) )
& ( ~ p202(X1)
| ~ p602(X1) )
& ( ~ p302(X1)
| ~ p402(X1) )
& ( ~ p302(X1)
| ~ p502(X1) )
& ( ~ p302(X1)
| ~ p602(X1) )
& ( ~ p402(X1)
| ~ p502(X1) )
& ( ~ p402(X1)
| ~ p602(X1) )
& ( ~ p502(X1)
| ~ p602(X1) )
& sP0(X1)
& sP15(X1)
& sP16(X1)
& sP17(X1)
& sP18(X1)
& sP19(X1)
& sP20(X1)
& sP21(X1)
& sP22(X1)
& ( ~ p303(X1)
| ~ p403(X1) )
& ( ~ p303(X1)
| ~ p503(X1) )
& ( ~ p303(X1)
| ~ p603(X1) )
& ( ~ p403(X1)
| ~ p503(X1) )
& ( ~ p403(X1)
| ~ p603(X1) )
& ( ~ p503(X1)
| ~ p603(X1) )
& sP1(X1)
& sP2(X1)
& sP23(X1)
& sP24(X1)
& sP25(X1)
& sP3(X1)
& sP26(X1)
& sP27(X1)
& sP28(X1)
& sP29(X1)
& sP30(X1)
& sP31(X1)
& ( ~ p404(X1)
| ~ p504(X1) )
& ( ~ p404(X1)
| ~ p604(X1) )
& ( ~ p504(X1)
| ~ p604(X1) )
& sP4(X1)
& sP5(X1)
& sP6(X1)
& sP32(X1)
& sP33(X1)
& sP7(X1)
& sP8(X1)
& sP34(X1)
& sP35(X1)
& sP9(X1)
& sP36(X1)
& sP37(X1)
& sP38(X1)
& sP39(X1)
& ( ~ p505(X1)
| ~ p605(X1) ) ) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f49,plain,
? [X0] :
( ( p101(X0)
| ! [X61] :
( p102(X61)
| ~ r1(X0,X61) )
| ! [X60] :
( p103(X60)
| ~ r1(X0,X60) )
| ! [X59] :
( p104(X59)
| ~ r1(X0,X59) )
| ! [X58] :
( p105(X58)
| ~ r1(X0,X58) ) )
& ( p201(X0)
| p202(X0)
| ! [X57] :
( p203(X57)
| ~ r1(X0,X57) )
| ! [X56] :
( p204(X56)
| ~ r1(X0,X56) )
| ! [X55] :
( p205(X55)
| ~ r1(X0,X55) ) )
& ( p301(X0)
| p302(X0)
| p303(X0)
| ! [X54] :
( p304(X54)
| ~ r1(X0,X54) )
| ! [X53] :
( p305(X53)
| ~ r1(X0,X53) ) )
& ( p401(X0)
| p402(X0)
| p403(X0)
| p404(X0)
| ! [X52] :
( p405(X52)
| ~ r1(X0,X52) ) )
& ( p501(X0)
| p502(X0)
| p503(X0)
| p504(X0)
| p505(X0) )
& ( p601(X0)
| p602(X0)
| p603(X0)
| p604(X0)
| p605(X0) )
& ! [X1] :
( sP40(X1)
| ~ r1(X0,X1) ) ),
inference(definition_folding,[],[f7,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8]) ).
fof(f169,plain,
! [X1] :
( ~ sP0(X1)
| ? [X46] :
( ~ p103(X46)
& r1(X1,X46) )
| ? [X45] :
( ~ p203(X45)
& r1(X1,X45) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f170,plain,
! [X0] :
( ~ sP0(X0)
| ? [X2] :
( ~ p103(X2)
& r1(X0,X2) )
| ? [X1] :
( ~ p203(X1)
& r1(X0,X1) ) ),
inference(rectify,[],[f169]) ).
fof(f171,plain,
! [X0] :
( ~ sP0(X0)
| ( ~ p103(sK90(X0))
& r1(X0,sK90(X0)) )
| ( ~ p203(sK89(X0))
& r1(X0,sK89(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK89,sK90]),skolemize(X1,sK89(X0)),skolemize(X2,sK90(X0))],[f170]) ).
fof(f346,plain,
! [X0] :
( ~ sP0(X0)
| ~ p103(sK90(X0))
| ~ p203(sK89(X0)) ),
inference(cnf_transformation,[],[f171]) ).
fof(f347,plain,
! [X0] :
( ~ sP0(X0)
| r1(X0,sK90(X0))
| ~ p203(sK89(X0)) ),
inference(cnf_transformation,[],[f171]) ).
fof(f348,plain,
! [X0] :
( ~ sP0(X0)
| ~ p103(sK90(X0))
| r1(X0,sK89(X0)) ),
inference(cnf_transformation,[],[f171]) ).
fof(f349,plain,
! [X0] :
( ~ sP0(X0)
| r1(X0,sK90(X0))
| r1(X0,sK89(X0)) ),
inference(cnf_transformation,[],[f171]) ).
tcf(c_221,plain,
! [X0: $i] :
( r1(X0,sK90(X0))
| r1(X0,sK89(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f349]) ).
tcf(c_222,plain,
! [X0: $i] :
( r1(X0,sK89(X0))
| ~ sP0(X0)
| ~ p103(sK90(X0)) ),
inference(cnf_transformation,[],[f348]) ).
tcf(c_223,plain,
! [X0: $i] :
( r1(X0,sK90(X0))
| ~ sP0(X0)
| ~ p203(sK89(X0)) ),
inference(cnf_transformation,[],[f347]) ).
tcf(c_224,plain,
! [X0: $i] :
( ~ sP0(X0)
| ~ p103(sK90(X0))
| ~ p203(sK89(X0)) ),
inference(cnf_transformation,[],[f346]) ).
tcf(c_370,plain,
( r1(sK91,sK90(sK91))
| ~ sP0(sK91)
| ~ p203(sK89(sK91)) ),
inference(instantiation,[status(thm)],[c_223]) ).
tcf(c_2813,plain,
! [X0: $i] :
( ~ sP40(X0)
| ~ p103(sK90(X0))
| ~ p203(sK89(X0)) ),
inference(resolution,[status(thm)],[c_94,c_224]) ).
tcf(c_2835,plain,
! [X0: $i] :
( r1(X0,sK89(X0))
| ~ sP40(X0)
| ~ p103(sK90(X0)) ),
inference(resolution,[status(thm)],[c_94,c_222]) ).
tcf(c_2836,plain,
( r1(sK91,sK89(sK91))
| ~ sP40(sK91)
| ~ p103(sK90(sK91)) ),
inference(instantiation,[status(thm)],[c_2835]) ).
tcf(c_2846,plain,
! [X0: $i] :
( r1(X0,sK90(X0))
| r1(X0,sK89(X0))
| ~ sP40(X0) ),
inference(resolution,[status(thm)],[c_94,c_221]) ).
tcf(c_2847,plain,
( r1(sK91,sK90(sK91))
| r1(sK91,sK89(sK91))
| ~ sP40(sK91) ),
inference(instantiation,[status(thm)],[c_2846]) ).
tcf(c_6580,plain,
! [X0: $i] :
( ~ iPr_def_11
| ~ sP40(X0)
| ~ p203(sK89(X0))
| ~ r1(sK91,sK90(X0)) ),
inference(resolution,[status(thm)],[c_2813,c_5961]) ).
tcf(c_6581,plain,
( ~ iPr_def_11
| ~ sP40(sK91)
| ~ p203(sK89(sK91))
| ~ r1(sK91,sK90(sK91)) ),
inference(instantiation,[status(thm)],[c_6580]) ).
tcf(c_6854,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_6853,c_6851,c_6849,c_6847,c_6845,c_6843,c_6837,c_6835,c_6833,c_6827,c_6825,c_6823,c_6821,c_6819,c_6817,c_6815,c_6813,c_6811,c_6809,c_6799,c_6793,c_6787,c_6783,c_6779,c_6596,c_6583,c_6581,c_6546,c_6532,c_6518,c_6504,c_6493,c_6485,c_6468,c_6454,c_6440,c_6426,c_6418,c_6416,c_6414,c_6409,c_6412,c_6381,c_6367,c_6359,c_6351,c_6343,c_6327,c_6322,c_6316,c_6314,c_6309,c_6307,c_6305,c_6297,c_6289,c_6281,c_6273,c_6265,c_6257,c_6249,c_6241,c_6239,c_6234,c_6229,c_6227,c_6225,c_6214,c_6206,c_6198,c_6169,c_6167,c_6108,c_6091,c_6083,c_6077,c_6071,c_6065,c_6064,c_5960,c_5959,c_5958,c_5957,c_5956,c_5972,c_5969,c_5965,c_3046,c_3045,c_3028,c_3027,c_3010,c_3009,c_2984,c_2906,c_2905,c_2888,c_2887,c_2870,c_2869,c_2847,c_2836,c_2791,c_2780,c_2735,c_2724,c_2657,c_2623,c_2612,c_2567,c_2556,c_2511,c_2500,c_2455,c_2444,c_2399,c_2388,c_2343,c_2332,c_406,c_402,c_398,c_394,c_390,c_386,c_384,c_383,c_378,c_374,c_370,c_368,c_366,c_364,c_362,c_360,c_358,c_356,c_354,c_352,c_350,c_348,c_346,c_344,c_342,c_340,c_338,c_337,c_336,c_335,c_334,c_332,c_330,c_328,c_326,c_324,c_322,c_320,c_318,c_317,c_316,c_315,c_314,c_312,c_311,c_310,c_226,c_227,c_308,c_307,c_306,c_305,c_304,c_303,c_302,c_301,c_300,c_299,c_298,c_297,c_296,c_295,c_294,c_293,c_292,c_291,c_290,c_289,c_288,c_284,c_277,c_275,c_273,c_272,c_271,c_270,c_269,c_268,c_267,c_266,c_265,c_264,c_263,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_250,c_249,c_248,c_247,c_246,c_245,c_244,c_243,c_242,c_241,c_240,c_239,c_238,c_237,c_236,c_235,c_234,c_233,c_232]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL666+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Thu Sep 24 00:08:17 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/0.42 Running first-order theorem proving
% 0.16/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.43
% 0.16/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.43
% 0.16/0.43 % Detected problem language: tptp
% 0.16/0.44 % Proving...
% 4.03/1.74 % SZS status Started for theBenchmark.p
% 4.03/1.74 % SZS status Theorem for theBenchmark.p
% 4.03/1.74
% 4.03/1.74 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 4.03/1.74
% 4.03/1.74 % ------ iProver source info
% 4.03/1.74
% 4.03/1.74 % git: date: 2026-07-19 20:42:38 +0200
% 4.03/1.74 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 4.03/1.74 % git: non_committed_changes: false
% 4.03/1.74
% 4.03/1.74 % ------ Parsing...
% 4.03/1.74 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 4.03/1.74
% 4.03/1.74 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe:1:0s pe:2:0s pe:4:0s pe:8:0s pe:16:0s pe:32:0s pe_e %
% 4.03/1.74
% 4.03/1.74 % ------ Preprocessing... gs_s sp: 14 0s gs_e snvd_s sp: 0 0s snvd_e
% 4.03/1.74 % ------ Proving...
% 4.03/1.74 % ------ Problem Properties
% 4.03/1.74
% 4.03/1.74 %
% 4.03/1.74 % clauses 150
% 4.03/1.74 % conjectures 13
% 4.03/1.74 % EPR 50
% 4.03/1.74 % Horn 125
% 4.03/1.74 % unary 1
% 4.03/1.74 % binary 1
% 4.03/1.74 % lits 486
% 4.03/1.74 % lits eq 0
% 4.03/1.74 % fd_pure 0
% 4.03/1.74 % fd_pseudo 0
% 4.03/1.74 % fd_cond 0
% 4.03/1.74 % fd_pseudo_cond 0
% 4.03/1.74 % AC symbols 0
% 4.03/1.74
% 4.03/1.74 % ------ Input Options Time Limit: Unbounded
% 4.03/1.74
% 4.03/1.74
% 4.03/1.74 % ------
% 4.03/1.74 % Current options:
% 4.03/1.74 % ------
% 4.03/1.74
% 4.03/1.74
% 4.03/1.74 %
% 4.03/1.74
% 4.03/1.74 % ------ Proving...
% 4.03/1.74 %
% 4.03/1.74
% 4.03/1.74 % SZS status Theorem for theBenchmark.p
% 4.03/1.74
% 4.03/1.74 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 4.03/1.76
% 4.03/1.76
%------------------------------------------------------------------------------