%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:02:36 PM UTC 2026
% Result : Theorem 15.08s 7.38s
% Output : Proof 15.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 3
% Syntax : Number of formulae : 91 ( 8 unt; 0 def)
% Number of atoms : 1270 ( 0 equ)
% Maximal formula atoms : 226 ( 13 avg)
% Number of connectives : 1918 ( 739 ~; 739 |; 439 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 43 ( 6 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 : 168 ( 0 sgn 126 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,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('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f2_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(negated_conjecture,[status(cth)],[f2]) ).
fof(f2_nnf,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)
| ! [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(nnf_transformation,[status(thm)],[f2_neg]) ).
fof(f2_sk,plain,
! [Y,X] :
( p100(sk0)
& ~ p101(sk0)
& ( ( ( ~ 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)
| ~ p100(X)
| p1(X)
| ~ r1(Y,X) )
& ( p1(Y)
| ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ~ p101(X)
| p2(X)
| ~ r1(Y,X) )
& ( p2(Y)
| ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ~ p102(X)
| p3(X)
| ~ r1(Y,X) )
& ( p3(Y)
| ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ~ p103(X)
| p4(X)
| ~ r1(Y,X) )
& ( p4(Y)
| ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ~ p104(X)
| p5(X)
| ~ r1(Y,X) )
& ( p5(Y)
| ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ~ p105(X)
| p6(X)
| ~ r1(Y,X) )
& ( p6(Y)
| ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ~ p106(X)
| p7(X)
| ~ r1(Y,X) )
& ( p7(Y)
| ~ p106(X)
| ~ p7(X)
| ~ r1(Y,X) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ~ p107(X)
| p8(X)
| ~ r1(Y,X) )
& ( p8(Y)
| ~ p107(X)
| ~ p8(X)
| ~ r1(Y,X) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ~ p108(X)
| p9(X)
| ~ r1(Y,X) )
& ( p9(Y)
| ~ p108(X)
| ~ p9(X)
| ~ r1(Y,X) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ~ p109(X)
| p10(X)
| ~ r1(Y,X) )
& ( p10(Y)
| ~ p109(X)
| ~ p10(X)
| ~ r1(Y,X) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ~ p110(X)
| p11(X)
| ~ r1(Y,X) )
& ( p11(Y)
| ~ p110(X)
| ~ p11(X)
| ~ r1(Y,X) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sk20(Y))
& ~ p102(sk20(Y))
& p2(sk20(Y))
& r1(Y,sk20(Y))
& p101(sk19(Y))
& ~ p102(sk19(Y))
& ~ p2(sk19(Y))
& r1(Y,sk19(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sk18(Y))
& ~ p103(sk18(Y))
& p3(sk18(Y))
& r1(Y,sk18(Y))
& p102(sk17(Y))
& ~ p103(sk17(Y))
& ~ p3(sk17(Y))
& r1(Y,sk17(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sk16(Y))
& ~ p104(sk16(Y))
& p4(sk16(Y))
& r1(Y,sk16(Y))
& p103(sk15(Y))
& ~ p104(sk15(Y))
& ~ p4(sk15(Y))
& r1(Y,sk15(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sk14(Y))
& ~ p105(sk14(Y))
& p5(sk14(Y))
& r1(Y,sk14(Y))
& p104(sk13(Y))
& ~ p105(sk13(Y))
& ~ p5(sk13(Y))
& r1(Y,sk13(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sk12(Y))
& ~ p106(sk12(Y))
& p6(sk12(Y))
& r1(Y,sk12(Y))
& p105(sk11(Y))
& ~ p106(sk11(Y))
& ~ p6(sk11(Y))
& r1(Y,sk11(Y)) ) )
& ( ~ p105(Y)
| p106(Y)
| ( p106(sk10(Y))
& ~ p107(sk10(Y))
& p7(sk10(Y))
& r1(Y,sk10(Y))
& p106(sk9(Y))
& ~ p107(sk9(Y))
& ~ p7(sk9(Y))
& r1(Y,sk9(Y)) ) )
& ( ~ p106(Y)
| p107(Y)
| ( p107(sk8(Y))
& ~ p108(sk8(Y))
& p8(sk8(Y))
& r1(Y,sk8(Y))
& p107(sk7(Y))
& ~ p108(sk7(Y))
& ~ p8(sk7(Y))
& r1(Y,sk7(Y)) ) )
& ( ~ p107(Y)
| p108(Y)
| ( p108(sk6(Y))
& ~ p109(sk6(Y))
& p9(sk6(Y))
& r1(Y,sk6(Y))
& p108(sk5(Y))
& ~ p109(sk5(Y))
& ~ p9(sk5(Y))
& r1(Y,sk5(Y)) ) )
& ( ~ p108(Y)
| p109(Y)
| ( p109(sk4(Y))
& ~ p110(sk4(Y))
& p10(sk4(Y))
& r1(Y,sk4(Y))
& p109(sk3(Y))
& ~ p110(sk3(Y))
& ~ p10(sk3(Y))
& r1(Y,sk3(Y)) ) )
& ( ~ p109(Y)
| p110(Y)
| ( p110(sk2(Y))
& ~ p111(sk2(Y))
& p11(sk2(Y))
& r1(Y,sk2(Y))
& p110(sk1(Y))
& ~ p111(sk1(Y))
& ~ p11(sk1(Y))
& r1(Y,sk1(Y)) ) ) )
| ~ r1(sk0,Y) )
& ( p5(Y)
| ~ r1(sk0,Y) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11,sk12,sk13,sk14,sk15,sk16,sk17,sk18,sk19,sk20])],[f2_nnf]) ).
cnf(c75,plain,
( ~ p100(X1)
| p101(X1)
| r1(X1,sk19(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f0,axiom,
! [X] : r1(X,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f0_nnf,plain,
! [X] : r1(X,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : r1(X,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
r1(X0,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p183,plain,
( ~ p100(sk0)
| p101(sk0)
| r1(sk0,sk19(sk0)) ),
inference(resolution,[status(thm)],[c75,c0]) ).
cnf(c117,plain,
p100(sk0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p219,plain,
( p101(sk0)
| r1(sk0,sk19(sk0)) ),
inference(resolution,[status(thm)],[p183,c117]) ).
cnf(c67,plain,
( ~ p101(X1)
| p102(X1)
| r1(X1,sk17(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p290,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| r1(sk19(sk0),sk17(sk19(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p219,c67]) ).
cnf(c78,plain,
( ~ p100(X1)
| p101(X1)
| p101(sk19(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p186,plain,
( ~ p100(sk0)
| p101(sk0)
| p101(sk19(sk0)) ),
inference(resolution,[status(thm)],[c78,c0]) ).
cnf(p220,plain,
( p101(sk0)
| p101(sk19(sk0)) ),
inference(resolution,[status(thm)],[p186,c117]) ).
cnf(p465,plain,
( p101(sk0)
| p102(sk19(sk0))
| r1(sk19(sk0),sk17(sk19(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p290,p220]) ).
cnf(p477,plain,
( p102(sk19(sk0))
| r1(sk19(sk0),sk17(sk19(sk0)))
| p101(sk0) ),
inference(factoring,[status(thm)],[p465]) ).
fof(f1,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity) ).
fof(f1_nnf,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p224,plain,
( r1(sk0,X0)
| ~ r1(sk19(sk0),X0)
| p101(sk0) ),
inference(resolution,[status(thm)],[p219,c1]) ).
cnf(p490,plain,
( r1(sk0,sk17(sk19(sk0)))
| p101(sk0)
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p477,p224]) ).
cnf(p565,plain,
( r1(sk0,sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p490]) ).
cnf(c59,plain,
( ~ p102(X1)
| p103(X1)
| r1(X1,sk15(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p695,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| r1(sk17(sk19(sk0)),sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p565,c59]) ).
cnf(c70,plain,
( ~ p101(X1)
| p102(X1)
| p102(sk17(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p293,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| p102(sk17(sk19(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p219,c70]) ).
cnf(p466,plain,
( p101(sk0)
| p102(sk19(sk0))
| p102(sk17(sk19(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p293,p220]) ).
cnf(p478,plain,
( p102(sk19(sk0))
| p102(sk17(sk19(sk0)))
| p101(sk0) ),
inference(factoring,[status(thm)],[p466]) ).
cnf(p1119,plain,
( p102(sk19(sk0))
| p101(sk0)
| p103(sk17(sk19(sk0)))
| r1(sk17(sk19(sk0)),sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p695,p478]) ).
cnf(p1143,plain,
( p102(sk19(sk0))
| p103(sk17(sk19(sk0)))
| r1(sk17(sk19(sk0)),sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1119]) ).
cnf(p1191,plain,
( p103(sk17(sk19(sk0)))
| r1(sk17(sk19(sk0)),sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1143]) ).
cnf(p637,plain,
( r1(sk0,X0)
| ~ r1(sk17(sk19(sk0)),X0)
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p565,c1]) ).
cnf(p1217,plain,
( r1(sk0,sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0)
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p1191,p637]) ).
cnf(p1389,plain,
( r1(sk0,sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1217]) ).
cnf(p1716,plain,
( r1(sk0,sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1389]) ).
cnf(c51,plain,
( ~ p103(X1)
| p104(X1)
| r1(X1,sk13(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p1947,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| r1(sk15(sk17(sk19(sk0))),sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p1716,c51]) ).
cnf(c62,plain,
( ~ p102(X1)
| p103(X1)
| p103(sk15(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p698,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p103(sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p565,c62]) ).
cnf(p1120,plain,
( p102(sk19(sk0))
| p101(sk0)
| p103(sk17(sk19(sk0)))
| p103(sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p698,p478]) ).
cnf(p1145,plain,
( p102(sk19(sk0))
| p103(sk17(sk19(sk0)))
| p103(sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1120]) ).
cnf(p1192,plain,
( p103(sk17(sk19(sk0)))
| p103(sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p1145]) ).
cnf(p3005,plain,
( p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0)
| p104(sk15(sk17(sk19(sk0))))
| r1(sk15(sk17(sk19(sk0))),sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p1947,p1192]) ).
cnf(p3187,plain,
( p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p104(sk15(sk17(sk19(sk0))))
| r1(sk15(sk17(sk19(sk0))),sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p3005]) ).
cnf(p3365,plain,
( p103(sk17(sk19(sk0)))
| p104(sk15(sk17(sk19(sk0))))
| r1(sk15(sk17(sk19(sk0))),sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p3187]) ).
cnf(p3479,plain,
( p104(sk15(sk17(sk19(sk0))))
| r1(sk15(sk17(sk19(sk0))),sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p3365]) ).
cnf(p1897,plain,
( r1(sk0,X0)
| ~ r1(sk15(sk17(sk19(sk0))),X0)
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p1716,c1]) ).
cnf(p3538,plain,
( r1(sk0,sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0)
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p3479,p1897]) ).
cnf(p3905,plain,
( r1(sk0,sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p3538]) ).
cnf(p4947,plain,
( r1(sk0,sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p3905]) ).
cnf(p5641,plain,
( r1(sk0,sk13(sk15(sk17(sk19(sk0)))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p4947]) ).
cnf(c2,plain,
( p5(X1)
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p6025,plain,
( p5(sk13(sk15(sk17(sk19(sk0)))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p5641,c2]) ).
cnf(c52,plain,
( ~ p103(X1)
| p104(X1)
| ~ p5(sk13(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p1948,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| ~ p5(sk13(sk15(sk17(sk19(sk0)))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p1716,c52]) ).
cnf(p8539,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0)
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p6025,p1948]) ).
cnf(p9481,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p8539]) ).
cnf(p10203,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p9481]) ).
cnf(p10543,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p10203]) ).
cnf(p10791,plain,
( ~ p103(sk15(sk17(sk19(sk0))))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p10543]) ).
cnf(p10983,plain,
( p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0)
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p10791,p1192]) ).
cnf(p11079,plain,
( p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p10983]) ).
cnf(p11131,plain,
( p103(sk17(sk19(sk0)))
| p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11079]) ).
cnf(p11147,plain,
( p104(sk15(sk17(sk19(sk0))))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11131]) ).
cnf(c61,plain,
( ~ p102(X1)
| p103(X1)
| ~ p104(sk15(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p697,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| ~ p104(sk15(sk17(sk19(sk0))))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p565,c61]) ).
cnf(p11155,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0)
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p11147,p697]) ).
cnf(p11199,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11155]) ).
cnf(p11331,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11199]) ).
cnf(p11419,plain,
( ~ p102(sk17(sk19(sk0)))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11331]) ).
cnf(p11463,plain,
( p102(sk19(sk0))
| p101(sk0)
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p11419,p478]) ).
cnf(p11483,plain,
( p102(sk19(sk0))
| p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11463]) ).
cnf(p11491,plain,
( p103(sk17(sk19(sk0)))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11483]) ).
cnf(c69,plain,
( ~ p101(X1)
| p102(X1)
| ~ p103(sk17(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p292,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| ~ p103(sk17(sk19(sk0)))
| p101(sk0) ),
inference(resolution,[status(thm)],[p219,c69]) ).
cnf(p11495,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| p101(sk0)
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p11491,p292]) ).
cnf(p11521,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11495]) ).
cnf(p11573,plain,
( ~ p101(sk19(sk0))
| p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11521]) ).
cnf(p11599,plain,
( p101(sk0)
| p102(sk19(sk0))
| p101(sk0) ),
inference(resolution,[status(thm)],[p11573,p220]) ).
cnf(p11609,plain,
( p102(sk19(sk0))
| p101(sk0) ),
inference(factoring,[status(thm)],[p11599]) ).
cnf(c77,plain,
( ~ p100(X1)
| p101(X1)
| ~ p102(sk19(X1))
| ~ r1(sk0,X1) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p185,plain,
( ~ p100(sk0)
| p101(sk0)
| ~ p102(sk19(sk0)) ),
inference(resolution,[status(thm)],[c77,c0]) ).
cnf(p11611,plain,
( ~ p100(sk0)
| p101(sk0)
| p101(sk0) ),
inference(resolution,[status(thm)],[p11609,p185]) ).
cnf(p11622,plain,
( ~ p100(sk0)
| p101(sk0) ),
inference(factoring,[status(thm)],[p11611]) ).
cnf(p11633,plain,
p101(sk0),
inference(resolution,[status(thm)],[p11622,c117]) ).
cnf(c116,plain,
~ p101(sk0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(p11634,plain,
$false,
inference(resolution,[status(thm)],[p11633,c116]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n016.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Thu Sep 24 00:17:48 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.08/7.38 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.08/7.38 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------