%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.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 : Thu Sep 24 01:08:31 PM UTC 2026
% Result : Theorem 75.66s 10.05s
% Output : CNFRefutation 75.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 26
% Syntax : Number of formulae : 138 ( 8 unt; 23 def)
% Number of atoms : 1720 ( 0 equ)
% Maximal formula atoms : 331 ( 12 avg)
% Number of connectives : 2765 (1183 ~; 909 |; 649 &)
% ( 23 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 58 ( 5 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 58 ( 57 usr; 24 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 1 con; 0-1 aty)
% Number of variables : 266 ( 233 !; 33 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : r1(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,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) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(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) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(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) ) ) )
& ( ~ ( p110(Y)
& ~ p111(Y) )
| ( ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& p12(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& ~ p12(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p111(Y)
& ~ p112(Y) )
| ( ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& p13(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& ~ p13(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p112(Y)
& ~ p113(Y) )
| ( ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& p14(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& ~ p14(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p113(Y)
& ~ p114(Y) )
| ( ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& p15(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& ~ p15(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p114(Y)
& ~ p115(Y) )
| ( ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& p16(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& ~ p16(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p7(Y)
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,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) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(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) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(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) ) ) )
& ( ~ ( p110(Y)
& ~ p111(Y) )
| ( ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& p12(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& ~ p12(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p111(Y)
& ~ p112(Y) )
| ( ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& p13(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& ~ p13(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p112(Y)
& ~ p113(Y) )
| ( ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& p14(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& ~ p14(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p113(Y)
& ~ p114(Y) )
| ( ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& p15(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& ~ p15(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p114(Y)
& ~ p115(Y) )
| ( ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& p16(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& ~ p16(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p7(Y)
| ~ r1(X,Y) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f6,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f7,plain,
! [X,Z] :
( r1(X,Z)
| ! [Y] :
( ~ r1(Y,Z)
| ~ r1(X,Y) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] :
( ~ r1(X2,X1)
| ~ r1(X0,X2)
| r1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f9,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) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(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) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(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) ) ) )
& ( ~ p110(Y)
| p111(Y)
| ( ? [X] :
( p111(X)
& ~ p112(X)
& p12(X)
& r1(Y,X) )
& ? [X] :
( p111(X)
& ~ p112(X)
& ~ p12(X)
& r1(Y,X) ) ) )
& ( ~ p111(Y)
| p112(Y)
| ( ? [X] :
( p112(X)
& ~ p113(X)
& p13(X)
& r1(Y,X) )
& ? [X] :
( p112(X)
& ~ p113(X)
& ~ p13(X)
& r1(Y,X) ) ) )
& ( ~ p112(Y)
| p113(Y)
| ( ? [X] :
( p113(X)
& ~ p114(X)
& p14(X)
& r1(Y,X) )
& ? [X] :
( p113(X)
& ~ p114(X)
& ~ p14(X)
& r1(Y,X) ) ) )
& ( ~ p113(Y)
| p114(Y)
| ( ? [X] :
( p114(X)
& ~ p115(X)
& p15(X)
& r1(Y,X) )
& ? [X] :
( p114(X)
& ~ p115(X)
& ~ p15(X)
& r1(Y,X) ) ) )
& ( ~ p114(Y)
| p115(Y)
| ( ? [X] :
( p115(X)
& ~ p116(X)
& p16(X)
& r1(Y,X) )
& ? [X] :
( p115(X)
& ~ p116(X)
& ~ p16(X)
& r1(Y,X) ) ) ) )
| ~ r1(X,Y) )
& ! [Y] :
( p7(Y)
| ~ r1(X,Y) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
( p100(sK0_skl)
& ~ p101(sK0_skl)
& ! [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) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(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) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sK30_skl(Y))
& ~ p102(sK30_skl(Y))
& p2(sK30_skl(Y))
& r1(Y,sK30_skl(Y))
& p101(sK29_skl(Y))
& ~ p102(sK29_skl(Y))
& ~ p2(sK29_skl(Y))
& r1(Y,sK29_skl(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK28_skl(Y))
& ~ p103(sK28_skl(Y))
& p3(sK28_skl(Y))
& r1(Y,sK28_skl(Y))
& p102(sK27_skl(Y))
& ~ p103(sK27_skl(Y))
& ~ p3(sK27_skl(Y))
& r1(Y,sK27_skl(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK26_skl(Y))
& ~ p104(sK26_skl(Y))
& p4(sK26_skl(Y))
& r1(Y,sK26_skl(Y))
& p103(sK25_skl(Y))
& ~ p104(sK25_skl(Y))
& ~ p4(sK25_skl(Y))
& r1(Y,sK25_skl(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK24_skl(Y))
& ~ p105(sK24_skl(Y))
& p5(sK24_skl(Y))
& r1(Y,sK24_skl(Y))
& p104(sK23_skl(Y))
& ~ p105(sK23_skl(Y))
& ~ p5(sK23_skl(Y))
& r1(Y,sK23_skl(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK22_skl(Y))
& ~ p106(sK22_skl(Y))
& p6(sK22_skl(Y))
& r1(Y,sK22_skl(Y))
& p105(sK21_skl(Y))
& ~ p106(sK21_skl(Y))
& ~ p6(sK21_skl(Y))
& r1(Y,sK21_skl(Y)) ) )
& ( ~ p105(Y)
| p106(Y)
| ( p106(sK20_skl(Y))
& ~ p107(sK20_skl(Y))
& p7(sK20_skl(Y))
& r1(Y,sK20_skl(Y))
& p106(sK19_skl(Y))
& ~ p107(sK19_skl(Y))
& ~ p7(sK19_skl(Y))
& r1(Y,sK19_skl(Y)) ) )
& ( ~ p106(Y)
| p107(Y)
| ( p107(sK18_skl(Y))
& ~ p108(sK18_skl(Y))
& p8(sK18_skl(Y))
& r1(Y,sK18_skl(Y))
& p107(sK17_skl(Y))
& ~ p108(sK17_skl(Y))
& ~ p8(sK17_skl(Y))
& r1(Y,sK17_skl(Y)) ) )
& ( ~ p107(Y)
| p108(Y)
| ( p108(sK16_skl(Y))
& ~ p109(sK16_skl(Y))
& p9(sK16_skl(Y))
& r1(Y,sK16_skl(Y))
& p108(sK15_skl(Y))
& ~ p109(sK15_skl(Y))
& ~ p9(sK15_skl(Y))
& r1(Y,sK15_skl(Y)) ) )
& ( ~ p108(Y)
| p109(Y)
| ( p109(sK14_skl(Y))
& ~ p110(sK14_skl(Y))
& p10(sK14_skl(Y))
& r1(Y,sK14_skl(Y))
& p109(sK13_skl(Y))
& ~ p110(sK13_skl(Y))
& ~ p10(sK13_skl(Y))
& r1(Y,sK13_skl(Y)) ) )
& ( ~ p109(Y)
| p110(Y)
| ( p110(sK12_skl(Y))
& ~ p111(sK12_skl(Y))
& p11(sK12_skl(Y))
& r1(Y,sK12_skl(Y))
& p110(sK11_skl(Y))
& ~ p111(sK11_skl(Y))
& ~ p11(sK11_skl(Y))
& r1(Y,sK11_skl(Y)) ) )
& ( ~ p110(Y)
| p111(Y)
| ( p111(sK10_skl(Y))
& ~ p112(sK10_skl(Y))
& p12(sK10_skl(Y))
& r1(Y,sK10_skl(Y))
& p111(sK9_skl(Y))
& ~ p112(sK9_skl(Y))
& ~ p12(sK9_skl(Y))
& r1(Y,sK9_skl(Y)) ) )
& ( ~ p111(Y)
| p112(Y)
| ( p112(sK8_skl(Y))
& ~ p113(sK8_skl(Y))
& p13(sK8_skl(Y))
& r1(Y,sK8_skl(Y))
& p112(sK7_skl(Y))
& ~ p113(sK7_skl(Y))
& ~ p13(sK7_skl(Y))
& r1(Y,sK7_skl(Y)) ) )
& ( ~ p112(Y)
| p113(Y)
| ( p113(sK6_skl(Y))
& ~ p114(sK6_skl(Y))
& p14(sK6_skl(Y))
& r1(Y,sK6_skl(Y))
& p113(sK5_skl(Y))
& ~ p114(sK5_skl(Y))
& ~ p14(sK5_skl(Y))
& r1(Y,sK5_skl(Y)) ) )
& ( ~ p113(Y)
| p114(Y)
| ( p114(sK4_skl(Y))
& ~ p115(sK4_skl(Y))
& p15(sK4_skl(Y))
& r1(Y,sK4_skl(Y))
& p114(sK3_skl(Y))
& ~ p115(sK3_skl(Y))
& ~ p15(sK3_skl(Y))
& r1(Y,sK3_skl(Y)) ) )
& ( ~ p114(Y)
| p115(Y)
| ( p115(sK2_skl(Y))
& ~ p116(sK2_skl(Y))
& p16(sK2_skl(Y))
& r1(Y,sK2_skl(Y))
& p115(sK1_skl(Y))
& ~ p116(sK1_skl(Y))
& ~ p16(sK1_skl(Y))
& r1(Y,sK1_skl(Y)) ) ) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p7(Y)
| ~ r1(sK0_skl,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl]),skolemize(X,sK0_skl),skolemize(X,sK1_skl(Y)),skolemize(X,sK2_skl(Y)),skolemize(X,sK3_skl(Y)),skolemize(X,sK4_skl(Y)),skolemize(X,sK5_skl(Y)),skolemize(X,sK6_skl(Y)),skolemize(X,sK7_skl(Y)),skolemize(X,sK8_skl(Y)),skolemize(X,sK9_skl(Y)),skolemize(X,sK10_skl(Y)),skolemize(X,sK11_skl(Y)),skolemize(X,sK12_skl(Y)),skolemize(X,sK13_skl(Y)),skolemize(X,sK14_skl(Y)),skolemize(X,sK15_skl(Y)),skolemize(X,sK16_skl(Y)),skolemize(X,sK17_skl(Y)),skolemize(X,sK18_skl(Y)),skolemize(X,sK19_skl(Y)),skolemize(X,sK20_skl(Y)),skolemize(X,sK21_skl(Y)),skolemize(X,sK22_skl(Y)),skolemize(X,sK23_skl(Y)),skolemize(X,sK24_skl(Y)),skolemize(X,sK25_skl(Y)),skolemize(X,sK26_skl(Y)),skolemize(X,sK27_skl(Y)),skolemize(X,sK28_skl(Y)),skolemize(X,sK29_skl(Y)),skolemize(X,sK30_skl(Y))],[f9]) ).
fof(f11,plain,
! [X0] :
( p7(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f84,plain,
! [X0] :
( p106(X0)
| r1(X0,sK19_skl(X0))
| ~ p105(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f85,plain,
! [X0] :
( p106(X0)
| ~ r1(sK0_skl,X0)
| ~ p7(sK19_skl(X0))
| ~ p105(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f96,plain,
! [X0] :
( ~ p104(X0)
| ~ r1(sK0_skl,X0)
| r1(X0,sK22_skl(X0))
| p105(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f98,plain,
! [X0] :
( p105(X0)
| ~ p106(sK22_skl(X0))
| ~ r1(sK0_skl,X0)
| ~ p104(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f99,plain,
! [X0] :
( p105(sK22_skl(X0))
| ~ r1(sK0_skl,X0)
| p105(X0)
| ~ p104(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f104,plain,
! [X0] :
( ~ r1(sK0_skl,X0)
| ~ p103(X0)
| p104(X0)
| r1(X0,sK24_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f106,plain,
! [X0] :
( ~ p105(sK24_skl(X0))
| ~ p103(X0)
| p104(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f107,plain,
! [X0] :
( p104(sK24_skl(X0))
| ~ r1(sK0_skl,X0)
| p104(X0)
| ~ p103(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f112,plain,
! [X0] :
( p103(X0)
| r1(X0,sK26_skl(X0))
| ~ p102(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f114,plain,
! [X0] :
( ~ r1(sK0_skl,X0)
| p103(X0)
| ~ p102(X0)
| ~ p104(sK26_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f115,plain,
! [X0] :
( p103(sK26_skl(X0))
| ~ p102(X0)
| p103(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f120,plain,
! [X0] :
( ~ r1(sK0_skl,X0)
| p102(X0)
| r1(X0,sK28_skl(X0))
| ~ p101(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f122,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| ~ p103(sK28_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f123,plain,
! [X0] :
( p102(sK28_skl(X0))
| ~ r1(sK0_skl,X0)
| ~ p101(X0)
| p102(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f124,plain,
! [X0] :
( r1(X0,sK29_skl(X0))
| p101(X0)
| ~ p100(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f126,plain,
! [X0] :
( ~ p100(X0)
| ~ p102(sK29_skl(X0))
| p101(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f127,plain,
! [X0] :
( ~ r1(sK0_skl,X0)
| p101(X0)
| p101(sK29_skl(X0))
| ~ p100(X0) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f180,plain,
~ p101(sK0_skl),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f181,plain,
p100(sK0_skl),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f189,plain,
( r1(sK0_skl,sK29_skl(sK0_skl))
| p101(sK0_skl)
| ~ r1(sK0_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f124,f181]) ).
fof(f190,definition,
( sQ0_spl
<=> r1(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f192,plain,
( sQ0_spl
| ~ r1(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f190]) ).
fof(f193,definition,
( sQ1_spl
<=> p101(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f194,plain,
( ~ sQ1_spl
| p101(sK0_skl) ),
inference(component_clause,[status(thm)],[f193]) ).
fof(f196,definition,
( sQ2_spl
<=> r1(sK0_skl,sK29_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f197,plain,
( ~ sQ2_spl
| r1(sK0_skl,sK29_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f196]) ).
fof(f199,plain,
( sQ2_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f189,f190,f193,f196]) ).
fof(f202,plain,
! [X0] :
( ~ sQ2_spl
| r1(sK0_skl,X0)
| ~ r1(sK29_skl(sK0_skl),X0) ),
inference(resolution,[status(thm)],[f197,f8]) ).
fof(f207,plain,
( ~ r1(sK0_skl,sK0_skl)
| p101(sK0_skl)
| p101(sK29_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f127,f181]) ).
fof(f208,definition,
( sQ3_spl
<=> p101(sK29_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f209,plain,
( ~ sQ3_spl
| p101(sK29_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f208]) ).
fof(f211,plain,
( ~ sQ0_spl
| sQ1_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f207,f208,f193,f190]) ).
fof(f212,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f192,f5]) ).
fof(f213,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f212]) ).
fof(f214,plain,
( ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f194,f180]) ).
fof(f215,plain,
~ sQ1_spl,
inference(contradiction_clause,[status(thm)],[f214]) ).
fof(f216,plain,
( ~ sQ3_spl
| p102(sK28_skl(sK29_skl(sK0_skl)))
| ~ r1(sK0_skl,sK29_skl(sK0_skl))
| p102(sK29_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f209,f123]) ).
fof(f223,definition,
( sQ5_spl
<=> p102(sK29_skl(sK0_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f224,plain,
( ~ sQ5_spl
| p102(sK29_skl(sK0_skl)) ),
inference(component_clause,[status(thm)],[f223]) ).
fof(f230,definition,
( sQ7_spl
<=> p102(sK28_skl(sK29_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( ~ sQ7_spl
| p102(sK28_skl(sK29_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f230]) ).
fof(f233,plain,
( ~ sQ3_spl
| sQ7_spl
| ~ sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f216,f223,f196,f230,f208]) ).
fof(f234,plain,
( ~ sQ5_spl
| ~ p100(sK0_skl)
| p101(sK0_skl)
| ~ r1(sK0_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f224,f126]) ).
fof(f240,definition,
( sQ8_spl
<=> p100(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f242,plain,
( sQ8_spl
| ~ p100(sK0_skl) ),
inference(component_clause,[status(thm)],[f240]) ).
fof(f243,plain,
( ~ sQ5_spl
| ~ sQ8_spl
| sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f234,f190,f193,f240,f223]) ).
fof(f267,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f242,f181]) ).
fof(f268,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f267]) ).
fof(f282,plain,
( ~ sQ7_spl
| p103(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| p103(sK28_skl(sK29_skl(sK0_skl)))
| ~ r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f231,f115]) ).
fof(f287,definition,
( sQ17_spl
<=> r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f288,plain,
( ~ sQ17_spl
| r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f289,plain,
( sQ17_spl
| ~ r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f287]) ).
fof(f297,definition,
( sQ20_spl
<=> p103(sK28_skl(sK29_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f298,plain,
( ~ sQ20_spl
| p103(sK28_skl(sK29_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f297]) ).
fof(f301,definition,
( sQ21_spl
<=> p103(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f302,plain,
( ~ sQ21_spl
| p103(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f304,plain,
( ~ sQ7_spl
| sQ21_spl
| sQ20_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f282,f287,f297,f301,f230]) ).
fof(f353,plain,
( ~ sQ7_spl
| p103(sK28_skl(sK29_skl(sK0_skl)))
| r1(sK28_skl(sK29_skl(sK0_skl)),sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| ~ r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f112,f231]) ).
fof(f354,definition,
( sQ33_spl
<=> r1(sK28_skl(sK29_skl(sK0_skl)),sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( ~ sQ33_spl
| r1(sK28_skl(sK29_skl(sK0_skl)),sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f354]) ).
fof(f357,plain,
( ~ sQ7_spl
| sQ20_spl
| sQ33_spl
| ~ sQ17_spl ),
inference(split_clause,[status(thm)],[f353,f287,f354,f297,f230]) ).
fof(f379,plain,
( ~ sQ3_spl
| ~ r1(sK0_skl,sK29_skl(sK0_skl))
| p102(sK29_skl(sK0_skl))
| r1(sK29_skl(sK0_skl),sK28_skl(sK29_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f120,f209]) ).
fof(f381,definition,
( sQ37_spl
<=> r1(sK29_skl(sK0_skl),sK28_skl(sK29_skl(sK0_skl))) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f382,plain,
( ~ sQ37_spl
| r1(sK29_skl(sK0_skl),sK28_skl(sK29_skl(sK0_skl))) ),
inference(component_clause,[status(thm)],[f381]) ).
fof(f384,plain,
( ~ sQ3_spl
| ~ sQ2_spl
| sQ5_spl
| sQ37_spl ),
inference(split_clause,[status(thm)],[f379,f381,f223,f196,f208]) ).
fof(f386,plain,
( ~ sQ2_spl
| ~ sQ37_spl
| r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f382,f202]) ).
fof(f389,plain,
( ~ sQ2_spl
| ~ sQ37_spl
| sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f386,f289]) ).
fof(f390,plain,
( ~ sQ2_spl
| ~ sQ37_spl
| sQ17_spl ),
inference(contradiction_clause,[status(thm)],[f389]) ).
fof(f391,plain,
( ~ sQ20_spl
| ~ p101(sK29_skl(sK0_skl))
| p102(sK29_skl(sK0_skl))
| ~ r1(sK0_skl,sK29_skl(sK0_skl)) ),
inference(resolution,[status(thm)],[f298,f122]) ).
fof(f417,plain,
( ~ sQ20_spl
| ~ sQ3_spl
| sQ5_spl
| ~ sQ2_spl ),
inference(split_clause,[status(thm)],[f391,f196,f223,f208,f297]) ).
fof(f452,plain,
! [X0] :
( ~ sQ17_spl
| ~ r1(sK28_skl(sK29_skl(sK0_skl)),X0)
| r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f288,f8]) ).
fof(f485,plain,
( ~ sQ21_spl
| ~ r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| p104(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| r1(sK26_skl(sK28_skl(sK29_skl(sK0_skl))),sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(resolution,[status(thm)],[f302,f104]) ).
fof(f486,plain,
( ~ sQ21_spl
| p104(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))
| ~ r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| p104(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(resolution,[status(thm)],[f302,f107]) ).
fof(f492,definition,
( sQ57_spl
<=> r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f494,plain,
( sQ57_spl
| ~ r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f492]) ).
fof(f496,definition,
( sQ58_spl
<=> p104(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f497,plain,
( ~ sQ58_spl
| p104(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(component_clause,[status(thm)],[f496]) ).
fof(f499,definition,
( sQ59_spl
<=> p104(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f500,plain,
( ~ sQ59_spl
| p104(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f499]) ).
fof(f502,plain,
( ~ sQ21_spl
| sQ59_spl
| ~ sQ57_spl
| sQ58_spl ),
inference(split_clause,[status(thm)],[f486,f496,f492,f499,f301]) ).
fof(f507,definition,
( sQ61_spl
<=> r1(sK26_skl(sK28_skl(sK29_skl(sK0_skl))),sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f508,plain,
( ~ sQ61_spl
| r1(sK26_skl(sK28_skl(sK29_skl(sK0_skl))),sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f507]) ).
fof(f510,plain,
( ~ sQ21_spl
| ~ sQ57_spl
| sQ58_spl
| sQ61_spl ),
inference(split_clause,[status(thm)],[f485,f507,f496,f492,f301]) ).
fof(f523,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(resolution,[status(thm)],[f355,f452]) ).
fof(f526,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| sQ57_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f523,f494]) ).
fof(f527,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| sQ57_spl ),
inference(contradiction_clause,[status(thm)],[f526]) ).
fof(f566,plain,
( ~ sQ58_spl
| ~ r1(sK0_skl,sK28_skl(sK29_skl(sK0_skl)))
| p103(sK28_skl(sK29_skl(sK0_skl)))
| ~ p102(sK28_skl(sK29_skl(sK0_skl))) ),
inference(resolution,[status(thm)],[f497,f114]) ).
fof(f582,plain,
( ~ sQ58_spl
| ~ sQ17_spl
| sQ20_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f566,f230,f297,f287,f496]) ).
fof(f620,plain,
! [X0] :
( ~ sQ17_spl
| ~ sQ33_spl
| ~ r1(sK26_skl(sK28_skl(sK29_skl(sK0_skl))),X0)
| r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f523,f8]) ).
fof(f647,plain,
( ~ sQ59_spl
| p105(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))
| ~ r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))
| p105(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(resolution,[status(thm)],[f500,f99]) ).
fof(f648,plain,
( ~ sQ59_spl
| ~ r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))
| r1(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))),sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))
| p105(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(resolution,[status(thm)],[f500,f96]) ).
fof(f651,definition,
( sQ87_spl
<=> r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f652,plain,
( ~ sQ87_spl
| r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f653,plain,
( sQ87_spl
| ~ r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f651]) ).
fof(f658,definition,
( sQ89_spl
<=> p105(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f659,plain,
( ~ sQ89_spl
| p105(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(component_clause,[status(thm)],[f658]) ).
fof(f661,definition,
( sQ90_spl
<=> p105(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f662,plain,
( ~ sQ90_spl
| p105(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(component_clause,[status(thm)],[f661]) ).
fof(f664,plain,
( ~ sQ59_spl
| sQ90_spl
| ~ sQ87_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f647,f658,f651,f661,f499]) ).
fof(f669,definition,
( sQ92_spl
<=> r1(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))),sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f670,plain,
( ~ sQ92_spl
| r1(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))),sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(component_clause,[status(thm)],[f669]) ).
fof(f672,plain,
( ~ sQ59_spl
| ~ sQ87_spl
| sQ92_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f648,f658,f669,f651,f499]) ).
fof(f2049,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| ~ sQ61_spl
| r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(resolution,[status(thm)],[f508,f620]) ).
fof(f2054,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| ~ sQ61_spl
| sQ87_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2049,f653]) ).
fof(f2055,plain,
( ~ sQ17_spl
| ~ sQ33_spl
| ~ sQ61_spl
| sQ87_spl ),
inference(contradiction_clause,[status(thm)],[f2054]) ).
fof(f2160,plain,
( ~ sQ89_spl
| ~ p103(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| p104(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))
| ~ r1(sK0_skl,sK26_skl(sK28_skl(sK29_skl(sK0_skl)))) ),
inference(resolution,[status(thm)],[f659,f106]) ).
fof(f2187,plain,
( ~ sQ89_spl
| ~ sQ21_spl
| sQ58_spl
| ~ sQ57_spl ),
inference(split_clause,[status(thm)],[f2160,f492,f496,f301,f658]) ).
fof(f2483,plain,
! [X0] :
( ~ sQ87_spl
| r1(sK0_skl,X0)
| ~ r1(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))),X0) ),
inference(resolution,[status(thm)],[f652,f8]) ).
fof(f3592,plain,
( ~ sQ90_spl
| p106(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))
| r1(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))),sK19_skl(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))))
| ~ r1(sK0_skl,sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(resolution,[status(thm)],[f662,f84]) ).
fof(f3598,definition,
( sQ638_spl
<=> r1(sK0_skl,sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ638_spl])],[split_symbol_definition]) ).
fof(f3600,plain,
( sQ638_spl
| ~ r1(sK0_skl,sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(component_clause,[status(thm)],[f3598]) ).
fof(f3609,definition,
( sQ641_spl
<=> r1(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))),sK19_skl(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))) ),
introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition]) ).
fof(f3610,plain,
( ~ sQ641_spl
| r1(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))),sK19_skl(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))) ),
inference(component_clause,[status(thm)],[f3609]) ).
fof(f3612,definition,
( sQ642_spl
<=> p106(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition]) ).
fof(f3613,plain,
( ~ sQ642_spl
| p106(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(component_clause,[status(thm)],[f3612]) ).
fof(f3615,plain,
( ~ sQ90_spl
| sQ642_spl
| sQ641_spl
| ~ sQ638_spl ),
inference(split_clause,[status(thm)],[f3592,f3598,f3609,f3612,f661]) ).
fof(f5522,plain,
( ~ sQ92_spl
| ~ sQ87_spl
| r1(sK0_skl,sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(resolution,[status(thm)],[f2483,f670]) ).
fof(f5525,plain,
( ~ sQ92_spl
| ~ sQ87_spl
| sQ638_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5522,f3600]) ).
fof(f5526,plain,
( ~ sQ92_spl
| ~ sQ87_spl
| sQ638_spl ),
inference(contradiction_clause,[status(thm)],[f5525]) ).
fof(f5529,plain,
( ~ sQ642_spl
| p105(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))
| ~ r1(sK0_skl,sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))
| ~ p104(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))) ),
inference(resolution,[status(thm)],[f3613,f98]) ).
fof(f5536,plain,
( ~ sQ642_spl
| sQ89_spl
| ~ sQ87_spl
| ~ sQ59_spl ),
inference(split_clause,[status(thm)],[f5529,f499,f651,f658,f3612]) ).
fof(f5884,plain,
! [X0] :
( ~ sQ92_spl
| ~ sQ87_spl
| r1(sK0_skl,X0)
| ~ r1(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))),X0) ),
inference(resolution,[status(thm)],[f5522,f8]) ).
fof(f13700,plain,
( ~ sQ641_spl
| ~ sQ92_spl
| ~ sQ87_spl
| r1(sK0_skl,sK19_skl(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))) ),
inference(resolution,[status(thm)],[f5884,f3610]) ).
fof(f14261,plain,
( ~ sQ641_spl
| ~ sQ92_spl
| ~ sQ87_spl
| p7(sK19_skl(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))) ),
inference(resolution,[status(thm)],[f13700,f11]) ).
fof(f14264,plain,
( ~ sQ641_spl
| ~ sQ92_spl
| ~ sQ87_spl
| p106(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))
| ~ r1(sK0_skl,sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl))))))
| ~ p105(sK22_skl(sK24_skl(sK26_skl(sK28_skl(sK29_skl(sK0_skl)))))) ),
inference(resolution,[status(thm)],[f14261,f85]) ).
fof(f14265,plain,
( ~ sQ641_spl
| ~ sQ92_spl
| ~ sQ87_spl
| sQ642_spl
| ~ sQ638_spl
| ~ sQ90_spl ),
inference(split_clause,[status(thm)],[f14264,f661,f3598,f3612,f651,f669,f3609]) ).
fof(f14266,plain,
$false,
inference(sat_refutation,[status(thm)],[f199,f211,f213,f215,f233,f243,f268,f304,f357,f384,f390,f417,f502,f510,f527,f582,f664,f672,f2055,f2187,f3615,f5526,f5536,f14265]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n012.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 00:53:23 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 75.66/10.05 % Refutation found
% 75.66/10.05 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.66/10.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.55/10.10 % Elapsed time: 9.739168 seconds
% 7.55/10.10 % CPU time: 77.078113 seconds
% 7.55/10.10 % Total memory used: 277.192 MB
% 7.55/10.10 % Net memory used: 254.822 MB
%------------------------------------------------------------------------------