%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:24 PM UTC 2026
% Result : Theorem 5.16s 1.20s
% Output : Proof 5.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 1
% Syntax : Number of formulae : 18 ( 8 unt; 0 def)
% Number of atoms : 920 ( 0 equ)
% Maximal formula atoms : 225 ( 51 avg)
% Number of connectives : 1375 ( 473 ~; 484 |; 418 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 2 prp; 0-2 aty)
% Number of functors : 38 ( 38 usr; 28 con; 0-1 aty)
% Number of variables : 255 ( 9 sgn 202 !; 40 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f0,conjecture,
~ ? [X] :
~ ( ~ ( ~ ( ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& p1(X) )
| p2(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| ! [X] :
( p1(X)
| ~ ( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| p5(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| p5(Y)
| ~ r1(X,Y) )
| ~ ( ~ ( ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X) )
| p3(X)
| ~ r1(Y,X) )
| p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| ! [X] :
( p2(X)
| ~ ( ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X) )
| p4(X)
| ~ r1(Y,X) )
| p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| ! [X] :
( p3(X)
| ~ ( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X) )
| p5(X)
| ~ r1(Y,X) )
| p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| ! [X] :
( p4(X)
| ~ ( ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X) )
| p6(X)
| ~ r1(Y,X) )
| p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| ! [X] :
( p5(X)
| ~ ( ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f0_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ( ~ ( ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& p1(X) )
| p2(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| ! [X] :
( p1(X)
| ~ ( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y) )
| p2(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p1(Y)
| ~ ( ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| p5(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| p5(Y)
| ~ r1(X,Y) )
| ~ ( ~ ( ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X) )
| p3(X)
| ~ r1(Y,X) )
| p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| ! [X] :
( p2(X)
| ~ ( ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y) )
| p3(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ ( ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X) )
| p4(X)
| ~ r1(Y,X) )
| p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| ! [X] :
( p3(X)
| ~ ( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y) )
| p4(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p3(Y)
| ~ ( ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X) )
| p5(X)
| ~ r1(Y,X) )
| p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| ! [X] :
( p4(X)
| ~ ( ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y) )
| p5(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p4(Y)
| ~ ( ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X) )
| p6(X)
| ~ r1(Y,X) )
| p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| ! [X] :
( p5(X)
| ~ ( ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y) )
| p6(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p5(Y)
| ~ ( ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| ~ r1(X,Y) ) ) ),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
? [X] :
( ( ? [Y] :
( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y)
& ~ p2(Y)
& ~ p1(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& p1(X)
& ~ p2(X)
& r1(Y,X) )
& ~ p1(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y)
& r1(X,Y) )
| ? [Y] :
( p1(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) )
& p1(Y)
& ~ p2(Y)
& ? [X] :
( ~ p1(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ p1(Y)
| p2(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p1(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& ~ p5(Y)
& r1(X,Y) )
& ? [Y] :
( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& ~ p5(Y)
& r1(X,Y) )
& ( ? [Y] :
( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y)
& ~ p3(Y)
& ~ p2(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
& p2(X)
& ~ p3(X)
& r1(Y,X) )
& ~ p2(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y)
& r1(X,Y) )
| ? [Y] :
( p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) )
& p2(Y)
& ~ p3(Y)
& ? [X] :
( ~ p2(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p2(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ p2(Y)
| p3(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ p3(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y)
& ~ p4(Y)
& ~ p3(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
& p3(X)
& ~ p4(X)
& r1(Y,X) )
& ~ p3(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y)
& r1(X,Y) )
| ? [Y] :
( p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) )
& p3(Y)
& ~ p4(Y)
& ? [X] :
( ~ p3(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p3(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ p3(Y)
| p4(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p3(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ p4(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y)
& ~ p5(Y)
& ~ p4(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
& p4(X)
& ~ p5(X)
& r1(Y,X) )
& ~ p4(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y)
& r1(X,Y) )
| ? [Y] :
( p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) )
& p4(Y)
& ~ p5(Y)
& ? [X] :
( ~ p4(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p4(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ p4(Y)
| p5(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p4(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ p5(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y)
& ~ p6(Y)
& ~ p5(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
& p5(X)
& ~ p6(X)
& r1(Y,X) )
& ~ p5(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y)
& r1(X,Y) )
| ? [Y] :
( p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) )
& p5(Y)
& ~ p6(Y)
& ? [X] :
( ~ p5(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p5(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ p5(Y)
| p6(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p5(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ p6(Y)
| ~ r1(X,Y) ) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [Y,X] :
( ( ( p1(sk37)
& ( p1(X)
| ~ r1(sk37,X) )
& p1(sk37)
& ~ p2(sk37)
& ~ p1(sk37)
& ( p2(X)
| ~ r1(sk37,X) )
& p2(sk37)
& r1(sk0,sk37) )
| ( p1(sk36)
& ( p1(Y)
| ~ r1(sk36,Y) )
& p1(sk36)
& ~ p2(sk36)
& r1(sk35,sk36)
& ~ p1(sk35)
& ( p2(X)
| ~ r1(sk35,X) )
& p2(sk35)
& r1(sk0,sk35) )
| ( p1(sk33)
& ( p1(X)
| ~ r1(sk33,X) )
& p1(sk33)
& ~ p2(sk33)
& ~ p1(sk34)
& ( p2(Y)
| ~ r1(sk34,Y) )
& p2(sk34)
& r1(sk33,sk34)
& r1(sk0,sk33) )
| ~ p1(Y)
| ( ~ p1(sk32(Y))
& r1(Y,sk32(Y)) )
| ~ p1(Y)
| p2(Y)
| ~ r1(sk0,Y)
| p1(Y)
| ( ~ p2(sk31(Y))
& r1(Y,sk31(Y)) )
| ~ p2(Y)
| ~ r1(sk0,Y) )
& p5(sk30)
& ( p5(X)
| ~ r1(sk30,X) )
& ~ p5(sk30)
& r1(sk0,sk30)
& p5(sk29)
& ( p5(X)
| ~ r1(sk29,X) )
& ~ p5(sk29)
& r1(sk0,sk29)
& ( ( p2(sk28)
& ( p2(X)
| ~ r1(sk28,X) )
& p2(sk28)
& ~ p3(sk28)
& ~ p2(sk28)
& ( p3(X)
| ~ r1(sk28,X) )
& p3(sk28)
& r1(sk0,sk28) )
| ( p2(sk27)
& ( p2(Y)
| ~ r1(sk27,Y) )
& p2(sk27)
& ~ p3(sk27)
& r1(sk26,sk27)
& ~ p2(sk26)
& ( p3(X)
| ~ r1(sk26,X) )
& p3(sk26)
& r1(sk0,sk26) )
| ( p2(sk24)
& ( p2(X)
| ~ r1(sk24,X) )
& p2(sk24)
& ~ p3(sk24)
& ~ p2(sk25)
& ( p3(Y)
| ~ r1(sk25,Y) )
& p3(sk25)
& r1(sk24,sk25)
& r1(sk0,sk24) )
| ~ p2(Y)
| ( ~ p2(sk23(Y))
& r1(Y,sk23(Y)) )
| ~ p2(Y)
| p3(Y)
| ~ r1(sk0,Y)
| p2(Y)
| ( ~ p3(sk22(Y))
& r1(Y,sk22(Y)) )
| ~ p3(Y)
| ~ r1(sk0,Y) )
& ( ( p3(sk21)
& ( p3(X)
| ~ r1(sk21,X) )
& p3(sk21)
& ~ p4(sk21)
& ~ p3(sk21)
& ( p4(X)
| ~ r1(sk21,X) )
& p4(sk21)
& r1(sk0,sk21) )
| ( p3(sk20)
& ( p3(Y)
| ~ r1(sk20,Y) )
& p3(sk20)
& ~ p4(sk20)
& r1(sk19,sk20)
& ~ p3(sk19)
& ( p4(X)
| ~ r1(sk19,X) )
& p4(sk19)
& r1(sk0,sk19) )
| ( p3(sk17)
& ( p3(X)
| ~ r1(sk17,X) )
& p3(sk17)
& ~ p4(sk17)
& ~ p3(sk18)
& ( p4(Y)
| ~ r1(sk18,Y) )
& p4(sk18)
& r1(sk17,sk18)
& r1(sk0,sk17) )
| ~ p3(Y)
| ( ~ p3(sk16(Y))
& r1(Y,sk16(Y)) )
| ~ p3(Y)
| p4(Y)
| ~ r1(sk0,Y)
| p3(Y)
| ( ~ p4(sk15(Y))
& r1(Y,sk15(Y)) )
| ~ p4(Y)
| ~ r1(sk0,Y) )
& ( ( p4(sk14)
& ( p4(X)
| ~ r1(sk14,X) )
& p4(sk14)
& ~ p5(sk14)
& ~ p4(sk14)
& ( p5(X)
| ~ r1(sk14,X) )
& p5(sk14)
& r1(sk0,sk14) )
| ( p4(sk13)
& ( p4(Y)
| ~ r1(sk13,Y) )
& p4(sk13)
& ~ p5(sk13)
& r1(sk12,sk13)
& ~ p4(sk12)
& ( p5(X)
| ~ r1(sk12,X) )
& p5(sk12)
& r1(sk0,sk12) )
| ( p4(sk10)
& ( p4(X)
| ~ r1(sk10,X) )
& p4(sk10)
& ~ p5(sk10)
& ~ p4(sk11)
& ( p5(Y)
| ~ r1(sk11,Y) )
& p5(sk11)
& r1(sk10,sk11)
& r1(sk0,sk10) )
| ~ p4(Y)
| ( ~ p4(sk9(Y))
& r1(Y,sk9(Y)) )
| ~ p4(Y)
| p5(Y)
| ~ r1(sk0,Y)
| p4(Y)
| ( ~ p5(sk8(Y))
& r1(Y,sk8(Y)) )
| ~ p5(Y)
| ~ r1(sk0,Y) )
& ( ( p5(sk7)
& ( p5(X)
| ~ r1(sk7,X) )
& p5(sk7)
& ~ p6(sk7)
& ~ p5(sk7)
& ( p6(X)
| ~ r1(sk7,X) )
& p6(sk7)
& r1(sk0,sk7) )
| ( p5(sk6)
& ( p5(Y)
| ~ r1(sk6,Y) )
& p5(sk6)
& ~ p6(sk6)
& r1(sk5,sk6)
& ~ p5(sk5)
& ( p6(X)
| ~ r1(sk5,X) )
& p6(sk5)
& r1(sk0,sk5) )
| ( p5(sk3)
& ( p5(X)
| ~ r1(sk3,X) )
& p5(sk3)
& ~ p6(sk3)
& ~ p5(sk4)
& ( p6(Y)
| ~ r1(sk4,Y) )
& p6(sk4)
& r1(sk3,sk4)
& r1(sk0,sk3) )
| ~ p5(Y)
| ( ~ p5(sk2(Y))
& r1(Y,sk2(Y)) )
| ~ p5(Y)
| p6(Y)
| ~ r1(sk0,Y)
| p5(Y)
| ( ~ p6(sk1(Y))
& r1(Y,sk1(Y)) )
| ~ p6(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,sk21,sk22,sk23,sk24,sk25,sk26,sk27,sk28,sk29,sk30,sk31,sk32,sk33,sk34,sk35,sk36,sk37])],[f0_nnf]) ).
cnf(c669,plain,
( def180(X1,X0)
| ~ def223(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(c672,plain,
def223(X1,X0),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p708,plain,
def180(X0,X1),
inference(resolution,[status(thm)],[c669,c672]) ).
cnf(c541,plain,
( def179(X0)
| ~ def180(X1,X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p709,plain,
def179(X0),
inference(resolution,[status(thm)],[p708,c541]) ).
cnf(c538,plain,
( def178(X0)
| ~ def179(X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p712,plain,
def178(X0),
inference(resolution,[status(thm)],[p709,c538]) ).
cnf(c535,plain,
( p5(sk30)
| ~ def178(X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p716,plain,
p5(sk30),
inference(resolution,[status(thm)],[p712,c535]) ).
cnf(c537,plain,
( def176
| ~ def179(X0) ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p711,plain,
def176,
inference(resolution,[status(thm)],[p709,c537]) ).
cnf(c529,plain,
( ~ p5(sk30)
| ~ def176 ),
inference(cnf_transformation,[status(esa),new_symbols(definition,[def0,def1,def2,def3,def4,def5,def6,def7,def8,def9,def10,def11,def12,def13,def14,def15,def16,def17,def18,def19,def20,def21,def22,def23,def24,def25,def26,def27,def28,def29,def30,def31,def32,def33,def34,def35,def36,def37,def38,def39,def40,def41,def42,def43,def44,def45,def46,def47,def48,def49,def50,def51,def52,def53,def54,def55,def56,def57,def58,def59,def60,def61,def62,def63,def64,def65,def66,def67,def68,def69,def70,def71,def72,def73,def74,def75,def76,def77,def78,def79,def80,def81,def82,def83,def84,def85,def86,def87,def88,def89,def90,def91,def92,def93,def94,def95,def96,def97,def98,def99,def100,def101,def102,def103,def104,def105,def106,def107,def108,def109,def110,def111,def112,def113,def114,def115,def116,def117,def118,def119,def120,def121,def122,def123,def124,def125,def126,def127,def128,def129,def130,def131,def132,def133,def134,def135,def136,def137,def138,def139,def140,def141,def142,def143,def144,def145,def146,def147,def148,def149,def150,def151,def152,def153,def154,def155,def156,def157,def158,def159,def160,def161,def162,def163,def164,def165,def166,def167,def168,def169,def170,def171,def172,def173,def174,def175,def176,def177,def178,def179,def180,def181,def182,def183,def184,def185,def186,def187,def188,def189,def190,def191,def192,def193,def194,def195,def196,def197,def198,def199,def200,def201,def202,def203,def204,def205,def206,def207,def208,def209,def210,def211,def212,def213,def214,def215,def216,def217,def218,def219,def220,def221,def222,def223])],[f0_sk]) ).
cnf(p713,plain,
~ p5(sk30),
inference(resolution,[status(thm)],[p711,c529]) ).
cnf(p726,plain,
$false,
inference(resolution,[status(thm)],[p716,p713]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL644+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n016.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 23:59:27 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.16/1.20 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.16/1.20 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------