%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL648+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n017.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 : Tue Sep 29 11:59:13 AM UTC 2026
% Result : Theorem 0.19s 0.50s
% Output : Refutation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
& p505(X1) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p405(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p405(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p205(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( p604(X1)
& p504(X1) )
| ( p604(X1)
& p404(X1) )
| ( p504(X1)
& p404(X1) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p204(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p603(X1)
& p503(X1) )
| ( p603(X1)
& p403(X1) )
| ( p503(X1)
& p403(X1) )
| ( p603(X1)
& p303(X1) )
| ( p503(X1)
& p303(X1) )
| ( p403(X1)
& p303(X1) )
| ( p603(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p503(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p403(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p303(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p603(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p503(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p403(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p303(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p203(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p602(X1)
& p502(X1) )
| ( p602(X1)
& p402(X1) )
| ( p502(X1)
& p402(X1) )
| ( p602(X1)
& p302(X1) )
| ( p502(X1)
& p302(X1) )
| ( p402(X1)
& p302(X1) )
| ( p602(X1)
& p202(X1) )
| ( p502(X1)
& p202(X1) )
| ( p402(X1)
& p202(X1) )
| ( p302(X1)
& p202(X1) )
| ( p602(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p502(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p402(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p302(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p202(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p601(X1)
& p501(X1) )
| ( p601(X1)
& p401(X1) )
| ( p501(X1)
& p401(X1) )
| ( p601(X1)
& p301(X1) )
| ( p501(X1)
& p301(X1) )
| ( p401(X1)
& p301(X1) )
| ( p601(X1)
& p201(X1) )
| ( p501(X1)
& p201(X1) )
| ( p401(X1)
& p201(X1) )
| ( p301(X1)
& p201(X1) )
| ( p601(X1)
& p101(X1) )
| ( p501(X1)
& p101(X1) )
| ( p401(X1)
& p101(X1) )
| ( p301(X1)
& p101(X1) )
| ( p201(X1)
& p101(X1) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
| p604(X1)
| p603(X1)
| p602(X1)
| p601(X1) )
& ( p505(X1)
| p504(X1)
| p503(X1)
| p502(X1)
| p501(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
| p404(X1)
| p403(X1)
| p402(X1)
| p401(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
| p303(X1)
| p302(X1)
| p301(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p205(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p204(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p203(X0) )
| p202(X1)
| p201(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p105(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p104(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p103(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p102(X0) )
| p101(X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
& p505(X1) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p405(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p405(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p305(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p205(X0) ) )
| ( p605(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( p505(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p205(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p105(X0) ) )
| ( p604(X1)
& p504(X1) )
| ( p604(X1)
& p404(X1) )
| ( p504(X1)
& p404(X1) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p304(X0) ) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p204(X0) ) )
| ( p604(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p504(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p404(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p204(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p104(X0) ) )
| ( p603(X1)
& p503(X1) )
| ( p603(X1)
& p403(X1) )
| ( p503(X1)
& p403(X1) )
| ( p603(X1)
& p303(X1) )
| ( p503(X1)
& p303(X1) )
| ( p403(X1)
& p303(X1) )
| ( p603(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p503(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p403(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p303(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p203(X0) ) )
| ( p603(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p503(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p403(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p303(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( ! [X0] :
( ~ r1(X1,X0)
| p203(X0) )
& ! [X0] :
( ~ r1(X1,X0)
| p103(X0) ) )
| ( p602(X1)
& p502(X1) )
| ( p602(X1)
& p402(X1) )
| ( p502(X1)
& p402(X1) )
| ( p602(X1)
& p302(X1) )
| ( p502(X1)
& p302(X1) )
| ( p402(X1)
& p302(X1) )
| ( p602(X1)
& p202(X1) )
| ( p502(X1)
& p202(X1) )
| ( p402(X1)
& p202(X1) )
| ( p302(X1)
& p202(X1) )
| ( p602(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p502(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p402(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p302(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p202(X1)
& ! [X0] :
( ~ r1(X1,X0)
| p102(X0) ) )
| ( p601(X1)
& p501(X1) )
| ( p601(X1)
& p401(X1) )
| ( p501(X1)
& p401(X1) )
| ( p601(X1)
& p301(X1) )
| ( p501(X1)
& p301(X1) )
| ( p401(X1)
& p301(X1) )
| ( p601(X1)
& p201(X1) )
| ( p501(X1)
& p201(X1) )
| ( p401(X1)
& p201(X1) )
| ( p301(X1)
& p201(X1) )
| ( p601(X1)
& p101(X1) )
| ( p501(X1)
& p101(X1) )
| ( p401(X1)
& p101(X1) )
| ( p301(X1)
& p101(X1) )
| ( p201(X1)
& p101(X1) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
| p604(X1)
| p603(X1)
| p602(X1)
| p601(X1) )
& ( p505(X1)
| p504(X1)
| p503(X1)
| p502(X1)
| p501(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p405(X0) )
| p404(X1)
| p403(X1)
| p402(X1)
| p401(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p305(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p304(X0) )
| p303(X1)
| p302(X1)
| p301(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p205(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p204(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p203(X0) )
| p202(X1)
| p201(X1) )
& ( ! [X0] :
( ~ r1(X1,X0)
| p105(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p104(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p103(X0) )
| ! [X0] :
( ~ r1(X1,X0)
| p102(X0) )
| p101(X1) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
& p505(X1) )
| ( p605(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p405(X2) ) )
| ( p505(X1)
& ! [X3] :
( ~ r1(X1,X3)
| p405(X3) ) )
| ( p605(X1)
& ! [X4] :
( ~ r1(X1,X4)
| p305(X4) ) )
| ( p505(X1)
& ! [X5] :
( ~ r1(X1,X5)
| p305(X5) ) )
| ( ! [X6] :
( ~ r1(X1,X6)
| p405(X6) )
& ! [X7] :
( ~ r1(X1,X7)
| p305(X7) ) )
| ( p605(X1)
& ! [X8] :
( ~ r1(X1,X8)
| p205(X8) ) )
| ( p505(X1)
& ! [X9] :
( ~ r1(X1,X9)
| p205(X9) ) )
| ( ! [X10] :
( ~ r1(X1,X10)
| p405(X10) )
& ! [X11] :
( ~ r1(X1,X11)
| p205(X11) ) )
| ( ! [X12] :
( ~ r1(X1,X12)
| p305(X12) )
& ! [X13] :
( ~ r1(X1,X13)
| p205(X13) ) )
| ( p605(X1)
& ! [X14] :
( ~ r1(X1,X14)
| p105(X14) ) )
| ( p505(X1)
& ! [X15] :
( ~ r1(X1,X15)
| p105(X15) ) )
| ( ! [X16] :
( ~ r1(X1,X16)
| p405(X16) )
& ! [X17] :
( ~ r1(X1,X17)
| p105(X17) ) )
| ( ! [X18] :
( ~ r1(X1,X18)
| p305(X18) )
& ! [X19] :
( ~ r1(X1,X19)
| p105(X19) ) )
| ( ! [X20] :
( ~ r1(X1,X20)
| p205(X20) )
& ! [X21] :
( ~ r1(X1,X21)
| p105(X21) ) )
| ( p604(X1)
& p504(X1) )
| ( p604(X1)
& p404(X1) )
| ( p504(X1)
& p404(X1) )
| ( p604(X1)
& ! [X22] :
( ~ r1(X1,X22)
| p304(X22) ) )
| ( p504(X1)
& ! [X23] :
( ~ r1(X1,X23)
| p304(X23) ) )
| ( p404(X1)
& ! [X24] :
( ~ r1(X1,X24)
| p304(X24) ) )
| ( p604(X1)
& ! [X25] :
( ~ r1(X1,X25)
| p204(X25) ) )
| ( p504(X1)
& ! [X26] :
( ~ r1(X1,X26)
| p204(X26) ) )
| ( p404(X1)
& ! [X27] :
( ~ r1(X1,X27)
| p204(X27) ) )
| ( ! [X28] :
( ~ r1(X1,X28)
| p304(X28) )
& ! [X29] :
( ~ r1(X1,X29)
| p204(X29) ) )
| ( p604(X1)
& ! [X30] :
( ~ r1(X1,X30)
| p104(X30) ) )
| ( p504(X1)
& ! [X31] :
( ~ r1(X1,X31)
| p104(X31) ) )
| ( p404(X1)
& ! [X32] :
( ~ r1(X1,X32)
| p104(X32) ) )
| ( ! [X33] :
( ~ r1(X1,X33)
| p304(X33) )
& ! [X34] :
( ~ r1(X1,X34)
| p104(X34) ) )
| ( ! [X35] :
( ~ r1(X1,X35)
| p204(X35) )
& ! [X36] :
( ~ r1(X1,X36)
| p104(X36) ) )
| ( p603(X1)
& p503(X1) )
| ( p603(X1)
& p403(X1) )
| ( p503(X1)
& p403(X1) )
| ( p603(X1)
& p303(X1) )
| ( p503(X1)
& p303(X1) )
| ( p403(X1)
& p303(X1) )
| ( p603(X1)
& ! [X37] :
( ~ r1(X1,X37)
| p203(X37) ) )
| ( p503(X1)
& ! [X38] :
( ~ r1(X1,X38)
| p203(X38) ) )
| ( p403(X1)
& ! [X39] :
( ~ r1(X1,X39)
| p203(X39) ) )
| ( p303(X1)
& ! [X40] :
( ~ r1(X1,X40)
| p203(X40) ) )
| ( p603(X1)
& ! [X41] :
( ~ r1(X1,X41)
| p103(X41) ) )
| ( p503(X1)
& ! [X42] :
( ~ r1(X1,X42)
| p103(X42) ) )
| ( p403(X1)
& ! [X43] :
( ~ r1(X1,X43)
| p103(X43) ) )
| ( p303(X1)
& ! [X44] :
( ~ r1(X1,X44)
| p103(X44) ) )
| ( ! [X45] :
( ~ r1(X1,X45)
| p203(X45) )
& ! [X46] :
( ~ r1(X1,X46)
| p103(X46) ) )
| ( p602(X1)
& p502(X1) )
| ( p602(X1)
& p402(X1) )
| ( p502(X1)
& p402(X1) )
| ( p602(X1)
& p302(X1) )
| ( p502(X1)
& p302(X1) )
| ( p402(X1)
& p302(X1) )
| ( p602(X1)
& p202(X1) )
| ( p502(X1)
& p202(X1) )
| ( p402(X1)
& p202(X1) )
| ( p302(X1)
& p202(X1) )
| ( p602(X1)
& ! [X47] :
( ~ r1(X1,X47)
| p102(X47) ) )
| ( p502(X1)
& ! [X48] :
( ~ r1(X1,X48)
| p102(X48) ) )
| ( p402(X1)
& ! [X49] :
( ~ r1(X1,X49)
| p102(X49) ) )
| ( p302(X1)
& ! [X50] :
( ~ r1(X1,X50)
| p102(X50) ) )
| ( p202(X1)
& ! [X51] :
( ~ r1(X1,X51)
| p102(X51) ) )
| ( p601(X1)
& p501(X1) )
| ( p601(X1)
& p401(X1) )
| ( p501(X1)
& p401(X1) )
| ( p601(X1)
& p301(X1) )
| ( p501(X1)
& p301(X1) )
| ( p401(X1)
& p301(X1) )
| ( p601(X1)
& p201(X1) )
| ( p501(X1)
& p201(X1) )
| ( p401(X1)
& p201(X1) )
| ( p301(X1)
& p201(X1) )
| ( p601(X1)
& p101(X1) )
| ( p501(X1)
& p101(X1) )
| ( p401(X1)
& p101(X1) )
| ( p301(X1)
& p101(X1) )
| ( p201(X1)
& p101(X1) ) ) )
| ! [X52] :
( ~ r1(X0,X52)
| ~ ( ( p605(X52)
| p604(X52)
| p603(X52)
| p602(X52)
| p601(X52) )
& ( p505(X52)
| p504(X52)
| p503(X52)
| p502(X52)
| p501(X52) )
& ( ! [X53] :
( ~ r1(X52,X53)
| p405(X53) )
| p404(X52)
| p403(X52)
| p402(X52)
| p401(X52) )
& ( ! [X54] :
( ~ r1(X52,X54)
| p305(X54) )
| ! [X55] :
( ~ r1(X52,X55)
| p304(X55) )
| p303(X52)
| p302(X52)
| p301(X52) )
& ( ! [X56] :
( ~ r1(X52,X56)
| p205(X56) )
| ! [X57] :
( ~ r1(X52,X57)
| p204(X57) )
| ! [X58] :
( ~ r1(X52,X58)
| p203(X58) )
| p202(X52)
| p201(X52) )
& ( ! [X59] :
( ~ r1(X52,X59)
| p105(X59) )
| ! [X60] :
( ~ r1(X52,X60)
| p104(X60) )
| ! [X61] :
( ~ r1(X52,X61)
| p103(X61) )
| ! [X62] :
( ~ r1(X52,X62)
| p102(X62) )
| p101(X52) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ( p605(X1)
& p505(X1) )
| ( p605(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p405(X2) ) )
| ( p505(X1)
& ! [X3] :
( ~ r1(X1,X3)
| p405(X3) ) )
| ( p605(X1)
& ! [X4] :
( ~ r1(X1,X4)
| p305(X4) ) )
| ( p505(X1)
& ! [X5] :
( ~ r1(X1,X5)
| p305(X5) ) )
| ( ! [X6] :
( ~ r1(X1,X6)
| p405(X6) )
& ! [X7] :
( ~ r1(X1,X7)
| p305(X7) ) )
| ( p605(X1)
& ! [X8] :
( ~ r1(X1,X8)
| p205(X8) ) )
| ( p505(X1)
& ! [X9] :
( ~ r1(X1,X9)
| p205(X9) ) )
| ( ! [X10] :
( ~ r1(X1,X10)
| p405(X10) )
& ! [X11] :
( ~ r1(X1,X11)
| p205(X11) ) )
| ( ! [X12] :
( ~ r1(X1,X12)
| p305(X12) )
& ! [X13] :
( ~ r1(X1,X13)
| p205(X13) ) )
| ( p605(X1)
& ! [X14] :
( ~ r1(X1,X14)
| p105(X14) ) )
| ( p505(X1)
& ! [X15] :
( ~ r1(X1,X15)
| p105(X15) ) )
| ( ! [X16] :
( ~ r1(X1,X16)
| p405(X16) )
& ! [X17] :
( ~ r1(X1,X17)
| p105(X17) ) )
| ( ! [X18] :
( ~ r1(X1,X18)
| p305(X18) )
& ! [X19] :
( ~ r1(X1,X19)
| p105(X19) ) )
| ( ! [X20] :
( ~ r1(X1,X20)
| p205(X20) )
& ! [X21] :
( ~ r1(X1,X21)
| p105(X21) ) )
| ( p604(X1)
& p504(X1) )
| ( p604(X1)
& p404(X1) )
| ( p504(X1)
& p404(X1) )
| ( p604(X1)
& ! [X22] :
( ~ r1(X1,X22)
| p304(X22) ) )
| ( p504(X1)
& ! [X23] :
( ~ r1(X1,X23)
| p304(X23) ) )
| ( p404(X1)
& ! [X24] :
( ~ r1(X1,X24)
| p304(X24) ) )
| ( p604(X1)
& ! [X25] :
( ~ r1(X1,X25)
| p204(X25) ) )
| ( p504(X1)
& ! [X26] :
( ~ r1(X1,X26)
| p204(X26) ) )
| ( p404(X1)
& ! [X27] :
( ~ r1(X1,X27)
| p204(X27) ) )
| ( ! [X28] :
( ~ r1(X1,X28)
| p304(X28) )
& ! [X29] :
( ~ r1(X1,X29)
| p204(X29) ) )
| ( p604(X1)
& ! [X30] :
( ~ r1(X1,X30)
| p104(X30) ) )
| ( p504(X1)
& ! [X31] :
( ~ r1(X1,X31)
| p104(X31) ) )
| ( p404(X1)
& ! [X32] :
( ~ r1(X1,X32)
| p104(X32) ) )
| ( ! [X33] :
( ~ r1(X1,X33)
| p304(X33) )
& ! [X34] :
( ~ r1(X1,X34)
| p104(X34) ) )
| ( ! [X35] :
( ~ r1(X1,X35)
| p204(X35) )
& ! [X36] :
( ~ r1(X1,X36)
| p104(X36) ) )
| ( p603(X1)
& p503(X1) )
| ( p603(X1)
& p403(X1) )
| ( p503(X1)
& p403(X1) )
| ( p603(X1)
& p303(X1) )
| ( p503(X1)
& p303(X1) )
| ( p403(X1)
& p303(X1) )
| ( p603(X1)
& ! [X37] :
( ~ r1(X1,X37)
| p203(X37) ) )
| ( p503(X1)
& ! [X38] :
( ~ r1(X1,X38)
| p203(X38) ) )
| ( p403(X1)
& ! [X39] :
( ~ r1(X1,X39)
| p203(X39) ) )
| ( p303(X1)
& ! [X40] :
( ~ r1(X1,X40)
| p203(X40) ) )
| ( p603(X1)
& ! [X41] :
( ~ r1(X1,X41)
| p103(X41) ) )
| ( p503(X1)
& ! [X42] :
( ~ r1(X1,X42)
| p103(X42) ) )
| ( p403(X1)
& ! [X43] :
( ~ r1(X1,X43)
| p103(X43) ) )
| ( p303(X1)
& ! [X44] :
( ~ r1(X1,X44)
| p103(X44) ) )
| ( ! [X45] :
( ~ r1(X1,X45)
| p203(X45) )
& ! [X46] :
( ~ r1(X1,X46)
| p103(X46) ) )
| ( p602(X1)
& p502(X1) )
| ( p602(X1)
& p402(X1) )
| ( p502(X1)
& p402(X1) )
| ( p602(X1)
& p302(X1) )
| ( p502(X1)
& p302(X1) )
| ( p402(X1)
& p302(X1) )
| ( p602(X1)
& p202(X1) )
| ( p502(X1)
& p202(X1) )
| ( p402(X1)
& p202(X1) )
| ( p302(X1)
& p202(X1) )
| ( p602(X1)
& ! [X47] :
( ~ r1(X1,X47)
| p102(X47) ) )
| ( p502(X1)
& ! [X48] :
( ~ r1(X1,X48)
| p102(X48) ) )
| ( p402(X1)
& ! [X49] :
( ~ r1(X1,X49)
| p102(X49) ) )
| ( p302(X1)
& ! [X50] :
( ~ r1(X1,X50)
| p102(X50) ) )
| ( p202(X1)
& ! [X51] :
( ~ r1(X1,X51)
| p102(X51) ) )
| ( p601(X1)
& p501(X1) )
| ( p601(X1)
& p401(X1) )
| ( p501(X1)
& p401(X1) )
| ( p601(X1)
& p301(X1) )
| ( p501(X1)
& p301(X1) )
| ( p401(X1)
& p301(X1) )
| ( p601(X1)
& p201(X1) )
| ( p501(X1)
& p201(X1) )
| ( p401(X1)
& p201(X1) )
| ( p301(X1)
& p201(X1) )
| ( p601(X1)
& p101(X1) )
| ( p501(X1)
& p101(X1) )
| ( p401(X1)
& p101(X1) )
| ( p301(X1)
& p101(X1) )
| ( p201(X1)
& p101(X1) ) ) )
| ! [X52] :
( ~ r1(X0,X52)
| ~ ( ( p605(X52)
| p604(X52)
| p603(X52)
| p602(X52)
| p601(X52) )
& ( p505(X52)
| p504(X52)
| p503(X52)
| p502(X52)
| p501(X52) )
& ( ! [X53] :
( ~ r1(X52,X53)
| p405(X53) )
| p404(X52)
| p403(X52)
| p402(X52)
| p401(X52) )
& ( ! [X54] :
( ~ r1(X52,X54)
| p305(X54) )
| ! [X55] :
( ~ r1(X52,X55)
| p304(X55) )
| p303(X52)
| p302(X52)
| p301(X52) )
& ( ! [X56] :
( ~ r1(X52,X56)
| p205(X56) )
| ! [X57] :
( ~ r1(X52,X57)
| p204(X57) )
| ! [X58] :
( ~ r1(X52,X58)
| p203(X58) )
| p202(X52)
| p201(X52) )
& ( ! [X59] :
( ~ r1(X52,X59)
| p105(X59) )
| ! [X60] :
( ~ r1(X52,X60)
| p104(X60) )
| ! [X61] :
( ~ r1(X52,X61)
| p103(X61) )
| ! [X62] :
( ~ r1(X52,X62)
| p102(X62) )
| p101(X52) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( ~ p605(X1)
| ~ p505(X1) )
& ( ~ p605(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p405(X2) ) )
& ( ~ p505(X1)
| ? [X3] :
( r1(X1,X3)
& ~ p405(X3) ) )
& ( ~ p605(X1)
| ? [X4] :
( r1(X1,X4)
& ~ p305(X4) ) )
& ( ~ p505(X1)
| ? [X5] :
( r1(X1,X5)
& ~ p305(X5) ) )
& ( ? [X6] :
( r1(X1,X6)
& ~ p405(X6) )
| ? [X7] :
( r1(X1,X7)
& ~ p305(X7) ) )
& ( ~ p605(X1)
| ? [X8] :
( r1(X1,X8)
& ~ p205(X8) ) )
& ( ~ p505(X1)
| ? [X9] :
( r1(X1,X9)
& ~ p205(X9) ) )
& ( ? [X10] :
( r1(X1,X10)
& ~ p405(X10) )
| ? [X11] :
( r1(X1,X11)
& ~ p205(X11) ) )
& ( ? [X12] :
( r1(X1,X12)
& ~ p305(X12) )
| ? [X13] :
( r1(X1,X13)
& ~ p205(X13) ) )
& ( ~ p605(X1)
| ? [X14] :
( r1(X1,X14)
& ~ p105(X14) ) )
& ( ~ p505(X1)
| ? [X15] :
( r1(X1,X15)
& ~ p105(X15) ) )
& ( ? [X16] :
( r1(X1,X16)
& ~ p405(X16) )
| ? [X17] :
( r1(X1,X17)
& ~ p105(X17) ) )
& ( ? [X18] :
( r1(X1,X18)
& ~ p305(X18) )
| ? [X19] :
( r1(X1,X19)
& ~ p105(X19) ) )
& ( ? [X20] :
( r1(X1,X20)
& ~ p205(X20) )
| ? [X21] :
( r1(X1,X21)
& ~ p105(X21) ) )
& ( ~ p604(X1)
| ~ p504(X1) )
& ( ~ p604(X1)
| ~ p404(X1) )
& ( ~ p504(X1)
| ~ p404(X1) )
& ( ~ p604(X1)
| ? [X22] :
( r1(X1,X22)
& ~ p304(X22) ) )
& ( ~ p504(X1)
| ? [X23] :
( r1(X1,X23)
& ~ p304(X23) ) )
& ( ~ p404(X1)
| ? [X24] :
( r1(X1,X24)
& ~ p304(X24) ) )
& ( ~ p604(X1)
| ? [X25] :
( r1(X1,X25)
& ~ p204(X25) ) )
& ( ~ p504(X1)
| ? [X26] :
( r1(X1,X26)
& ~ p204(X26) ) )
& ( ~ p404(X1)
| ? [X27] :
( r1(X1,X27)
& ~ p204(X27) ) )
& ( ? [X28] :
( r1(X1,X28)
& ~ p304(X28) )
| ? [X29] :
( r1(X1,X29)
& ~ p204(X29) ) )
& ( ~ p604(X1)
| ? [X30] :
( r1(X1,X30)
& ~ p104(X30) ) )
& ( ~ p504(X1)
| ? [X31] :
( r1(X1,X31)
& ~ p104(X31) ) )
& ( ~ p404(X1)
| ? [X32] :
( r1(X1,X32)
& ~ p104(X32) ) )
& ( ? [X33] :
( r1(X1,X33)
& ~ p304(X33) )
| ? [X34] :
( r1(X1,X34)
& ~ p104(X34) ) )
& ( ? [X35] :
( r1(X1,X35)
& ~ p204(X35) )
| ? [X36] :
( r1(X1,X36)
& ~ p104(X36) ) )
& ( ~ p603(X1)
| ~ p503(X1) )
& ( ~ p603(X1)
| ~ p403(X1) )
& ( ~ p503(X1)
| ~ p403(X1) )
& ( ~ p603(X1)
| ~ p303(X1) )
& ( ~ p503(X1)
| ~ p303(X1) )
& ( ~ p403(X1)
| ~ p303(X1) )
& ( ~ p603(X1)
| ? [X37] :
( r1(X1,X37)
& ~ p203(X37) ) )
& ( ~ p503(X1)
| ? [X38] :
( r1(X1,X38)
& ~ p203(X38) ) )
& ( ~ p403(X1)
| ? [X39] :
( r1(X1,X39)
& ~ p203(X39) ) )
& ( ~ p303(X1)
| ? [X40] :
( r1(X1,X40)
& ~ p203(X40) ) )
& ( ~ p603(X1)
| ? [X41] :
( r1(X1,X41)
& ~ p103(X41) ) )
& ( ~ p503(X1)
| ? [X42] :
( r1(X1,X42)
& ~ p103(X42) ) )
& ( ~ p403(X1)
| ? [X43] :
( r1(X1,X43)
& ~ p103(X43) ) )
& ( ~ p303(X1)
| ? [X44] :
( r1(X1,X44)
& ~ p103(X44) ) )
& ( ? [X45] :
( r1(X1,X45)
& ~ p203(X45) )
| ? [X46] :
( r1(X1,X46)
& ~ p103(X46) ) )
& ( ~ p602(X1)
| ~ p502(X1) )
& ( ~ p602(X1)
| ~ p402(X1) )
& ( ~ p502(X1)
| ~ p402(X1) )
& ( ~ p602(X1)
| ~ p302(X1) )
& ( ~ p502(X1)
| ~ p302(X1) )
& ( ~ p402(X1)
| ~ p302(X1) )
& ( ~ p602(X1)
| ~ p202(X1) )
& ( ~ p502(X1)
| ~ p202(X1) )
& ( ~ p402(X1)
| ~ p202(X1) )
& ( ~ p302(X1)
| ~ p202(X1) )
& ( ~ p602(X1)
| ? [X47] :
( r1(X1,X47)
& ~ p102(X47) ) )
& ( ~ p502(X1)
| ? [X48] :
( r1(X1,X48)
& ~ p102(X48) ) )
& ( ~ p402(X1)
| ? [X49] :
( r1(X1,X49)
& ~ p102(X49) ) )
& ( ~ p302(X1)
| ? [X50] :
( r1(X1,X50)
& ~ p102(X50) ) )
& ( ~ p202(X1)
| ? [X51] :
( r1(X1,X51)
& ~ p102(X51) ) )
& ( ~ p601(X1)
| ~ p501(X1) )
& ( ~ p601(X1)
| ~ p401(X1) )
& ( ~ p501(X1)
| ~ p401(X1) )
& ( ~ p601(X1)
| ~ p301(X1) )
& ( ~ p501(X1)
| ~ p301(X1) )
& ( ~ p401(X1)
| ~ p301(X1) )
& ( ~ p601(X1)
| ~ p201(X1) )
& ( ~ p501(X1)
| ~ p201(X1) )
& ( ~ p401(X1)
| ~ p201(X1) )
& ( ~ p301(X1)
| ~ p201(X1) )
& ( ~ p601(X1)
| ~ p101(X1) )
& ( ~ p501(X1)
| ~ p101(X1) )
& ( ~ p401(X1)
| ~ p101(X1) )
& ( ~ p301(X1)
| ~ p101(X1) )
& ( ~ p201(X1)
| ~ p101(X1) ) ) )
& ? [X52] :
( r1(X0,X52)
& ( p605(X52)
| p604(X52)
| p603(X52)
| p602(X52)
| p601(X52) )
& ( p505(X52)
| p504(X52)
| p503(X52)
| p502(X52)
| p501(X52) )
& ( ! [X53] :
( ~ r1(X52,X53)
| p405(X53) )
| p404(X52)
| p403(X52)
| p402(X52)
| p401(X52) )
& ( ! [X54] :
( ~ r1(X52,X54)
| p305(X54) )
| ! [X55] :
( ~ r1(X52,X55)
| p304(X55) )
| p303(X52)
| p302(X52)
| p301(X52) )
& ( ! [X56] :
( ~ r1(X52,X56)
| p205(X56) )
| ! [X57] :
( ~ r1(X52,X57)
| p204(X57) )
| ! [X58] :
( ~ r1(X52,X58)
| p203(X58) )
| p202(X52)
| p201(X52) )
& ( ! [X59] :
( ~ r1(X52,X59)
| p105(X59) )
| ! [X60] :
( ~ r1(X52,X60)
| p104(X60) )
| ! [X61] :
( ~ r1(X52,X61)
| p103(X61) )
| ! [X62] :
( ~ r1(X52,X62)
| p102(X62) )
| p101(X52) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( ~ p605(X1)
| ~ p505(X1) )
& ( ~ p605(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p405(X2) ) )
& ( ~ p505(X1)
| ? [X3] :
( r1(X1,X3)
& ~ p405(X3) ) )
& ( ~ p605(X1)
| ? [X4] :
( r1(X1,X4)
& ~ p305(X4) ) )
& ( ~ p505(X1)
| ? [X5] :
( r1(X1,X5)
& ~ p305(X5) ) )
& ( ? [X6] :
( r1(X1,X6)
& ~ p405(X6) )
| ? [X7] :
( r1(X1,X7)
& ~ p305(X7) ) )
& ( ~ p605(X1)
| ? [X8] :
( r1(X1,X8)
& ~ p205(X8) ) )
& ( ~ p505(X1)
| ? [X9] :
( r1(X1,X9)
& ~ p205(X9) ) )
& ( ? [X10] :
( r1(X1,X10)
& ~ p405(X10) )
| ? [X11] :
( r1(X1,X11)
& ~ p205(X11) ) )
& ( ? [X12] :
( r1(X1,X12)
& ~ p305(X12) )
| ? [X13] :
( r1(X1,X13)
& ~ p205(X13) ) )
& ( ~ p605(X1)
| ? [X14] :
( r1(X1,X14)
& ~ p105(X14) ) )
& ( ~ p505(X1)
| ? [X15] :
( r1(X1,X15)
& ~ p105(X15) ) )
& ( ? [X16] :
( r1(X1,X16)
& ~ p405(X16) )
| ? [X17] :
( r1(X1,X17)
& ~ p105(X17) ) )
& ( ? [X18] :
( r1(X1,X18)
& ~ p305(X18) )
| ? [X19] :
( r1(X1,X19)
& ~ p105(X19) ) )
& ( ? [X20] :
( r1(X1,X20)
& ~ p205(X20) )
| ? [X21] :
( r1(X1,X21)
& ~ p105(X21) ) )
& ( ~ p604(X1)
| ~ p504(X1) )
& ( ~ p604(X1)
| ~ p404(X1) )
& ( ~ p504(X1)
| ~ p404(X1) )
& ( ~ p604(X1)
| ? [X22] :
( r1(X1,X22)
& ~ p304(X22) ) )
& ( ~ p504(X1)
| ? [X23] :
( r1(X1,X23)
& ~ p304(X23) ) )
& ( ~ p404(X1)
| ? [X24] :
( r1(X1,X24)
& ~ p304(X24) ) )
& ( ~ p604(X1)
| ? [X25] :
( r1(X1,X25)
& ~ p204(X25) ) )
& ( ~ p504(X1)
| ? [X26] :
( r1(X1,X26)
& ~ p204(X26) ) )
& ( ~ p404(X1)
| ? [X27] :
( r1(X1,X27)
& ~ p204(X27) ) )
& ( ? [X28] :
( r1(X1,X28)
& ~ p304(X28) )
| ? [X29] :
( r1(X1,X29)
& ~ p204(X29) ) )
& ( ~ p604(X1)
| ? [X30] :
( r1(X1,X30)
& ~ p104(X30) ) )
& ( ~ p504(X1)
| ? [X31] :
( r1(X1,X31)
& ~ p104(X31) ) )
& ( ~ p404(X1)
| ? [X32] :
( r1(X1,X32)
& ~ p104(X32) ) )
& ( ? [X33] :
( r1(X1,X33)
& ~ p304(X33) )
| ? [X34] :
( r1(X1,X34)
& ~ p104(X34) ) )
& ( ? [X35] :
( r1(X1,X35)
& ~ p204(X35) )
| ? [X36] :
( r1(X1,X36)
& ~ p104(X36) ) )
& ( ~ p603(X1)
| ~ p503(X1) )
& ( ~ p603(X1)
| ~ p403(X1) )
& ( ~ p503(X1)
| ~ p403(X1) )
& ( ~ p603(X1)
| ~ p303(X1) )
& ( ~ p503(X1)
| ~ p303(X1) )
& ( ~ p403(X1)
| ~ p303(X1) )
& ( ~ p603(X1)
| ? [X37] :
( r1(X1,X37)
& ~ p203(X37) ) )
& ( ~ p503(X1)
| ? [X38] :
( r1(X1,X38)
& ~ p203(X38) ) )
& ( ~ p403(X1)
| ? [X39] :
( r1(X1,X39)
& ~ p203(X39) ) )
& ( ~ p303(X1)
| ? [X40] :
( r1(X1,X40)
& ~ p203(X40) ) )
& ( ~ p603(X1)
| ? [X41] :
( r1(X1,X41)
& ~ p103(X41) ) )
& ( ~ p503(X1)
| ? [X42] :
( r1(X1,X42)
& ~ p103(X42) ) )
& ( ~ p403(X1)
| ? [X43] :
( r1(X1,X43)
& ~ p103(X43) ) )
& ( ~ p303(X1)
| ? [X44] :
( r1(X1,X44)
& ~ p103(X44) ) )
& ( ? [X45] :
( r1(X1,X45)
& ~ p203(X45) )
| ? [X46] :
( r1(X1,X46)
& ~ p103(X46) ) )
& ( ~ p602(X1)
| ~ p502(X1) )
& ( ~ p602(X1)
| ~ p402(X1) )
& ( ~ p502(X1)
| ~ p402(X1) )
& ( ~ p602(X1)
| ~ p302(X1) )
& ( ~ p502(X1)
| ~ p302(X1) )
& ( ~ p402(X1)
| ~ p302(X1) )
& ( ~ p602(X1)
| ~ p202(X1) )
& ( ~ p502(X1)
| ~ p202(X1) )
& ( ~ p402(X1)
| ~ p202(X1) )
& ( ~ p302(X1)
| ~ p202(X1) )
& ( ~ p602(X1)
| ? [X47] :
( r1(X1,X47)
& ~ p102(X47) ) )
& ( ~ p502(X1)
| ? [X48] :
( r1(X1,X48)
& ~ p102(X48) ) )
& ( ~ p402(X1)
| ? [X49] :
( r1(X1,X49)
& ~ p102(X49) ) )
& ( ~ p302(X1)
| ? [X50] :
( r1(X1,X50)
& ~ p102(X50) ) )
& ( ~ p202(X1)
| ? [X51] :
( r1(X1,X51)
& ~ p102(X51) ) )
& ( ~ p601(X1)
| ~ p501(X1) )
& ( ~ p601(X1)
| ~ p401(X1) )
& ( ~ p501(X1)
| ~ p401(X1) )
& ( ~ p601(X1)
| ~ p301(X1) )
& ( ~ p501(X1)
| ~ p301(X1) )
& ( ~ p401(X1)
| ~ p301(X1) )
& ( ~ p601(X1)
| ~ p201(X1) )
& ( ~ p501(X1)
| ~ p201(X1) )
& ( ~ p401(X1)
| ~ p201(X1) )
& ( ~ p301(X1)
| ~ p201(X1) )
& ( ~ p601(X1)
| ~ p101(X1) )
& ( ~ p501(X1)
| ~ p101(X1) )
& ( ~ p401(X1)
| ~ p101(X1) )
& ( ~ p301(X1)
| ~ p101(X1) )
& ( ~ p201(X1)
| ~ p101(X1) ) ) )
& ? [X52] :
( r1(X0,X52)
& ( p605(X52)
| p604(X52)
| p603(X52)
| p602(X52)
| p601(X52) )
& ( p505(X52)
| p504(X52)
| p503(X52)
| p502(X52)
| p501(X52) )
& ( ! [X53] :
( ~ r1(X52,X53)
| p405(X53) )
| p404(X52)
| p403(X52)
| p402(X52)
| p401(X52) )
& ( ! [X54] :
( ~ r1(X52,X54)
| p305(X54) )
| ! [X55] :
( ~ r1(X52,X55)
| p304(X55) )
| p303(X52)
| p302(X52)
| p301(X52) )
& ( ! [X56] :
( ~ r1(X52,X56)
| p205(X56) )
| ! [X57] :
( ~ r1(X52,X57)
| p204(X57) )
| ! [X58] :
( ~ r1(X52,X58)
| p203(X58) )
| p202(X52)
| p201(X52) )
& ( ! [X59] :
( ~ r1(X52,X59)
| p105(X59) )
| ! [X60] :
( ~ r1(X52,X60)
| p104(X60) )
| ! [X61] :
( ~ r1(X52,X61)
| p103(X61) )
| ! [X62] :
( ~ r1(X52,X62)
| p102(X62) )
| p101(X52) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X1] :
( ? [X45] :
( r1(X1,X45)
& ~ p203(X45) )
| ? [X46] :
( r1(X1,X46)
& ~ p103(X46) )
| ~ sP0(X1) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X1] :
( ? [X35] :
( r1(X1,X35)
& ~ p204(X35) )
| ? [X36] :
( r1(X1,X36)
& ~ p104(X36) )
| ~ sP1(X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X1] :
( ? [X33] :
( r1(X1,X33)
& ~ p304(X33) )
| ? [X34] :
( r1(X1,X34)
& ~ p104(X34) )
| ~ sP2(X1) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X1] :
( ? [X28] :
( r1(X1,X28)
& ~ p304(X28) )
| ? [X29] :
( r1(X1,X29)
& ~ p204(X29) )
| ~ sP3(X1) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X1] :
( ? [X20] :
( r1(X1,X20)
& ~ p205(X20) )
| ? [X21] :
( r1(X1,X21)
& ~ p105(X21) )
| ~ sP4(X1) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X1] :
( ? [X18] :
( r1(X1,X18)
& ~ p305(X18) )
| ? [X19] :
( r1(X1,X19)
& ~ p105(X19) )
| ~ sP5(X1) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X1] :
( ? [X16] :
( r1(X1,X16)
& ~ p405(X16) )
| ? [X17] :
( r1(X1,X17)
& ~ p105(X17) )
| ~ sP6(X1) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X1] :
( ? [X12] :
( r1(X1,X12)
& ~ p305(X12) )
| ? [X13] :
( r1(X1,X13)
& ~ p205(X13) )
| ~ sP7(X1) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X1] :
( ? [X10] :
( r1(X1,X10)
& ~ p405(X10) )
| ? [X11] :
( r1(X1,X11)
& ~ p205(X11) )
| ~ sP8(X1) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X1] :
( ? [X6] :
( r1(X1,X6)
& ~ p405(X6) )
| ? [X7] :
( r1(X1,X7)
& ~ p305(X7) )
| ~ sP9(X1) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X1] :
( ~ p202(X1)
| ? [X51] :
( r1(X1,X51)
& ~ p102(X51) )
| ~ sP10(X1) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X1] :
( ~ p302(X1)
| ? [X50] :
( r1(X1,X50)
& ~ p102(X50) )
| ~ sP11(X1) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X1] :
( ~ p402(X1)
| ? [X49] :
( r1(X1,X49)
& ~ p102(X49) )
| ~ sP12(X1) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X1] :
( ~ p502(X1)
| ? [X48] :
( r1(X1,X48)
& ~ p102(X48) )
| ~ sP13(X1) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X1] :
( ~ p602(X1)
| ? [X47] :
( r1(X1,X47)
& ~ p102(X47) )
| ~ sP14(X1) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X1] :
( ~ p303(X1)
| ? [X44] :
( r1(X1,X44)
& ~ p103(X44) )
| ~ sP15(X1) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X1] :
( ~ p403(X1)
| ? [X43] :
( r1(X1,X43)
& ~ p103(X43) )
| ~ sP16(X1) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X1] :
( ~ p503(X1)
| ? [X42] :
( r1(X1,X42)
& ~ p103(X42) )
| ~ sP17(X1) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X1] :
( ~ p603(X1)
| ? [X41] :
( r1(X1,X41)
& ~ p103(X41) )
| ~ sP18(X1) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X1] :
( ~ p303(X1)
| ? [X40] :
( r1(X1,X40)
& ~ p203(X40) )
| ~ sP19(X1) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X1] :
( ~ p403(X1)
| ? [X39] :
( r1(X1,X39)
& ~ p203(X39) )
| ~ sP20(X1) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X1] :
( ~ p503(X1)
| ? [X38] :
( r1(X1,X38)
& ~ p203(X38) )
| ~ sP21(X1) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X1] :
( ~ p603(X1)
| ? [X37] :
( r1(X1,X37)
& ~ p203(X37) )
| ~ sP22(X1) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X1] :
( ~ p404(X1)
| ? [X32] :
( r1(X1,X32)
& ~ p104(X32) )
| ~ sP23(X1) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X1] :
( ~ p504(X1)
| ? [X31] :
( r1(X1,X31)
& ~ p104(X31) )
| ~ sP24(X1) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X1] :
( ~ p604(X1)
| ? [X30] :
( r1(X1,X30)
& ~ p104(X30) )
| ~ sP25(X1) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X1] :
( ~ p404(X1)
| ? [X27] :
( r1(X1,X27)
& ~ p204(X27) )
| ~ sP26(X1) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X1] :
( ~ p504(X1)
| ? [X26] :
( r1(X1,X26)
& ~ p204(X26) )
| ~ sP27(X1) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X1] :
( ~ p604(X1)
| ? [X25] :
( r1(X1,X25)
& ~ p204(X25) )
| ~ sP28(X1) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X1] :
( ~ p404(X1)
| ? [X24] :
( r1(X1,X24)
& ~ p304(X24) )
| ~ sP29(X1) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X1] :
( ~ p504(X1)
| ? [X23] :
( r1(X1,X23)
& ~ p304(X23) )
| ~ sP30(X1) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X1] :
( ~ p604(X1)
| ? [X22] :
( r1(X1,X22)
& ~ p304(X22) )
| ~ sP31(X1) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X1] :
( ~ p505(X1)
| ? [X15] :
( r1(X1,X15)
& ~ p105(X15) )
| ~ sP32(X1) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X1] :
( ~ p605(X1)
| ? [X14] :
( r1(X1,X14)
& ~ p105(X14) )
| ~ sP33(X1) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X1] :
( ~ p505(X1)
| ? [X9] :
( r1(X1,X9)
& ~ p205(X9) )
| ~ sP34(X1) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X1] :
( ~ p605(X1)
| ? [X8] :
( r1(X1,X8)
& ~ p205(X8) )
| ~ sP35(X1) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f43,definition,
! [X1] :
( ~ p505(X1)
| ? [X5] :
( r1(X1,X5)
& ~ p305(X5) )
| ~ sP36(X1) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f44,definition,
! [X1] :
( ~ p605(X1)
| ? [X4] :
( r1(X1,X4)
& ~ p305(X4) )
| ~ sP37(X1) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f45,definition,
! [X1] :
( ~ p505(X1)
| ? [X3] :
( r1(X1,X3)
& ~ p405(X3) )
| ~ sP38(X1) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f46,definition,
! [X1] :
( ~ p605(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p405(X2) )
| ~ sP39(X1) ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f47,definition,
! [X1] :
( ( ( ~ p605(X1)
| ~ p505(X1) )
& sP39(X1)
& sP38(X1)
& sP37(X1)
& sP36(X1)
& sP9(X1)
& sP35(X1)
& sP34(X1)
& sP8(X1)
& sP7(X1)
& sP33(X1)
& sP32(X1)
& sP6(X1)
& sP5(X1)
& sP4(X1)
& ( ~ p604(X1)
| ~ p504(X1) )
& ( ~ p604(X1)
| ~ p404(X1) )
& ( ~ p504(X1)
| ~ p404(X1) )
& sP31(X1)
& sP30(X1)
& sP29(X1)
& sP28(X1)
& sP27(X1)
& sP26(X1)
& sP3(X1)
& sP25(X1)
& sP24(X1)
& sP23(X1)
& sP2(X1)
& sP1(X1)
& ( ~ p603(X1)
| ~ p503(X1) )
& ( ~ p603(X1)
| ~ p403(X1) )
& ( ~ p503(X1)
| ~ p403(X1) )
& ( ~ p603(X1)
| ~ p303(X1) )
& ( ~ p503(X1)
| ~ p303(X1) )
& ( ~ p403(X1)
| ~ p303(X1) )
& sP22(X1)
& sP21(X1)
& sP20(X1)
& sP19(X1)
& sP18(X1)
& sP17(X1)
& sP16(X1)
& sP15(X1)
& sP0(X1)
& ( ~ p602(X1)
| ~ p502(X1) )
& ( ~ p602(X1)
| ~ p402(X1) )
& ( ~ p502(X1)
| ~ p402(X1) )
& ( ~ p602(X1)
| ~ p302(X1) )
& ( ~ p502(X1)
| ~ p302(X1) )
& ( ~ p402(X1)
| ~ p302(X1) )
& ( ~ p602(X1)
| ~ p202(X1) )
& ( ~ p502(X1)
| ~ p202(X1) )
& ( ~ p402(X1)
| ~ p202(X1) )
& ( ~ p302(X1)
| ~ p202(X1) )
& sP14(X1)
& sP13(X1)
& sP12(X1)
& sP11(X1)
& sP10(X1)
& ( ~ p601(X1)
| ~ p501(X1) )
& ( ~ p601(X1)
| ~ p401(X1) )
& ( ~ p501(X1)
| ~ p401(X1) )
& ( ~ p601(X1)
| ~ p301(X1) )
& ( ~ p501(X1)
| ~ p301(X1) )
& ( ~ p401(X1)
| ~ p301(X1) )
& ( ~ p601(X1)
| ~ p201(X1) )
& ( ~ p501(X1)
| ~ p201(X1) )
& ( ~ p401(X1)
| ~ p201(X1) )
& ( ~ p301(X1)
| ~ p201(X1) )
& ( ~ p601(X1)
| ~ p101(X1) )
& ( ~ p501(X1)
| ~ p101(X1) )
& ( ~ p401(X1)
| ~ p101(X1) )
& ( ~ p301(X1)
| ~ p101(X1) )
& ( ~ p201(X1)
| ~ p101(X1) ) )
| ~ sP40(X1) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f48,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| sP40(X1) )
& ? [X52] :
( r1(X0,X52)
& ( p605(X52)
| p604(X52)
| p603(X52)
| p602(X52)
| p601(X52) )
& ( p505(X52)
| p504(X52)
| p503(X52)
| p502(X52)
| p501(X52) )
& ( ! [X53] :
( ~ r1(X52,X53)
| p405(X53) )
| p404(X52)
| p403(X52)
| p402(X52)
| p401(X52) )
& ( ! [X54] :
( ~ r1(X52,X54)
| p305(X54) )
| ! [X55] :
( ~ r1(X52,X55)
| p304(X55) )
| p303(X52)
| p302(X52)
| p301(X52) )
& ( ! [X56] :
( ~ r1(X52,X56)
| p205(X56) )
| ! [X57] :
( ~ r1(X52,X57)
| p204(X57) )
| ! [X58] :
( ~ r1(X52,X58)
| p203(X58) )
| p202(X52)
| p201(X52) )
& ( ! [X59] :
( ~ r1(X52,X59)
| p105(X59) )
| ! [X60] :
( ~ r1(X52,X60)
| p104(X60) )
| ! [X61] :
( ~ r1(X52,X61)
| p103(X61) )
| ! [X62] :
( ~ r1(X52,X62)
| p102(X62) )
| p101(X52) ) ) ),
inference(definition_folding,[],[f6,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,f7]) ).
fof(f49,plain,
! [X1] :
( ( ( ~ p605(X1)
| ~ p505(X1) )
& sP39(X1)
& sP38(X1)
& sP37(X1)
& sP36(X1)
& sP9(X1)
& sP35(X1)
& sP34(X1)
& sP8(X1)
& sP7(X1)
& sP33(X1)
& sP32(X1)
& sP6(X1)
& sP5(X1)
& sP4(X1)
& ( ~ p604(X1)
| ~ p504(X1) )
& ( ~ p604(X1)
| ~ p404(X1) )
& ( ~ p504(X1)
| ~ p404(X1) )
& sP31(X1)
& sP30(X1)
& sP29(X1)
& sP28(X1)
& sP27(X1)
& sP26(X1)
& sP3(X1)
& sP25(X1)
& sP24(X1)
& sP23(X1)
& sP2(X1)
& sP1(X1)
& ( ~ p603(X1)
| ~ p503(X1) )
& ( ~ p603(X1)
| ~ p403(X1) )
& ( ~ p503(X1)
| ~ p403(X1) )
& ( ~ p603(X1)
| ~ p303(X1) )
& ( ~ p503(X1)
| ~ p303(X1) )
& ( ~ p403(X1)
| ~ p303(X1) )
& sP22(X1)
& sP21(X1)
& sP20(X1)
& sP19(X1)
& sP18(X1)
& sP17(X1)
& sP16(X1)
& sP15(X1)
& sP0(X1)
& ( ~ p602(X1)
| ~ p502(X1) )
& ( ~ p602(X1)
| ~ p402(X1) )
& ( ~ p502(X1)
| ~ p402(X1) )
& ( ~ p602(X1)
| ~ p302(X1) )
& ( ~ p502(X1)
| ~ p302(X1) )
& ( ~ p402(X1)
| ~ p302(X1) )
& ( ~ p602(X1)
| ~ p202(X1) )
& ( ~ p502(X1)
| ~ p202(X1) )
& ( ~ p402(X1)
| ~ p202(X1) )
& ( ~ p302(X1)
| ~ p202(X1) )
& sP14(X1)
& sP13(X1)
& sP12(X1)
& sP11(X1)
& sP10(X1)
& ( ~ p601(X1)
| ~ p501(X1) )
& ( ~ p601(X1)
| ~ p401(X1) )
& ( ~ p501(X1)
| ~ p401(X1) )
& ( ~ p601(X1)
| ~ p301(X1) )
& ( ~ p501(X1)
| ~ p301(X1) )
& ( ~ p401(X1)
| ~ p301(X1) )
& ( ~ p601(X1)
| ~ p201(X1) )
& ( ~ p501(X1)
| ~ p201(X1) )
& ( ~ p401(X1)
| ~ p201(X1) )
& ( ~ p301(X1)
| ~ p201(X1) )
& ( ~ p601(X1)
| ~ p101(X1) )
& ( ~ p501(X1)
| ~ p101(X1) )
& ( ~ p401(X1)
| ~ p101(X1) )
& ( ~ p301(X1)
| ~ p101(X1) )
& ( ~ p201(X1)
| ~ p101(X1) ) )
| ~ sP40(X1) ),
inference(nnf_transformation,[],[f47]) ).
fof(f50,plain,
! [X0] :
( ( ( ~ p605(X0)
| ~ p505(X0) )
& sP39(X0)
& sP38(X0)
& sP37(X0)
& sP36(X0)
& sP9(X0)
& sP35(X0)
& sP34(X0)
& sP8(X0)
& sP7(X0)
& sP33(X0)
& sP32(X0)
& sP6(X0)
& sP5(X0)
& sP4(X0)
& ( ~ p604(X0)
| ~ p504(X0) )
& ( ~ p604(X0)
| ~ p404(X0) )
& ( ~ p504(X0)
| ~ p404(X0) )
& sP31(X0)
& sP30(X0)
& sP29(X0)
& sP28(X0)
& sP27(X0)
& sP26(X0)
& sP3(X0)
& sP25(X0)
& sP24(X0)
& sP23(X0)
& sP2(X0)
& sP1(X0)
& ( ~ p603(X0)
| ~ p503(X0) )
& ( ~ p603(X0)
| ~ p403(X0) )
& ( ~ p503(X0)
| ~ p403(X0) )
& ( ~ p603(X0)
| ~ p303(X0) )
& ( ~ p503(X0)
| ~ p303(X0) )
& ( ~ p403(X0)
| ~ p303(X0) )
& sP22(X0)
& sP21(X0)
& sP20(X0)
& sP19(X0)
& sP18(X0)
& sP17(X0)
& sP16(X0)
& sP15(X0)
& sP0(X0)
& ( ~ p602(X0)
| ~ p502(X0) )
& ( ~ p602(X0)
| ~ p402(X0) )
& ( ~ p502(X0)
| ~ p402(X0) )
& ( ~ p602(X0)
| ~ p302(X0) )
& ( ~ p502(X0)
| ~ p302(X0) )
& ( ~ p402(X0)
| ~ p302(X0) )
& ( ~ p602(X0)
| ~ p202(X0) )
& ( ~ p502(X0)
| ~ p202(X0) )
& ( ~ p402(X0)
| ~ p202(X0) )
& ( ~ p302(X0)
| ~ p202(X0) )
& sP14(X0)
& sP13(X0)
& sP12(X0)
& sP11(X0)
& sP10(X0)
& ( ~ p601(X0)
| ~ p501(X0) )
& ( ~ p601(X0)
| ~ p401(X0) )
& ( ~ p501(X0)
| ~ p401(X0) )
& ( ~ p601(X0)
| ~ p301(X0) )
& ( ~ p501(X0)
| ~ p301(X0) )
& ( ~ p401(X0)
| ~ p301(X0) )
& ( ~ p601(X0)
| ~ p201(X0) )
& ( ~ p501(X0)
| ~ p201(X0) )
& ( ~ p401(X0)
| ~ p201(X0) )
& ( ~ p301(X0)
| ~ p201(X0) )
& ( ~ p601(X0)
| ~ p101(X0) )
& ( ~ p501(X0)
| ~ p101(X0) )
& ( ~ p401(X0)
| ~ p101(X0) )
& ( ~ p301(X0)
| ~ p101(X0) )
& ( ~ p201(X0)
| ~ p101(X0) ) )
| ~ sP40(X0) ),
inference(rectify,[],[f49]) ).
fof(f51,plain,
! [X1] :
( ~ p605(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p405(X2) )
| ~ sP39(X1) ),
inference(nnf_transformation,[],[f46]) ).
fof(f52,plain,
! [X0] :
( ~ p605(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p405(X1) )
| ~ sP39(X0) ),
inference(rectify,[],[f51]) ).
fof(f53,plain,
! [X0] :
( ~ p605(X0)
| ( r1(X0,sK41(X0))
& ~ p405(sK41(X0)) )
| ~ sP39(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK41]),skolemize(X1,sK41(X0))],[f52]) ).
fof(f54,plain,
! [X1] :
( ~ p505(X1)
| ? [X3] :
( r1(X1,X3)
& ~ p405(X3) )
| ~ sP38(X1) ),
inference(nnf_transformation,[],[f45]) ).
fof(f55,plain,
! [X0] :
( ~ p505(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p405(X1) )
| ~ sP38(X0) ),
inference(rectify,[],[f54]) ).
fof(f56,plain,
! [X0] :
( ~ p505(X0)
| ( r1(X0,sK42(X0))
& ~ p405(sK42(X0)) )
| ~ sP38(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK42]),skolemize(X1,sK42(X0))],[f55]) ).
fof(f57,plain,
! [X1] :
( ~ p605(X1)
| ? [X4] :
( r1(X1,X4)
& ~ p305(X4) )
| ~ sP37(X1) ),
inference(nnf_transformation,[],[f44]) ).
fof(f58,plain,
! [X0] :
( ~ p605(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p305(X1) )
| ~ sP37(X0) ),
inference(rectify,[],[f57]) ).
fof(f59,plain,
! [X0] :
( ~ p605(X0)
| ( r1(X0,sK43(X0))
& ~ p305(sK43(X0)) )
| ~ sP37(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK43]),skolemize(X1,sK43(X0))],[f58]) ).
fof(f60,plain,
! [X1] :
( ~ p505(X1)
| ? [X5] :
( r1(X1,X5)
& ~ p305(X5) )
| ~ sP36(X1) ),
inference(nnf_transformation,[],[f43]) ).
fof(f61,plain,
! [X0] :
( ~ p505(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p305(X1) )
| ~ sP36(X0) ),
inference(rectify,[],[f60]) ).
fof(f62,plain,
! [X0] :
( ~ p505(X0)
| ( r1(X0,sK44(X0))
& ~ p305(sK44(X0)) )
| ~ sP36(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK44]),skolemize(X1,sK44(X0))],[f61]) ).
fof(f63,plain,
! [X1] :
( ~ p605(X1)
| ? [X8] :
( r1(X1,X8)
& ~ p205(X8) )
| ~ sP35(X1) ),
inference(nnf_transformation,[],[f42]) ).
fof(f64,plain,
! [X0] :
( ~ p605(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p205(X1) )
| ~ sP35(X0) ),
inference(rectify,[],[f63]) ).
fof(f65,plain,
! [X0] :
( ~ p605(X0)
| ( r1(X0,sK45(X0))
& ~ p205(sK45(X0)) )
| ~ sP35(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK45]),skolemize(X1,sK45(X0))],[f64]) ).
fof(f66,plain,
! [X1] :
( ~ p505(X1)
| ? [X9] :
( r1(X1,X9)
& ~ p205(X9) )
| ~ sP34(X1) ),
inference(nnf_transformation,[],[f41]) ).
fof(f67,plain,
! [X0] :
( ~ p505(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p205(X1) )
| ~ sP34(X0) ),
inference(rectify,[],[f66]) ).
fof(f68,plain,
! [X0] :
( ~ p505(X0)
| ( r1(X0,sK46(X0))
& ~ p205(sK46(X0)) )
| ~ sP34(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK46]),skolemize(X1,sK46(X0))],[f67]) ).
fof(f69,plain,
! [X1] :
( ~ p605(X1)
| ? [X14] :
( r1(X1,X14)
& ~ p105(X14) )
| ~ sP33(X1) ),
inference(nnf_transformation,[],[f40]) ).
fof(f70,plain,
! [X0] :
( ~ p605(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p105(X1) )
| ~ sP33(X0) ),
inference(rectify,[],[f69]) ).
fof(f71,plain,
! [X0] :
( ~ p605(X0)
| ( r1(X0,sK47(X0))
& ~ p105(sK47(X0)) )
| ~ sP33(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK47]),skolemize(X1,sK47(X0))],[f70]) ).
fof(f72,plain,
! [X1] :
( ~ p505(X1)
| ? [X15] :
( r1(X1,X15)
& ~ p105(X15) )
| ~ sP32(X1) ),
inference(nnf_transformation,[],[f39]) ).
fof(f73,plain,
! [X0] :
( ~ p505(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p105(X1) )
| ~ sP32(X0) ),
inference(rectify,[],[f72]) ).
fof(f74,plain,
! [X0] :
( ~ p505(X0)
| ( r1(X0,sK48(X0))
& ~ p105(sK48(X0)) )
| ~ sP32(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK48]),skolemize(X1,sK48(X0))],[f73]) ).
fof(f75,plain,
! [X1] :
( ~ p604(X1)
| ? [X22] :
( r1(X1,X22)
& ~ p304(X22) )
| ~ sP31(X1) ),
inference(nnf_transformation,[],[f38]) ).
fof(f76,plain,
! [X0] :
( ~ p604(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p304(X1) )
| ~ sP31(X0) ),
inference(rectify,[],[f75]) ).
fof(f77,plain,
! [X0] :
( ~ p604(X0)
| ( r1(X0,sK49(X0))
& ~ p304(sK49(X0)) )
| ~ sP31(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49]),skolemize(X1,sK49(X0))],[f76]) ).
fof(f78,plain,
! [X1] :
( ~ p504(X1)
| ? [X23] :
( r1(X1,X23)
& ~ p304(X23) )
| ~ sP30(X1) ),
inference(nnf_transformation,[],[f37]) ).
fof(f79,plain,
! [X0] :
( ~ p504(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p304(X1) )
| ~ sP30(X0) ),
inference(rectify,[],[f78]) ).
fof(f80,plain,
! [X0] :
( ~ p504(X0)
| ( r1(X0,sK50(X0))
& ~ p304(sK50(X0)) )
| ~ sP30(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK50]),skolemize(X1,sK50(X0))],[f79]) ).
fof(f81,plain,
! [X1] :
( ~ p404(X1)
| ? [X24] :
( r1(X1,X24)
& ~ p304(X24) )
| ~ sP29(X1) ),
inference(nnf_transformation,[],[f36]) ).
fof(f82,plain,
! [X0] :
( ~ p404(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p304(X1) )
| ~ sP29(X0) ),
inference(rectify,[],[f81]) ).
fof(f83,plain,
! [X0] :
( ~ p404(X0)
| ( r1(X0,sK51(X0))
& ~ p304(sK51(X0)) )
| ~ sP29(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK51]),skolemize(X1,sK51(X0))],[f82]) ).
fof(f84,plain,
! [X1] :
( ~ p604(X1)
| ? [X25] :
( r1(X1,X25)
& ~ p204(X25) )
| ~ sP28(X1) ),
inference(nnf_transformation,[],[f35]) ).
fof(f85,plain,
! [X0] :
( ~ p604(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p204(X1) )
| ~ sP28(X0) ),
inference(rectify,[],[f84]) ).
fof(f86,plain,
! [X0] :
( ~ p604(X0)
| ( r1(X0,sK52(X0))
& ~ p204(sK52(X0)) )
| ~ sP28(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK52]),skolemize(X1,sK52(X0))],[f85]) ).
fof(f87,plain,
! [X1] :
( ~ p504(X1)
| ? [X26] :
( r1(X1,X26)
& ~ p204(X26) )
| ~ sP27(X1) ),
inference(nnf_transformation,[],[f34]) ).
fof(f88,plain,
! [X0] :
( ~ p504(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p204(X1) )
| ~ sP27(X0) ),
inference(rectify,[],[f87]) ).
fof(f89,plain,
! [X0] :
( ~ p504(X0)
| ( r1(X0,sK53(X0))
& ~ p204(sK53(X0)) )
| ~ sP27(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK53]),skolemize(X1,sK53(X0))],[f88]) ).
fof(f90,plain,
! [X1] :
( ~ p404(X1)
| ? [X27] :
( r1(X1,X27)
& ~ p204(X27) )
| ~ sP26(X1) ),
inference(nnf_transformation,[],[f33]) ).
fof(f91,plain,
! [X0] :
( ~ p404(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p204(X1) )
| ~ sP26(X0) ),
inference(rectify,[],[f90]) ).
fof(f92,plain,
! [X0] :
( ~ p404(X0)
| ( r1(X0,sK54(X0))
& ~ p204(sK54(X0)) )
| ~ sP26(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK54]),skolemize(X1,sK54(X0))],[f91]) ).
fof(f93,plain,
! [X1] :
( ~ p604(X1)
| ? [X30] :
( r1(X1,X30)
& ~ p104(X30) )
| ~ sP25(X1) ),
inference(nnf_transformation,[],[f32]) ).
fof(f94,plain,
! [X0] :
( ~ p604(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p104(X1) )
| ~ sP25(X0) ),
inference(rectify,[],[f93]) ).
fof(f95,plain,
! [X0] :
( ~ p604(X0)
| ( r1(X0,sK55(X0))
& ~ p104(sK55(X0)) )
| ~ sP25(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55]),skolemize(X1,sK55(X0))],[f94]) ).
fof(f96,plain,
! [X1] :
( ~ p504(X1)
| ? [X31] :
( r1(X1,X31)
& ~ p104(X31) )
| ~ sP24(X1) ),
inference(nnf_transformation,[],[f31]) ).
fof(f97,plain,
! [X0] :
( ~ p504(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p104(X1) )
| ~ sP24(X0) ),
inference(rectify,[],[f96]) ).
fof(f98,plain,
! [X0] :
( ~ p504(X0)
| ( r1(X0,sK56(X0))
& ~ p104(sK56(X0)) )
| ~ sP24(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56]),skolemize(X1,sK56(X0))],[f97]) ).
fof(f99,plain,
! [X1] :
( ~ p404(X1)
| ? [X32] :
( r1(X1,X32)
& ~ p104(X32) )
| ~ sP23(X1) ),
inference(nnf_transformation,[],[f30]) ).
fof(f100,plain,
! [X0] :
( ~ p404(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p104(X1) )
| ~ sP23(X0) ),
inference(rectify,[],[f99]) ).
fof(f101,plain,
! [X0] :
( ~ p404(X0)
| ( r1(X0,sK57(X0))
& ~ p104(sK57(X0)) )
| ~ sP23(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK57]),skolemize(X1,sK57(X0))],[f100]) ).
fof(f102,plain,
! [X1] :
( ~ p603(X1)
| ? [X37] :
( r1(X1,X37)
& ~ p203(X37) )
| ~ sP22(X1) ),
inference(nnf_transformation,[],[f29]) ).
fof(f103,plain,
! [X0] :
( ~ p603(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p203(X1) )
| ~ sP22(X0) ),
inference(rectify,[],[f102]) ).
fof(f104,plain,
! [X0] :
( ~ p603(X0)
| ( r1(X0,sK58(X0))
& ~ p203(sK58(X0)) )
| ~ sP22(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK58]),skolemize(X1,sK58(X0))],[f103]) ).
fof(f105,plain,
! [X1] :
( ~ p503(X1)
| ? [X38] :
( r1(X1,X38)
& ~ p203(X38) )
| ~ sP21(X1) ),
inference(nnf_transformation,[],[f28]) ).
fof(f106,plain,
! [X0] :
( ~ p503(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p203(X1) )
| ~ sP21(X0) ),
inference(rectify,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ~ p503(X0)
| ( r1(X0,sK59(X0))
& ~ p203(sK59(X0)) )
| ~ sP21(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK59]),skolemize(X1,sK59(X0))],[f106]) ).
fof(f108,plain,
! [X1] :
( ~ p403(X1)
| ? [X39] :
( r1(X1,X39)
& ~ p203(X39) )
| ~ sP20(X1) ),
inference(nnf_transformation,[],[f27]) ).
fof(f109,plain,
! [X0] :
( ~ p403(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p203(X1) )
| ~ sP20(X0) ),
inference(rectify,[],[f108]) ).
fof(f110,plain,
! [X0] :
( ~ p403(X0)
| ( r1(X0,sK60(X0))
& ~ p203(sK60(X0)) )
| ~ sP20(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK60]),skolemize(X1,sK60(X0))],[f109]) ).
fof(f111,plain,
! [X1] :
( ~ p303(X1)
| ? [X40] :
( r1(X1,X40)
& ~ p203(X40) )
| ~ sP19(X1) ),
inference(nnf_transformation,[],[f26]) ).
fof(f112,plain,
! [X0] :
( ~ p303(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p203(X1) )
| ~ sP19(X0) ),
inference(rectify,[],[f111]) ).
fof(f113,plain,
! [X0] :
( ~ p303(X0)
| ( r1(X0,sK61(X0))
& ~ p203(sK61(X0)) )
| ~ sP19(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK61]),skolemize(X1,sK61(X0))],[f112]) ).
fof(f114,plain,
! [X1] :
( ~ p603(X1)
| ? [X41] :
( r1(X1,X41)
& ~ p103(X41) )
| ~ sP18(X1) ),
inference(nnf_transformation,[],[f25]) ).
fof(f115,plain,
! [X0] :
( ~ p603(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p103(X1) )
| ~ sP18(X0) ),
inference(rectify,[],[f114]) ).
fof(f116,plain,
! [X0] :
( ~ p603(X0)
| ( r1(X0,sK62(X0))
& ~ p103(sK62(X0)) )
| ~ sP18(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK62]),skolemize(X1,sK62(X0))],[f115]) ).
fof(f117,plain,
! [X1] :
( ~ p503(X1)
| ? [X42] :
( r1(X1,X42)
& ~ p103(X42) )
| ~ sP17(X1) ),
inference(nnf_transformation,[],[f24]) ).
fof(f118,plain,
! [X0] :
( ~ p503(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p103(X1) )
| ~ sP17(X0) ),
inference(rectify,[],[f117]) ).
fof(f119,plain,
! [X0] :
( ~ p503(X0)
| ( r1(X0,sK63(X0))
& ~ p103(sK63(X0)) )
| ~ sP17(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK63]),skolemize(X1,sK63(X0))],[f118]) ).
fof(f120,plain,
! [X1] :
( ~ p403(X1)
| ? [X43] :
( r1(X1,X43)
& ~ p103(X43) )
| ~ sP16(X1) ),
inference(nnf_transformation,[],[f23]) ).
fof(f121,plain,
! [X0] :
( ~ p403(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p103(X1) )
| ~ sP16(X0) ),
inference(rectify,[],[f120]) ).
fof(f122,plain,
! [X0] :
( ~ p403(X0)
| ( r1(X0,sK64(X0))
& ~ p103(sK64(X0)) )
| ~ sP16(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64]),skolemize(X1,sK64(X0))],[f121]) ).
fof(f123,plain,
! [X1] :
( ~ p303(X1)
| ? [X44] :
( r1(X1,X44)
& ~ p103(X44) )
| ~ sP15(X1) ),
inference(nnf_transformation,[],[f22]) ).
fof(f124,plain,
! [X0] :
( ~ p303(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p103(X1) )
| ~ sP15(X0) ),
inference(rectify,[],[f123]) ).
fof(f125,plain,
! [X0] :
( ~ p303(X0)
| ( r1(X0,sK65(X0))
& ~ p103(sK65(X0)) )
| ~ sP15(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK65]),skolemize(X1,sK65(X0))],[f124]) ).
fof(f126,plain,
! [X1] :
( ~ p602(X1)
| ? [X47] :
( r1(X1,X47)
& ~ p102(X47) )
| ~ sP14(X1) ),
inference(nnf_transformation,[],[f21]) ).
fof(f127,plain,
! [X0] :
( ~ p602(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p102(X1) )
| ~ sP14(X0) ),
inference(rectify,[],[f126]) ).
fof(f128,plain,
! [X0] :
( ~ p602(X0)
| ( r1(X0,sK66(X0))
& ~ p102(sK66(X0)) )
| ~ sP14(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK66]),skolemize(X1,sK66(X0))],[f127]) ).
fof(f129,plain,
! [X1] :
( ~ p502(X1)
| ? [X48] :
( r1(X1,X48)
& ~ p102(X48) )
| ~ sP13(X1) ),
inference(nnf_transformation,[],[f20]) ).
fof(f130,plain,
! [X0] :
( ~ p502(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p102(X1) )
| ~ sP13(X0) ),
inference(rectify,[],[f129]) ).
fof(f131,plain,
! [X0] :
( ~ p502(X0)
| ( r1(X0,sK67(X0))
& ~ p102(sK67(X0)) )
| ~ sP13(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67]),skolemize(X1,sK67(X0))],[f130]) ).
fof(f132,plain,
! [X1] :
( ~ p402(X1)
| ? [X49] :
( r1(X1,X49)
& ~ p102(X49) )
| ~ sP12(X1) ),
inference(nnf_transformation,[],[f19]) ).
fof(f133,plain,
! [X0] :
( ~ p402(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p102(X1) )
| ~ sP12(X0) ),
inference(rectify,[],[f132]) ).
fof(f134,plain,
! [X0] :
( ~ p402(X0)
| ( r1(X0,sK68(X0))
& ~ p102(sK68(X0)) )
| ~ sP12(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK68]),skolemize(X1,sK68(X0))],[f133]) ).
fof(f135,plain,
! [X1] :
( ~ p302(X1)
| ? [X50] :
( r1(X1,X50)
& ~ p102(X50) )
| ~ sP11(X1) ),
inference(nnf_transformation,[],[f18]) ).
fof(f136,plain,
! [X0] :
( ~ p302(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p102(X1) )
| ~ sP11(X0) ),
inference(rectify,[],[f135]) ).
fof(f137,plain,
! [X0] :
( ~ p302(X0)
| ( r1(X0,sK69(X0))
& ~ p102(sK69(X0)) )
| ~ sP11(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK69]),skolemize(X1,sK69(X0))],[f136]) ).
fof(f138,plain,
! [X1] :
( ~ p202(X1)
| ? [X51] :
( r1(X1,X51)
& ~ p102(X51) )
| ~ sP10(X1) ),
inference(nnf_transformation,[],[f17]) ).
fof(f139,plain,
! [X0] :
( ~ p202(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p102(X1) )
| ~ sP10(X0) ),
inference(rectify,[],[f138]) ).
fof(f140,plain,
! [X0] :
( ~ p202(X0)
| ( r1(X0,sK70(X0))
& ~ p102(sK70(X0)) )
| ~ sP10(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK70]),skolemize(X1,sK70(X0))],[f139]) ).
fof(f141,plain,
! [X1] :
( ? [X6] :
( r1(X1,X6)
& ~ p405(X6) )
| ? [X7] :
( r1(X1,X7)
& ~ p305(X7) )
| ~ sP9(X1) ),
inference(nnf_transformation,[],[f16]) ).
fof(f142,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p405(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p305(X2) )
| ~ sP9(X0) ),
inference(rectify,[],[f141]) ).
fof(f143,plain,
! [X0] :
( ( r1(X0,sK71(X0))
& ~ p405(sK71(X0)) )
| ( r1(X0,sK72(X0))
& ~ p305(sK72(X0)) )
| ~ sP9(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72]),skolemize(X1,sK71(X0)),skolemize(X2,sK72(X0))],[f142]) ).
fof(f144,plain,
! [X1] :
( ? [X10] :
( r1(X1,X10)
& ~ p405(X10) )
| ? [X11] :
( r1(X1,X11)
& ~ p205(X11) )
| ~ sP8(X1) ),
inference(nnf_transformation,[],[f15]) ).
fof(f145,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p405(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p205(X2) )
| ~ sP8(X0) ),
inference(rectify,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ( r1(X0,sK73(X0))
& ~ p405(sK73(X0)) )
| ( r1(X0,sK74(X0))
& ~ p205(sK74(X0)) )
| ~ sP8(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK73,sK74]),skolemize(X1,sK73(X0)),skolemize(X2,sK74(X0))],[f145]) ).
fof(f147,plain,
! [X1] :
( ? [X12] :
( r1(X1,X12)
& ~ p305(X12) )
| ? [X13] :
( r1(X1,X13)
& ~ p205(X13) )
| ~ sP7(X1) ),
inference(nnf_transformation,[],[f14]) ).
fof(f148,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p305(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p205(X2) )
| ~ sP7(X0) ),
inference(rectify,[],[f147]) ).
fof(f149,plain,
! [X0] :
( ( r1(X0,sK75(X0))
& ~ p305(sK75(X0)) )
| ( r1(X0,sK76(X0))
& ~ p205(sK76(X0)) )
| ~ sP7(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK75,sK76]),skolemize(X1,sK75(X0)),skolemize(X2,sK76(X0))],[f148]) ).
fof(f150,plain,
! [X1] :
( ? [X16] :
( r1(X1,X16)
& ~ p405(X16) )
| ? [X17] :
( r1(X1,X17)
& ~ p105(X17) )
| ~ sP6(X1) ),
inference(nnf_transformation,[],[f13]) ).
fof(f151,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p405(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p105(X2) )
| ~ sP6(X0) ),
inference(rectify,[],[f150]) ).
fof(f152,plain,
! [X0] :
( ( r1(X0,sK77(X0))
& ~ p405(sK77(X0)) )
| ( r1(X0,sK78(X0))
& ~ p105(sK78(X0)) )
| ~ sP6(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK77,sK78]),skolemize(X1,sK77(X0)),skolemize(X2,sK78(X0))],[f151]) ).
fof(f153,plain,
! [X1] :
( ? [X18] :
( r1(X1,X18)
& ~ p305(X18) )
| ? [X19] :
( r1(X1,X19)
& ~ p105(X19) )
| ~ sP5(X1) ),
inference(nnf_transformation,[],[f12]) ).
fof(f154,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p305(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p105(X2) )
| ~ sP5(X0) ),
inference(rectify,[],[f153]) ).
fof(f155,plain,
! [X0] :
( ( r1(X0,sK79(X0))
& ~ p305(sK79(X0)) )
| ( r1(X0,sK80(X0))
& ~ p105(sK80(X0)) )
| ~ sP5(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK79,sK80]),skolemize(X1,sK79(X0)),skolemize(X2,sK80(X0))],[f154]) ).
fof(f156,plain,
! [X1] :
( ? [X20] :
( r1(X1,X20)
& ~ p205(X20) )
| ? [X21] :
( r1(X1,X21)
& ~ p105(X21) )
| ~ sP4(X1) ),
inference(nnf_transformation,[],[f11]) ).
fof(f157,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p205(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p105(X2) )
| ~ sP4(X0) ),
inference(rectify,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ( r1(X0,sK81(X0))
& ~ p205(sK81(X0)) )
| ( r1(X0,sK82(X0))
& ~ p105(sK82(X0)) )
| ~ sP4(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK81,sK82]),skolemize(X1,sK81(X0)),skolemize(X2,sK82(X0))],[f157]) ).
fof(f159,plain,
! [X1] :
( ? [X28] :
( r1(X1,X28)
& ~ p304(X28) )
| ? [X29] :
( r1(X1,X29)
& ~ p204(X29) )
| ~ sP3(X1) ),
inference(nnf_transformation,[],[f10]) ).
fof(f160,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p304(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p204(X2) )
| ~ sP3(X0) ),
inference(rectify,[],[f159]) ).
fof(f161,plain,
! [X0] :
( ( r1(X0,sK83(X0))
& ~ p304(sK83(X0)) )
| ( r1(X0,sK84(X0))
& ~ p204(sK84(X0)) )
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK83,sK84]),skolemize(X1,sK83(X0)),skolemize(X2,sK84(X0))],[f160]) ).
fof(f162,plain,
! [X1] :
( ? [X33] :
( r1(X1,X33)
& ~ p304(X33) )
| ? [X34] :
( r1(X1,X34)
& ~ p104(X34) )
| ~ sP2(X1) ),
inference(nnf_transformation,[],[f9]) ).
fof(f163,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p304(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p104(X2) )
| ~ sP2(X0) ),
inference(rectify,[],[f162]) ).
fof(f164,plain,
! [X0] :
( ( r1(X0,sK85(X0))
& ~ p304(sK85(X0)) )
| ( r1(X0,sK86(X0))
& ~ p104(sK86(X0)) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK85,sK86]),skolemize(X1,sK85(X0)),skolemize(X2,sK86(X0))],[f163]) ).
fof(f165,plain,
! [X1] :
( ? [X35] :
( r1(X1,X35)
& ~ p204(X35) )
| ? [X36] :
( r1(X1,X36)
& ~ p104(X36) )
| ~ sP1(X1) ),
inference(nnf_transformation,[],[f8]) ).
fof(f166,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p204(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p104(X2) )
| ~ sP1(X0) ),
inference(rectify,[],[f165]) ).
fof(f167,plain,
! [X0] :
( ( r1(X0,sK87(X0))
& ~ p204(sK87(X0)) )
| ( r1(X0,sK88(X0))
& ~ p104(sK88(X0)) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK87,sK88]),skolemize(X1,sK87(X0)),skolemize(X2,sK88(X0))],[f166]) ).
fof(f168,plain,
! [X1] :
( ? [X45] :
( r1(X1,X45)
& ~ p203(X45) )
| ? [X46] :
( r1(X1,X46)
& ~ p103(X46) )
| ~ sP0(X1) ),
inference(nnf_transformation,[],[f7]) ).
fof(f169,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p203(X1) )
| ? [X2] :
( r1(X0,X2)
& ~ p103(X2) )
| ~ sP0(X0) ),
inference(rectify,[],[f168]) ).
fof(f170,plain,
! [X0] :
( ( r1(X0,sK89(X0))
& ~ p203(sK89(X0)) )
| ( r1(X0,sK90(X0))
& ~ p103(sK90(X0)) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK89,sK90]),skolemize(X1,sK89(X0)),skolemize(X2,sK90(X0))],[f169]) ).
fof(f171,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| sP40(X1) )
& ? [X2] :
( r1(X0,X2)
& ( p605(X2)
| p604(X2)
| p603(X2)
| p602(X2)
| p601(X2) )
& ( p505(X2)
| p504(X2)
| p503(X2)
| p502(X2)
| p501(X2) )
& ( ! [X3] :
( ~ r1(X2,X3)
| p405(X3) )
| p404(X2)
| p403(X2)
| p402(X2)
| p401(X2) )
& ( ! [X4] :
( ~ r1(X2,X4)
| p305(X4) )
| ! [X5] :
( ~ r1(X2,X5)
| p304(X5) )
| p303(X2)
| p302(X2)
| p301(X2) )
& ( ! [X6] :
( ~ r1(X2,X6)
| p205(X6) )
| ! [X7] :
( ~ r1(X2,X7)
| p204(X7) )
| ! [X8] :
( ~ r1(X2,X8)
| p203(X8) )
| p202(X2)
| p201(X2) )
& ( ! [X9] :
( ~ r1(X2,X9)
| p105(X9) )
| ! [X10] :
( ~ r1(X2,X10)
| p104(X10) )
| ! [X11] :
( ~ r1(X2,X11)
| p103(X11) )
| ! [X12] :
( ~ r1(X2,X12)
| p102(X12) )
| p101(X2) ) ) ),
inference(rectify,[],[f48]) ).
fof(f172,plain,
( ! [X1] :
( ~ r1(sK91,X1)
| sP40(X1) )
& r1(sK91,sK92)
& ( p605(sK92)
| p604(sK92)
| p603(sK92)
| p602(sK92)
| p601(sK92) )
& ( p505(sK92)
| p504(sK92)
| p503(sK92)
| p502(sK92)
| p501(sK92) )
& ( ! [X3] :
( ~ r1(sK92,X3)
| p405(X3) )
| p404(sK92)
| p403(sK92)
| p402(sK92)
| p401(sK92) )
& ( ! [X4] :
( ~ r1(sK92,X4)
| p305(X4) )
| ! [X5] :
( ~ r1(sK92,X5)
| p304(X5) )
| p303(sK92)
| p302(sK92)
| p301(sK92) )
& ( ! [X6] :
( ~ r1(sK92,X6)
| p205(X6) )
| ! [X7] :
( ~ r1(sK92,X7)
| p204(X7) )
| ! [X8] :
( ~ r1(sK92,X8)
| p203(X8) )
| p202(sK92)
| p201(sK92) )
& ( ! [X9] :
( ~ r1(sK92,X9)
| p105(X9) )
| ! [X10] :
( ~ r1(sK92,X10)
| p104(X10) )
| ! [X11] :
( ~ r1(sK92,X11)
| p103(X11) )
| ! [X12] :
( ~ r1(sK92,X12)
| p102(X12) )
| p101(sK92) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK91,sK92]),skolemize(X0,sK91),skolemize(X2,sK92)],[f171]) ).
fof(f173,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p201(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f174,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p301(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f175,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f176,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f177,plain,
! [X0] :
( ~ sP40(X0)
| ~ p101(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f178,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p301(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f179,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f180,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f181,plain,
! [X0] :
( ~ sP40(X0)
| ~ p201(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f182,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p401(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f183,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f184,plain,
! [X0] :
( ~ sP40(X0)
| ~ p301(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f185,plain,
! [X0] :
( ~ sP40(X0)
| ~ p401(X0)
| ~ p501(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f186,plain,
! [X0] :
( ~ sP40(X0)
| ~ p401(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f187,plain,
! [X0] :
( ~ sP40(X0)
| ~ p501(X0)
| ~ p601(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f188,plain,
! [X0] :
( ~ sP40(X0)
| sP10(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f189,plain,
! [X0] :
( ~ sP40(X0)
| sP11(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f190,plain,
! [X0] :
( ~ sP40(X0)
| sP12(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f191,plain,
! [X0] :
( ~ sP40(X0)
| sP13(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f192,plain,
! [X0] :
( ~ sP40(X0)
| sP14(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f193,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p302(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f194,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p402(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f195,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f196,plain,
! [X0] :
( ~ sP40(X0)
| ~ p202(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f197,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p402(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f198,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f199,plain,
! [X0] :
( ~ sP40(X0)
| ~ p302(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f200,plain,
! [X0] :
( ~ sP40(X0)
| ~ p402(X0)
| ~ p502(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f201,plain,
! [X0] :
( ~ sP40(X0)
| ~ p402(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f202,plain,
! [X0] :
( ~ sP40(X0)
| ~ p502(X0)
| ~ p602(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f203,plain,
! [X0] :
( ~ sP40(X0)
| sP0(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f204,plain,
! [X0] :
( ~ sP40(X0)
| sP15(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f205,plain,
! [X0] :
( ~ sP40(X0)
| sP16(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f206,plain,
! [X0] :
( ~ sP40(X0)
| sP17(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f207,plain,
! [X0] :
( ~ sP40(X0)
| sP18(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f208,plain,
! [X0] :
( ~ sP40(X0)
| sP19(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f209,plain,
! [X0] :
( ~ sP40(X0)
| sP20(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f210,plain,
! [X0] :
( ~ sP40(X0)
| sP21(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f211,plain,
! [X0] :
( ~ sP40(X0)
| sP22(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f212,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p403(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f213,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f214,plain,
! [X0] :
( ~ sP40(X0)
| ~ p303(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f215,plain,
! [X0] :
( ~ sP40(X0)
| ~ p403(X0)
| ~ p503(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f216,plain,
! [X0] :
( ~ sP40(X0)
| ~ p403(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f217,plain,
! [X0] :
( ~ sP40(X0)
| ~ p503(X0)
| ~ p603(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f218,plain,
! [X0] :
( ~ sP40(X0)
| sP1(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f219,plain,
! [X0] :
( ~ sP40(X0)
| sP2(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f220,plain,
! [X0] :
( ~ sP40(X0)
| sP23(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f221,plain,
! [X0] :
( ~ sP40(X0)
| sP24(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f222,plain,
! [X0] :
( ~ sP40(X0)
| sP25(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f223,plain,
! [X0] :
( ~ sP40(X0)
| sP3(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f224,plain,
! [X0] :
( ~ sP40(X0)
| sP26(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f225,plain,
! [X0] :
( ~ sP40(X0)
| sP27(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f226,plain,
! [X0] :
( ~ sP40(X0)
| sP28(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f227,plain,
! [X0] :
( ~ sP40(X0)
| sP29(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f228,plain,
! [X0] :
( ~ sP40(X0)
| sP30(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f229,plain,
! [X0] :
( ~ sP40(X0)
| sP31(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f230,plain,
! [X0] :
( ~ sP40(X0)
| ~ p404(X0)
| ~ p504(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f231,plain,
! [X0] :
( ~ sP40(X0)
| ~ p404(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f232,plain,
! [X0] :
( ~ sP40(X0)
| ~ p504(X0)
| ~ p604(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f233,plain,
! [X0] :
( ~ sP40(X0)
| sP4(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f234,plain,
! [X0] :
( ~ sP40(X0)
| sP5(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f235,plain,
! [X0] :
( ~ sP40(X0)
| sP6(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f236,plain,
! [X0] :
( ~ sP40(X0)
| sP32(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f237,plain,
! [X0] :
( ~ sP40(X0)
| sP33(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f238,plain,
! [X0] :
( ~ sP40(X0)
| sP7(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f239,plain,
! [X0] :
( ~ sP40(X0)
| sP8(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f240,plain,
! [X0] :
( ~ sP40(X0)
| sP34(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f241,plain,
! [X0] :
( ~ sP40(X0)
| sP35(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f242,plain,
! [X0] :
( ~ sP40(X0)
| sP9(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f243,plain,
! [X0] :
( ~ sP40(X0)
| sP36(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f244,plain,
! [X0] :
( ~ sP40(X0)
| sP37(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f245,plain,
! [X0] :
( ~ sP40(X0)
| sP38(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f246,plain,
! [X0] :
( ~ sP40(X0)
| sP39(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f247,plain,
! [X0] :
( ~ sP40(X0)
| ~ p505(X0)
| ~ p605(X0) ),
inference(cnf_transformation,[],[f50]) ).
fof(f248,plain,
! [X0] :
( ~ p405(sK41(X0))
| ~ p605(X0)
| ~ sP39(X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f249,plain,
! [X0] :
( r1(X0,sK41(X0))
| ~ p605(X0)
| ~ sP39(X0) ),
inference(cnf_transformation,[],[f53]) ).
fof(f250,plain,
! [X0] :
( ~ p405(sK42(X0))
| ~ p505(X0)
| ~ sP38(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f251,plain,
! [X0] :
( r1(X0,sK42(X0))
| ~ p505(X0)
| ~ sP38(X0) ),
inference(cnf_transformation,[],[f56]) ).
fof(f252,plain,
! [X0] :
( ~ p305(sK43(X0))
| ~ p605(X0)
| ~ sP37(X0) ),
inference(cnf_transformation,[],[f59]) ).
fof(f253,plain,
! [X0] :
( r1(X0,sK43(X0))
| ~ p605(X0)
| ~ sP37(X0) ),
inference(cnf_transformation,[],[f59]) ).
fof(f254,plain,
! [X0] :
( ~ p305(sK44(X0))
| ~ p505(X0)
| ~ sP36(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f255,plain,
! [X0] :
( r1(X0,sK44(X0))
| ~ p505(X0)
| ~ sP36(X0) ),
inference(cnf_transformation,[],[f62]) ).
fof(f256,plain,
! [X0] :
( ~ p205(sK45(X0))
| ~ p605(X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f257,plain,
! [X0] :
( r1(X0,sK45(X0))
| ~ p605(X0)
| ~ sP35(X0) ),
inference(cnf_transformation,[],[f65]) ).
fof(f258,plain,
! [X0] :
( ~ p205(sK46(X0))
| ~ p505(X0)
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f68]) ).
fof(f259,plain,
! [X0] :
( r1(X0,sK46(X0))
| ~ p505(X0)
| ~ sP34(X0) ),
inference(cnf_transformation,[],[f68]) ).
fof(f260,plain,
! [X0] :
( ~ p105(sK47(X0))
| ~ p605(X0)
| ~ sP33(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f261,plain,
! [X0] :
( r1(X0,sK47(X0))
| ~ p605(X0)
| ~ sP33(X0) ),
inference(cnf_transformation,[],[f71]) ).
fof(f262,plain,
! [X0] :
( ~ p105(sK48(X0))
| ~ p505(X0)
| ~ sP32(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f263,plain,
! [X0] :
( r1(X0,sK48(X0))
| ~ p505(X0)
| ~ sP32(X0) ),
inference(cnf_transformation,[],[f74]) ).
fof(f264,plain,
! [X0] :
( ~ p304(sK49(X0))
| ~ p604(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f265,plain,
! [X0] :
( r1(X0,sK49(X0))
| ~ p604(X0)
| ~ sP31(X0) ),
inference(cnf_transformation,[],[f77]) ).
fof(f266,plain,
! [X0] :
( ~ p304(sK50(X0))
| ~ p504(X0)
| ~ sP30(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f267,plain,
! [X0] :
( r1(X0,sK50(X0))
| ~ p504(X0)
| ~ sP30(X0) ),
inference(cnf_transformation,[],[f80]) ).
fof(f268,plain,
! [X0] :
( ~ p304(sK51(X0))
| ~ p404(X0)
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f269,plain,
! [X0] :
( r1(X0,sK51(X0))
| ~ p404(X0)
| ~ sP29(X0) ),
inference(cnf_transformation,[],[f83]) ).
fof(f270,plain,
! [X0] :
( ~ p204(sK52(X0))
| ~ p604(X0)
| ~ sP28(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f271,plain,
! [X0] :
( r1(X0,sK52(X0))
| ~ p604(X0)
| ~ sP28(X0) ),
inference(cnf_transformation,[],[f86]) ).
fof(f272,plain,
! [X0] :
( ~ p204(sK53(X0))
| ~ p504(X0)
| ~ sP27(X0) ),
inference(cnf_transformation,[],[f89]) ).
fof(f273,plain,
! [X0] :
( r1(X0,sK53(X0))
| ~ p504(X0)
| ~ sP27(X0) ),
inference(cnf_transformation,[],[f89]) ).
fof(f274,plain,
! [X0] :
( ~ p204(sK54(X0))
| ~ p404(X0)
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f92]) ).
fof(f275,plain,
! [X0] :
( r1(X0,sK54(X0))
| ~ p404(X0)
| ~ sP26(X0) ),
inference(cnf_transformation,[],[f92]) ).
fof(f276,plain,
! [X0] :
( ~ p104(sK55(X0))
| ~ p604(X0)
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f277,plain,
! [X0] :
( r1(X0,sK55(X0))
| ~ p604(X0)
| ~ sP25(X0) ),
inference(cnf_transformation,[],[f95]) ).
fof(f278,plain,
! [X0] :
( ~ p104(sK56(X0))
| ~ p504(X0)
| ~ sP24(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f279,plain,
! [X0] :
( r1(X0,sK56(X0))
| ~ p504(X0)
| ~ sP24(X0) ),
inference(cnf_transformation,[],[f98]) ).
fof(f280,plain,
! [X0] :
( ~ p104(sK57(X0))
| ~ p404(X0)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f281,plain,
! [X0] :
( r1(X0,sK57(X0))
| ~ p404(X0)
| ~ sP23(X0) ),
inference(cnf_transformation,[],[f101]) ).
fof(f282,plain,
! [X0] :
( ~ p203(sK58(X0))
| ~ p603(X0)
| ~ sP22(X0) ),
inference(cnf_transformation,[],[f104]) ).
fof(f283,plain,
! [X0] :
( r1(X0,sK58(X0))
| ~ p603(X0)
| ~ sP22(X0) ),
inference(cnf_transformation,[],[f104]) ).
fof(f284,plain,
! [X0] :
( ~ p203(sK59(X0))
| ~ p503(X0)
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f285,plain,
! [X0] :
( r1(X0,sK59(X0))
| ~ p503(X0)
| ~ sP21(X0) ),
inference(cnf_transformation,[],[f107]) ).
fof(f286,plain,
! [X0] :
( ~ p203(sK60(X0))
| ~ p403(X0)
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f287,plain,
! [X0] :
( r1(X0,sK60(X0))
| ~ p403(X0)
| ~ sP20(X0) ),
inference(cnf_transformation,[],[f110]) ).
fof(f288,plain,
! [X0] :
( ~ p203(sK61(X0))
| ~ p303(X0)
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f289,plain,
! [X0] :
( r1(X0,sK61(X0))
| ~ p303(X0)
| ~ sP19(X0) ),
inference(cnf_transformation,[],[f113]) ).
fof(f290,plain,
! [X0] :
( ~ p103(sK62(X0))
| ~ p603(X0)
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f291,plain,
! [X0] :
( r1(X0,sK62(X0))
| ~ p603(X0)
| ~ sP18(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f292,plain,
! [X0] :
( ~ p103(sK63(X0))
| ~ p503(X0)
| ~ sP17(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f293,plain,
! [X0] :
( r1(X0,sK63(X0))
| ~ p503(X0)
| ~ sP17(X0) ),
inference(cnf_transformation,[],[f119]) ).
fof(f294,plain,
! [X0] :
( ~ p103(sK64(X0))
| ~ p403(X0)
| ~ sP16(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f295,plain,
! [X0] :
( r1(X0,sK64(X0))
| ~ p403(X0)
| ~ sP16(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f296,plain,
! [X0] :
( ~ p103(sK65(X0))
| ~ p303(X0)
| ~ sP15(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f297,plain,
! [X0] :
( r1(X0,sK65(X0))
| ~ p303(X0)
| ~ sP15(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f298,plain,
! [X0] :
( ~ p102(sK66(X0))
| ~ p602(X0)
| ~ sP14(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f299,plain,
! [X0] :
( r1(X0,sK66(X0))
| ~ p602(X0)
| ~ sP14(X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f300,plain,
! [X0] :
( ~ p102(sK67(X0))
| ~ p502(X0)
| ~ sP13(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f301,plain,
! [X0] :
( r1(X0,sK67(X0))
| ~ p502(X0)
| ~ sP13(X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f302,plain,
! [X0] :
( ~ p102(sK68(X0))
| ~ p402(X0)
| ~ sP12(X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f303,plain,
! [X0] :
( r1(X0,sK68(X0))
| ~ p402(X0)
| ~ sP12(X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f304,plain,
! [X0] :
( ~ p102(sK69(X0))
| ~ p302(X0)
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f305,plain,
! [X0] :
( r1(X0,sK69(X0))
| ~ p302(X0)
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f306,plain,
! [X0] :
( ~ p102(sK70(X0))
| ~ p202(X0)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f307,plain,
! [X0] :
( r1(X0,sK70(X0))
| ~ p202(X0)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f140]) ).
fof(f308,plain,
! [X0] :
( ~ p305(sK72(X0))
| ~ p405(sK71(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f309,plain,
! [X0] :
( r1(X0,sK72(X0))
| ~ p405(sK71(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f310,plain,
! [X0] :
( r1(X0,sK71(X0))
| ~ p305(sK72(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f311,plain,
! [X0] :
( r1(X0,sK72(X0))
| r1(X0,sK71(X0))
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f312,plain,
! [X0] :
( ~ p205(sK74(X0))
| ~ p405(sK73(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f313,plain,
! [X0] :
( r1(X0,sK74(X0))
| ~ p405(sK73(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f314,plain,
! [X0] :
( r1(X0,sK73(X0))
| ~ p205(sK74(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f315,plain,
! [X0] :
( r1(X0,sK74(X0))
| r1(X0,sK73(X0))
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f316,plain,
! [X0] :
( ~ p205(sK76(X0))
| ~ p305(sK75(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f317,plain,
! [X0] :
( r1(X0,sK76(X0))
| ~ p305(sK75(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f318,plain,
! [X0] :
( r1(X0,sK75(X0))
| ~ p205(sK76(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f319,plain,
! [X0] :
( r1(X0,sK76(X0))
| r1(X0,sK75(X0))
| ~ sP7(X0) ),
inference(cnf_transformation,[],[f149]) ).
fof(f320,plain,
! [X0] :
( ~ p105(sK78(X0))
| ~ p405(sK77(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f321,plain,
! [X0] :
( r1(X0,sK78(X0))
| ~ p405(sK77(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f322,plain,
! [X0] :
( r1(X0,sK77(X0))
| ~ p105(sK78(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f323,plain,
! [X0] :
( r1(X0,sK78(X0))
| r1(X0,sK77(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f152]) ).
fof(f324,plain,
! [X0] :
( ~ p105(sK80(X0))
| ~ p305(sK79(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f325,plain,
! [X0] :
( r1(X0,sK80(X0))
| ~ p305(sK79(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f326,plain,
! [X0] :
( r1(X0,sK79(X0))
| ~ p105(sK80(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f327,plain,
! [X0] :
( r1(X0,sK80(X0))
| r1(X0,sK79(X0))
| ~ sP5(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f328,plain,
! [X0] :
( ~ p105(sK82(X0))
| ~ p205(sK81(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f329,plain,
! [X0] :
( r1(X0,sK82(X0))
| ~ p205(sK81(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f330,plain,
! [X0] :
( r1(X0,sK81(X0))
| ~ p105(sK82(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f331,plain,
! [X0] :
( r1(X0,sK82(X0))
| r1(X0,sK81(X0))
| ~ sP4(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f332,plain,
! [X0] :
( ~ p204(sK84(X0))
| ~ p304(sK83(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f333,plain,
! [X0] :
( r1(X0,sK84(X0))
| ~ p304(sK83(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f334,plain,
! [X0] :
( r1(X0,sK83(X0))
| ~ p204(sK84(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f335,plain,
! [X0] :
( r1(X0,sK84(X0))
| r1(X0,sK83(X0))
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f161]) ).
fof(f336,plain,
! [X0] :
( ~ p104(sK86(X0))
| ~ p304(sK85(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f337,plain,
! [X0] :
( r1(X0,sK86(X0))
| ~ p304(sK85(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f338,plain,
! [X0] :
( r1(X0,sK85(X0))
| ~ p104(sK86(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f339,plain,
! [X0] :
( r1(X0,sK86(X0))
| r1(X0,sK85(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f164]) ).
fof(f340,plain,
! [X0] :
( ~ p104(sK88(X0))
| ~ p204(sK87(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f167]) ).
fof(f341,plain,
! [X0] :
( r1(X0,sK88(X0))
| ~ p204(sK87(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f167]) ).
fof(f342,plain,
! [X0] :
( r1(X0,sK87(X0))
| ~ p104(sK88(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f167]) ).
fof(f343,plain,
! [X0] :
( r1(X0,sK88(X0))
| r1(X0,sK87(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f167]) ).
fof(f344,plain,
! [X0] :
( ~ p103(sK90(X0))
| ~ p203(sK89(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f345,plain,
! [X0] :
( r1(X0,sK90(X0))
| ~ p203(sK89(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f346,plain,
! [X0] :
( r1(X0,sK89(X0))
| ~ p103(sK90(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f347,plain,
! [X0] :
( r1(X0,sK90(X0))
| r1(X0,sK89(X0))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f170]) ).
fof(f348,plain,
! [X10,X11,X9,X12] :
( ~ r1(sK92,X9)
| p105(X9)
| ~ r1(sK92,X10)
| p104(X10)
| ~ r1(sK92,X11)
| p103(X11)
| ~ r1(sK92,X12)
| p102(X12)
| p101(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f349,plain,
! [X8,X6,X7] :
( ~ r1(sK92,X6)
| p205(X6)
| ~ r1(sK92,X7)
| p204(X7)
| ~ r1(sK92,X8)
| p203(X8)
| p202(sK92)
| p201(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f350,plain,
! [X4,X5] :
( ~ r1(sK92,X4)
| p305(X4)
| ~ r1(sK92,X5)
| p304(X5)
| p303(sK92)
| p302(sK92)
| p301(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f351,plain,
! [X3] :
( ~ r1(sK92,X3)
| p405(X3)
| p404(sK92)
| p403(sK92)
| p402(sK92)
| p401(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f352,plain,
( p505(sK92)
| p504(sK92)
| p503(sK92)
| p502(sK92)
| p501(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f353,plain,
( p605(sK92)
| p604(sK92)
| p603(sK92)
| p602(sK92)
| p601(sK92) ),
inference(cnf_transformation,[],[f172]) ).
fof(f354,plain,
r1(sK91,sK92),
inference(cnf_transformation,[],[f172]) ).
fof(f355,plain,
! [X1] :
( ~ r1(sK91,X1)
| sP40(X1) ),
inference(cnf_transformation,[],[f172]) ).
fof(f357,definition,
( spl93_1
<=> p101(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_1])],[avatar_definition]) ).
fof(f361,definition,
( spl93_2
<=> ! [X12] :
( ~ r1(sK92,X12)
| p102(X12) ) ),
introduced(definition,[new_symbols(definition,[spl93_2])],[avatar_definition]) ).
fof(f362,plain,
( ! [X12] :
( ~ r1(sK92,X12)
| p102(X12) )
| ~ spl93_2 ),
inference(avatar_component_clause,[],[f361]) ).
fof(f364,definition,
( spl93_3
<=> ! [X11] :
( ~ r1(sK92,X11)
| p103(X11) ) ),
introduced(definition,[new_symbols(definition,[spl93_3])],[avatar_definition]) ).
fof(f365,plain,
( ! [X11] :
( ~ r1(sK92,X11)
| p103(X11) )
| ~ spl93_3 ),
inference(avatar_component_clause,[],[f364]) ).
fof(f367,definition,
( spl93_4
<=> ! [X10] :
( ~ r1(sK92,X10)
| p104(X10) ) ),
introduced(definition,[new_symbols(definition,[spl93_4])],[avatar_definition]) ).
fof(f368,plain,
( ! [X10] :
( ~ r1(sK92,X10)
| p104(X10) )
| ~ spl93_4 ),
inference(avatar_component_clause,[],[f367]) ).
fof(f370,definition,
( spl93_5
<=> ! [X9] :
( ~ r1(sK92,X9)
| p105(X9) ) ),
introduced(definition,[new_symbols(definition,[spl93_5])],[avatar_definition]) ).
fof(f371,plain,
( ! [X9] :
( ~ r1(sK92,X9)
| p105(X9) )
| ~ spl93_5 ),
inference(avatar_component_clause,[],[f370]) ).
fof(f372,plain,
( spl93_1
| spl93_2
| spl93_3
| spl93_4
| spl93_5 ),
inference(avatar_split_clause,[],[f348,f370,f367,f364,f361,f357]) ).
fof(f374,definition,
( spl93_6
<=> p201(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_6])],[avatar_definition]) ).
fof(f376,plain,
( p201(sK92)
| ~ spl93_6 ),
inference(avatar_component_clause,[],[f374]) ).
fof(f378,definition,
( spl93_7
<=> p202(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_7])],[avatar_definition]) ).
fof(f380,plain,
( p202(sK92)
| ~ spl93_7 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl93_8
<=> ! [X8] :
( ~ r1(sK92,X8)
| p203(X8) ) ),
introduced(definition,[new_symbols(definition,[spl93_8])],[avatar_definition]) ).
fof(f383,plain,
( ! [X8] :
( ~ r1(sK92,X8)
| p203(X8) )
| ~ spl93_8 ),
inference(avatar_component_clause,[],[f382]) ).
fof(f385,definition,
( spl93_9
<=> ! [X7] :
( ~ r1(sK92,X7)
| p204(X7) ) ),
introduced(definition,[new_symbols(definition,[spl93_9])],[avatar_definition]) ).
fof(f386,plain,
( ! [X7] :
( ~ r1(sK92,X7)
| p204(X7) )
| ~ spl93_9 ),
inference(avatar_component_clause,[],[f385]) ).
fof(f388,definition,
( spl93_10
<=> ! [X6] :
( ~ r1(sK92,X6)
| p205(X6) ) ),
introduced(definition,[new_symbols(definition,[spl93_10])],[avatar_definition]) ).
fof(f389,plain,
( ! [X6] :
( ~ r1(sK92,X6)
| p205(X6) )
| ~ spl93_10 ),
inference(avatar_component_clause,[],[f388]) ).
fof(f390,plain,
( spl93_6
| spl93_7
| spl93_8
| spl93_9
| spl93_10 ),
inference(avatar_split_clause,[],[f349,f388,f385,f382,f378,f374]) ).
fof(f392,definition,
( spl93_11
<=> p301(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_11])],[avatar_definition]) ).
fof(f394,plain,
( p301(sK92)
| ~ spl93_11 ),
inference(avatar_component_clause,[],[f392]) ).
fof(f396,definition,
( spl93_12
<=> p302(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_12])],[avatar_definition]) ).
fof(f398,plain,
( p302(sK92)
| ~ spl93_12 ),
inference(avatar_component_clause,[],[f396]) ).
fof(f400,definition,
( spl93_13
<=> p303(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_13])],[avatar_definition]) ).
fof(f402,plain,
( p303(sK92)
| ~ spl93_13 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f404,definition,
( spl93_14
<=> ! [X5] :
( ~ r1(sK92,X5)
| p304(X5) ) ),
introduced(definition,[new_symbols(definition,[spl93_14])],[avatar_definition]) ).
fof(f405,plain,
( ! [X5] :
( ~ r1(sK92,X5)
| p304(X5) )
| ~ spl93_14 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f407,definition,
( spl93_15
<=> ! [X4] :
( ~ r1(sK92,X4)
| p305(X4) ) ),
introduced(definition,[new_symbols(definition,[spl93_15])],[avatar_definition]) ).
fof(f408,plain,
( ! [X4] :
( ~ r1(sK92,X4)
| p305(X4) )
| ~ spl93_15 ),
inference(avatar_component_clause,[],[f407]) ).
fof(f409,plain,
( spl93_11
| spl93_12
| spl93_13
| spl93_14
| spl93_15 ),
inference(avatar_split_clause,[],[f350,f407,f404,f400,f396,f392]) ).
fof(f411,definition,
( spl93_16
<=> p401(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_16])],[avatar_definition]) ).
fof(f413,plain,
( p401(sK92)
| ~ spl93_16 ),
inference(avatar_component_clause,[],[f411]) ).
fof(f415,definition,
( spl93_17
<=> p402(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_17])],[avatar_definition]) ).
fof(f419,definition,
( spl93_18
<=> p403(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_18])],[avatar_definition]) ).
fof(f421,plain,
( p403(sK92)
| ~ spl93_18 ),
inference(avatar_component_clause,[],[f419]) ).
fof(f423,definition,
( spl93_19
<=> p404(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_19])],[avatar_definition]) ).
fof(f427,definition,
( spl93_20
<=> ! [X3] :
( ~ r1(sK92,X3)
| p405(X3) ) ),
introduced(definition,[new_symbols(definition,[spl93_20])],[avatar_definition]) ).
fof(f428,plain,
( ! [X3] :
( ~ r1(sK92,X3)
| p405(X3) )
| ~ spl93_20 ),
inference(avatar_component_clause,[],[f427]) ).
fof(f429,plain,
( spl93_16
| spl93_17
| spl93_18
| spl93_19
| spl93_20 ),
inference(avatar_split_clause,[],[f351,f427,f423,f419,f415,f411]) ).
fof(f431,definition,
( spl93_21
<=> p501(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_21])],[avatar_definition]) ).
fof(f433,plain,
( p501(sK92)
| ~ spl93_21 ),
inference(avatar_component_clause,[],[f431]) ).
fof(f435,definition,
( spl93_22
<=> p502(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_22])],[avatar_definition]) ).
fof(f437,plain,
( p502(sK92)
| ~ spl93_22 ),
inference(avatar_component_clause,[],[f435]) ).
fof(f439,definition,
( spl93_23
<=> p503(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_23])],[avatar_definition]) ).
fof(f443,definition,
( spl93_24
<=> p504(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_24])],[avatar_definition]) ).
fof(f445,plain,
( p504(sK92)
| ~ spl93_24 ),
inference(avatar_component_clause,[],[f443]) ).
fof(f447,definition,
( spl93_25
<=> p505(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_25])],[avatar_definition]) ).
fof(f449,plain,
( p505(sK92)
| ~ spl93_25 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f450,plain,
( spl93_21
| spl93_22
| spl93_23
| spl93_24
| spl93_25 ),
inference(avatar_split_clause,[],[f352,f447,f443,f439,f435,f431]) ).
fof(f452,definition,
( spl93_26
<=> p601(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_26])],[avatar_definition]) ).
fof(f454,plain,
( p601(sK92)
| ~ spl93_26 ),
inference(avatar_component_clause,[],[f452]) ).
fof(f456,definition,
( spl93_27
<=> p602(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_27])],[avatar_definition]) ).
fof(f458,plain,
( p602(sK92)
| ~ spl93_27 ),
inference(avatar_component_clause,[],[f456]) ).
fof(f460,definition,
( spl93_28
<=> p603(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_28])],[avatar_definition]) ).
fof(f464,definition,
( spl93_29
<=> p604(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_29])],[avatar_definition]) ).
fof(f468,definition,
( spl93_30
<=> p605(sK92) ),
introduced(definition,[new_symbols(definition,[spl93_30])],[avatar_definition]) ).
fof(f471,plain,
( spl93_26
| spl93_27
| spl93_28
| spl93_29
| spl93_30 ),
inference(avatar_split_clause,[],[f353,f468,f464,f460,f456,f452]) ).
fof(f472,plain,
sP40(sK92),
inference(resolution,[],[f355,f354]) ).
fof(f473,plain,
sP10(sK92),
inference(resolution,[],[f188,f472]) ).
fof(f474,plain,
sP11(sK92),
inference(resolution,[],[f189,f472]) ).
fof(f475,plain,
sP12(sK92),
inference(resolution,[],[f190,f472]) ).
fof(f476,plain,
sP13(sK92),
inference(resolution,[],[f191,f472]) ).
fof(f477,plain,
sP14(sK92),
inference(resolution,[],[f192,f472]) ).
fof(f478,plain,
sP0(sK92),
inference(resolution,[],[f203,f472]) ).
fof(f479,plain,
sP15(sK92),
inference(resolution,[],[f204,f472]) ).
fof(f480,plain,
sP16(sK92),
inference(resolution,[],[f205,f472]) ).
fof(f481,plain,
sP17(sK92),
inference(resolution,[],[f206,f472]) ).
fof(f482,plain,
sP18(sK92),
inference(resolution,[],[f207,f472]) ).
fof(f483,plain,
sP19(sK92),
inference(resolution,[],[f208,f472]) ).
fof(f484,plain,
sP20(sK92),
inference(resolution,[],[f209,f472]) ).
fof(f485,plain,
sP21(sK92),
inference(resolution,[],[f210,f472]) ).
fof(f486,plain,
sP22(sK92),
inference(resolution,[],[f211,f472]) ).
fof(f487,plain,
sP1(sK92),
inference(resolution,[],[f218,f472]) ).
fof(f488,plain,
sP2(sK92),
inference(resolution,[],[f219,f472]) ).
fof(f489,plain,
sP23(sK92),
inference(resolution,[],[f220,f472]) ).
fof(f490,plain,
sP24(sK92),
inference(resolution,[],[f221,f472]) ).
fof(f491,plain,
sP25(sK92),
inference(resolution,[],[f222,f472]) ).
fof(f492,plain,
sP3(sK92),
inference(resolution,[],[f223,f472]) ).
fof(f493,plain,
sP26(sK92),
inference(resolution,[],[f224,f472]) ).
fof(f494,plain,
sP27(sK92),
inference(resolution,[],[f225,f472]) ).
fof(f495,plain,
sP28(sK92),
inference(resolution,[],[f226,f472]) ).
fof(f496,plain,
sP29(sK92),
inference(resolution,[],[f227,f472]) ).
fof(f497,plain,
sP30(sK92),
inference(resolution,[],[f228,f472]) ).
fof(f498,plain,
sP31(sK92),
inference(resolution,[],[f229,f472]) ).
fof(f499,plain,
sP4(sK92),
inference(resolution,[],[f233,f472]) ).
fof(f500,plain,
sP5(sK92),
inference(resolution,[],[f234,f472]) ).
fof(f501,plain,
sP6(sK92),
inference(resolution,[],[f235,f472]) ).
fof(f502,plain,
sP32(sK92),
inference(resolution,[],[f236,f472]) ).
fof(f503,plain,
sP33(sK92),
inference(resolution,[],[f237,f472]) ).
fof(f504,plain,
sP7(sK92),
inference(resolution,[],[f238,f472]) ).
fof(f505,plain,
sP8(sK92),
inference(resolution,[],[f239,f472]) ).
fof(f506,plain,
sP34(sK92),
inference(resolution,[],[f240,f472]) ).
fof(f507,plain,
sP35(sK92),
inference(resolution,[],[f241,f472]) ).
fof(f508,plain,
sP9(sK92),
inference(resolution,[],[f242,f472]) ).
fof(f509,plain,
sP36(sK92),
inference(resolution,[],[f243,f472]) ).
fof(f510,plain,
sP37(sK92),
inference(resolution,[],[f244,f472]) ).
fof(f511,plain,
sP38(sK92),
inference(resolution,[],[f245,f472]) ).
fof(f512,plain,
sP39(sK92),
inference(resolution,[],[f246,f472]) ).
fof(f513,plain,
( ~ p101(sK92)
| ~ p201(sK92) ),
inference(resolution,[],[f173,f472]) ).
fof(f516,plain,
( ~ p101(sK92)
| ~ p301(sK92) ),
inference(resolution,[],[f174,f472]) ).
fof(f517,plain,
( ~ p101(sK92)
| ~ p401(sK92) ),
inference(resolution,[],[f175,f472]) ).
fof(f518,plain,
( ~ p101(sK92)
| ~ p501(sK92) ),
inference(resolution,[],[f176,f472]) ).
fof(f519,plain,
( ~ p101(sK92)
| ~ p601(sK92) ),
inference(resolution,[],[f177,f472]) ).
fof(f520,plain,
( ~ p201(sK92)
| ~ p301(sK92) ),
inference(resolution,[],[f178,f472]) ).
fof(f521,plain,
( ~ p301(sK92)
| ~ spl93_6 ),
inference(forward_subsumption_resolution,[],[f520,f376]) ).
fof(f522,plain,
( $false
| ~ spl93_6
| ~ spl93_11 ),
inference(forward_subsumption_resolution,[],[f521,f394]) ).
fof(f523,plain,
( ~ spl93_6
| ~ spl93_11 ),
inference(avatar_contradiction_clause,[],[f522]) ).
fof(f526,plain,
( ~ p201(sK92)
| ~ p401(sK92) ),
inference(resolution,[],[f179,f472]) ).
fof(f527,plain,
( ~ p201(sK92)
| ~ p501(sK92) ),
inference(resolution,[],[f180,f472]) ).
fof(f528,plain,
( ~ p201(sK92)
| ~ p601(sK92) ),
inference(resolution,[],[f181,f472]) ).
fof(f529,plain,
( ~ p301(sK92)
| ~ p401(sK92) ),
inference(resolution,[],[f182,f472]) ).
fof(f530,plain,
( ~ p401(sK92)
| ~ spl93_11 ),
inference(forward_subsumption_resolution,[],[f529,f394]) ).
fof(f531,plain,
( $false
| ~ spl93_11
| ~ spl93_16 ),
inference(forward_subsumption_resolution,[],[f530,f413]) ).
fof(f532,plain,
( ~ spl93_11
| ~ spl93_16 ),
inference(avatar_contradiction_clause,[],[f531]) ).
fof(f533,plain,
( ~ p301(sK92)
| ~ spl93_16 ),
inference(forward_subsumption_resolution,[],[f529,f413]) ).
fof(f534,plain,
( ~ spl93_11
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f533,f411,f392]) ).
fof(f535,plain,
( ~ p301(sK92)
| ~ p501(sK92) ),
inference(resolution,[],[f183,f472]) ).
fof(f536,plain,
( ~ p301(sK92)
| ~ p601(sK92) ),
inference(resolution,[],[f184,f472]) ).
fof(f537,plain,
( ~ p401(sK92)
| ~ p501(sK92) ),
inference(resolution,[],[f185,f472]) ).
fof(f543,plain,
( ~ p401(sK92)
| ~ p601(sK92) ),
inference(resolution,[],[f186,f472]) ).
fof(f544,plain,
( ~ p501(sK92)
| ~ p601(sK92) ),
inference(resolution,[],[f187,f472]) ).
fof(f545,plain,
( ~ p601(sK92)
| ~ spl93_21 ),
inference(forward_subsumption_resolution,[],[f544,f433]) ).
fof(f546,plain,
( $false
| ~ spl93_21
| ~ spl93_26 ),
inference(forward_subsumption_resolution,[],[f545,f454]) ).
fof(f547,plain,
( ~ spl93_21
| ~ spl93_26 ),
inference(avatar_contradiction_clause,[],[f546]) ).
fof(f550,plain,
( ~ p202(sK92)
| ~ p302(sK92) ),
inference(resolution,[],[f193,f472]) ).
fof(f551,plain,
( ~ p302(sK92)
| ~ spl93_7 ),
inference(forward_subsumption_resolution,[],[f550,f380]) ).
fof(f552,plain,
( $false
| ~ spl93_7
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f551,f398]) ).
fof(f553,plain,
( ~ spl93_7
| ~ spl93_12 ),
inference(avatar_contradiction_clause,[],[f552]) ).
fof(f554,plain,
( ~ p202(sK92)
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f550,f398]) ).
fof(f555,plain,
( ~ spl93_7
| ~ spl93_12 ),
inference(avatar_split_clause,[],[f554,f396,f378]) ).
fof(f556,plain,
( ~ p202(sK92)
| ~ p402(sK92) ),
inference(resolution,[],[f194,f472]) ).
fof(f557,plain,
( ~ p202(sK92)
| ~ p502(sK92) ),
inference(resolution,[],[f195,f472]) ).
fof(f558,plain,
( ~ p202(sK92)
| ~ p602(sK92) ),
inference(resolution,[],[f196,f472]) ).
fof(f559,plain,
( ~ p302(sK92)
| ~ p402(sK92) ),
inference(resolution,[],[f197,f472]) ).
fof(f560,plain,
( ~ p402(sK92)
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f559,f398]) ).
fof(f563,plain,
( ~ spl93_17
| ~ spl93_12 ),
inference(avatar_split_clause,[],[f560,f396,f415]) ).
fof(f564,plain,
( ~ p302(sK92)
| ~ p502(sK92) ),
inference(resolution,[],[f198,f472]) ).
fof(f565,plain,
( ~ p502(sK92)
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f564,f398]) ).
fof(f566,plain,
( $false
| ~ spl93_12
| ~ spl93_22 ),
inference(forward_subsumption_resolution,[],[f565,f437]) ).
fof(f567,plain,
( ~ spl93_12
| ~ spl93_22 ),
inference(avatar_contradiction_clause,[],[f566]) ).
fof(f569,plain,
( ~ p302(sK92)
| ~ p602(sK92) ),
inference(resolution,[],[f199,f472]) ).
fof(f570,plain,
( ~ p602(sK92)
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f569,f398]) ).
fof(f571,plain,
( ~ spl93_27
| ~ spl93_12 ),
inference(avatar_split_clause,[],[f570,f396,f456]) ).
fof(f572,plain,
( ~ p402(sK92)
| ~ p502(sK92) ),
inference(resolution,[],[f200,f472]) ).
fof(f573,plain,
( ~ p402(sK92)
| ~ p602(sK92) ),
inference(resolution,[],[f201,f472]) ).
fof(f574,plain,
( ~ p502(sK92)
| ~ p602(sK92) ),
inference(resolution,[],[f202,f472]) ).
fof(f575,plain,
( ~ p303(sK92)
| ~ p403(sK92) ),
inference(resolution,[],[f212,f472]) ).
fof(f578,plain,
( ~ p303(sK92)
| ~ p503(sK92) ),
inference(resolution,[],[f213,f472]) ).
fof(f579,plain,
( ~ p303(sK92)
| ~ p603(sK92) ),
inference(resolution,[],[f214,f472]) ).
fof(f580,plain,
( ~ p403(sK92)
| ~ p503(sK92) ),
inference(resolution,[],[f215,f472]) ).
fof(f585,plain,
( ~ p403(sK92)
| ~ p603(sK92) ),
inference(resolution,[],[f216,f472]) ).
fof(f586,plain,
( ~ p603(sK92)
| ~ spl93_18 ),
inference(forward_subsumption_resolution,[],[f585,f421]) ).
fof(f587,plain,
( ~ spl93_28
| ~ spl93_18 ),
inference(avatar_split_clause,[],[f586,f419,f460]) ).
fof(f588,plain,
( ~ p503(sK92)
| ~ p603(sK92) ),
inference(resolution,[],[f217,f472]) ).
fof(f589,plain,
( ~ p404(sK92)
| ~ p504(sK92) ),
inference(resolution,[],[f230,f472]) ).
fof(f590,plain,
( ~ p404(sK92)
| ~ spl93_24 ),
inference(forward_subsumption_resolution,[],[f589,f445]) ).
fof(f591,plain,
( ~ spl93_19
| ~ spl93_24 ),
inference(avatar_split_clause,[],[f590,f443,f423]) ).
fof(f592,plain,
( ~ p404(sK92)
| ~ p604(sK92) ),
inference(resolution,[],[f231,f472]) ).
fof(f593,plain,
( ~ p504(sK92)
| ~ p604(sK92) ),
inference(resolution,[],[f232,f472]) ).
fof(f594,plain,
( ~ p604(sK92)
| ~ spl93_24 ),
inference(forward_subsumption_resolution,[],[f593,f445]) ).
fof(f595,plain,
( ~ spl93_29
| ~ spl93_24 ),
inference(avatar_split_clause,[],[f594,f443,f464]) ).
fof(f596,plain,
( ~ p505(sK92)
| ~ p605(sK92) ),
inference(resolution,[],[f247,f472]) ).
fof(f597,plain,
( ~ spl93_30
| ~ spl93_25 ),
inference(avatar_split_clause,[],[f596,f447,f468]) ).
fof(f807,plain,
( ~ p403(sK92)
| ~ sP20(sK92)
| p203(sK60(sK92))
| ~ spl93_8 ),
inference(resolution,[],[f287,f383]) ).
fof(f810,plain,
( ~ p403(sK92)
| ~ sP20(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f807,f286]) ).
fof(f825,plain,
( ~ sP20(sK92)
| ~ spl93_8
| ~ spl93_18 ),
inference(forward_subsumption_resolution,[],[f810,f421]) ).
fof(f826,plain,
( $false
| ~ spl93_8
| ~ spl93_18 ),
inference(forward_subsumption_resolution,[],[f825,f484]) ).
fof(f827,plain,
( ~ spl93_8
| ~ spl93_18 ),
inference(avatar_contradiction_clause,[],[f826]) ).
fof(f829,plain,
( ~ p403(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f810,f484]) ).
fof(f835,plain,
( ~ spl93_18
| ~ spl93_8 ),
inference(avatar_split_clause,[],[f829,f382,f419]) ).
fof(f836,plain,
( p405(sK41(sK92))
| ~ p605(sK92)
| ~ sP39(sK92)
| ~ spl93_20 ),
inference(resolution,[],[f428,f249]) ).
fof(f837,plain,
( p405(sK42(sK92))
| ~ p505(sK92)
| ~ sP38(sK92)
| ~ spl93_20 ),
inference(resolution,[],[f428,f251]) ).
fof(f859,plain,
( ~ p605(sK92)
| ~ sP39(sK92)
| ~ spl93_20 ),
inference(forward_subsumption_resolution,[],[f836,f248]) ).
fof(f977,plain,
( ~ p302(sK92)
| ~ sP11(sK92)
| p102(sK69(sK92))
| ~ spl93_2 ),
inference(resolution,[],[f305,f362]) ).
fof(f978,plain,
( ~ p302(sK92)
| ~ sP11(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f977,f304]) ).
fof(f994,plain,
( ~ sP11(sK92)
| ~ spl93_2
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f978,f398]) ).
fof(f997,plain,
( $false
| ~ spl93_2
| ~ spl93_12 ),
inference(forward_subsumption_resolution,[],[f994,f474]) ).
fof(f998,plain,
( ~ spl93_2
| ~ spl93_12 ),
inference(avatar_contradiction_clause,[],[f997]) ).
fof(f1007,plain,
( ~ spl93_26
| ~ spl93_1 ),
inference(avatar_split_clause,[],[f519,f357,f452]) ).
fof(f1015,plain,
( ~ p505(sK92)
| ~ sP38(sK92)
| ~ spl93_20 ),
inference(forward_subsumption_resolution,[],[f837,f250]) ).
fof(f1016,plain,
( ~ spl93_29
| ~ spl93_24 ),
inference(avatar_split_clause,[],[f593,f443,f464]) ).
fof(f1088,plain,
( ~ p505(sK92)
| ~ spl93_20 ),
inference(forward_subsumption_resolution,[],[f1015,f511]) ).
fof(f1119,plain,
( ~ spl93_25
| ~ spl93_20 ),
inference(avatar_split_clause,[],[f1088,f427,f447]) ).
fof(f1126,plain,
( ~ p605(sK92)
| ~ spl93_20 ),
inference(forward_subsumption_resolution,[],[f859,f512]) ).
fof(f1127,plain,
( ~ spl93_21
| ~ spl93_1 ),
inference(avatar_split_clause,[],[f518,f357,f431]) ).
fof(f1128,plain,
( ~ spl93_26
| ~ spl93_21 ),
inference(avatar_split_clause,[],[f544,f431,f452]) ).
fof(f1159,plain,
( ~ spl93_30
| ~ spl93_20 ),
inference(avatar_split_clause,[],[f1126,f427,f468]) ).
fof(f1162,plain,
( ~ spl93_22
| ~ spl93_12 ),
inference(avatar_split_clause,[],[f564,f396,f435]) ).
fof(f1165,plain,
( ~ spl93_21
| ~ spl93_11 ),
inference(avatar_split_clause,[],[f535,f392,f431]) ).
fof(f1166,plain,
( ~ spl93_26
| ~ spl93_11 ),
inference(avatar_split_clause,[],[f536,f392,f452]) ).
fof(f1167,plain,
( ~ spl93_11
| ~ spl93_1 ),
inference(avatar_split_clause,[],[f516,f357,f392]) ).
fof(f1211,plain,
( p103(sK64(sK92))
| ~ p403(sK92)
| ~ sP16(sK92)
| ~ spl93_3 ),
inference(resolution,[],[f365,f295]) ).
fof(f1218,plain,
( ~ p403(sK92)
| ~ sP16(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f1211,f294]) ).
fof(f1228,plain,
( p304(sK49(sK92))
| ~ p604(sK92)
| ~ sP31(sK92)
| ~ spl93_14 ),
inference(resolution,[],[f405,f265]) ).
fof(f1229,plain,
( p304(sK50(sK92))
| ~ p504(sK92)
| ~ sP30(sK92)
| ~ spl93_14 ),
inference(resolution,[],[f405,f267]) ).
fof(f1250,plain,
( ~ p504(sK92)
| ~ sP30(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f1229,f266]) ).
fof(f1251,plain,
( ~ p604(sK92)
| ~ sP31(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f1228,f264]) ).
fof(f1298,definition,
( spl93_123
<=> p405(sK71(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_123])],[avatar_definition]) ).
fof(f1382,definition,
( spl93_137
<=> p405(sK73(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_137])],[avatar_definition]) ).
fof(f1457,definition,
( spl93_149
<=> p305(sK75(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_149])],[avatar_definition]) ).
fof(f1536,definition,
( spl93_162
<=> p405(sK77(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_162])],[avatar_definition]) ).
fof(f1611,definition,
( spl93_174
<=> p305(sK79(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_174])],[avatar_definition]) ).
fof(f1690,definition,
( spl93_187
<=> p205(sK81(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_187])],[avatar_definition]) ).
fof(f1769,definition,
( spl93_200
<=> p304(sK83(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_200])],[avatar_definition]) ).
fof(f1844,definition,
( spl93_212
<=> p304(sK85(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_212])],[avatar_definition]) ).
fof(f1919,definition,
( spl93_224
<=> p204(sK87(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_224])],[avatar_definition]) ).
fof(f1973,plain,
( ~ p203(sK89(sK92))
| ~ sP0(sK92)
| p103(sK90(sK92))
| ~ spl93_3 ),
inference(resolution,[],[f345,f365]) ).
fof(f1978,plain,
( ~ p203(sK89(sK92))
| ~ sP0(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f1973,f344]) ).
fof(f1998,definition,
( spl93_237
<=> p203(sK89(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_237])],[avatar_definition]) ).
fof(f2000,plain,
( ~ p203(sK89(sK92))
| spl93_237 ),
inference(avatar_component_clause,[],[f1998]) ).
fof(f2007,plain,
( ~ p203(sK89(sK92))
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f1978,f478]) ).
fof(f2013,plain,
( ~ spl93_237
| ~ spl93_3 ),
inference(avatar_split_clause,[],[f2007,f364,f1998]) ).
fof(f2053,definition,
( spl93_244
<=> r1(sK92,sK71(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_244])],[avatar_definition]) ).
fof(f2055,plain,
( r1(sK92,sK71(sK92))
| ~ spl93_244 ),
inference(avatar_component_clause,[],[f2053]) ).
fof(f2070,definition,
( spl93_245
<=> r1(sK92,sK73(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_245])],[avatar_definition]) ).
fof(f2072,plain,
( r1(sK92,sK73(sK92))
| ~ spl93_245 ),
inference(avatar_component_clause,[],[f2070]) ).
fof(f2087,definition,
( spl93_246
<=> r1(sK92,sK75(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_246])],[avatar_definition]) ).
fof(f2089,plain,
( r1(sK92,sK75(sK92))
| ~ spl93_246 ),
inference(avatar_component_clause,[],[f2087]) ).
fof(f2104,definition,
( spl93_247
<=> r1(sK92,sK77(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_247])],[avatar_definition]) ).
fof(f2106,plain,
( r1(sK92,sK77(sK92))
| ~ spl93_247 ),
inference(avatar_component_clause,[],[f2104]) ).
fof(f2121,definition,
( spl93_248
<=> r1(sK92,sK79(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_248])],[avatar_definition]) ).
fof(f2123,plain,
( r1(sK92,sK79(sK92))
| ~ spl93_248 ),
inference(avatar_component_clause,[],[f2121]) ).
fof(f2138,definition,
( spl93_249
<=> r1(sK92,sK81(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_249])],[avatar_definition]) ).
fof(f2140,plain,
( r1(sK92,sK81(sK92))
| ~ spl93_249 ),
inference(avatar_component_clause,[],[f2138]) ).
fof(f2155,definition,
( spl93_250
<=> r1(sK92,sK83(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_250])],[avatar_definition]) ).
fof(f2157,plain,
( r1(sK92,sK83(sK92))
| ~ spl93_250 ),
inference(avatar_component_clause,[],[f2155]) ).
fof(f2172,definition,
( spl93_251
<=> r1(sK92,sK85(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_251])],[avatar_definition]) ).
fof(f2174,plain,
( r1(sK92,sK85(sK92))
| ~ spl93_251 ),
inference(avatar_component_clause,[],[f2172]) ).
fof(f2189,definition,
( spl93_252
<=> r1(sK92,sK87(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_252])],[avatar_definition]) ).
fof(f2191,plain,
( r1(sK92,sK87(sK92))
| ~ spl93_252 ),
inference(avatar_component_clause,[],[f2189]) ).
fof(f2198,plain,
( r1(sK92,sK89(sK92))
| ~ sP0(sK92)
| p103(sK90(sK92))
| ~ spl93_3 ),
inference(resolution,[],[f347,f365]) ).
fof(f2203,plain,
( r1(sK92,sK89(sK92))
| ~ sP0(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f2198,f346]) ).
fof(f2206,definition,
( spl93_253
<=> r1(sK92,sK89(sK92)) ),
introduced(definition,[new_symbols(definition,[spl93_253])],[avatar_definition]) ).
fof(f2208,plain,
( r1(sK92,sK89(sK92))
| ~ spl93_253 ),
inference(avatar_component_clause,[],[f2206]) ).
fof(f2211,plain,
( r1(sK92,sK89(sK92))
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f2203,f478]) ).
fof(f2213,plain,
( spl93_253
| ~ spl93_3 ),
inference(avatar_split_clause,[],[f2211,f364,f2206]) ).
fof(f2216,plain,
( p405(sK71(sK92))
| ~ spl93_20
| ~ spl93_244 ),
inference(resolution,[],[f2055,f428]) ).
fof(f2223,plain,
( ~ p202(sK92)
| ~ spl93_22 ),
inference(forward_subsumption_resolution,[],[f557,f437]) ).
fof(f2225,plain,
( ~ spl93_7
| ~ spl93_22 ),
inference(avatar_split_clause,[],[f2223,f435,f378]) ).
fof(f2231,plain,
( ~ p201(sK92)
| ~ spl93_26 ),
inference(forward_subsumption_resolution,[],[f528,f454]) ).
fof(f2232,plain,
( ~ spl93_6
| ~ spl93_26 ),
inference(avatar_split_clause,[],[f2231,f452,f374]) ).
fof(f2247,plain,
( p104(sK55(sK92))
| ~ p604(sK92)
| ~ sP25(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f277]) ).
fof(f2248,plain,
( p104(sK56(sK92))
| ~ p504(sK92)
| ~ sP24(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f279]) ).
fof(f2285,plain,
( p104(sK86(sK92))
| r1(sK92,sK85(sK92))
| ~ sP2(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f339]) ).
fof(f2286,plain,
( p104(sK86(sK92))
| ~ p304(sK85(sK92))
| ~ sP2(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f337]) ).
fof(f2288,plain,
( p104(sK88(sK92))
| r1(sK92,sK87(sK92))
| ~ sP1(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f343]) ).
fof(f2289,plain,
( p104(sK88(sK92))
| ~ p204(sK87(sK92))
| ~ sP1(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f341]) ).
fof(f2294,plain,
( ~ p204(sK87(sK92))
| ~ sP1(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2289,f340]) ).
fof(f2295,plain,
( r1(sK92,sK87(sK92))
| ~ sP1(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2288,f342]) ).
fof(f2296,plain,
( ~ p304(sK85(sK92))
| ~ sP2(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2286,f336]) ).
fof(f2297,plain,
( r1(sK92,sK85(sK92))
| ~ sP2(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2285,f338]) ).
fof(f2306,plain,
( ~ p504(sK92)
| ~ sP24(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2248,f278]) ).
fof(f2307,plain,
( ~ p604(sK92)
| ~ sP25(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2247,f276]) ).
fof(f2313,plain,
( r1(sK92,sK87(sK92))
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2295,f487]) ).
fof(f2314,plain,
( r1(sK92,sK85(sK92))
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2297,f488]) ).
fof(f2351,plain,
( spl93_252
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f2313,f367,f2189]) ).
fof(f2352,plain,
( spl93_251
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f2314,f367,f2172]) ).
fof(f2357,plain,
( p205(sK45(sK92))
| ~ p605(sK92)
| ~ sP35(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f257]) ).
fof(f2358,plain,
( p205(sK46(sK92))
| ~ p505(sK92)
| ~ sP34(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f259]) ).
fof(f2387,plain,
( p205(sK74(sK92))
| r1(sK92,sK73(sK92))
| ~ sP8(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f315]) ).
fof(f2388,plain,
( p205(sK74(sK92))
| ~ p405(sK73(sK92))
| ~ sP8(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f313]) ).
fof(f2390,plain,
( p205(sK76(sK92))
| r1(sK92,sK75(sK92))
| ~ sP7(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f319]) ).
fof(f2391,plain,
( p205(sK76(sK92))
| ~ p305(sK75(sK92))
| ~ sP7(sK92)
| ~ spl93_10 ),
inference(resolution,[],[f389,f317]) ).
fof(f2420,plain,
( ~ p305(sK75(sK92))
| ~ sP7(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2391,f316]) ).
fof(f2421,plain,
( r1(sK92,sK75(sK92))
| ~ sP7(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2390,f318]) ).
fof(f2422,plain,
( ~ p405(sK73(sK92))
| ~ sP8(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2388,f312]) ).
fof(f2423,plain,
( r1(sK92,sK73(sK92))
| ~ sP8(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2387,f314]) ).
fof(f2426,plain,
( ~ p505(sK92)
| ~ sP34(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2358,f258]) ).
fof(f2427,plain,
( ~ p605(sK92)
| ~ sP35(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2357,f256]) ).
fof(f2463,plain,
( r1(sK92,sK75(sK92))
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2421,f504]) ).
fof(f2464,plain,
( r1(sK92,sK73(sK92))
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2423,f505]) ).
fof(f2471,plain,
( spl93_246
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f2463,f388,f2087]) ).
fof(f2472,plain,
( spl93_245
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f2464,f388,f2070]) ).
fof(f2475,plain,
( p305(sK43(sK92))
| ~ p605(sK92)
| ~ sP37(sK92)
| ~ spl93_15 ),
inference(resolution,[],[f408,f253]) ).
fof(f2476,plain,
( p305(sK44(sK92))
| ~ p505(sK92)
| ~ sP36(sK92)
| ~ spl93_15 ),
inference(resolution,[],[f408,f255]) ).
fof(f2504,plain,
( p305(sK72(sK92))
| r1(sK92,sK71(sK92))
| ~ sP9(sK92)
| ~ spl93_15 ),
inference(resolution,[],[f408,f311]) ).
fof(f2505,plain,
( p305(sK72(sK92))
| ~ p405(sK71(sK92))
| ~ sP9(sK92)
| ~ spl93_15 ),
inference(resolution,[],[f408,f309]) ).
fof(f2542,plain,
( ~ p405(sK71(sK92))
| ~ sP9(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2505,f308]) ).
fof(f2543,plain,
( r1(sK92,sK71(sK92))
| ~ sP9(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2504,f310]) ).
fof(f2545,plain,
( ~ p505(sK92)
| ~ sP36(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2476,f254]) ).
fof(f2546,plain,
( ~ p605(sK92)
| ~ sP37(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2475,f252]) ).
fof(f2592,plain,
( r1(sK92,sK71(sK92))
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2543,f508]) ).
fof(f2594,plain,
( spl93_244
| ~ spl93_15 ),
inference(avatar_split_clause,[],[f2592,f407,f2053]) ).
fof(f2655,plain,
( p103(sK65(sK92))
| ~ p303(sK92)
| ~ sP15(sK92)
| ~ spl93_3 ),
inference(resolution,[],[f365,f297]) ).
fof(f2703,plain,
( ~ p303(sK92)
| ~ sP15(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f2655,f296]) ).
fof(f2717,plain,
( ~ sP15(sK92)
| ~ spl93_3
| ~ spl93_13 ),
inference(forward_subsumption_resolution,[],[f2703,f402]) ).
fof(f2719,plain,
( $false
| ~ spl93_3
| ~ spl93_13 ),
inference(forward_subsumption_resolution,[],[f2717,f479]) ).
fof(f2720,plain,
( ~ spl93_3
| ~ spl93_13 ),
inference(avatar_contradiction_clause,[],[f2719]) ).
fof(f2741,plain,
( p104(sK57(sK92))
| ~ p404(sK92)
| ~ sP23(sK92)
| ~ spl93_4 ),
inference(resolution,[],[f368,f281]) ).
fof(f2824,plain,
( p204(sK52(sK92))
| ~ p604(sK92)
| ~ sP28(sK92)
| ~ spl93_9 ),
inference(resolution,[],[f386,f271]) ).
fof(f2825,plain,
( p204(sK53(sK92))
| ~ p504(sK92)
| ~ sP27(sK92)
| ~ spl93_9 ),
inference(resolution,[],[f386,f273]) ).
fof(f2826,plain,
( p204(sK54(sK92))
| ~ p404(sK92)
| ~ sP26(sK92)
| ~ spl93_9 ),
inference(resolution,[],[f386,f275]) ).
fof(f2862,plain,
( p204(sK84(sK92))
| r1(sK92,sK83(sK92))
| ~ sP3(sK92)
| ~ spl93_9 ),
inference(resolution,[],[f386,f335]) ).
fof(f2863,plain,
( p204(sK84(sK92))
| ~ p304(sK83(sK92))
| ~ sP3(sK92)
| ~ spl93_9 ),
inference(resolution,[],[f386,f333]) ).
fof(f2876,plain,
( ~ p304(sK83(sK92))
| ~ sP3(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2863,f332]) ).
fof(f2877,plain,
( r1(sK92,sK83(sK92))
| ~ sP3(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2862,f334]) ).
fof(f2887,plain,
( ~ p504(sK92)
| ~ sP27(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2825,f272]) ).
fof(f2888,plain,
( ~ p604(sK92)
| ~ sP28(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2824,f270]) ).
fof(f2904,plain,
( r1(sK92,sK83(sK92))
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2877,f492]) ).
fof(f2938,plain,
( spl93_250
| ~ spl93_9 ),
inference(avatar_split_clause,[],[f2904,f385,f2155]) ).
fof(f2942,plain,
( p405(sK73(sK92))
| ~ spl93_20
| ~ spl93_245 ),
inference(resolution,[],[f2072,f428]) ).
fof(f2947,plain,
( ~ p404(sK92)
| ~ sP23(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2741,f280]) ).
fof(f2951,plain,
( ~ p404(sK92)
| ~ sP26(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2826,f274]) ).
fof(f2953,plain,
( ~ p404(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2947,f489]) ).
fof(f2969,plain,
( ~ p404(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2951,f493]) ).
fof(f2975,plain,
( ~ spl93_19
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f2953,f367,f423]) ).
fof(f2976,plain,
( ~ spl93_19
| ~ spl93_9 ),
inference(avatar_split_clause,[],[f2969,f385,f423]) ).
fof(f3008,plain,
( p102(sK67(sK92))
| ~ p502(sK92)
| ~ sP13(sK92)
| ~ spl93_2 ),
inference(resolution,[],[f362,f301]) ).
fof(f3011,plain,
( p102(sK70(sK92))
| ~ p202(sK92)
| ~ sP10(sK92)
| ~ spl93_2 ),
inference(resolution,[],[f362,f307]) ).
fof(f3051,plain,
( ~ p202(sK92)
| ~ sP10(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f3011,f306]) ).
fof(f3053,plain,
( ~ p502(sK92)
| ~ sP13(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f3008,f300]) ).
fof(f3110,plain,
( ~ p402(sK92)
| ~ spl93_22 ),
inference(forward_subsumption_resolution,[],[f572,f437]) ).
fof(f3111,plain,
( ~ spl93_17
| ~ spl93_22 ),
inference(avatar_split_clause,[],[f3110,f435,f415]) ).
fof(f3119,plain,
( p105(sK47(sK92))
| ~ p605(sK92)
| ~ sP33(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f261]) ).
fof(f3120,plain,
( p105(sK48(sK92))
| ~ p505(sK92)
| ~ sP32(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f263]) ).
fof(f3153,plain,
( p105(sK78(sK92))
| r1(sK92,sK77(sK92))
| ~ sP6(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f323]) ).
fof(f3154,plain,
( p105(sK78(sK92))
| ~ p405(sK77(sK92))
| ~ sP6(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f321]) ).
fof(f3156,plain,
( p105(sK80(sK92))
| r1(sK92,sK79(sK92))
| ~ sP5(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f327]) ).
fof(f3157,plain,
( p105(sK80(sK92))
| ~ p305(sK79(sK92))
| ~ sP5(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f325]) ).
fof(f3159,plain,
( p105(sK82(sK92))
| r1(sK92,sK81(sK92))
| ~ sP4(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f331]) ).
fof(f3160,plain,
( p105(sK82(sK92))
| ~ p205(sK81(sK92))
| ~ sP4(sK92)
| ~ spl93_5 ),
inference(resolution,[],[f371,f329]) ).
fof(f3177,plain,
( ~ p205(sK81(sK92))
| ~ sP4(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3160,f328]) ).
fof(f3178,plain,
( r1(sK92,sK81(sK92))
| ~ sP4(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3159,f330]) ).
fof(f3179,plain,
( ~ p305(sK79(sK92))
| ~ sP5(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3157,f324]) ).
fof(f3180,plain,
( r1(sK92,sK79(sK92))
| ~ sP5(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3156,f326]) ).
fof(f3181,plain,
( ~ p405(sK77(sK92))
| ~ sP6(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3154,f320]) ).
fof(f3182,plain,
( r1(sK92,sK77(sK92))
| ~ sP6(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3153,f322]) ).
fof(f3191,plain,
( ~ p505(sK92)
| ~ sP32(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3120,f262]) ).
fof(f3192,plain,
( ~ p605(sK92)
| ~ sP33(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3119,f260]) ).
fof(f3213,plain,
( r1(sK92,sK81(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3178,f499]) ).
fof(f3214,plain,
( r1(sK92,sK79(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3180,f500]) ).
fof(f3215,plain,
( r1(sK92,sK77(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3182,f501]) ).
fof(f3228,plain,
( spl93_249
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f3213,f370,f2138]) ).
fof(f3229,plain,
( spl93_248
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f3214,f370,f2121]) ).
fof(f3230,plain,
( spl93_247
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f3215,f370,f2104]) ).
fof(f3325,plain,
( p205(sK81(sK92))
| ~ spl93_10
| ~ spl93_249 ),
inference(resolution,[],[f2140,f389]) ).
fof(f3335,plain,
( ~ spl93_18
| ~ spl93_13 ),
inference(avatar_split_clause,[],[f575,f400,f419]) ).
fof(f3464,plain,
( p305(sK75(sK92))
| ~ spl93_15
| ~ spl93_246 ),
inference(resolution,[],[f408,f2089]) ).
fof(f3466,plain,
( p305(sK79(sK92))
| ~ spl93_15
| ~ spl93_248 ),
inference(resolution,[],[f408,f2123]) ).
fof(f3551,plain,
( ~ p305(sK79(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3179,f500]) ).
fof(f3554,plain,
( spl93_174
| ~ spl93_15
| ~ spl93_248 ),
inference(avatar_split_clause,[],[f3466,f2121,f407,f1611]) ).
fof(f3557,plain,
( ~ spl93_174
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f3551,f370,f1611]) ).
fof(f3663,plain,
( p204(sK87(sK92))
| ~ spl93_9
| ~ spl93_252 ),
inference(resolution,[],[f2191,f386]) ).
fof(f3668,plain,
( ~ p204(sK87(sK92))
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2294,f487]) ).
fof(f3671,plain,
( spl93_224
| ~ spl93_9
| ~ spl93_252 ),
inference(avatar_split_clause,[],[f3663,f2189,f385,f1919]) ).
fof(f3674,plain,
( ~ spl93_224
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f3668,f367,f1919]) ).
fof(f3683,plain,
( ~ p502(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f3053,f476]) ).
fof(f3684,plain,
( ~ p504(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2887,f494]) ).
fof(f3693,plain,
( ~ spl93_22
| ~ spl93_2 ),
inference(avatar_split_clause,[],[f3683,f361,f435]) ).
fof(f3694,plain,
( ~ spl93_24
| ~ spl93_9 ),
inference(avatar_split_clause,[],[f3684,f385,f443]) ).
fof(f3730,plain,
( ~ p505(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2545,f509]) ).
fof(f3739,plain,
( ~ spl93_25
| ~ spl93_15 ),
inference(avatar_split_clause,[],[f3730,f407,f447]) ).
fof(f3777,plain,
( ~ p604(sK92)
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2888,f495]) ).
fof(f3784,plain,
( ~ spl93_29
| ~ spl93_9 ),
inference(avatar_split_clause,[],[f3777,f385,f464]) ).
fof(f3810,plain,
( ~ p605(sK92)
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2546,f510]) ).
fof(f3819,plain,
( ~ spl93_30
| ~ spl93_15 ),
inference(avatar_split_clause,[],[f3810,f407,f468]) ).
fof(f3855,plain,
( ~ spl93_27
| ~ spl93_22 ),
inference(avatar_split_clause,[],[f574,f435,f456]) ).
fof(f3868,plain,
( ~ spl93_28
| ~ spl93_18 ),
inference(avatar_split_clause,[],[f585,f419,f460]) ).
fof(f3877,plain,
( ~ spl93_26
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f543,f411,f452]) ).
fof(f3878,plain,
( ~ spl93_16
| ~ spl93_1 ),
inference(avatar_split_clause,[],[f517,f357,f411]) ).
fof(f3919,plain,
( ~ p403(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f1218,f480]) ).
fof(f3921,plain,
( ~ spl93_18
| ~ spl93_3 ),
inference(avatar_split_clause,[],[f3919,f364,f419]) ).
fof(f3949,plain,
( p103(sK62(sK92))
| ~ p603(sK92)
| ~ sP18(sK92)
| ~ spl93_3 ),
inference(resolution,[],[f365,f291]) ).
fof(f3997,plain,
( ~ p603(sK92)
| ~ sP18(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f3949,f290]) ).
fof(f4016,plain,
( spl93_137
| ~ spl93_20
| ~ spl93_245 ),
inference(avatar_split_clause,[],[f2942,f2070,f427,f1382]) ).
fof(f4017,plain,
( spl93_123
| ~ spl93_20
| ~ spl93_244 ),
inference(avatar_split_clause,[],[f2216,f2053,f427,f1298]) ).
fof(f4020,plain,
( ~ p405(sK71(sK92))
| ~ spl93_15 ),
inference(forward_subsumption_resolution,[],[f2542,f508]) ).
fof(f4024,plain,
( ~ spl93_123
| ~ spl93_15 ),
inference(avatar_split_clause,[],[f4020,f407,f1298]) ).
fof(f4025,plain,
( ~ p603(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f3997,f482]) ).
fof(f4028,plain,
( ~ spl93_28
| ~ spl93_23 ),
inference(avatar_split_clause,[],[f588,f439,f460]) ).
fof(f4033,plain,
( ~ spl93_28
| ~ spl93_3 ),
inference(avatar_split_clause,[],[f4025,f364,f460]) ).
fof(f4082,plain,
( p103(sK63(sK92))
| ~ p503(sK92)
| ~ sP17(sK92)
| ~ spl93_3 ),
inference(resolution,[],[f365,f293]) ).
fof(f4132,plain,
( ~ p503(sK92)
| ~ sP17(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f4082,f292]) ).
fof(f4153,plain,
( ~ p503(sK92)
| ~ spl93_3 ),
inference(forward_subsumption_resolution,[],[f4132,f481]) ).
fof(f4179,plain,
( ~ spl93_23
| ~ spl93_3 ),
inference(avatar_split_clause,[],[f4153,f364,f439]) ).
fof(f4183,plain,
( p304(sK83(sK92))
| ~ spl93_14
| ~ spl93_250 ),
inference(resolution,[],[f405,f2157]) ).
fof(f4194,plain,
( p304(sK51(sK92))
| ~ p404(sK92)
| ~ sP29(sK92)
| ~ spl93_14 ),
inference(resolution,[],[f405,f269]) ).
fof(f4253,plain,
( ~ p404(sK92)
| ~ sP29(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f4194,f268]) ).
fof(f4279,plain,
( ~ p304(sK83(sK92))
| ~ spl93_9 ),
inference(forward_subsumption_resolution,[],[f2876,f492]) ).
fof(f4283,plain,
( spl93_200
| ~ spl93_14
| ~ spl93_250 ),
inference(avatar_split_clause,[],[f4183,f2155,f404,f1769]) ).
fof(f4284,plain,
( ~ spl93_200
| ~ spl93_9 ),
inference(avatar_split_clause,[],[f4279,f385,f1769]) ).
fof(f4289,plain,
( ~ p202(sK92)
| ~ spl93_27 ),
inference(forward_subsumption_resolution,[],[f558,f458]) ).
fof(f4294,plain,
( ~ spl93_7
| ~ spl93_27 ),
inference(avatar_split_clause,[],[f4289,f456,f378]) ).
fof(f4305,plain,
( ~ p201(sK92)
| ~ spl93_16 ),
inference(forward_subsumption_resolution,[],[f526,f413]) ).
fof(f4306,plain,
( ~ spl93_6
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f4305,f411,f374]) ).
fof(f4335,plain,
( p203(sK58(sK92))
| ~ p603(sK92)
| ~ sP22(sK92)
| ~ spl93_8 ),
inference(resolution,[],[f383,f283]) ).
fof(f4336,plain,
( p203(sK59(sK92))
| ~ p503(sK92)
| ~ sP21(sK92)
| ~ spl93_8 ),
inference(resolution,[],[f383,f285]) ).
fof(f4338,plain,
( p203(sK61(sK92))
| ~ p303(sK92)
| ~ sP19(sK92)
| ~ spl93_8 ),
inference(resolution,[],[f383,f289]) ).
fof(f4389,plain,
( ~ p303(sK92)
| ~ sP19(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4338,f288]) ).
fof(f4391,plain,
( ~ p503(sK92)
| ~ sP21(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4336,f284]) ).
fof(f4392,plain,
( ~ p603(sK92)
| ~ sP22(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4335,f282]) ).
fof(f4422,plain,
( p304(sK85(sK92))
| ~ spl93_14
| ~ spl93_251 ),
inference(resolution,[],[f2174,f405]) ).
fof(f4429,plain,
( spl93_212
| ~ spl93_14
| ~ spl93_251 ),
inference(avatar_split_clause,[],[f4422,f2172,f404,f1844]) ).
fof(f4433,plain,
( p203(sK89(sK92))
| ~ spl93_8
| ~ spl93_253 ),
inference(resolution,[],[f2208,f383]) ).
fof(f4438,plain,
( $false
| ~ spl93_8
| spl93_237
| ~ spl93_253 ),
inference(forward_subsumption_resolution,[],[f4433,f2000]) ).
fof(f4439,plain,
( ~ spl93_8
| spl93_237
| ~ spl93_253 ),
inference(avatar_contradiction_clause,[],[f4438]) ).
fof(f4440,plain,
( ~ sP34(sK92)
| ~ spl93_10
| ~ spl93_25 ),
inference(forward_subsumption_resolution,[],[f2426,f449]) ).
fof(f4443,plain,
( spl93_187
| ~ spl93_10
| ~ spl93_249 ),
inference(avatar_split_clause,[],[f3325,f2138,f388,f1690]) ).
fof(f4445,plain,
( $false
| ~ spl93_10
| ~ spl93_25 ),
inference(forward_subsumption_resolution,[],[f4440,f506]) ).
fof(f4446,plain,
( ~ spl93_10
| ~ spl93_25 ),
inference(avatar_contradiction_clause,[],[f4445]) ).
fof(f4453,plain,
( ~ p405(sK73(sK92))
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2422,f505]) ).
fof(f4459,plain,
( ~ p505(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2426,f506]) ).
fof(f4464,plain,
( ~ p504(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f1250,f497]) ).
fof(f4468,plain,
( ~ spl93_137
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f4453,f388,f1382]) ).
fof(f4489,plain,
( ~ spl93_25
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f4459,f388,f447]) ).
fof(f4505,plain,
( ~ spl93_24
| ~ spl93_14 ),
inference(avatar_split_clause,[],[f4464,f404,f443]) ).
fof(f4516,plain,
( ~ spl93_21
| ~ spl93_16 ),
inference(avatar_split_clause,[],[f537,f411,f431]) ).
fof(f4531,plain,
( ~ spl93_24
| ~ spl93_19 ),
inference(avatar_split_clause,[],[f589,f423,f443]) ).
fof(f4537,plain,
( ~ p404(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f4253,f496]) ).
fof(f4563,plain,
( ~ spl93_19
| ~ spl93_14 ),
inference(avatar_split_clause,[],[f4537,f404,f423]) ).
fof(f4572,plain,
( ~ p605(sK92)
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2427,f507]) ).
fof(f4576,plain,
( ~ spl93_27
| ~ spl93_17 ),
inference(avatar_split_clause,[],[f573,f415,f456]) ).
fof(f4617,plain,
( ~ spl93_30
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f4572,f388,f468]) ).
fof(f4628,plain,
( ~ spl93_17
| ~ spl93_7 ),
inference(avatar_split_clause,[],[f556,f378,f415]) ).
fof(f4629,plain,
( ~ spl93_27
| ~ spl93_7 ),
inference(avatar_split_clause,[],[f558,f378,f456]) ).
fof(f4630,plain,
( ~ spl93_21
| ~ spl93_6 ),
inference(avatar_split_clause,[],[f527,f374,f431]) ).
fof(f4631,plain,
( ~ spl93_16
| ~ spl93_6 ),
inference(avatar_split_clause,[],[f526,f374,f411]) ).
fof(f4635,plain,
( ~ p604(sK92)
| ~ spl93_14 ),
inference(forward_subsumption_resolution,[],[f1251,f498]) ).
fof(f4639,plain,
( ~ spl93_29
| ~ spl93_19 ),
inference(avatar_split_clause,[],[f592,f423,f464]) ).
fof(f4655,plain,
( ~ spl93_29
| ~ spl93_14 ),
inference(avatar_split_clause,[],[f4635,f404,f464]) ).
fof(f4667,plain,
( ~ p202(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f3051,f473]) ).
fof(f4677,plain,
( ~ spl93_7
| ~ spl93_2 ),
inference(avatar_split_clause,[],[f4667,f361,f378]) ).
fof(f4707,plain,
( p102(sK66(sK92))
| ~ p602(sK92)
| ~ sP14(sK92)
| ~ spl93_2 ),
inference(resolution,[],[f362,f299]) ).
fof(f4709,plain,
( p102(sK68(sK92))
| ~ p402(sK92)
| ~ sP12(sK92)
| ~ spl93_2 ),
inference(resolution,[],[f362,f303]) ).
fof(f4751,plain,
( ~ p402(sK92)
| ~ sP12(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f4709,f302]) ).
fof(f4753,plain,
( ~ p602(sK92)
| ~ sP14(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f4707,f298]) ).
fof(f4780,plain,
( ~ p205(sK81(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3177,f499]) ).
fof(f4783,plain,
( ~ spl93_187
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f4780,f370,f1690]) ).
fof(f4786,plain,
( ~ p503(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4391,f485]) ).
fof(f4797,plain,
( ~ spl93_23
| ~ spl93_8 ),
inference(avatar_split_clause,[],[f4786,f382,f439]) ).
fof(f4801,plain,
( ~ spl93_23
| ~ spl93_13 ),
inference(avatar_split_clause,[],[f578,f400,f439]) ).
fof(f4802,plain,
( ~ p303(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4389,f483]) ).
fof(f4803,plain,
( ~ spl93_13
| ~ spl93_8 ),
inference(avatar_split_clause,[],[f4802,f382,f400]) ).
fof(f4805,plain,
( ~ p504(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2306,f490]) ).
fof(f4812,plain,
( ~ spl93_24
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f4805,f367,f443]) ).
fof(f4818,plain,
( ~ p602(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f4753,f477]) ).
fof(f4819,plain,
( ~ p402(sK92)
| ~ spl93_2 ),
inference(forward_subsumption_resolution,[],[f4751,f475]) ).
fof(f4820,plain,
( ~ spl93_23
| ~ spl93_18 ),
inference(avatar_split_clause,[],[f580,f419,f439]) ).
fof(f4821,plain,
( ~ spl93_27
| ~ spl93_2 ),
inference(avatar_split_clause,[],[f4818,f361,f456]) ).
fof(f4822,plain,
( ~ spl93_17
| ~ spl93_2 ),
inference(avatar_split_clause,[],[f4819,f361,f415]) ).
fof(f4832,plain,
( ~ spl93_28
| ~ spl93_13 ),
inference(avatar_split_clause,[],[f579,f400,f460]) ).
fof(f4833,plain,
( ~ spl93_6
| ~ spl93_1 ),
inference(avatar_split_clause,[],[f513,f357,f374]) ).
fof(f4834,plain,
( ~ spl93_11
| ~ spl93_6 ),
inference(avatar_split_clause,[],[f520,f374,f392]) ).
fof(f4835,plain,
( ~ p605(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3192,f503]) ).
fof(f4840,plain,
( ~ spl93_30
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f4835,f370,f468]) ).
fof(f4949,plain,
( p405(sK77(sK92))
| ~ spl93_20
| ~ spl93_247 ),
inference(resolution,[],[f428,f2106]) ).
fof(f5037,plain,
( ~ p405(sK77(sK92))
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3181,f501]) ).
fof(f5040,plain,
( spl93_162
| ~ spl93_20
| ~ spl93_247 ),
inference(avatar_split_clause,[],[f4949,f2104,f427,f1536]) ).
fof(f5041,plain,
( ~ spl93_162
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f5037,f370,f1536]) ).
fof(f5043,plain,
( ~ p304(sK85(sK92))
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2296,f488]) ).
fof(f5044,plain,
( ~ p604(sK92)
| ~ spl93_4 ),
inference(forward_subsumption_resolution,[],[f2307,f491]) ).
fof(f5064,plain,
( ~ spl93_212
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f5043,f367,f1844]) ).
fof(f5065,plain,
( ~ spl93_29
| ~ spl93_4 ),
inference(avatar_split_clause,[],[f5044,f367,f464]) ).
fof(f5089,plain,
( ~ p505(sK92)
| ~ spl93_5 ),
inference(forward_subsumption_resolution,[],[f3191,f502]) ).
fof(f5093,plain,
( ~ spl93_25
| ~ spl93_5 ),
inference(avatar_split_clause,[],[f5089,f370,f447]) ).
fof(f5100,plain,
( ~ p603(sK92)
| ~ spl93_8 ),
inference(forward_subsumption_resolution,[],[f4392,f486]) ).
fof(f5101,plain,
( ~ spl93_28
| ~ spl93_8 ),
inference(avatar_split_clause,[],[f5100,f382,f460]) ).
fof(f5102,plain,
( ~ p305(sK75(sK92))
| ~ spl93_10 ),
inference(forward_subsumption_resolution,[],[f2420,f504]) ).
fof(f5106,plain,
( spl93_149
| ~ spl93_15
| ~ spl93_246 ),
inference(avatar_split_clause,[],[f3464,f2087,f407,f1457]) ).
fof(f5116,plain,
( ~ spl93_149
| ~ spl93_10 ),
inference(avatar_split_clause,[],[f5102,f388,f1457]) ).
cnf(s1,plain,
( spl93_1
| spl93_2
| spl93_3
| spl93_4
| spl93_5 ),
inference(sat_conversion,[],[f372]) ).
cnf(s2,plain,
( spl93_6
| spl93_7
| spl93_8
| spl93_9
| spl93_10 ),
inference(sat_conversion,[],[f390]) ).
cnf(s3,plain,
( spl93_11
| spl93_12
| spl93_13
| spl93_14
| spl93_15 ),
inference(sat_conversion,[],[f409]) ).
cnf(s4,plain,
( spl93_16
| spl93_17
| spl93_18
| spl93_19
| spl93_20 ),
inference(sat_conversion,[],[f429]) ).
cnf(s5,plain,
( spl93_21
| spl93_22
| spl93_23
| spl93_24
| spl93_25 ),
inference(sat_conversion,[],[f450]) ).
cnf(s6,plain,
( spl93_26
| spl93_27
| spl93_28
| spl93_29
| spl93_30 ),
inference(sat_conversion,[],[f471]) ).
cnf(s8,plain,
( ~ spl93_6
| ~ spl93_11 ),
inference(sat_conversion,[],[f523]) ).
cnf(s10,plain,
( ~ spl93_11
| ~ spl93_16 ),
inference(sat_conversion,[],[f532]) ).
cnf(s11,plain,
( ~ spl93_11
| ~ spl93_16 ),
inference(sat_conversion,[],[f534]) ).
cnf(s14,plain,
( ~ spl93_21
| ~ spl93_26 ),
inference(sat_conversion,[],[f547]) ).
cnf(s16,plain,
( ~ spl93_7
| ~ spl93_12 ),
inference(sat_conversion,[],[f553]) ).
cnf(s17,plain,
( ~ spl93_7
| ~ spl93_12 ),
inference(sat_conversion,[],[f555]) ).
cnf(s19,plain,
( ~ spl93_12
| ~ spl93_17 ),
inference(sat_conversion,[],[f563]) ).
cnf(s20,plain,
( ~ spl93_12
| ~ spl93_22 ),
inference(sat_conversion,[],[f567]) ).
cnf(s22,plain,
( ~ spl93_12
| ~ spl93_27 ),
inference(sat_conversion,[],[f571]) ).
cnf(s26,plain,
( ~ spl93_18
| ~ spl93_28 ),
inference(sat_conversion,[],[f587]) ).
cnf(s27,plain,
( ~ spl93_19
| ~ spl93_24 ),
inference(sat_conversion,[],[f591]) ).
cnf(s28,plain,
( ~ spl93_24
| ~ spl93_29 ),
inference(sat_conversion,[],[f595]) ).
cnf(s29,plain,
( ~ spl93_25
| ~ spl93_30 ),
inference(sat_conversion,[],[f597]) ).
cnf(s44,plain,
( ~ spl93_8
| ~ spl93_18 ),
inference(sat_conversion,[],[f827]) ).
cnf(s46,plain,
( ~ spl93_8
| ~ spl93_18 ),
inference(sat_conversion,[],[f835]) ).
cnf(s55,plain,
( ~ spl93_2
| ~ spl93_12 ),
inference(sat_conversion,[],[f998]) ).
cnf(s57,plain,
( ~ spl93_1
| ~ spl93_26 ),
inference(sat_conversion,[],[f1007]) ).
cnf(s58,plain,
( ~ spl93_24
| ~ spl93_29 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s78,plain,
( ~ spl93_20
| ~ spl93_25 ),
inference(sat_conversion,[],[f1119]) ).
cnf(s80,plain,
( ~ spl93_1
| ~ spl93_21 ),
inference(sat_conversion,[],[f1127]) ).
cnf(s81,plain,
( ~ spl93_21
| ~ spl93_26 ),
inference(sat_conversion,[],[f1128]) ).
cnf(s88,plain,
( ~ spl93_20
| ~ spl93_30 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s91,plain,
( ~ spl93_12
| ~ spl93_22 ),
inference(sat_conversion,[],[f1162]) ).
cnf(s92,plain,
( ~ spl93_11
| ~ spl93_21 ),
inference(sat_conversion,[],[f1165]) ).
cnf(s93,plain,
( ~ spl93_11
| ~ spl93_26 ),
inference(sat_conversion,[],[f1166]) ).
cnf(s94,plain,
( ~ spl93_1
| ~ spl93_11 ),
inference(sat_conversion,[],[f1167]) ).
cnf(s186,plain,
( ~ spl93_3
| ~ spl93_237 ),
inference(sat_conversion,[],[f2013]) ).
cnf(s230,plain,
( ~ spl93_3
| spl93_253 ),
inference(sat_conversion,[],[f2213]) ).
cnf(s235,plain,
( ~ spl93_7
| ~ spl93_22 ),
inference(sat_conversion,[],[f2225]) ).
cnf(s237,plain,
( ~ spl93_6
| ~ spl93_26 ),
inference(sat_conversion,[],[f2232]) ).
cnf(s246,plain,
( ~ spl93_4
| spl93_252 ),
inference(sat_conversion,[],[f2351]) ).
cnf(s247,plain,
( ~ spl93_4
| spl93_251 ),
inference(sat_conversion,[],[f2352]) ).
cnf(s256,plain,
( ~ spl93_10
| spl93_246 ),
inference(sat_conversion,[],[f2471]) ).
cnf(s257,plain,
( ~ spl93_10
| spl93_245 ),
inference(sat_conversion,[],[f2472]) ).
cnf(s267,plain,
( ~ spl93_15
| spl93_244 ),
inference(sat_conversion,[],[f2594]) ).
cnf(s285,plain,
( ~ spl93_3
| ~ spl93_13 ),
inference(sat_conversion,[],[f2720]) ).
cnf(s310,plain,
( ~ spl93_9
| spl93_250 ),
inference(sat_conversion,[],[f2938]) ).
cnf(s317,plain,
( ~ spl93_4
| ~ spl93_19 ),
inference(sat_conversion,[],[f2975]) ).
cnf(s318,plain,
( ~ spl93_9
| ~ spl93_19 ),
inference(sat_conversion,[],[f2976]) ).
cnf(s338,plain,
( ~ spl93_17
| ~ spl93_22 ),
inference(sat_conversion,[],[f3111]) ).
cnf(s344,plain,
( ~ spl93_5
| spl93_249 ),
inference(sat_conversion,[],[f3228]) ).
cnf(s345,plain,
( ~ spl93_5
| spl93_248 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s346,plain,
( ~ spl93_5
| spl93_247 ),
inference(sat_conversion,[],[f3230]) ).
cnf(s362,plain,
( ~ spl93_13
| ~ spl93_18 ),
inference(sat_conversion,[],[f3335]) ).
cnf(s382,plain,
( ~ spl93_15
| spl93_174
| ~ spl93_248 ),
inference(sat_conversion,[],[f3554]) ).
cnf(s385,plain,
( ~ spl93_5
| ~ spl93_174 ),
inference(sat_conversion,[],[f3557]) ).
cnf(s401,plain,
( ~ spl93_9
| spl93_224
| ~ spl93_252 ),
inference(sat_conversion,[],[f3671]) ).
cnf(s404,plain,
( ~ spl93_4
| ~ spl93_224 ),
inference(sat_conversion,[],[f3674]) ).
cnf(s414,plain,
( ~ spl93_2
| ~ spl93_22 ),
inference(sat_conversion,[],[f3693]) ).
cnf(s415,plain,
( ~ spl93_9
| ~ spl93_24 ),
inference(sat_conversion,[],[f3694]) ).
cnf(s424,plain,
( ~ spl93_15
| ~ spl93_25 ),
inference(sat_conversion,[],[f3739]) ).
cnf(s435,plain,
( ~ spl93_9
| ~ spl93_29 ),
inference(sat_conversion,[],[f3784]) ).
cnf(s442,plain,
( ~ spl93_15
| ~ spl93_30 ),
inference(sat_conversion,[],[f3819]) ).
cnf(s451,plain,
( ~ spl93_22
| ~ spl93_27 ),
inference(sat_conversion,[],[f3855]) ).
cnf(s454,plain,
( ~ spl93_18
| ~ spl93_28 ),
inference(sat_conversion,[],[f3868]) ).
cnf(s455,plain,
( ~ spl93_16
| ~ spl93_26 ),
inference(sat_conversion,[],[f3877]) ).
cnf(s456,plain,
( ~ spl93_1
| ~ spl93_16 ),
inference(sat_conversion,[],[f3878]) ).
cnf(s468,plain,
( ~ spl93_3
| ~ spl93_18 ),
inference(sat_conversion,[],[f3921]) ).
cnf(s482,plain,
( ~ spl93_20
| spl93_137
| ~ spl93_245 ),
inference(sat_conversion,[],[f4016]) ).
cnf(s483,plain,
( ~ spl93_20
| spl93_123
| ~ spl93_244 ),
inference(sat_conversion,[],[f4017]) ).
cnf(s486,plain,
( ~ spl93_15
| ~ spl93_123 ),
inference(sat_conversion,[],[f4024]) ).
cnf(s498,plain,
( ~ spl93_23
| ~ spl93_28 ),
inference(sat_conversion,[],[f4028]) ).
cnf(s499,plain,
( ~ spl93_3
| ~ spl93_28 ),
inference(sat_conversion,[],[f4033]) ).
cnf(s527,plain,
( ~ spl93_3
| ~ spl93_23 ),
inference(sat_conversion,[],[f4179]) ).
cnf(s540,plain,
( ~ spl93_14
| spl93_200
| ~ spl93_250 ),
inference(sat_conversion,[],[f4283]) ).
cnf(s541,plain,
( ~ spl93_9
| ~ spl93_200 ),
inference(sat_conversion,[],[f4284]) ).
cnf(s547,plain,
( ~ spl93_7
| ~ spl93_27 ),
inference(sat_conversion,[],[f4294]) ).
cnf(s550,plain,
( ~ spl93_6
| ~ spl93_16 ),
inference(sat_conversion,[],[f4306]) ).
cnf(s576,plain,
( ~ spl93_14
| spl93_212
| ~ spl93_251 ),
inference(sat_conversion,[],[f4429]) ).
cnf(s581,plain,
( ~ spl93_8
| spl93_237
| ~ spl93_253 ),
inference(sat_conversion,[],[f4439]) ).
cnf(s583,plain,
( ~ spl93_10
| spl93_187
| ~ spl93_249 ),
inference(sat_conversion,[],[f4443]) ).
cnf(s586,plain,
( ~ spl93_10
| ~ spl93_25 ),
inference(sat_conversion,[],[f4446]) ).
cnf(s590,plain,
( ~ spl93_10
| ~ spl93_137 ),
inference(sat_conversion,[],[f4468]) ).
cnf(s596,plain,
( ~ spl93_10
| ~ spl93_25 ),
inference(sat_conversion,[],[f4489]) ).
cnf(s601,plain,
( ~ spl93_14
| ~ spl93_24 ),
inference(sat_conversion,[],[f4505]) ).
cnf(s606,plain,
( ~ spl93_16
| ~ spl93_21 ),
inference(sat_conversion,[],[f4516]) ).
cnf(s610,plain,
( ~ spl93_19
| ~ spl93_24 ),
inference(sat_conversion,[],[f4531]) ).
cnf(s616,plain,
( ~ spl93_14
| ~ spl93_19 ),
inference(sat_conversion,[],[f4563]) ).
cnf(s617,plain,
( ~ spl93_17
| ~ spl93_27 ),
inference(sat_conversion,[],[f4576]) ).
cnf(s626,plain,
( ~ spl93_10
| ~ spl93_30 ),
inference(sat_conversion,[],[f4617]) ).
cnf(s630,plain,
( ~ spl93_7
| ~ spl93_17 ),
inference(sat_conversion,[],[f4628]) ).
cnf(s631,plain,
( ~ spl93_7
| ~ spl93_27 ),
inference(sat_conversion,[],[f4629]) ).
cnf(s632,plain,
( ~ spl93_6
| ~ spl93_21 ),
inference(sat_conversion,[],[f4630]) ).
cnf(s633,plain,
( ~ spl93_6
| ~ spl93_16 ),
inference(sat_conversion,[],[f4631]) ).
cnf(s643,plain,
( ~ spl93_19
| ~ spl93_29 ),
inference(sat_conversion,[],[f4639]) ).
cnf(s647,plain,
( ~ spl93_14
| ~ spl93_29 ),
inference(sat_conversion,[],[f4655]) ).
cnf(s662,plain,
( ~ spl93_2
| ~ spl93_7 ),
inference(sat_conversion,[],[f4677]) ).
cnf(s675,plain,
( ~ spl93_5
| ~ spl93_187 ),
inference(sat_conversion,[],[f4783]) ).
cnf(s678,plain,
( ~ spl93_8
| ~ spl93_23 ),
inference(sat_conversion,[],[f4797]) ).
cnf(s682,plain,
( ~ spl93_13
| ~ spl93_23 ),
inference(sat_conversion,[],[f4801]) ).
cnf(s683,plain,
( ~ spl93_8
| ~ spl93_13 ),
inference(sat_conversion,[],[f4803]) ).
cnf(s688,plain,
( ~ spl93_4
| ~ spl93_24 ),
inference(sat_conversion,[],[f4812]) ).
cnf(s705,plain,
( ~ spl93_18
| ~ spl93_23 ),
inference(sat_conversion,[],[f4820]) ).
cnf(s706,plain,
( ~ spl93_2
| ~ spl93_27 ),
inference(sat_conversion,[],[f4821]) ).
cnf(s707,plain,
( ~ spl93_2
| ~ spl93_17 ),
inference(sat_conversion,[],[f4822]) ).
cnf(s721,plain,
( ~ spl93_13
| ~ spl93_28 ),
inference(sat_conversion,[],[f4832]) ).
cnf(s722,plain,
( ~ spl93_1
| ~ spl93_6 ),
inference(sat_conversion,[],[f4833]) ).
cnf(s723,plain,
( ~ spl93_6
| ~ spl93_11 ),
inference(sat_conversion,[],[f4834]) ).
cnf(s732,plain,
( ~ spl93_5
| ~ spl93_30 ),
inference(sat_conversion,[],[f4840]) ).
cnf(s758,plain,
( ~ spl93_20
| spl93_162
| ~ spl93_247 ),
inference(sat_conversion,[],[f5040]) ).
cnf(s759,plain,
( ~ spl93_5
| ~ spl93_162 ),
inference(sat_conversion,[],[f5041]) ).
cnf(s773,plain,
( ~ spl93_4
| ~ spl93_212 ),
inference(sat_conversion,[],[f5064]) ).
cnf(s774,plain,
( ~ spl93_4
| ~ spl93_29 ),
inference(sat_conversion,[],[f5065]) ).
cnf(s804,plain,
( ~ spl93_5
| ~ spl93_25 ),
inference(sat_conversion,[],[f5093]) ).
cnf(s819,plain,
( ~ spl93_8
| ~ spl93_28 ),
inference(sat_conversion,[],[f5101]) ).
cnf(s841,plain,
( ~ spl93_15
| spl93_149
| ~ spl93_246 ),
inference(sat_conversion,[],[f5106]) ).
cnf(s855,plain,
( ~ spl93_10
| ~ spl93_149 ),
inference(sat_conversion,[],[f5116]) ).
cnf(s857,plain,
( ~ spl93_17
| ~ spl93_13
| ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s14,s5,s6,s338,s617,s804,s732,s435,s415,s721,s682]) ).
cnf(s858,plain,
( ~ spl93_13
| ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s451,s6,s5,s455,s606,s4,s857,s362,s682,s721,s804,s732,s758,s759,s346,s435,s415,s318]) ).
cnf(s859,plain,
( ~ spl93_18
| ~ spl93_12
| ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s14,s6,s5,s454,s705,s804,s732,s435,s415,s91,s22]) ).
cnf(s860,plain,
( ~ spl93_12
| ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s498,s6,s5,s455,s606,s4,s859,s19,s22,s91,s804,s732,s758,s759,s346,s435,s415,s318]) ).
cnf(s861,plain,
( ~ spl93_17
| ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s498,s5,s6,s338,s617,s804,s732,s435,s415,s93,s92,s3,s860,s540,s310,s541,s858,s382,s385,s345]) ).
cnf(s862,plain,
( ~ spl93_9
| ~ spl93_5 ),
inference(rat,[],[s451,s6,s5,s454,s705,s4,s861,s11,s92,s93,s3,s860,s858,s540,s310,s318,s415,s435,s541,s804,s732,s758,s759,s346,s382,s385,s345]) ).
cnf(s863,plain,
( ~ spl93_21
| ~ spl93_17
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s647,s6,s3,s81,s92,s732,s382,s385,s345,s819,s683,s617,s19]) ).
cnf(s864,plain,
( ~ spl93_17
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s93,s6,s3,s58,s601,s5,s863,s19,s338,s617,s804,s732,s382,s385,s345,s819,s683,s678]) ).
cnf(s865,plain,
( ~ spl93_21
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s22,s3,s6,s616,s643,s4,s81,s92,s606,s732,s758,s759,s346,s382,s385,s345,s819,s683,s46,s864]) ).
cnf(s866,plain,
( ~ spl93_26
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s20,s5,s3,s610,s616,s4,s93,s455,s804,s758,s759,s346,s382,s385,s345,s683,s678,s46,s864,s865]) ).
cnf(s867,plain,
( ~ spl93_14
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s451,s5,s6,s601,s647,s804,s732,s819,s678,s865,s866]) ).
cnf(s868,plain,
( ~ spl93_12
| ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s28,s6,s5,s22,s91,s804,s732,s819,s678,s865,s866]) ).
cnf(s869,plain,
( ~ spl93_8
| ~ spl93_5 ),
inference(rat,[],[s451,s5,s6,s610,s643,s4,s11,s3,s868,s867,s866,s865,s864,s46,s678,s683,s819,s804,s732,s758,s759,s346,s382,s385,s345]) ).
cnf(s870,plain,
( ~ spl93_13
| ~ spl93_21
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s643,s4,s6,s362,s721,s732,s758,s759,s346,s631,s630,s606,s81]) ).
cnf(s871,plain,
( ~ spl93_21
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s26,s4,s6,s616,s647,s3,s870,s81,s92,s606,s732,s758,s759,s346,s382,s385,s345,s631,s630,s17]) ).
cnf(s872,plain,
( ~ spl93_13
| spl93_16
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s610,s4,s5,s362,s682,s804,s758,s759,s346,s630,s235,s871]) ).
cnf(s873,plain,
( ~ spl93_26
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s705,s5,s4,s601,s616,s3,s872,s93,s455,s804,s758,s759,s346,s382,s385,s345,s630,s235,s17,s871]) ).
cnf(s874,plain,
( ~ spl93_13
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s28,s5,s6,s682,s721,s804,s732,s631,s235,s871,s873]) ).
cnf(s875,plain,
( ~ spl93_29
| ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s4,s705,s11,s5,s3,s58,s643,s647,s804,s758,s759,s346,s382,s385,s345,s630,s235,s17,s871,s874]) ).
cnf(s876,plain,
( ~ spl93_7
| ~ spl93_5 ),
inference(rat,[],[s10,s3,s4,s601,s610,s5,s454,s498,s6,s875,s874,s873,s871,s17,s235,s630,s631,s804,s732,s758,s759,s346,s382,s385,s345]) ).
cnf(s877,plain,
( ~ spl93_17
| ~ spl93_13
| ~ spl93_5 ),
inference(rat,[],[s28,s5,s6,s338,s617,s804,s732,s632,s237,s2,s876,s869,s862,s583,s675,s344,s721,s682]) ).
cnf(s878,plain,
( ~ spl93_13
| ~ spl93_5 ),
inference(rat,[],[s451,s5,s6,s610,s643,s4,s877,s362,s682,s721,s804,s732,s758,s759,s346,s633,s632,s237,s2,s876,s869,s862,s583,s675,s344]) ).
cnf(s879,plain,
( ~ spl93_17
| ~ spl93_5 ),
inference(rat,[],[s498,s5,s6,s601,s647,s3,s19,s338,s617,s804,s732,s382,s385,s345,s723,s632,s237,s2,s876,s869,s862,s583,s675,s344,s878]) ).
cnf(s880,plain,
( ~ spl93_29
| ~ spl93_5 ),
inference(rat,[],[s5,s705,s91,s4,s3,s58,s643,s647,s804,s758,s759,s346,s382,s385,s345,s723,s633,s632,s2,s876,s869,s862,s583,s675,s344,s878,s879]) ).
cnf(s881,plain,
( ~ spl93_28
| ~ spl93_5 ),
inference(rat,[],[s20,s5,s3,s610,s616,s4,s454,s498,s804,s758,s759,s346,s382,s385,s345,s723,s633,s632,s2,s876,s869,s862,s583,s675,s344,s878,s879]) ).
cnf(s882,plain,
~ spl93_5,
inference(rat,[],[s705,s5,s4,s601,s616,s3,s22,s451,s6,s881,s880,s879,s878,s237,s632,s633,s723,s2,s876,s869,s862,s382,s583,s758,s344,s345,s346,s385,s675,s732,s759,s804]) ).
cnf(s883,plain,
( ~ spl93_17
| ~ spl93_13
| ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s626,s6,s2,s617,s630,s774,s401,s246,s404,s632,s81,s721,s683]) ).
cnf(s884,plain,
( ~ spl93_13
| ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s482,s257,s590,s2,s631,s6,s88,s4,s883,s362,s683,s721,s774,s317,s401,s246,s404,s632,s606,s81]) ).
cnf(s885,plain,
( ~ spl93_17
| ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s841,s256,s855,s2,s819,s6,s442,s3,s19,s617,s630,s774,s576,s247,s773,s401,s246,s404,s632,s92,s81,s884]) ).
cnf(s886,plain,
( ~ spl93_30
| ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s2,s46,s17,s4,s3,s88,s442,s626,s317,s576,s247,s773,s401,s246,s404,s632,s606,s92,s884,s885]) ).
cnf(s887,plain,
( ~ spl93_10
| ~ spl93_20 ),
inference(rat,[],[s482,s257,s590]) ).
cnf(s888,plain,
( ~ spl93_28
| ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s483,s267,s486,s3,s17,s2,s887,s4,s454,s819,s317,s576,s247,s773,s401,s246,s404,s632,s606,s92,s884,s885]) ).
cnf(s889,plain,
( ~ spl93_21
| ~ spl93_4 ),
inference(rat,[],[s841,s256,s855,s2,s46,s4,s483,s267,s486,s3,s22,s631,s6,s888,s886,s885,s884,s81,s92,s606,s632,s774,s317,s576,s247,s773,s401,s246,s404]) ).
cnf(s890,plain,
( ~ spl93_17
| ~ spl93_13
| spl93_6
| ~ spl93_4 ),
inference(rat,[],[s586,s5,s2,s338,s630,s688,s401,s246,s404,s889,s683,s682]) ).
cnf(s891,plain,
( ~ spl93_13
| ~ spl93_26
| ~ spl93_4 ),
inference(rat,[],[s235,s2,s5,s887,s78,s4,s890,s362,s682,s683,s688,s317,s401,s246,s404,s889,s455,s237]) ).
cnf(s892,plain,
( ~ spl93_17
| ~ spl93_26
| ~ spl93_4 ),
inference(rat,[],[s841,s256,s855,s2,s678,s5,s424,s3,s19,s338,s630,s688,s576,s247,s773,s401,s246,s404,s889,s237,s93,s891]) ).
cnf(s893,plain,
( ~ spl93_10
| ~ spl93_26
| ~ spl93_4 ),
inference(rat,[],[s5,s91,s705,s3,s4,s841,s887,s256,s596,s855,s688,s317,s576,s247,s773,s889,s455,s93,s891,s892]) ).
cnf(s894,plain,
( ~ spl93_8
| ~ spl93_26
| ~ spl93_4 ),
inference(rat,[],[s483,s267,s486,s3,s91,s5,s78,s4,s46,s678,s688,s317,s576,s247,s773,s889,s455,s93,s891,s892]) ).
cnf(s895,plain,
( ~ spl93_26
| ~ spl93_4 ),
inference(rat,[],[s4,s705,s483,s5,s267,s424,s486,s3,s17,s235,s2,s894,s893,s892,s891,s93,s237,s455,s688,s317,s576,s247,s773,s401,s246,s404,s889]) ).
cnf(s896,plain,
( ~ spl93_17
| ~ spl93_13
| ~ spl93_4 ),
inference(rat,[],[s29,s5,s6,s338,s617,s774,s688,s889,s895,s721,s682]) ).
cnf(s897,plain,
( ~ spl93_10
| ~ spl93_13
| ~ spl93_4 ),
inference(rat,[],[s451,s5,s6,s596,s626,s774,s688,s889,s895,s721,s682]) ).
cnf(s898,plain,
( ~ spl93_7
| ~ spl93_13
| ~ spl93_4 ),
inference(rat,[],[s29,s5,s6,s235,s631,s774,s688,s889,s895,s721,s682]) ).
cnf(s899,plain,
( ~ spl93_13
| ~ spl93_4 ),
inference(rat,[],[s451,s5,s6,s78,s88,s4,s633,s2,s898,s897,s896,s362,s682,s683,s721,s774,s688,s317,s401,s246,s404,s889,s895]) ).
cnf(s900,plain,
( ~ spl93_10
| ~ spl93_17
| ~ spl93_4 ),
inference(rat,[],[s498,s5,s6,s596,s626,s774,s688,s889,s895,s617,s338]) ).
cnf(s901,plain,
( ~ spl93_17
| spl93_6
| ~ spl93_4 ),
inference(rat,[],[s29,s5,s6,s678,s819,s2,s900,s338,s617,s630,s774,s688,s401,s246,s404,s889,s895]) ).
cnf(s902,plain,
( ~ spl93_23
| ~ spl93_10
| spl93_17
| ~ spl93_4 ),
inference(rat,[],[s3,s22,s11,s6,s4,s498,s705,s774,s317,s576,s247,s773,s895,s899,s626,s887,s841,s256,s855]) ).
cnf(s903,plain,
( ~ spl93_10
| spl93_17
| ~ spl93_4 ),
inference(rat,[],[s4,s11,s454,s3,s6,s91,s451,s5,s902,s841,s887,s256,s596,s626,s855,s774,s688,s317,s576,s247,s773,s889,s895,s899]) ).
cnf(s904,plain,
( ~ spl93_25
| ~ spl93_8
| spl93_17
| ~ spl93_4 ),
inference(rat,[],[s3,s22,s11,s6,s4,s29,s78,s424,s774,s317,s576,s247,s773,s895,s899,s819,s46]) ).
cnf(s905,plain,
( ~ spl93_8
| spl93_17
| ~ spl93_4 ),
inference(rat,[],[s10,s4,s3,s88,s442,s6,s91,s451,s5,s904,s46,s678,s819,s774,s688,s317,s576,s247,s773,s889,s895,s899]) ).
cnf(s906,plain,
( ~ spl93_25
| spl93_6
| ~ spl93_4 ),
inference(rat,[],[s4,s454,s11,s6,s3,s29,s78,s424,s774,s317,s576,s247,s773,s895,s899,s631,s17,s2,s905,s401,s246,s404,s903,s901]) ).
cnf(s907,plain,
( spl93_6
| ~ spl93_4 ),
inference(rat,[],[s10,s4,s3,s88,s442,s6,s498,s705,s5,s906,s17,s235,s631,s2,s905,s903,s901,s774,s688,s317,s576,s247,s773,s401,s246,s404,s889,s895,s899]) ).
cnf(s908,plain,
( ~ spl93_17
| ~ spl93_4 ),
inference(rat,[],[s498,s5,s6,s424,s442,s3,s19,s338,s617,s774,s688,s576,s247,s773,s889,s895,s899,s723,s907]) ).
cnf(s909,plain,
( ~ spl93_25
| ~ spl93_4 ),
inference(rat,[],[s6,s454,s22,s4,s3,s29,s78,s424,s774,s317,s576,s247,s773,s895,s899,s723,s633,s907,s908]) ).
cnf(s910,plain,
( ~ spl93_23
| ~ spl93_4 ),
inference(rat,[],[s483,s267,s486,s3,s22,s6,s88,s4,s498,s705,s774,s317,s576,s247,s773,s895,s899,s723,s633,s907,s908]) ).
cnf(s911,plain,
~ spl93_4,
inference(rat,[],[s4,s454,s483,s6,s267,s442,s486,s3,s91,s451,s5,s910,s909,s908,s633,s723,s907,s899,s895,s889,s576,s247,s317,s688,s773,s774]) ).
cnf(s912,plain,
( ~ spl93_30
| ~ spl93_17
| ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s540,s310,s541,s3,s2,s442,s626,s285,s581,s186,s230,s632,s92,s630,s19]) ).
cnf(s913,plain,
( ~ spl93_17
| ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s841,s256,s855,s2,s3,s435,s647,s6,s912,s19,s617,s630,s499,s285,s581,s186,s230,s632,s92,s81]) ).
cnf(s914,plain,
( ~ spl93_30
| ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s16,s2,s3,s318,s616,s4,s88,s442,s626,s468,s285,s581,s186,s230,s632,s606,s92,s913]) ).
cnf(s915,plain,
( ~ spl93_29
| ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s483,s267,s486,s3,s17,s2,s887,s4,s435,s643,s647,s468,s285,s581,s186,s230,s632,s606,s92,s913]) ).
cnf(s916,plain,
( ~ spl93_9
| ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s483,s267,s486,s3,s540,s4,s310,s318,s541,s468,s285,s606,s92,s913,s22,s6,s915,s914,s81,s499]) ).
cnf(s917,plain,
( ~ spl93_21
| ~ spl93_3 ),
inference(rat,[],[s616,s3,s4,s841,s887,s256,s855,s2,s916,s22,s631,s6,s915,s914,s913,s81,s92,s606,s632,s499,s468,s285,s581,s186,s230]) ).
cnf(s918,plain,
( ~ spl93_9
| spl93_11
| ~ spl93_17
| ~ spl93_3 ),
inference(rat,[],[s3,s424,s540,s5,s310,s415,s541,s527,s285,s917,s338,s19]) ).
cnf(s919,plain,
( ~ spl93_26
| ~ spl93_17
| ~ spl93_3 ),
inference(rat,[],[s3,s601,s841,s5,s256,s596,s855,s2,s918,s93,s237,s527,s285,s581,s186,s230,s917,s630,s338,s19]) ).
cnf(s920,plain,
( ~ spl93_9
| ~ spl93_17
| ~ spl93_3 ),
inference(rat,[],[s29,s5,s6,s415,s435,s527,s499,s917,s617,s338,s919]) ).
cnf(s921,plain,
( ~ spl93_30
| ~ spl93_17
| ~ spl93_3 ),
inference(rat,[],[s3,s601,s723,s5,s2,s29,s442,s626,s527,s285,s581,s186,s230,s917,s630,s338,s19,s920]) ).
cnf(s922,plain,
( ~ spl93_17
| ~ spl93_3 ),
inference(rat,[],[s8,s3,s2,s424,s596,s5,s58,s647,s6,s921,s920,s919,s19,s338,s617,s630,s527,s499,s285,s581,s186,s230,s917]) ).
cnf(s923,plain,
( ~ spl93_9
| ~ spl93_26
| ~ spl93_3 ),
inference(rat,[],[s483,s267,s486,s3,s91,s5,s78,s540,s4,s310,s318,s415,s541,s527,s468,s285,s917,s922,s455,s93]) ).
cnf(s924,plain,
( ~ spl93_15
| ~ spl93_26
| ~ spl93_3 ),
inference(rat,[],[s841,s256,s855,s2,s235,s5,s610,s4,s483,s267,s424,s486,s527,s468,s581,s186,s230,s917,s922,s455,s237,s923]) ).
cnf(s925,plain,
( ~ spl93_14
| ~ spl93_26
| ~ spl93_3 ),
inference(rat,[],[s235,s2,s5,s887,s78,s4,s601,s616,s527,s468,s581,s186,s230,s917,s922,s455,s237,s923]) ).
cnf(s926,plain,
( ~ spl93_26
| ~ spl93_3 ),
inference(rat,[],[s610,s4,s5,s887,s596,s2,s17,s91,s3,s925,s924,s923,s93,s237,s455,s527,s468,s285,s581,s186,s230,s917,s922]) ).
cnf(s927,plain,
( ~ spl93_15
| ~ spl93_9
| ~ spl93_3 ),
inference(rat,[],[s451,s5,s6,s424,s442,s527,s499,s917,s926,s435,s415]) ).
cnf(s928,plain,
( ~ spl93_12
| ~ spl93_9
| ~ spl93_3 ),
inference(rat,[],[s29,s6,s5,s22,s91,s527,s499,s917,s926,s435,s415]) ).
cnf(s929,plain,
( ~ spl93_9
| ~ spl93_3 ),
inference(rat,[],[s451,s5,s6,s78,s88,s4,s11,s3,s928,s927,s540,s310,s318,s415,s435,s541,s527,s499,s468,s285,s917,s922,s926]) ).
cnf(s930,plain,
( ~ spl93_10
| ~ spl93_15 ),
inference(rat,[],[s841,s256,s855]) ).
cnf(s931,plain,
( ~ spl93_24
| ~ spl93_15
| ~ spl93_3 ),
inference(rat,[],[s2,s631,s633,s6,s4,s58,s610,s499,s468,s581,s186,s230,s922,s926,s929,s442,s483,s267,s486,s930]) ).
cnf(s932,plain,
( ~ spl93_15
| ~ spl93_3 ),
inference(rat,[],[s4,s633,s643,s2,s6,s235,s451,s5,s931,s930,s483,s267,s424,s442,s486,s527,s499,s468,s581,s186,s230,s917,s922,s926,s929]) ).
cnf(s933,plain,
( ~ spl93_25
| ~ spl93_14
| ~ spl93_3 ),
inference(rat,[],[s2,s631,s633,s6,s4,s29,s78,s596,s499,s468,s581,s186,s230,s922,s926,s929,s647,s616]) ).
cnf(s934,plain,
( ~ spl93_14
| ~ spl93_3 ),
inference(rat,[],[s550,s4,s2,s88,s626,s6,s235,s451,s5,s933,s601,s616,s647,s527,s499,s468,s581,s186,s230,s917,s922,s926,s929]) ).
cnf(s935,plain,
( ~ spl93_25
| ~ spl93_12
| ~ spl93_3 ),
inference(rat,[],[s4,s643,s633,s6,s2,s29,s78,s596,s499,s468,s581,s186,s230,s922,s926,s929,s22,s17]) ).
cnf(s936,plain,
( ~ spl93_12
| ~ spl93_3 ),
inference(rat,[],[s550,s4,s2,s88,s626,s6,s58,s610,s5,s935,s17,s22,s91,s527,s499,s468,s581,s186,s230,s917,s922,s926,s929]) ).
cnf(s937,plain,
( ~ spl93_25
| ~ spl93_3 ),
inference(rat,[],[s6,s643,s631,s4,s2,s29,s78,s596,s499,s468,s581,s186,s230,s922,s926,s929,s723,s11,s3,s936,s932,s934,s285]) ).
cnf(s938,plain,
( ~ spl93_24
| ~ spl93_3 ),
inference(rat,[],[s631,s2,s6,s887,s88,s4,s58,s610,s499,s468,s581,s186,s230,s922,s926,s929,s723,s11,s3,s936,s932,s934,s285]) ).
cnf(s939,plain,
~ spl93_3,
inference(rat,[],[s643,s4,s6,s887,s626,s2,s235,s451,s5,s938,s937,s11,s723,s3,s936,s934,s932,s929,s926,s922,s917,s581,s186,s230,s285,s468,s499,s527]) ).
cnf(s940,plain,
( ~ spl93_13
| ~ spl93_9
| ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s88,s4,s6,s362,s721,s707,s706,s606,s81,s435,s318]) ).
cnf(s941,plain,
( ~ spl93_9
| ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s4,s454,s483,s6,s267,s442,s486,s3,s940,s540,s310,s318,s435,s541,s707,s706,s55,s606,s92,s81]) ).
cnf(s942,plain,
( ~ spl93_13
| ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s643,s4,s6,s887,s626,s2,s362,s683,s721,s707,s706,s662,s632,s606,s81,s941]) ).
cnf(s943,plain,
( ~ spl93_30
| ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s4,s616,s46,s3,s2,s88,s442,s626,s707,s662,s55,s632,s606,s92,s941,s942]) ).
cnf(s944,plain,
( ~ spl93_29
| ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s44,s4,s2,s483,s930,s267,s486,s3,s643,s647,s707,s662,s55,s632,s606,s92,s941,s942]) ).
cnf(s945,plain,
( ~ spl93_21
| ~ spl93_2 ),
inference(rat,[],[s616,s3,s4,s930,s887,s2,s454,s819,s6,s944,s943,s942,s941,s81,s92,s606,s632,s707,s706,s662,s55]) ).
cnf(s946,plain,
( ~ spl93_13
| ~ spl93_9
| spl93_16
| ~ spl93_2 ),
inference(rat,[],[s78,s4,s5,s362,s682,s707,s414,s945,s415,s318]) ).
cnf(s947,plain,
( ~ spl93_9
| ~ spl93_26
| ~ spl93_2 ),
inference(rat,[],[s4,s705,s483,s5,s267,s424,s486,s3,s946,s540,s310,s318,s415,s541,s707,s414,s55,s945,s455,s93]) ).
cnf(s948,plain,
( ~ spl93_13
| ~ spl93_26
| ~ spl93_2 ),
inference(rat,[],[s27,s4,s5,s887,s596,s2,s362,s682,s683,s707,s662,s414,s945,s455,s237,s947]) ).
cnf(s949,plain,
( ~ spl93_20
| ~ spl93_26
| ~ spl93_2 ),
inference(rat,[],[s483,s267,s486,s3,s601,s5,s678,s2,s887,s78,s662,s414,s55,s945,s237,s93,s947,s948]) ).
cnf(s950,plain,
( ~ spl93_19
| ~ spl93_26
| ~ spl93_2 ),
inference(rat,[],[s678,s2,s5,s930,s424,s3,s610,s616,s662,s414,s55,s945,s237,s93,s947,s948]) ).
cnf(s951,plain,
( ~ spl93_26
| ~ spl93_2 ),
inference(rat,[],[s601,s3,s5,s930,s596,s2,s46,s705,s4,s950,s949,s948,s947,s93,s237,s455,s707,s662,s414,s55,s945]) ).
cnf(s952,plain,
( ~ spl93_13
| ~ spl93_9
| ~ spl93_2 ),
inference(rat,[],[s29,s5,s6,s682,s721,s706,s414,s945,s951,s435,s415]) ).
cnf(s953,plain,
( ~ spl93_20
| ~ spl93_9
| ~ spl93_2 ),
inference(rat,[],[s498,s5,s6,s78,s88,s706,s414,s945,s951,s435,s415]) ).
cnf(s954,plain,
( ~ spl93_18
| ~ spl93_9
| ~ spl93_2 ),
inference(rat,[],[s29,s6,s5,s454,s705,s706,s414,s945,s951,s435,s415]) ).
cnf(s955,plain,
( ~ spl93_9
| ~ spl93_2 ),
inference(rat,[],[s498,s5,s6,s424,s442,s3,s11,s4,s954,s953,s952,s540,s310,s318,s415,s435,s541,s707,s706,s414,s55,s945,s951]) ).
cnf(s956,plain,
( ~ spl93_20
| ~ spl93_13
| ~ spl93_2 ),
inference(rat,[],[s28,s5,s6,s78,s88,s706,s414,s945,s951,s721,s682]) ).
cnf(s957,plain,
( ~ spl93_19
| ~ spl93_13
| ~ spl93_2 ),
inference(rat,[],[s29,s5,s6,s610,s643,s706,s414,s945,s951,s721,s682]) ).
cnf(s958,plain,
( ~ spl93_13
| ~ spl93_2 ),
inference(rat,[],[s28,s5,s6,s596,s626,s2,s633,s4,s957,s956,s362,s682,s683,s721,s707,s706,s662,s414,s945,s951,s955]) ).
cnf(s959,plain,
( ~ spl93_15
| ~ spl93_20 ),
inference(rat,[],[s483,s267,s486]) ).
cnf(s960,plain,
( ~ spl93_23
| ~ spl93_20
| ~ spl93_2 ),
inference(rat,[],[s3,s647,s723,s6,s2,s498,s678,s706,s662,s55,s951,s955,s958,s88,s887,s959]) ).
cnf(s961,plain,
( ~ spl93_20
| ~ spl93_2 ),
inference(rat,[],[s2,s819,s723,s6,s3,s58,s601,s5,s960,s959,s887,s78,s88,s706,s662,s414,s55,s945,s951,s955,s958]) ).
cnf(s962,plain,
( ~ spl93_25
| ~ spl93_19
| ~ spl93_2 ),
inference(rat,[],[s2,s819,s723,s6,s3,s29,s424,s596,s706,s662,s55,s951,s955,s958,s643,s616]) ).
cnf(s963,plain,
( ~ spl93_19
| ~ spl93_2 ),
inference(rat,[],[s8,s3,s2,s442,s626,s6,s498,s678,s5,s962,s610,s616,s643,s706,s662,s414,s55,s945,s951,s955,s958]) ).
cnf(s964,plain,
( ~ spl93_25
| ~ spl93_18
| ~ spl93_2 ),
inference(rat,[],[s3,s647,s723,s6,s2,s29,s424,s596,s706,s662,s55,s951,s955,s958,s454,s46]) ).
cnf(s965,plain,
( ~ spl93_18
| ~ spl93_2 ),
inference(rat,[],[s8,s3,s2,s442,s626,s6,s58,s601,s5,s964,s46,s454,s705,s706,s662,s414,s55,s945,s951,s955,s958]) ).
cnf(s966,plain,
( ~ spl93_25
| ~ spl93_2 ),
inference(rat,[],[s6,s647,s819,s3,s2,s29,s424,s596,s706,s662,s55,s951,s955,s958,s633,s11,s4,s965,s961,s707,s963]) ).
cnf(s967,plain,
( ~ spl93_23
| ~ spl93_2 ),
inference(rat,[],[s647,s3,s6,s930,s626,s2,s498,s678,s706,s662,s55,s951,s955,s958,s633,s11,s4,s965,s961,s707,s963]) ).
cnf(s968,plain,
~ spl93_2,
inference(rat,[],[s819,s2,s6,s930,s442,s3,s58,s601,s5,s967,s966,s11,s633,s4,s965,s963,s961,s958,s955,s951,s945,s55,s414,s662,s706,s707]) ).
cnf(s969,plain,
spl93_1,
inference(rat,[],[s1,s939,s882,s911,s968]) ).
cnf(s970,plain,
~ spl93_6,
inference(rat,[],[s722,s969]) ).
cnf(s971,plain,
~ spl93_16,
inference(rat,[],[s456,s969]) ).
cnf(s972,plain,
~ spl93_11,
inference(rat,[],[s94,s969]) ).
cnf(s973,plain,
~ spl93_21,
inference(rat,[],[s80,s969]) ).
cnf(s974,plain,
~ spl93_26,
inference(rat,[],[s57,s969]) ).
cnf(s975,plain,
( ~ spl93_17
| ~ spl93_9
| ~ spl93_13 ),
inference(rat,[],[s29,s5,s6,s338,s617,s721,s682,s435,s415,s973,s974]) ).
cnf(s976,plain,
( ~ spl93_9
| ~ spl93_13 ),
inference(rat,[],[s451,s5,s6,s78,s88,s4,s975,s318,s415,s435,s721,s682,s362,s973,s974,s971]) ).
cnf(s977,plain,
( ~ spl93_17
| spl93_24
| ~ spl93_13 ),
inference(rat,[],[s586,s5,s2,s338,s630,s683,s682,s976,s973,s970]) ).
cnf(s978,plain,
( ~ spl93_25
| spl93_17
| ~ spl93_13 ),
inference(rat,[],[s6,s643,s631,s4,s2,s29,s78,s596,s721,s683,s362,s976,s974,s971,s970]) ).
cnf(s979,plain,
( spl93_24
| ~ spl93_13 ),
inference(rat,[],[s643,s4,s6,s887,s626,s2,s235,s451,s5,s978,s977,s721,s683,s682,s362,s976,s971,s974,s970,s973]) ).
cnf(s980,plain,
( ~ spl93_17
| ~ spl93_13 ),
inference(rat,[],[s626,s6,s2,s617,s630,s721,s683,s976,s58,s979,s974,s970]) ).
cnf(s981,plain,
~ spl93_13,
inference(rat,[],[s547,s2,s6,s887,s88,s4,s980,s58,s610,s979,s976,s362,s683,s721,s970,s974,s971]) ).
cnf(s982,plain,
( ~ spl93_17
| ~ spl93_9 ),
inference(rat,[],[s498,s5,s6,s424,s442,s3,s19,s338,s617,s435,s415,s540,s310,s541,s973,s974,s972,s981]) ).
cnf(s983,plain,
( ~ spl93_25
| ~ spl93_9 ),
inference(rat,[],[s6,s454,s22,s4,s3,s29,s78,s424,s435,s318,s540,s310,s541,s982,s974,s971,s972,s981]) ).
cnf(s984,plain,
( ~ spl93_23
| ~ spl93_9 ),
inference(rat,[],[s22,s3,s6,s959,s88,s4,s498,s705,s435,s318,s540,s310,s541,s982,s972,s981,s974,s971]) ).
cnf(s985,plain,
~ spl93_9,
inference(rat,[],[s26,s4,s6,s959,s442,s3,s91,s451,s5,s984,s983,s982,s540,s310,s318,s415,s435,s541,s971,s974,s972,s981,s973]) ).
cnf(s986,plain,
( ~ spl93_25
| ~ spl93_17 ),
inference(rat,[],[s6,s647,s819,s3,s2,s29,s424,s596,s630,s617,s19,s974,s972,s981,s985,s970]) ).
cnf(s987,plain,
( ~ spl93_23
| ~ spl93_17 ),
inference(rat,[],[s647,s3,s6,s930,s626,s2,s498,s678,s630,s617,s19,s972,s981,s974,s985,s970]) ).
cnf(s988,plain,
~ spl93_17,
inference(rat,[],[s819,s2,s6,s930,s442,s3,s58,s601,s5,s987,s986,s19,s338,s617,s630,s985,s970,s974,s972,s981,s973]) ).
cnf(s989,plain,
( ~ spl93_29
| ~ spl93_25 ),
inference(rat,[],[s2,s46,s17,s4,s3,s643,s647,s596,s424,s78,s985,s970,s988,s971,s972,s981]) ).
cnf(s990,plain,
( ~ spl93_28
| ~ spl93_25 ),
inference(rat,[],[s3,s616,s17,s4,s2,s454,s819,s596,s424,s78,s972,s981,s988,s971,s985,s970]) ).
cnf(s991,plain,
~ spl93_25,
inference(rat,[],[s4,s616,s46,s3,s2,s22,s631,s6,s990,s989,s29,s78,s424,s596,s988,s971,s972,s981,s985,s970,s974]) ).
cnf(s992,plain,
( ~ spl93_30
| ~ spl93_23 ),
inference(rat,[],[s3,s616,s17,s4,s2,s88,s442,s626,s705,s678,s972,s981,s988,s971,s985,s970]) ).
cnf(s993,plain,
( ~ spl93_29
| ~ spl93_23 ),
inference(rat,[],[s16,s3,s2,s959,s887,s4,s643,s647,s705,s678,s972,s981,s985,s970,s988,s971]) ).
cnf(s994,plain,
~ spl93_23,
inference(rat,[],[s616,s3,s4,s930,s887,s2,s22,s631,s6,s993,s992,s498,s678,s705,s972,s981,s988,s971,s985,s970,s974]) ).
cnf(s995,plain,
( ~ spl93_30
| ~ spl93_22 ),
inference(rat,[],[s4,s616,s46,s3,s2,s88,s442,s626,s235,s91,s988,s971,s972,s981,s985,s970]) ).
cnf(s996,plain,
( ~ spl93_29
| ~ spl93_22 ),
inference(rat,[],[s44,s4,s2,s959,s930,s3,s643,s647,s235,s91,s988,s971,s985,s970,s972,s981]) ).
cnf(s997,plain,
~ spl93_22,
inference(rat,[],[s616,s3,s4,s930,s887,s2,s454,s819,s6,s996,s995,s91,s235,s451,s972,s981,s988,s971,s985,s970,s974]) ).
cnf(s998,plain,
spl93_24,
inference(rat,[],[s5,s973,s994,s991,s997]) ).
cnf(s999,plain,
~ spl93_19,
inference(rat,[],[s610,s998]) ).
cnf(s1000,plain,
~ spl93_14,
inference(rat,[],[s601,s998]) ).
cnf(s1001,plain,
~ spl93_29,
inference(rat,[],[s58,s998]) ).
cnf(s1002,plain,
~ spl93_30,
inference(rat,[],[s2,s46,s17,s4,s3,s88,s442,s626,s985,s970,s988,s999,s971,s972,s1000,s981]) ).
cnf(s1003,plain,
~ spl93_28,
inference(rat,[],[s16,s3,s2,s959,s887,s4,s454,s819,s972,s1000,s981,s985,s970,s988,s999,s971]) ).
cnf(s1004,plain,
spl93_27,
inference(rat,[],[s6,s1001,s974,s1002,s1003]) ).
cnf(s1005,plain,
~ spl93_7,
inference(rat,[],[s631,s1004]) ).
cnf(s1006,plain,
~ spl93_12,
inference(rat,[],[s22,s1004]) ).
cnf(s1007,plain,
spl93_15,
inference(rat,[],[s3,s981,s1000,s972,s1006]) ).
cnf(s1010,plain,
~ spl93_10,
inference(rat,[],[s930,s1007]) ).
cnf(s1014,plain,
~ spl93_20,
inference(rat,[],[s959,s1007]) ).
cnf(s1016,plain,
spl93_8,
inference(rat,[],[s2,s970,s985,s1005,s1010]) ).
cnf(s1017,plain,
spl93_18,
inference(rat,[],[s4,s971,s999,s988,s1014]) ).
cnf(s1018,plain,
$false,
inference(rat,[],[s44,s1017,s1016]) ).
fof(f5117,plain,
$false,
inference(avatar_sat_refutation,[],[s1018]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL648+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.41 % Computer : n017.cluster.edu
% 0.11/0.41 % Model : x86_64 x86_64
% 0.11/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.41 % Memory : 8046.5625MB
% 0.11/0.41 % OS : Linux 6.8.0-71-generic
% 0.11/0.41 % CPULimit : 300
% 0.11/0.41 % WCLimit : 300
% 0.11/0.41 % DateTime : Sun Sep 27 16:10:21 UTC 2026
% 0.11/0.41 % CPUTime :
% 0.11/0.41 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.44 Running first-order model finding
% 0.11/0.44 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.50 % (2774792)Will run a generic schedule for satisfiability detection.
% 0.19/0.50 % (2774800)dis+10_1_sil=32000:sp=arity:random_seed=2974044162:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.50 % (2774798)% WARNING: option uhcvi not known.
% 0.19/0.50 % (2774797)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=671050672_2999 on theBenchmark for (2999ds/0Mi)
% 0.19/0.50 % (2774802)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3968832433:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.19/0.50 % (2774798)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=653072333:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.19/0.50 % (2774799)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=122688437:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.19/0.50 % (2774803)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=20795048:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.19/0.50 % (2774801)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1183591026:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.19/0.50 % TRYING [1]
% 0.19/0.50 % TRYING [2]
% 0.19/0.50 % (2774800) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2774792-2774800"...
% 0.19/0.50 % (2774801) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2774792-2774801"...
% 0.19/0.50 % (2774800)...printing done.
% 0.19/0.50 % (2774800)Refutation found. Thanks to Tanya!
% 0.19/0.50 % SZS status Theorem for theBenchmark
% 0.19/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.51 % (2774800)------------------------------
% 0.19/0.51 % (2774800)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.51 % (2774800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.51 % (2774800)CaDiCaL version: 2.1.3
% 0.19/0.51 % (2774800)Termination reason: Refutation
% 0.19/0.51 % (2774800)Time elapsed: 0.034 s
% 0.19/0.51 % (2774800)Peak memory usage: 14 MB
% 0.19/0.51 % (2774800)Instructions burned: 101 (million)
% 0.19/0.51 % (2774792)Success in time 0.052 s
% 0.19/0.51 % Vampire exiting
%------------------------------------------------------------------------------