%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:59:28 AM UTC 2026
% Result : Theorem 1.37s 0.68s
% Output : CNFRefutation 1.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 3
% Syntax : Number of formulae : 64 ( 20 unt; 0 def)
% Number of atoms : 1526 ( 0 equ)
% Maximal formula atoms : 489 ( 23 avg)
% Number of connectives : 2526 (1064 ~; 907 |; 554 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 119 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 1 con; 0-1 aty)
% Number of variables : 318 ( 0 sgn 276 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(reflexivity,axiom,
! [X] : r1(X,X),
file('theBenchmark.p',reflexivity) ).
fof(transitivity,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('theBenchmark.p',transitivity) ).
fof(main,conjecture,
~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X] :
( ~ p106(X)
| p7(X)
| ~ r1(Y,X) ) )
& ( p7(Y)
| ! [X] :
( ~ p106(X)
| ~ p7(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X] :
( ~ p107(X)
| p8(X)
| ~ r1(Y,X) ) )
& ( p8(Y)
| ! [X] :
( ~ p107(X)
| ~ p8(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X] :
( ~ p108(X)
| p9(X)
| ~ r1(Y,X) ) )
& ( p9(Y)
| ! [X] :
( ~ p108(X)
| ~ p9(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X] :
( ~ p109(X)
| p10(X)
| ~ r1(Y,X) ) )
& ( p10(Y)
| ! [X] :
( ~ p109(X)
| ~ p10(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X] :
( ~ p110(X)
| p11(X)
| ~ r1(Y,X) ) )
& ( p11(Y)
| ! [X] :
( ~ p110(X)
| ~ p11(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p105(Y)
& ~ p106(Y) )
| ( ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& p7(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& ~ p7(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p106(Y)
& ~ p107(Y) )
| ( ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& p8(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& ~ p8(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p107(Y)
& ~ p108(Y) )
| ( ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& p9(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& ~ p9(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p108(Y)
& ~ p109(Y) )
| ( ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& p10(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& ~ p10(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p109(Y)
& ~ p110(Y) )
| ( ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& p11(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& ~ p11(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) ),
file('theBenchmark.p',main) ).
fof(main_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X] :
( ~ p106(X)
| p7(X)
| ~ r1(Y,X) ) )
& ( p7(Y)
| ! [X] :
( ~ p106(X)
| ~ p7(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X] :
( ~ p107(X)
| p8(X)
| ~ r1(Y,X) ) )
& ( p8(Y)
| ! [X] :
( ~ p107(X)
| ~ p8(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X] :
( ~ p108(X)
| p9(X)
| ~ r1(Y,X) ) )
& ( p9(Y)
| ! [X] :
( ~ p108(X)
| ~ p9(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X] :
( ~ p109(X)
| p10(X)
| ~ r1(Y,X) ) )
& ( p10(Y)
| ! [X] :
( ~ p109(X)
| ~ p10(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X] :
( ~ p110(X)
| p11(X)
| ~ r1(Y,X) ) )
& ( p11(Y)
| ! [X] :
( ~ p110(X)
| ~ p11(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p105(Y)
& ~ p106(Y) )
| ( ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& p7(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& ~ p7(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p106(Y)
& ~ p107(Y) )
| ( ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& p8(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& ~ p8(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p107(Y)
& ~ p108(Y) )
| ( ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& p9(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& ~ p9(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p108(Y)
& ~ p109(Y) )
| ( ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& p10(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& ~ p10(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p109(Y)
& ~ p110(Y) )
| ( ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& p11(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& ~ p11(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(nnf_3,plain,
? [X] :
( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X42] :
( ~ p100(X42)
| p1(X42)
| ~ r1(Y,X42) ) )
& ( p1(Y)
| ! [X41] :
( ~ p100(X41)
| ~ p1(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X40] :
( ~ p101(X40)
| p2(X40)
| ~ r1(Y,X40) ) )
& ( p2(Y)
| ! [X39] :
( ~ p101(X39)
| ~ p2(X39)
| ~ r1(Y,X39) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X38] :
( ~ p102(X38)
| p3(X38)
| ~ r1(Y,X38) ) )
& ( p3(Y)
| ! [X37] :
( ~ p102(X37)
| ~ p3(X37)
| ~ r1(Y,X37) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X36] :
( ~ p103(X36)
| p4(X36)
| ~ r1(Y,X36) ) )
& ( p4(Y)
| ! [X35] :
( ~ p103(X35)
| ~ p4(X35)
| ~ r1(Y,X35) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X34] :
( ~ p104(X34)
| p5(X34)
| ~ r1(Y,X34) ) )
& ( p5(Y)
| ! [X33] :
( ~ p104(X33)
| ~ p5(X33)
| ~ r1(Y,X33) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X32] :
( ~ p105(X32)
| p6(X32)
| ~ r1(Y,X32) ) )
& ( p6(Y)
| ! [X31] :
( ~ p105(X31)
| ~ p6(X31)
| ~ r1(Y,X31) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X30] :
( ~ p106(X30)
| p7(X30)
| ~ r1(Y,X30) ) )
& ( p7(Y)
| ! [X29] :
( ~ p106(X29)
| ~ p7(X29)
| ~ r1(Y,X29) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X28] :
( ~ p107(X28)
| p8(X28)
| ~ r1(Y,X28) ) )
& ( p8(Y)
| ! [X27] :
( ~ p107(X27)
| ~ p8(X27)
| ~ r1(Y,X27) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X26] :
( ~ p108(X26)
| p9(X26)
| ~ r1(Y,X26) ) )
& ( p9(Y)
| ! [X25] :
( ~ p108(X25)
| ~ p9(X25)
| ~ r1(Y,X25) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X24] :
( ~ p109(X24)
| p10(X24)
| ~ r1(Y,X24) ) )
& ( p10(Y)
| ! [X23] :
( ~ p109(X23)
| ~ p10(X23)
| ~ r1(Y,X23) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X22] :
( ~ p110(X22)
| p11(X22)
| ~ r1(Y,X22) ) )
& ( p11(Y)
| ! [X21] :
( ~ p110(X21)
| ~ p11(X21)
| ~ r1(Y,X21) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( ? [X20] :
( p101(X20)
& ~ p102(X20)
& p2(X20)
& r1(Y,X20) )
& ? [X19] :
( p101(X19)
& ~ p102(X19)
& ~ p2(X19)
& r1(Y,X19) ) ) )
& ( ~ p101(Y)
| p102(Y)
| ( ? [X18] :
( p102(X18)
& ~ p103(X18)
& p3(X18)
& r1(Y,X18) )
& ? [X17] :
( p102(X17)
& ~ p103(X17)
& ~ p3(X17)
& r1(Y,X17) ) ) )
& ( ~ p102(Y)
| p103(Y)
| ( ? [X16] :
( p103(X16)
& ~ p104(X16)
& p4(X16)
& r1(Y,X16) )
& ? [X15] :
( p103(X15)
& ~ p104(X15)
& ~ p4(X15)
& r1(Y,X15) ) ) )
& ( ~ p103(Y)
| p104(Y)
| ( ? [X14] :
( p104(X14)
& ~ p105(X14)
& p5(X14)
& r1(Y,X14) )
& ? [X13] :
( p104(X13)
& ~ p105(X13)
& ~ p5(X13)
& r1(Y,X13) ) ) )
& ( ~ p104(Y)
| p105(Y)
| ( ? [X12] :
( p105(X12)
& ~ p106(X12)
& p6(X12)
& r1(Y,X12) )
& ? [X11] :
( p105(X11)
& ~ p106(X11)
& ~ p6(X11)
& r1(Y,X11) ) ) )
& ( ~ p105(Y)
| p106(Y)
| ( ? [X10] :
( p106(X10)
& ~ p107(X10)
& p7(X10)
& r1(Y,X10) )
& ? [X9] :
( p106(X9)
& ~ p107(X9)
& ~ p7(X9)
& r1(Y,X9) ) ) )
& ( ~ p106(Y)
| p107(Y)
| ( ? [X8] :
( p107(X8)
& ~ p108(X8)
& p8(X8)
& r1(Y,X8) )
& ? [X7] :
( p107(X7)
& ~ p108(X7)
& ~ p8(X7)
& r1(Y,X7) ) ) )
& ( ~ p107(Y)
| p108(Y)
| ( ? [X6] :
( p108(X6)
& ~ p109(X6)
& p9(X6)
& r1(Y,X6) )
& ? [X5] :
( p108(X5)
& ~ p109(X5)
& ~ p9(X5)
& r1(Y,X5) ) ) )
& ( ~ p108(Y)
| p109(Y)
| ( ? [X4] :
( p109(X4)
& ~ p110(X4)
& p10(X4)
& r1(Y,X4) )
& ? [X3] :
( p109(X3)
& ~ p110(X3)
& ~ p10(X3)
& r1(Y,X3) ) ) )
& ( ~ p109(Y)
| p110(Y)
| ( ? [X2] :
( p110(X2)
& ~ p111(X2)
& p11(X2)
& r1(Y,X2) )
& ? [X1] :
( p110(X1)
& ~ p111(X1)
& ~ p11(X1)
& r1(Y,X1) ) ) ) )
| ~ r1(X,Y) )
& ! [X0] :
( p5(X0)
| ~ r1(X,X0) ) ),
inference(fof_nnf,[status(thm)],[main_neg]) ).
fof(sk_main_neg_sk,plain,
( p100(sK0)
& ~ p101(sK0)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X42] :
( ~ p100(X42)
| p1(X42)
| ~ r1(Y,X42) ) )
& ( p1(Y)
| ! [X41] :
( ~ p100(X41)
| ~ p1(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X40] :
( ~ p101(X40)
| p2(X40)
| ~ r1(Y,X40) ) )
& ( p2(Y)
| ! [X39] :
( ~ p101(X39)
| ~ p2(X39)
| ~ r1(Y,X39) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X38] :
( ~ p102(X38)
| p3(X38)
| ~ r1(Y,X38) ) )
& ( p3(Y)
| ! [X37] :
( ~ p102(X37)
| ~ p3(X37)
| ~ r1(Y,X37) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X36] :
( ~ p103(X36)
| p4(X36)
| ~ r1(Y,X36) ) )
& ( p4(Y)
| ! [X35] :
( ~ p103(X35)
| ~ p4(X35)
| ~ r1(Y,X35) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X34] :
( ~ p104(X34)
| p5(X34)
| ~ r1(Y,X34) ) )
& ( p5(Y)
| ! [X33] :
( ~ p104(X33)
| ~ p5(X33)
| ~ r1(Y,X33) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X32] :
( ~ p105(X32)
| p6(X32)
| ~ r1(Y,X32) ) )
& ( p6(Y)
| ! [X31] :
( ~ p105(X31)
| ~ p6(X31)
| ~ r1(Y,X31) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X30] :
( ~ p106(X30)
| p7(X30)
| ~ r1(Y,X30) ) )
& ( p7(Y)
| ! [X29] :
( ~ p106(X29)
| ~ p7(X29)
| ~ r1(Y,X29) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X28] :
( ~ p107(X28)
| p8(X28)
| ~ r1(Y,X28) ) )
& ( p8(Y)
| ! [X27] :
( ~ p107(X27)
| ~ p8(X27)
| ~ r1(Y,X27) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X26] :
( ~ p108(X26)
| p9(X26)
| ~ r1(Y,X26) ) )
& ( p9(Y)
| ! [X25] :
( ~ p108(X25)
| ~ p9(X25)
| ~ r1(Y,X25) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X24] :
( ~ p109(X24)
| p10(X24)
| ~ r1(Y,X24) ) )
& ( p10(Y)
| ! [X23] :
( ~ p109(X23)
| ~ p10(X23)
| ~ r1(Y,X23) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X22] :
( ~ p110(X22)
| p11(X22)
| ~ r1(Y,X22) ) )
& ( p11(Y)
| ! [X21] :
( ~ p110(X21)
| ~ p11(X21)
| ~ r1(Y,X21) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sK20(Y))
& ~ p102(sK20(Y))
& p2(sK20(Y))
& r1(Y,sK20(Y))
& p101(sK1(Y))
& ~ p102(sK1(Y))
& ~ p2(sK1(Y))
& r1(Y,sK1(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK19(Y))
& ~ p103(sK19(Y))
& p3(sK19(Y))
& r1(Y,sK19(Y))
& p102(sK2(Y))
& ~ p103(sK2(Y))
& ~ p3(sK2(Y))
& r1(Y,sK2(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK18(Y))
& ~ p104(sK18(Y))
& p4(sK18(Y))
& r1(Y,sK18(Y))
& p103(sK3(Y))
& ~ p104(sK3(Y))
& ~ p4(sK3(Y))
& r1(Y,sK3(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK17(Y))
& ~ p105(sK17(Y))
& p5(sK17(Y))
& r1(Y,sK17(Y))
& p104(sK4(Y))
& ~ p105(sK4(Y))
& ~ p5(sK4(Y))
& r1(Y,sK4(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK16(Y))
& ~ p106(sK16(Y))
& p6(sK16(Y))
& r1(Y,sK16(Y))
& p105(sK15(Y))
& ~ p106(sK15(Y))
& ~ p6(sK15(Y))
& r1(Y,sK15(Y)) ) )
& ( ~ p105(Y)
| p106(Y)
| ( p106(sK14(Y))
& ~ p107(sK14(Y))
& p7(sK14(Y))
& r1(Y,sK14(Y))
& p106(sK13(Y))
& ~ p107(sK13(Y))
& ~ p7(sK13(Y))
& r1(Y,sK13(Y)) ) )
& ( ~ p106(Y)
| p107(Y)
| ( p107(sK12(Y))
& ~ p108(sK12(Y))
& p8(sK12(Y))
& r1(Y,sK12(Y))
& p107(sK11(Y))
& ~ p108(sK11(Y))
& ~ p8(sK11(Y))
& r1(Y,sK11(Y)) ) )
& ( ~ p107(Y)
| p108(Y)
| ( p108(sK10(Y))
& ~ p109(sK10(Y))
& p9(sK10(Y))
& r1(Y,sK10(Y))
& p108(sK9(Y))
& ~ p109(sK9(Y))
& ~ p9(sK9(Y))
& r1(Y,sK9(Y)) ) )
& ( ~ p108(Y)
| p109(Y)
| ( p109(sK8(Y))
& ~ p110(sK8(Y))
& p10(sK8(Y))
& r1(Y,sK8(Y))
& p109(sK7(Y))
& ~ p110(sK7(Y))
& ~ p10(sK7(Y))
& r1(Y,sK7(Y)) ) )
& ( ~ p109(Y)
| p110(Y)
| ( p110(sK6(Y))
& ~ p111(sK6(Y))
& p11(sK6(Y))
& r1(Y,sK6(Y))
& p110(sK5(Y))
& ~ p111(sK5(Y))
& ~ p11(sK5(Y))
& r1(Y,sK5(Y)) ) ) )
| ~ r1(sK0,Y) )
& ! [X0] :
( p5(X0)
| ~ r1(sK0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK4,sK17,sK3,sK18,sK2,sK19,sK1,sK20]),skolemize(X,sK0),skolemize(X1,sK5(Y)),skolemize(X2,sK6(Y)),skolemize(X3,sK7(Y)),skolemize(X4,sK8(Y)),skolemize(X5,sK9(Y)),skolemize(X6,sK10(Y)),skolemize(X7,sK11(Y)),skolemize(X8,sK12(Y)),skolemize(X9,sK13(Y)),skolemize(X10,sK14(Y)),skolemize(X11,sK15(Y)),skolemize(X12,sK16(Y)),skolemize(X13,sK4(Y)),skolemize(X14,sK17(Y)),skolemize(X15,sK3(Y)),skolemize(X16,sK18(Y)),skolemize(X17,sK2(Y)),skolemize(X18,sK19(Y)),skolemize(X19,sK1(Y)),skolemize(X20,sK20(Y))],[nnf_3]) ).
fof(sk_main_neg,plain,
( p100(sK0)
& ~ p101(sK0)
& ! [VAR_0] :
( ~ p101(VAR_0)
| p100(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p101(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p102(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p103(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p104(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p105(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p106(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p107(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p108(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p109(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p110(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_0)
| ~ p1(VAR_0)
| ~ p100(VAR_1)
| p1(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_0)
| p1(VAR_0)
| ~ p100(VAR_1)
| ~ p1(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_0)
| ~ p2(VAR_0)
| ~ p101(VAR_1)
| p2(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_0)
| p2(VAR_0)
| ~ p101(VAR_1)
| ~ p2(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_0)
| ~ p3(VAR_0)
| ~ p102(VAR_1)
| p3(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_0)
| p3(VAR_0)
| ~ p102(VAR_1)
| ~ p3(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_0)
| ~ p4(VAR_0)
| ~ p103(VAR_1)
| p4(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_0)
| p4(VAR_0)
| ~ p103(VAR_1)
| ~ p4(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_0)
| ~ p5(VAR_0)
| ~ p104(VAR_1)
| p5(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_0)
| p5(VAR_0)
| ~ p104(VAR_1)
| ~ p5(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p105(VAR_0)
| ~ p6(VAR_0)
| ~ p105(VAR_1)
| p6(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p105(VAR_0)
| p6(VAR_0)
| ~ p105(VAR_1)
| ~ p6(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p106(VAR_0)
| ~ p7(VAR_0)
| ~ p106(VAR_1)
| p7(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p106(VAR_0)
| p7(VAR_0)
| ~ p106(VAR_1)
| ~ p7(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p107(VAR_0)
| ~ p8(VAR_0)
| ~ p107(VAR_1)
| p8(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p107(VAR_0)
| p8(VAR_0)
| ~ p107(VAR_1)
| ~ p8(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p108(VAR_0)
| ~ p9(VAR_0)
| ~ p108(VAR_1)
| p9(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p108(VAR_0)
| p9(VAR_0)
| ~ p108(VAR_1)
| ~ p9(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p109(VAR_0)
| ~ p10(VAR_0)
| ~ p109(VAR_1)
| p10(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p109(VAR_0)
| p10(VAR_0)
| ~ p109(VAR_1)
| ~ p10(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p110(VAR_0)
| ~ p11(VAR_0)
| ~ p110(VAR_1)
| p11(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p110(VAR_0)
| p11(VAR_0)
| ~ p110(VAR_1)
| ~ p11(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p2(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p2(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p102(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p3(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p102(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p3(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p103(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p4(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p103(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p4(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p5(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p5(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p6(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p6(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p106(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p107(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p7(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| r1(VAR_0,sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p106(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p107(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p7(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| r1(VAR_0,sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p107(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p8(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p107(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p8(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p9(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p9(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p10(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p10(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p11(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p11(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p5(VAR_0)
| ~ r1(sK0,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_main_neg_sk]) ).
cnf(c_4,negated_conjecture,
p100(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_5,negated_conjecture,
~ p101(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_42,negated_conjecture,
( ~ p100(A)
| p101(A)
| p101(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_43,negated_conjecture,
( ~ p100(A)
| p101(A)
| ~ p102(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_45,negated_conjecture,
( ~ p100(A)
| p101(A)
| r1(A,sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_50,negated_conjecture,
( ~ p101(A)
| p102(A)
| p102(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_51,negated_conjecture,
( ~ p101(A)
| p102(A)
| ~ p103(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_53,negated_conjecture,
( ~ p101(A)
| p102(A)
| r1(A,sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_58,negated_conjecture,
( ~ p102(A)
| p103(A)
| p103(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_59,negated_conjecture,
( ~ p102(A)
| p103(A)
| ~ p104(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_61,negated_conjecture,
( ~ p102(A)
| p103(A)
| r1(A,sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_68,negated_conjecture,
( ~ p103(A)
| p104(A)
| ~ p5(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_69,negated_conjecture,
( ~ p103(A)
| p104(A)
| r1(A,sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_116,negated_conjecture,
( p5(A)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_117,plain,
( r1(A,C)
| ~ r1(B,C)
| ~ r1(A,B) ),
inference(clausify,[status(thm)],[transitivity]) ).
cnf(c_118,plain,
r1(A,A),
inference(clausify,[status(thm)],[reflexivity]) ).
cnf(c_1992,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_118,c_45]) ).
cnf(c_1993,negated_conjecture,
( ~ p100(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_1992]) ).
cnf(c_182,negated_conjecture,
r1(sK0,sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_1993]) ).
cnf(c_1994,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_118,c_43]) ).
cnf(c_1995,negated_conjecture,
( ~ p100(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_1994]) ).
cnf(c_184,negated_conjecture,
~ p102(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_1995]) ).
cnf(c_1996,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_118,c_42]) ).
cnf(c_1997,negated_conjecture,
( ~ p100(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_1996]) ).
cnf(c_185,negated_conjecture,
p101(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_1997]) ).
cnf(c_226,plain,
( r1(sK0,A)
| ~ r1(sK1(sK0),A) ),
inference(resolve,[status(thm)],[c_182,c_117]) ).
cnf(c_1998,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_182,c_53]) ).
cnf(c_1999,negated_conjecture,
( ~ p101(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_184,c_1998]) ).
cnf(c_282,negated_conjecture,
r1(sK1(sK0),sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_185,c_1999]) ).
cnf(c_2000,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_182,c_51]) ).
cnf(c_2001,negated_conjecture,
( ~ p101(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_184,c_2000]) ).
cnf(c_284,negated_conjecture,
~ p103(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_185,c_2001]) ).
cnf(c_2002,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_182,c_50]) ).
cnf(c_2003,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_184,c_2002]) ).
cnf(c_285,negated_conjecture,
p102(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_185,c_2003]) ).
cnf(c_435,plain,
r1(sK0,sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_282,c_226]) ).
cnf(c_450,plain,
( r1(sK0,A)
| ~ r1(sK2(sK1(sK0)),A) ),
inference(resolve,[status(thm)],[c_435,c_117]) ).
cnf(c_2004,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_435,c_61]) ).
cnf(c_2005,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_284,c_2004]) ).
cnf(c_498,negated_conjecture,
r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_285,c_2005]) ).
cnf(c_2006,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_435,c_59]) ).
cnf(c_2007,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_284,c_2006]) ).
cnf(c_500,negated_conjecture,
~ p104(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_285,c_2007]) ).
cnf(c_2008,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_435,c_58]) ).
cnf(c_2009,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_284,c_2008]) ).
cnf(c_501,negated_conjecture,
p103(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_285,c_2009]) ).
cnf(c_891,plain,
r1(sK0,sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_498,c_450]) ).
cnf(c_942,plain,
( r1(sK0,A)
| ~ r1(sK3(sK2(sK1(sK0))),A) ),
inference(resolve,[status(thm)],[c_891,c_117]) ).
cnf(c_2010,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_891,c_69]) ).
cnf(c_2011,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_500,c_2010]) ).
cnf(c_982,negated_conjecture,
r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_501,c_2011]) ).
cnf(c_2012,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| ~ p5(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_891,c_68]) ).
cnf(c_2013,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| ~ p5(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_500,c_2012]) ).
cnf(c_983,negated_conjecture,
~ p5(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_501,c_2013]) ).
cnf(c_1750,plain,
r1(sK0,sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_982,c_942]) ).
cnf(c_2014,negated_conjecture,
p5(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1750,c_116]) ).
cnf(c_1991,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_983,c_2014]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.43 % Computer : n005.cluster.edu
% 0.16/0.43 % Model : x86_64 x86_64
% 0.16/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.43 % Memory : 8046.5625MB
% 0.16/0.43 % OS : Linux 6.8.0-71-generic
% 0.16/0.43 % CPULimit : 300
% 0.16/0.43 % WCLimit : 300
% 0.16/0.43 % DateTime : Fri Sep 25 23:14:18 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.43 % Process 498606 was started by sandbox2 on n005,
% 0.16/0.43 % Fri Sep 25 23:14:18 2026
% 0.16/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.16/0.49
% 0.16/0.49 % From the command line: assign(max_seconds, 300).
% 1.37/0.68
% 1.37/0.68 % given #500 (W,wt=28): 1403 -p1(f15(f18(f19(c1)))) | p1(f19(c1)). [resolve(909,a,322,a),unit_del(b,1267)].
% 1.37/0.68
% 1.37/0.68 % SZS status Theorem for theBenchmark
% 1.37/0.68
% 1.37/0.68 % Proof 1 at 0.11 (+ 0.05) seconds.
% 1.37/0.68 % Length of proof is 37.
% 1.37/0.68 % Level of proof is 9.
% 1.37/0.68 % Maximum clause weight is 35.000.
% 1.37/0.68 % Given clauses 645.
% 1.37/0.68
% 1.37/0.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------