%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n014.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:25 PM UTC 2026
% Result : Theorem 144.38s 26.36s
% Output : Proof 144.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 1
% Syntax : Number of formulae : 26 ( 12 unt; 0 def)
% Number of atoms : 2652 ( 0 equ)
% Maximal formula atoms : 655 ( 102 avg)
% Number of connectives : 3983 (1357 ~;1408 |;1218 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 46 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 26 usr; 2 prp; 0-2 aty)
% Number of functors : 108 ( 108 usr; 78 con; 0-1 aty)
% Number of variables : 721 ( 17 sgn 582 !; 110 ?)
% 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] :
( ~ ( 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) ) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) ) )
| p15(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) ) )
| p15(Y)
| ~ r1(X,Y) )
| ~ ( ~ ( ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X) )
| p7(X)
| ~ r1(Y,X) )
| p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| ! [X] :
( p6(X)
| ~ ( ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p7(X)
& ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X) )
| p8(X)
| ~ r1(Y,X) )
| p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| ! [X] :
( p7(X)
| ~ ( ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p8(X)
& ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X) )
| p9(X)
| ~ r1(Y,X) )
| p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| ! [X] :
( p8(X)
| ~ ( ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p9(X)
& ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X) )
| p10(X)
| ~ r1(Y,X) )
| p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| ! [X] :
( p9(X)
| ~ ( ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p10(X)
& ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X) )
| p11(X)
| ~ r1(Y,X) )
| p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| ! [X] :
( p10(X)
| ~ ( ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p11(X)
& ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X) )
| p12(X)
| ~ r1(Y,X) )
| p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| ! [X] :
( p11(X)
| ~ ( ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p12(X)
& ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X) )
| p13(X)
| ~ r1(Y,X) )
| p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| ! [X] :
( p12(X)
| ~ ( ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p13(X)
& ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X) )
| p14(X)
| ~ r1(Y,X) )
| p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| ! [X] :
( p13(X)
| ~ ( ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p14(X)
& ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X) )
| p15(X)
| ~ r1(Y,X) )
| p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| ! [X] :
( p14(X)
| ~ ( ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p15(X)
& ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X) )
| p16(X)
| ~ r1(Y,X) )
| p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| ! [X] :
( p15(X)
| ~ ( ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(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] :
( ~ ( 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) ) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) ) )
| p15(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) ) )
| p15(Y)
| ~ r1(X,Y) )
| ~ ( ~ ( ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X) )
| p7(X)
| ~ r1(Y,X) )
| p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| ! [X] :
( p6(X)
| ~ ( ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y) )
| p7(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p6(Y)
| ~ ( ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p7(X)
& ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X) )
| p8(X)
| ~ r1(Y,X) )
| p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| ! [X] :
( p7(X)
| ~ ( ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y) )
| p8(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p7(Y)
| ~ ( ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p8(X)
& ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X) )
| p9(X)
| ~ r1(Y,X) )
| p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| ! [X] :
( p8(X)
| ~ ( ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y) )
| p9(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p8(Y)
| ~ ( ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p9(X)
& ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X) )
| p10(X)
| ~ r1(Y,X) )
| p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| ! [X] :
( p9(X)
| ~ ( ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y) )
| p10(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p9(Y)
| ~ ( ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p10(X)
& ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X) )
| p11(X)
| ~ r1(Y,X) )
| p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| ! [X] :
( p10(X)
| ~ ( ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y) )
| p11(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p10(Y)
| ~ ( ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p11(X)
& ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X) )
| p12(X)
| ~ r1(Y,X) )
| p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| ! [X] :
( p11(X)
| ~ ( ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y) )
| p12(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p11(Y)
| ~ ( ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p12(X)
& ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X) )
| p13(X)
| ~ r1(Y,X) )
| p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| ! [X] :
( p12(X)
| ~ ( ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y) )
| p13(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p12(Y)
| ~ ( ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p13(X)
& ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X) )
| p14(X)
| ~ r1(Y,X) )
| p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| ! [X] :
( p13(X)
| ~ ( ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y) )
| p14(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p13(Y)
| ~ ( ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p14(X)
& ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X) )
| p15(X)
| ~ r1(Y,X) )
| p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| ! [X] :
( p14(X)
| ~ ( ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y) )
| p15(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p14(Y)
| ~ ( ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p15(X)
& ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X) )
| p16(X)
| ~ r1(Y,X) )
| p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| ! [X] :
( p15(X)
| ~ ( ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y) )
| p16(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p15(Y)
| ~ ( ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(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] :
( 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) ) )
& ? [Y] :
( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& ~ p15(Y)
& r1(X,Y) )
& ? [Y] :
( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& ~ p15(Y)
& r1(X,Y) )
& ( ? [Y] :
( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y)
& ~ p7(Y)
& ~ p6(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
& p6(X)
& ~ p7(X)
& r1(Y,X) )
& ~ p6(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y)
& r1(X,Y) )
| ? [Y] :
( p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) )
& p6(Y)
& ~ p7(Y)
& ? [X] :
( ~ p6(X)
& ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p6(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ p6(Y)
| p7(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p6(Y)
| ? [X] :
( ~ p7(X)
& r1(Y,X) )
| ~ p7(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y)
& ~ p8(Y)
& ~ p7(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p7(X)
& ! [Y] :
( p7(Y)
| ~ r1(X,Y) )
& p7(X)
& ~ p8(X)
& r1(Y,X) )
& ~ p7(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y)
& r1(X,Y) )
| ? [Y] :
( p7(Y)
& ! [X] :
( p7(X)
| ~ r1(Y,X) )
& p7(Y)
& ~ p8(Y)
& ? [X] :
( ~ p7(X)
& ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p7(Y)
| ? [X] :
( ~ p7(X)
& r1(Y,X) )
| ~ p7(Y)
| p8(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p7(Y)
| ? [X] :
( ~ p8(X)
& r1(Y,X) )
| ~ p8(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y)
& ~ p9(Y)
& ~ p8(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p8(X)
& ! [Y] :
( p8(Y)
| ~ r1(X,Y) )
& p8(X)
& ~ p9(X)
& r1(Y,X) )
& ~ p8(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y)
& r1(X,Y) )
| ? [Y] :
( p8(Y)
& ! [X] :
( p8(X)
| ~ r1(Y,X) )
& p8(Y)
& ~ p9(Y)
& ? [X] :
( ~ p8(X)
& ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p8(Y)
| ? [X] :
( ~ p8(X)
& r1(Y,X) )
| ~ p8(Y)
| p9(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p8(Y)
| ? [X] :
( ~ p9(X)
& r1(Y,X) )
| ~ p9(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y)
& ~ p10(Y)
& ~ p9(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p9(X)
& ! [Y] :
( p9(Y)
| ~ r1(X,Y) )
& p9(X)
& ~ p10(X)
& r1(Y,X) )
& ~ p9(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y)
& r1(X,Y) )
| ? [Y] :
( p9(Y)
& ! [X] :
( p9(X)
| ~ r1(Y,X) )
& p9(Y)
& ~ p10(Y)
& ? [X] :
( ~ p9(X)
& ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p9(Y)
| ? [X] :
( ~ p9(X)
& r1(Y,X) )
| ~ p9(Y)
| p10(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p9(Y)
| ? [X] :
( ~ p10(X)
& r1(Y,X) )
| ~ p10(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y)
& ~ p11(Y)
& ~ p10(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p10(X)
& ! [Y] :
( p10(Y)
| ~ r1(X,Y) )
& p10(X)
& ~ p11(X)
& r1(Y,X) )
& ~ p10(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y)
& r1(X,Y) )
| ? [Y] :
( p10(Y)
& ! [X] :
( p10(X)
| ~ r1(Y,X) )
& p10(Y)
& ~ p11(Y)
& ? [X] :
( ~ p10(X)
& ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p10(Y)
| ? [X] :
( ~ p10(X)
& r1(Y,X) )
| ~ p10(Y)
| p11(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p10(Y)
| ? [X] :
( ~ p11(X)
& r1(Y,X) )
| ~ p11(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y)
& ~ p12(Y)
& ~ p11(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p11(X)
& ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
& p11(X)
& ~ p12(X)
& r1(Y,X) )
& ~ p11(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y)
& r1(X,Y) )
| ? [Y] :
( p11(Y)
& ! [X] :
( p11(X)
| ~ r1(Y,X) )
& p11(Y)
& ~ p12(Y)
& ? [X] :
( ~ p11(X)
& ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p11(Y)
| ? [X] :
( ~ p11(X)
& r1(Y,X) )
| ~ p11(Y)
| p12(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p11(Y)
| ? [X] :
( ~ p12(X)
& r1(Y,X) )
| ~ p12(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y)
& ~ p13(Y)
& ~ p12(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p12(X)
& ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
& p12(X)
& ~ p13(X)
& r1(Y,X) )
& ~ p12(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y)
& r1(X,Y) )
| ? [Y] :
( p12(Y)
& ! [X] :
( p12(X)
| ~ r1(Y,X) )
& p12(Y)
& ~ p13(Y)
& ? [X] :
( ~ p12(X)
& ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p12(Y)
| ? [X] :
( ~ p12(X)
& r1(Y,X) )
| ~ p12(Y)
| p13(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p12(Y)
| ? [X] :
( ~ p13(X)
& r1(Y,X) )
| ~ p13(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y)
& ~ p14(Y)
& ~ p13(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p13(X)
& ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
& p13(X)
& ~ p14(X)
& r1(Y,X) )
& ~ p13(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y)
& r1(X,Y) )
| ? [Y] :
( p13(Y)
& ! [X] :
( p13(X)
| ~ r1(Y,X) )
& p13(Y)
& ~ p14(Y)
& ? [X] :
( ~ p13(X)
& ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p13(Y)
| ? [X] :
( ~ p13(X)
& r1(Y,X) )
| ~ p13(Y)
| p14(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p13(Y)
| ? [X] :
( ~ p14(X)
& r1(Y,X) )
| ~ p14(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y)
& ~ p15(Y)
& ~ p14(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p14(X)
& ! [Y] :
( p14(Y)
| ~ r1(X,Y) )
& p14(X)
& ~ p15(X)
& r1(Y,X) )
& ~ p14(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y)
& r1(X,Y) )
| ? [Y] :
( p14(Y)
& ! [X] :
( p14(X)
| ~ r1(Y,X) )
& p14(Y)
& ~ p15(Y)
& ? [X] :
( ~ p14(X)
& ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p14(Y)
| ? [X] :
( ~ p14(X)
& r1(Y,X) )
| ~ p14(Y)
| p15(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p14(Y)
| ? [X] :
( ~ p15(X)
& r1(Y,X) )
| ~ p15(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y)
& ~ p16(Y)
& ~ p15(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p15(X)
& ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
& p15(X)
& ~ p16(X)
& r1(Y,X) )
& ~ p15(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y)
& r1(X,Y) )
| ? [Y] :
( p15(Y)
& ! [X] :
( p15(X)
| ~ r1(Y,X) )
& p15(Y)
& ~ p16(Y)
& ? [X] :
( ~ p15(X)
& ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p15(Y)
| ? [X] :
( ~ p15(X)
& r1(Y,X) )
| ~ p15(Y)
| p16(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p15(Y)
| ? [X] :
( ~ p16(X)
& r1(Y,X) )
| ~ p16(Y)
| ~ r1(X,Y) ) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [Y,X] :
( ( ( p1(sk107)
& ( p1(X)
| ~ r1(sk107,X) )
& p1(sk107)
& ~ p2(sk107)
& ~ p1(sk107)
& ( p2(X)
| ~ r1(sk107,X) )
& p2(sk107)
& r1(sk0,sk107) )
| ( p1(sk106)
& ( p1(Y)
| ~ r1(sk106,Y) )
& p1(sk106)
& ~ p2(sk106)
& r1(sk105,sk106)
& ~ p1(sk105)
& ( p2(X)
| ~ r1(sk105,X) )
& p2(sk105)
& r1(sk0,sk105) )
| ( p1(sk103)
& ( p1(X)
| ~ r1(sk103,X) )
& p1(sk103)
& ~ p2(sk103)
& ~ p1(sk104)
& ( p2(Y)
| ~ r1(sk104,Y) )
& p2(sk104)
& r1(sk103,sk104)
& r1(sk0,sk103) )
| ~ p1(Y)
| ( ~ p1(sk102(Y))
& r1(Y,sk102(Y)) )
| ~ p1(Y)
| p2(Y)
| ~ r1(sk0,Y)
| p1(Y)
| ( ~ p2(sk101(Y))
& r1(Y,sk101(Y)) )
| ~ p2(Y)
| ~ r1(sk0,Y) )
& ( ( p2(sk100)
& ( p2(X)
| ~ r1(sk100,X) )
& p2(sk100)
& ~ p3(sk100)
& ~ p2(sk100)
& ( p3(X)
| ~ r1(sk100,X) )
& p3(sk100)
& r1(sk0,sk100) )
| ( p2(sk99)
& ( p2(Y)
| ~ r1(sk99,Y) )
& p2(sk99)
& ~ p3(sk99)
& r1(sk98,sk99)
& ~ p2(sk98)
& ( p3(X)
| ~ r1(sk98,X) )
& p3(sk98)
& r1(sk0,sk98) )
| ( p2(sk96)
& ( p2(X)
| ~ r1(sk96,X) )
& p2(sk96)
& ~ p3(sk96)
& ~ p2(sk97)
& ( p3(Y)
| ~ r1(sk97,Y) )
& p3(sk97)
& r1(sk96,sk97)
& r1(sk0,sk96) )
| ~ p2(Y)
| ( ~ p2(sk95(Y))
& r1(Y,sk95(Y)) )
| ~ p2(Y)
| p3(Y)
| ~ r1(sk0,Y)
| p2(Y)
| ( ~ p3(sk94(Y))
& r1(Y,sk94(Y)) )
| ~ p3(Y)
| ~ r1(sk0,Y) )
& ( ( p3(sk93)
& ( p3(X)
| ~ r1(sk93,X) )
& p3(sk93)
& ~ p4(sk93)
& ~ p3(sk93)
& ( p4(X)
| ~ r1(sk93,X) )
& p4(sk93)
& r1(sk0,sk93) )
| ( p3(sk92)
& ( p3(Y)
| ~ r1(sk92,Y) )
& p3(sk92)
& ~ p4(sk92)
& r1(sk91,sk92)
& ~ p3(sk91)
& ( p4(X)
| ~ r1(sk91,X) )
& p4(sk91)
& r1(sk0,sk91) )
| ( p3(sk89)
& ( p3(X)
| ~ r1(sk89,X) )
& p3(sk89)
& ~ p4(sk89)
& ~ p3(sk90)
& ( p4(Y)
| ~ r1(sk90,Y) )
& p4(sk90)
& r1(sk89,sk90)
& r1(sk0,sk89) )
| ~ p3(Y)
| ( ~ p3(sk88(Y))
& r1(Y,sk88(Y)) )
| ~ p3(Y)
| p4(Y)
| ~ r1(sk0,Y)
| p3(Y)
| ( ~ p4(sk87(Y))
& r1(Y,sk87(Y)) )
| ~ p4(Y)
| ~ r1(sk0,Y) )
& ( ( p4(sk86)
& ( p4(X)
| ~ r1(sk86,X) )
& p4(sk86)
& ~ p5(sk86)
& ~ p4(sk86)
& ( p5(X)
| ~ r1(sk86,X) )
& p5(sk86)
& r1(sk0,sk86) )
| ( p4(sk85)
& ( p4(Y)
| ~ r1(sk85,Y) )
& p4(sk85)
& ~ p5(sk85)
& r1(sk84,sk85)
& ~ p4(sk84)
& ( p5(X)
| ~ r1(sk84,X) )
& p5(sk84)
& r1(sk0,sk84) )
| ( p4(sk82)
& ( p4(X)
| ~ r1(sk82,X) )
& p4(sk82)
& ~ p5(sk82)
& ~ p4(sk83)
& ( p5(Y)
| ~ r1(sk83,Y) )
& p5(sk83)
& r1(sk82,sk83)
& r1(sk0,sk82) )
| ~ p4(Y)
| ( ~ p4(sk81(Y))
& r1(Y,sk81(Y)) )
| ~ p4(Y)
| p5(Y)
| ~ r1(sk0,Y)
| p4(Y)
| ( ~ p5(sk80(Y))
& r1(Y,sk80(Y)) )
| ~ p5(Y)
| ~ r1(sk0,Y) )
& ( ( p5(sk79)
& ( p5(X)
| ~ r1(sk79,X) )
& p5(sk79)
& ~ p6(sk79)
& ~ p5(sk79)
& ( p6(X)
| ~ r1(sk79,X) )
& p6(sk79)
& r1(sk0,sk79) )
| ( p5(sk78)
& ( p5(Y)
| ~ r1(sk78,Y) )
& p5(sk78)
& ~ p6(sk78)
& r1(sk77,sk78)
& ~ p5(sk77)
& ( p6(X)
| ~ r1(sk77,X) )
& p6(sk77)
& r1(sk0,sk77) )
| ( p5(sk75)
& ( p5(X)
| ~ r1(sk75,X) )
& p5(sk75)
& ~ p6(sk75)
& ~ p5(sk76)
& ( p6(Y)
| ~ r1(sk76,Y) )
& p6(sk76)
& r1(sk75,sk76)
& r1(sk0,sk75) )
| ~ p5(Y)
| ( ~ p5(sk74(Y))
& r1(Y,sk74(Y)) )
| ~ p5(Y)
| p6(Y)
| ~ r1(sk0,Y)
| p5(Y)
| ( ~ p6(sk73(Y))
& r1(Y,sk73(Y)) )
| ~ p6(Y)
| ~ r1(sk0,Y) )
& p15(sk72)
& ( p15(X)
| ~ r1(sk72,X) )
& ~ p15(sk72)
& r1(sk0,sk72)
& p15(sk71)
& ( p15(X)
| ~ r1(sk71,X) )
& ~ p15(sk71)
& r1(sk0,sk71)
& ( ( p6(sk70)
& ( p6(X)
| ~ r1(sk70,X) )
& p6(sk70)
& ~ p7(sk70)
& ~ p6(sk70)
& ( p7(X)
| ~ r1(sk70,X) )
& p7(sk70)
& r1(sk0,sk70) )
| ( p6(sk69)
& ( p6(Y)
| ~ r1(sk69,Y) )
& p6(sk69)
& ~ p7(sk69)
& r1(sk68,sk69)
& ~ p6(sk68)
& ( p7(X)
| ~ r1(sk68,X) )
& p7(sk68)
& r1(sk0,sk68) )
| ( p6(sk66)
& ( p6(X)
| ~ r1(sk66,X) )
& p6(sk66)
& ~ p7(sk66)
& ~ p6(sk67)
& ( p7(Y)
| ~ r1(sk67,Y) )
& p7(sk67)
& r1(sk66,sk67)
& r1(sk0,sk66) )
| ~ p6(Y)
| ( ~ p6(sk65(Y))
& r1(Y,sk65(Y)) )
| ~ p6(Y)
| p7(Y)
| ~ r1(sk0,Y)
| p6(Y)
| ( ~ p7(sk64(Y))
& r1(Y,sk64(Y)) )
| ~ p7(Y)
| ~ r1(sk0,Y) )
& ( ( p7(sk63)
& ( p7(X)
| ~ r1(sk63,X) )
& p7(sk63)
& ~ p8(sk63)
& ~ p7(sk63)
& ( p8(X)
| ~ r1(sk63,X) )
& p8(sk63)
& r1(sk0,sk63) )
| ( p7(sk62)
& ( p7(Y)
| ~ r1(sk62,Y) )
& p7(sk62)
& ~ p8(sk62)
& r1(sk61,sk62)
& ~ p7(sk61)
& ( p8(X)
| ~ r1(sk61,X) )
& p8(sk61)
& r1(sk0,sk61) )
| ( p7(sk59)
& ( p7(X)
| ~ r1(sk59,X) )
& p7(sk59)
& ~ p8(sk59)
& ~ p7(sk60)
& ( p8(Y)
| ~ r1(sk60,Y) )
& p8(sk60)
& r1(sk59,sk60)
& r1(sk0,sk59) )
| ~ p7(Y)
| ( ~ p7(sk58(Y))
& r1(Y,sk58(Y)) )
| ~ p7(Y)
| p8(Y)
| ~ r1(sk0,Y)
| p7(Y)
| ( ~ p8(sk57(Y))
& r1(Y,sk57(Y)) )
| ~ p8(Y)
| ~ r1(sk0,Y) )
& ( ( p8(sk56)
& ( p8(X)
| ~ r1(sk56,X) )
& p8(sk56)
& ~ p9(sk56)
& ~ p8(sk56)
& ( p9(X)
| ~ r1(sk56,X) )
& p9(sk56)
& r1(sk0,sk56) )
| ( p8(sk55)
& ( p8(Y)
| ~ r1(sk55,Y) )
& p8(sk55)
& ~ p9(sk55)
& r1(sk54,sk55)
& ~ p8(sk54)
& ( p9(X)
| ~ r1(sk54,X) )
& p9(sk54)
& r1(sk0,sk54) )
| ( p8(sk52)
& ( p8(X)
| ~ r1(sk52,X) )
& p8(sk52)
& ~ p9(sk52)
& ~ p8(sk53)
& ( p9(Y)
| ~ r1(sk53,Y) )
& p9(sk53)
& r1(sk52,sk53)
& r1(sk0,sk52) )
| ~ p8(Y)
| ( ~ p8(sk51(Y))
& r1(Y,sk51(Y)) )
| ~ p8(Y)
| p9(Y)
| ~ r1(sk0,Y)
| p8(Y)
| ( ~ p9(sk50(Y))
& r1(Y,sk50(Y)) )
| ~ p9(Y)
| ~ r1(sk0,Y) )
& ( ( p9(sk49)
& ( p9(X)
| ~ r1(sk49,X) )
& p9(sk49)
& ~ p10(sk49)
& ~ p9(sk49)
& ( p10(X)
| ~ r1(sk49,X) )
& p10(sk49)
& r1(sk0,sk49) )
| ( p9(sk48)
& ( p9(Y)
| ~ r1(sk48,Y) )
& p9(sk48)
& ~ p10(sk48)
& r1(sk47,sk48)
& ~ p9(sk47)
& ( p10(X)
| ~ r1(sk47,X) )
& p10(sk47)
& r1(sk0,sk47) )
| ( p9(sk45)
& ( p9(X)
| ~ r1(sk45,X) )
& p9(sk45)
& ~ p10(sk45)
& ~ p9(sk46)
& ( p10(Y)
| ~ r1(sk46,Y) )
& p10(sk46)
& r1(sk45,sk46)
& r1(sk0,sk45) )
| ~ p9(Y)
| ( ~ p9(sk44(Y))
& r1(Y,sk44(Y)) )
| ~ p9(Y)
| p10(Y)
| ~ r1(sk0,Y)
| p9(Y)
| ( ~ p10(sk43(Y))
& r1(Y,sk43(Y)) )
| ~ p10(Y)
| ~ r1(sk0,Y) )
& ( ( p10(sk42)
& ( p10(X)
| ~ r1(sk42,X) )
& p10(sk42)
& ~ p11(sk42)
& ~ p10(sk42)
& ( p11(X)
| ~ r1(sk42,X) )
& p11(sk42)
& r1(sk0,sk42) )
| ( p10(sk41)
& ( p10(Y)
| ~ r1(sk41,Y) )
& p10(sk41)
& ~ p11(sk41)
& r1(sk40,sk41)
& ~ p10(sk40)
& ( p11(X)
| ~ r1(sk40,X) )
& p11(sk40)
& r1(sk0,sk40) )
| ( p10(sk38)
& ( p10(X)
| ~ r1(sk38,X) )
& p10(sk38)
& ~ p11(sk38)
& ~ p10(sk39)
& ( p11(Y)
| ~ r1(sk39,Y) )
& p11(sk39)
& r1(sk38,sk39)
& r1(sk0,sk38) )
| ~ p10(Y)
| ( ~ p10(sk37(Y))
& r1(Y,sk37(Y)) )
| ~ p10(Y)
| p11(Y)
| ~ r1(sk0,Y)
| p10(Y)
| ( ~ p11(sk36(Y))
& r1(Y,sk36(Y)) )
| ~ p11(Y)
| ~ r1(sk0,Y) )
& ( ( p11(sk35)
& ( p11(X)
| ~ r1(sk35,X) )
& p11(sk35)
& ~ p12(sk35)
& ~ p11(sk35)
& ( p12(X)
| ~ r1(sk35,X) )
& p12(sk35)
& r1(sk0,sk35) )
| ( p11(sk34)
& ( p11(Y)
| ~ r1(sk34,Y) )
& p11(sk34)
& ~ p12(sk34)
& r1(sk33,sk34)
& ~ p11(sk33)
& ( p12(X)
| ~ r1(sk33,X) )
& p12(sk33)
& r1(sk0,sk33) )
| ( p11(sk31)
& ( p11(X)
| ~ r1(sk31,X) )
& p11(sk31)
& ~ p12(sk31)
& ~ p11(sk32)
& ( p12(Y)
| ~ r1(sk32,Y) )
& p12(sk32)
& r1(sk31,sk32)
& r1(sk0,sk31) )
| ~ p11(Y)
| ( ~ p11(sk30(Y))
& r1(Y,sk30(Y)) )
| ~ p11(Y)
| p12(Y)
| ~ r1(sk0,Y)
| p11(Y)
| ( ~ p12(sk29(Y))
& r1(Y,sk29(Y)) )
| ~ p12(Y)
| ~ r1(sk0,Y) )
& ( ( p12(sk28)
& ( p12(X)
| ~ r1(sk28,X) )
& p12(sk28)
& ~ p13(sk28)
& ~ p12(sk28)
& ( p13(X)
| ~ r1(sk28,X) )
& p13(sk28)
& r1(sk0,sk28) )
| ( p12(sk27)
& ( p12(Y)
| ~ r1(sk27,Y) )
& p12(sk27)
& ~ p13(sk27)
& r1(sk26,sk27)
& ~ p12(sk26)
& ( p13(X)
| ~ r1(sk26,X) )
& p13(sk26)
& r1(sk0,sk26) )
| ( p12(sk24)
& ( p12(X)
| ~ r1(sk24,X) )
& p12(sk24)
& ~ p13(sk24)
& ~ p12(sk25)
& ( p13(Y)
| ~ r1(sk25,Y) )
& p13(sk25)
& r1(sk24,sk25)
& r1(sk0,sk24) )
| ~ p12(Y)
| ( ~ p12(sk23(Y))
& r1(Y,sk23(Y)) )
| ~ p12(Y)
| p13(Y)
| ~ r1(sk0,Y)
| p12(Y)
| ( ~ p13(sk22(Y))
& r1(Y,sk22(Y)) )
| ~ p13(Y)
| ~ r1(sk0,Y) )
& ( ( p13(sk21)
& ( p13(X)
| ~ r1(sk21,X) )
& p13(sk21)
& ~ p14(sk21)
& ~ p13(sk21)
& ( p14(X)
| ~ r1(sk21,X) )
& p14(sk21)
& r1(sk0,sk21) )
| ( p13(sk20)
& ( p13(Y)
| ~ r1(sk20,Y) )
& p13(sk20)
& ~ p14(sk20)
& r1(sk19,sk20)
& ~ p13(sk19)
& ( p14(X)
| ~ r1(sk19,X) )
& p14(sk19)
& r1(sk0,sk19) )
| ( p13(sk17)
& ( p13(X)
| ~ r1(sk17,X) )
& p13(sk17)
& ~ p14(sk17)
& ~ p13(sk18)
& ( p14(Y)
| ~ r1(sk18,Y) )
& p14(sk18)
& r1(sk17,sk18)
& r1(sk0,sk17) )
| ~ p13(Y)
| ( ~ p13(sk16(Y))
& r1(Y,sk16(Y)) )
| ~ p13(Y)
| p14(Y)
| ~ r1(sk0,Y)
| p13(Y)
| ( ~ p14(sk15(Y))
& r1(Y,sk15(Y)) )
| ~ p14(Y)
| ~ r1(sk0,Y) )
& ( ( p14(sk14)
& ( p14(X)
| ~ r1(sk14,X) )
& p14(sk14)
& ~ p15(sk14)
& ~ p14(sk14)
& ( p15(X)
| ~ r1(sk14,X) )
& p15(sk14)
& r1(sk0,sk14) )
| ( p14(sk13)
& ( p14(Y)
| ~ r1(sk13,Y) )
& p14(sk13)
& ~ p15(sk13)
& r1(sk12,sk13)
& ~ p14(sk12)
& ( p15(X)
| ~ r1(sk12,X) )
& p15(sk12)
& r1(sk0,sk12) )
| ( p14(sk10)
& ( p14(X)
| ~ r1(sk10,X) )
& p14(sk10)
& ~ p15(sk10)
& ~ p14(sk11)
& ( p15(Y)
| ~ r1(sk11,Y) )
& p15(sk11)
& r1(sk10,sk11)
& r1(sk0,sk10) )
| ~ p14(Y)
| ( ~ p14(sk9(Y))
& r1(Y,sk9(Y)) )
| ~ p14(Y)
| p15(Y)
| ~ r1(sk0,Y)
| p14(Y)
| ( ~ p15(sk8(Y))
& r1(Y,sk8(Y)) )
| ~ p15(Y)
| ~ r1(sk0,Y) )
& ( ( p15(sk7)
& ( p15(X)
| ~ r1(sk7,X) )
& p15(sk7)
& ~ p16(sk7)
& ~ p15(sk7)
& ( p16(X)
| ~ r1(sk7,X) )
& p16(sk7)
& r1(sk0,sk7) )
| ( p15(sk6)
& ( p15(Y)
| ~ r1(sk6,Y) )
& p15(sk6)
& ~ p16(sk6)
& r1(sk5,sk6)
& ~ p15(sk5)
& ( p16(X)
| ~ r1(sk5,X) )
& p16(sk5)
& r1(sk0,sk5) )
| ( p15(sk3)
& ( p15(X)
| ~ r1(sk3,X) )
& p15(sk3)
& ~ p16(sk3)
& ~ p15(sk4)
& ( p16(Y)
| ~ r1(sk4,Y) )
& p16(sk4)
& r1(sk3,sk4)
& r1(sk0,sk3) )
| ~ p15(Y)
| ( ~ p15(sk2(Y))
& r1(Y,sk2(Y)) )
| ~ p15(Y)
| p16(Y)
| ~ r1(sk0,Y)
| p15(Y)
| ( ~ p16(sk1(Y))
& r1(Y,sk1(Y)) )
| ~ p16(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,sk38,sk39,sk40,sk41,sk42,sk43,sk44,sk45,sk46,sk47,sk48,sk49,sk50,sk51,sk52,sk53,sk54,sk55,sk56,sk57,sk58,sk59,sk60,sk61,sk62,sk63,sk64,sk65,sk66,sk67,sk68,sk69,sk70,sk71,sk72,sk73,sk74,sk75,sk76,sk77,sk78,sk79,sk80,sk81,sk82,sk83,sk84,sk85,sk86,sk87,sk88,sk89,sk90,sk91,sk92,sk93,sk94,sk95,sk96,sk97,sk98,sk99,sk100,sk101,sk102,sk103,sk104,sk105,sk106,sk107])],[f0_nnf]) ).
cnf(c1959,plain,
( def610(X1,X0)
| ~ def653(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(c1962,plain,
def653(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3958,plain,
def610(X0,X1),
inference(resolution,[status(thm)],[c1959,c1962]) ).
cnf(c1830,plain,
( def567(X1,X0)
| ~ def610(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3959,plain,
def567(X0,X1),
inference(resolution,[status(thm)],[p3958,c1830]) ).
cnf(c1701,plain,
( def524(X1,X0)
| ~ def567(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3961,plain,
def524(X0,X1),
inference(resolution,[status(thm)],[p3959,c1701]) ).
cnf(c1572,plain,
( def481(X1,X0)
| ~ def524(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3963,plain,
def481(X0,X1),
inference(resolution,[status(thm)],[p3961,c1572]) ).
cnf(c1443,plain,
( def438(X1,X0)
| ~ def481(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3965,plain,
def438(X0,X1),
inference(resolution,[status(thm)],[p3963,c1443]) ).
cnf(c1315,plain,
( def437(X0)
| ~ def438(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3967,plain,
def437(X0),
inference(resolution,[status(thm)],[p3965,c1315]) ).
cnf(c1312,plain,
( def436(X0)
| ~ def437(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3970,plain,
def436(X0),
inference(resolution,[status(thm)],[p3967,c1312]) ).
cnf(c1309,plain,
( p15(sk72)
| ~ def436(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3974,plain,
p15(sk72),
inference(resolution,[status(thm)],[p3970,c1309]) ).
cnf(c1311,plain,
( def434
| ~ def437(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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3969,plain,
def434,
inference(resolution,[status(thm)],[p3967,c1311]) ).
cnf(c1303,plain,
( ~ p15(sk72)
| ~ def434 ),
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,def224,def225,def226,def227,def228,def229,def230,def231,def232,def233,def234,def235,def236,def237,def238,def239,def240,def241,def242,def243,def244,def245,def246,def247,def248,def249,def250,def251,def252,def253,def254,def255,def256,def257,def258,def259,def260,def261,def262,def263,def264,def265,def266,def267,def268,def269,def270,def271,def272,def273,def274,def275,def276,def277,def278,def279,def280,def281,def282,def283,def284,def285,def286,def287,def288,def289,def290,def291,def292,def293,def294,def295,def296,def297,def298,def299,def300,def301,def302,def303,def304,def305,def306,def307,def308,def309,def310,def311,def312,def313,def314,def315,def316,def317,def318,def319,def320,def321,def322,def323,def324,def325,def326,def327,def328,def329,def330,def331,def332,def333,def334,def335,def336,def337,def338,def339,def340,def341,def342,def343,def344,def345,def346,def347,def348,def349,def350,def351,def352,def353,def354,def355,def356,def357,def358,def359,def360,def361,def362,def363,def364,def365,def366,def367,def368,def369,def370,def371,def372,def373,def374,def375,def376,def377,def378,def379,def380,def381,def382,def383,def384,def385,def386,def387,def388,def389,def390,def391,def392,def393,def394,def395,def396,def397,def398,def399,def400,def401,def402,def403,def404,def405,def406,def407,def408,def409,def410,def411,def412,def413,def414,def415,def416,def417,def418,def419,def420,def421,def422,def423,def424,def425,def426,def427,def428,def429,def430,def431,def432,def433,def434,def435,def436,def437,def438,def439,def440,def441,def442,def443,def444,def445,def446,def447,def448,def449,def450,def451,def452,def453,def454,def455,def456,def457,def458,def459,def460,def461,def462,def463,def464,def465,def466,def467,def468,def469,def470,def471,def472,def473,def474,def475,def476,def477,def478,def479,def480,def481,def482,def483,def484,def485,def486,def487,def488,def489,def490,def491,def492,def493,def494,def495,def496,def497,def498,def499,def500,def501,def502,def503,def504,def505,def506,def507,def508,def509,def510,def511,def512,def513,def514,def515,def516,def517,def518,def519,def520,def521,def522,def523,def524,def525,def526,def527,def528,def529,def530,def531,def532,def533,def534,def535,def536,def537,def538,def539,def540,def541,def542,def543,def544,def545,def546,def547,def548,def549,def550,def551,def552,def553,def554,def555,def556,def557,def558,def559,def560,def561,def562,def563,def564,def565,def566,def567,def568,def569,def570,def571,def572,def573,def574,def575,def576,def577,def578,def579,def580,def581,def582,def583,def584,def585,def586,def587,def588,def589,def590,def591,def592,def593,def594,def595,def596,def597,def598,def599,def600,def601,def602,def603,def604,def605,def606,def607,def608,def609,def610,def611,def612,def613,def614,def615,def616,def617,def618,def619,def620,def621,def622,def623,def624,def625,def626,def627,def628,def629,def630,def631,def632,def633,def634,def635,def636,def637,def638,def639,def640,def641,def642,def643,def644,def645,def646,def647,def648,def649,def650,def651,def652,def653])],[f0_sk]) ).
cnf(p3971,plain,
~ p15(sk72),
inference(resolution,[status(thm)],[p3969,c1303]) ).
cnf(p3984,plain,
$false,
inference(resolution,[status(thm)],[p3974,p3971]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL644+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.18/5.44 % Computer : n014.cluster.edu
% 0.18/5.44 % Model : x86_64 x86_64
% 0.18/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.44 % Memory : 8046.5625MB
% 0.18/5.44 % OS : Linux 6.8.0-71-generic
% 0.18/5.44 % CPULimit : 300
% 0.18/5.44 % WCLimit : 300
% 0.18/5.44 % DateTime : Wed Sep 23 23:54:09 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.18/5.45 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 144.38/26.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 144.38/26.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------