%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n001.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 70.78s 9.47s
% Output : Proof 70.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 1
% Syntax : Number of formulae : 28 ( 13 unt; 0 def)
% Number of atoms : 3515 ( 0 equ)
% Maximal formula atoms : 870 ( 125 avg)
% Number of connectives : 5285 (1798 ~;1869 |;1618 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 8 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 2 prp; 0-2 aty)
% Number of functors : 143 ( 143 usr; 103 con; 0-1 aty)
% Number of variables : 950 ( 19 sgn 772 !; 145 ?)
% 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] :
( ~ ( 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] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) ) )
| p20(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) ) )
| p20(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) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p16(X)
& ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X) )
| p17(X)
| ~ r1(Y,X) )
| p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| ! [X] :
( p16(X)
| ~ ( ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p17(X)
& ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X) )
| p18(X)
| ~ r1(Y,X) )
| p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| ! [X] :
( p17(X)
| ~ ( ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p18(X)
& ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X) )
| p19(X)
| ~ r1(Y,X) )
| p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| ! [X] :
( p18(X)
| ~ ( ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p19(X)
& ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X) )
| p20(X)
| ~ r1(Y,X) )
| p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| ! [X] :
( p19(X)
| ~ ( ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p20(X)
& ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X) )
| p21(X)
| ~ r1(Y,X) )
| p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| ! [X] :
( p20(X)
| ~ ( ! [Y] :
( p21(Y)
| ~ r1(X,Y) )
& p21(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(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] :
( ~ ( 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] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) ) )
| p20(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) ) )
| p20(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) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p16(X)
& ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X) )
| p17(X)
| ~ r1(Y,X) )
| p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| ! [X] :
( p16(X)
| ~ ( ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y) )
| p17(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p16(Y)
| ~ ( ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p17(X)
& ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X) )
| p18(X)
| ~ r1(Y,X) )
| p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| ! [X] :
( p17(X)
| ~ ( ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y) )
| p18(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p17(Y)
| ~ ( ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p18(X)
& ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X) )
| p19(X)
| ~ r1(Y,X) )
| p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| ! [X] :
( p18(X)
| ~ ( ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y) )
| p19(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p18(Y)
| ~ ( ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p19(X)
& ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X) )
| p20(X)
| ~ r1(Y,X) )
| p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| ! [X] :
( p19(X)
| ~ ( ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y) )
| p20(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p19(Y)
| ~ ( ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| ~ r1(X,Y) ) )
| ~ ( ~ ( ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ ( p20(X)
& ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X) )
| p21(X)
| ~ r1(Y,X) )
| p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| ! [X] :
( p20(X)
| ~ ( ! [Y] :
( p21(Y)
| ~ r1(X,Y) )
& p21(X) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ! [Y] :
( ~ ( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y) )
| p21(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p20(Y)
| ~ ( ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(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] :
( 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] :
( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& ~ p20(Y)
& r1(X,Y) )
& ? [Y] :
( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& ~ p20(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) ) )
& ( ? [Y] :
( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y)
& ~ p17(Y)
& ~ p16(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p16(X)
& ! [Y] :
( p16(Y)
| ~ r1(X,Y) )
& p16(X)
& ~ p17(X)
& r1(Y,X) )
& ~ p16(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y)
& r1(X,Y) )
| ? [Y] :
( p16(Y)
& ! [X] :
( p16(X)
| ~ r1(Y,X) )
& p16(Y)
& ~ p17(Y)
& ? [X] :
( ~ p16(X)
& ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p16(Y)
| ? [X] :
( ~ p16(X)
& r1(Y,X) )
| ~ p16(Y)
| p17(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p16(Y)
| ? [X] :
( ~ p17(X)
& r1(Y,X) )
| ~ p17(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y)
& ~ p18(Y)
& ~ p17(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p17(X)
& ! [Y] :
( p17(Y)
| ~ r1(X,Y) )
& p17(X)
& ~ p18(X)
& r1(Y,X) )
& ~ p17(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y)
& r1(X,Y) )
| ? [Y] :
( p17(Y)
& ! [X] :
( p17(X)
| ~ r1(Y,X) )
& p17(Y)
& ~ p18(Y)
& ? [X] :
( ~ p17(X)
& ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p17(Y)
| ? [X] :
( ~ p17(X)
& r1(Y,X) )
| ~ p17(Y)
| p18(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p17(Y)
| ? [X] :
( ~ p18(X)
& r1(Y,X) )
| ~ p18(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y)
& ~ p19(Y)
& ~ p18(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p18(X)
& ! [Y] :
( p18(Y)
| ~ r1(X,Y) )
& p18(X)
& ~ p19(X)
& r1(Y,X) )
& ~ p18(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y)
& r1(X,Y) )
| ? [Y] :
( p18(Y)
& ! [X] :
( p18(X)
| ~ r1(Y,X) )
& p18(Y)
& ~ p19(Y)
& ? [X] :
( ~ p18(X)
& ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p18(Y)
| ? [X] :
( ~ p18(X)
& r1(Y,X) )
| ~ p18(Y)
| p19(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p18(Y)
| ? [X] :
( ~ p19(X)
& r1(Y,X) )
| ~ p19(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y)
& ~ p20(Y)
& ~ p19(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p19(X)
& ! [Y] :
( p19(Y)
| ~ r1(X,Y) )
& p19(X)
& ~ p20(X)
& r1(Y,X) )
& ~ p19(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y)
& r1(X,Y) )
| ? [Y] :
( p19(Y)
& ! [X] :
( p19(X)
| ~ r1(Y,X) )
& p19(Y)
& ~ p20(Y)
& ? [X] :
( ~ p19(X)
& ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p19(Y)
| ? [X] :
( ~ p19(X)
& r1(Y,X) )
| ~ p19(Y)
| p20(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p19(Y)
| ? [X] :
( ~ p20(X)
& r1(Y,X) )
| ~ p20(Y)
| ~ r1(X,Y) ) )
& ( ? [Y] :
( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y)
& ~ p21(Y)
& ~ p20(Y)
& ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y)
& r1(X,Y) )
| ? [Y] :
( ? [X] :
( p20(X)
& ! [Y] :
( p20(Y)
| ~ r1(X,Y) )
& p20(X)
& ~ p21(X)
& r1(Y,X) )
& ~ p20(Y)
& ! [X] :
( p21(X)
| ~ r1(Y,X) )
& p21(Y)
& r1(X,Y) )
| ? [Y] :
( p20(Y)
& ! [X] :
( p20(X)
| ~ r1(Y,X) )
& p20(Y)
& ~ p21(Y)
& ? [X] :
( ~ p20(X)
& ! [Y] :
( p21(Y)
| ~ r1(X,Y) )
& p21(X)
& r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ~ p20(Y)
| ? [X] :
( ~ p20(X)
& r1(Y,X) )
| ~ p20(Y)
| p21(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p20(Y)
| ? [X] :
( ~ p21(X)
& r1(Y,X) )
| ~ p21(Y)
| ~ r1(X,Y) ) ) ),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
! [Y,X] :
( ( ( p1(sk142)
& ( p1(X)
| ~ r1(sk142,X) )
& p1(sk142)
& ~ p2(sk142)
& ~ p1(sk142)
& ( p2(X)
| ~ r1(sk142,X) )
& p2(sk142)
& r1(sk0,sk142) )
| ( p1(sk141)
& ( p1(Y)
| ~ r1(sk141,Y) )
& p1(sk141)
& ~ p2(sk141)
& r1(sk140,sk141)
& ~ p1(sk140)
& ( p2(X)
| ~ r1(sk140,X) )
& p2(sk140)
& r1(sk0,sk140) )
| ( p1(sk138)
& ( p1(X)
| ~ r1(sk138,X) )
& p1(sk138)
& ~ p2(sk138)
& ~ p1(sk139)
& ( p2(Y)
| ~ r1(sk139,Y) )
& p2(sk139)
& r1(sk138,sk139)
& r1(sk0,sk138) )
| ~ p1(Y)
| ( ~ p1(sk137(Y))
& r1(Y,sk137(Y)) )
| ~ p1(Y)
| p2(Y)
| ~ r1(sk0,Y)
| p1(Y)
| ( ~ p2(sk136(Y))
& r1(Y,sk136(Y)) )
| ~ p2(Y)
| ~ r1(sk0,Y) )
& ( ( p2(sk135)
& ( p2(X)
| ~ r1(sk135,X) )
& p2(sk135)
& ~ p3(sk135)
& ~ p2(sk135)
& ( p3(X)
| ~ r1(sk135,X) )
& p3(sk135)
& r1(sk0,sk135) )
| ( p2(sk134)
& ( p2(Y)
| ~ r1(sk134,Y) )
& p2(sk134)
& ~ p3(sk134)
& r1(sk133,sk134)
& ~ p2(sk133)
& ( p3(X)
| ~ r1(sk133,X) )
& p3(sk133)
& r1(sk0,sk133) )
| ( p2(sk131)
& ( p2(X)
| ~ r1(sk131,X) )
& p2(sk131)
& ~ p3(sk131)
& ~ p2(sk132)
& ( p3(Y)
| ~ r1(sk132,Y) )
& p3(sk132)
& r1(sk131,sk132)
& r1(sk0,sk131) )
| ~ p2(Y)
| ( ~ p2(sk130(Y))
& r1(Y,sk130(Y)) )
| ~ p2(Y)
| p3(Y)
| ~ r1(sk0,Y)
| p2(Y)
| ( ~ p3(sk129(Y))
& r1(Y,sk129(Y)) )
| ~ p3(Y)
| ~ r1(sk0,Y) )
& ( ( p3(sk128)
& ( p3(X)
| ~ r1(sk128,X) )
& p3(sk128)
& ~ p4(sk128)
& ~ p3(sk128)
& ( p4(X)
| ~ r1(sk128,X) )
& p4(sk128)
& r1(sk0,sk128) )
| ( p3(sk127)
& ( p3(Y)
| ~ r1(sk127,Y) )
& p3(sk127)
& ~ p4(sk127)
& r1(sk126,sk127)
& ~ p3(sk126)
& ( p4(X)
| ~ r1(sk126,X) )
& p4(sk126)
& r1(sk0,sk126) )
| ( p3(sk124)
& ( p3(X)
| ~ r1(sk124,X) )
& p3(sk124)
& ~ p4(sk124)
& ~ p3(sk125)
& ( p4(Y)
| ~ r1(sk125,Y) )
& p4(sk125)
& r1(sk124,sk125)
& r1(sk0,sk124) )
| ~ p3(Y)
| ( ~ p3(sk123(Y))
& r1(Y,sk123(Y)) )
| ~ p3(Y)
| p4(Y)
| ~ r1(sk0,Y)
| p3(Y)
| ( ~ p4(sk122(Y))
& r1(Y,sk122(Y)) )
| ~ p4(Y)
| ~ r1(sk0,Y) )
& ( ( p4(sk121)
& ( p4(X)
| ~ r1(sk121,X) )
& p4(sk121)
& ~ p5(sk121)
& ~ p4(sk121)
& ( p5(X)
| ~ r1(sk121,X) )
& p5(sk121)
& r1(sk0,sk121) )
| ( p4(sk120)
& ( p4(Y)
| ~ r1(sk120,Y) )
& p4(sk120)
& ~ p5(sk120)
& r1(sk119,sk120)
& ~ p4(sk119)
& ( p5(X)
| ~ r1(sk119,X) )
& p5(sk119)
& r1(sk0,sk119) )
| ( p4(sk117)
& ( p4(X)
| ~ r1(sk117,X) )
& p4(sk117)
& ~ p5(sk117)
& ~ p4(sk118)
& ( p5(Y)
| ~ r1(sk118,Y) )
& p5(sk118)
& r1(sk117,sk118)
& r1(sk0,sk117) )
| ~ p4(Y)
| ( ~ p4(sk116(Y))
& r1(Y,sk116(Y)) )
| ~ p4(Y)
| p5(Y)
| ~ r1(sk0,Y)
| p4(Y)
| ( ~ p5(sk115(Y))
& r1(Y,sk115(Y)) )
| ~ p5(Y)
| ~ r1(sk0,Y) )
& ( ( p5(sk114)
& ( p5(X)
| ~ r1(sk114,X) )
& p5(sk114)
& ~ p6(sk114)
& ~ p5(sk114)
& ( p6(X)
| ~ r1(sk114,X) )
& p6(sk114)
& r1(sk0,sk114) )
| ( p5(sk113)
& ( p5(Y)
| ~ r1(sk113,Y) )
& p5(sk113)
& ~ p6(sk113)
& r1(sk112,sk113)
& ~ p5(sk112)
& ( p6(X)
| ~ r1(sk112,X) )
& p6(sk112)
& r1(sk0,sk112) )
| ( p5(sk110)
& ( p5(X)
| ~ r1(sk110,X) )
& p5(sk110)
& ~ p6(sk110)
& ~ p5(sk111)
& ( p6(Y)
| ~ r1(sk111,Y) )
& p6(sk111)
& r1(sk110,sk111)
& r1(sk0,sk110) )
| ~ p5(Y)
| ( ~ p5(sk109(Y))
& r1(Y,sk109(Y)) )
| ~ p5(Y)
| p6(Y)
| ~ r1(sk0,Y)
| p5(Y)
| ( ~ p6(sk108(Y))
& r1(Y,sk108(Y)) )
| ~ p6(Y)
| ~ r1(sk0,Y) )
& ( ( p6(sk107)
& ( p6(X)
| ~ r1(sk107,X) )
& p6(sk107)
& ~ p7(sk107)
& ~ p6(sk107)
& ( p7(X)
| ~ r1(sk107,X) )
& p7(sk107)
& r1(sk0,sk107) )
| ( p6(sk106)
& ( p6(Y)
| ~ r1(sk106,Y) )
& p6(sk106)
& ~ p7(sk106)
& r1(sk105,sk106)
& ~ p6(sk105)
& ( p7(X)
| ~ r1(sk105,X) )
& p7(sk105)
& r1(sk0,sk105) )
| ( p6(sk103)
& ( p6(X)
| ~ r1(sk103,X) )
& p6(sk103)
& ~ p7(sk103)
& ~ p6(sk104)
& ( p7(Y)
| ~ r1(sk104,Y) )
& p7(sk104)
& r1(sk103,sk104)
& r1(sk0,sk103) )
| ~ p6(Y)
| ( ~ p6(sk102(Y))
& r1(Y,sk102(Y)) )
| ~ p6(Y)
| p7(Y)
| ~ r1(sk0,Y)
| p6(Y)
| ( ~ p7(sk101(Y))
& r1(Y,sk101(Y)) )
| ~ p7(Y)
| ~ r1(sk0,Y) )
& p20(sk100)
& ( p20(X)
| ~ r1(sk100,X) )
& ~ p20(sk100)
& r1(sk0,sk100)
& p20(sk99)
& ( p20(X)
| ~ r1(sk99,X) )
& ~ p20(sk99)
& r1(sk0,sk99)
& ( ( p7(sk98)
& ( p7(X)
| ~ r1(sk98,X) )
& p7(sk98)
& ~ p8(sk98)
& ~ p7(sk98)
& ( p8(X)
| ~ r1(sk98,X) )
& p8(sk98)
& r1(sk0,sk98) )
| ( p7(sk97)
& ( p7(Y)
| ~ r1(sk97,Y) )
& p7(sk97)
& ~ p8(sk97)
& r1(sk96,sk97)
& ~ p7(sk96)
& ( p8(X)
| ~ r1(sk96,X) )
& p8(sk96)
& r1(sk0,sk96) )
| ( p7(sk94)
& ( p7(X)
| ~ r1(sk94,X) )
& p7(sk94)
& ~ p8(sk94)
& ~ p7(sk95)
& ( p8(Y)
| ~ r1(sk95,Y) )
& p8(sk95)
& r1(sk94,sk95)
& r1(sk0,sk94) )
| ~ p7(Y)
| ( ~ p7(sk93(Y))
& r1(Y,sk93(Y)) )
| ~ p7(Y)
| p8(Y)
| ~ r1(sk0,Y)
| p7(Y)
| ( ~ p8(sk92(Y))
& r1(Y,sk92(Y)) )
| ~ p8(Y)
| ~ r1(sk0,Y) )
& ( ( p8(sk91)
& ( p8(X)
| ~ r1(sk91,X) )
& p8(sk91)
& ~ p9(sk91)
& ~ p8(sk91)
& ( p9(X)
| ~ r1(sk91,X) )
& p9(sk91)
& r1(sk0,sk91) )
| ( p8(sk90)
& ( p8(Y)
| ~ r1(sk90,Y) )
& p8(sk90)
& ~ p9(sk90)
& r1(sk89,sk90)
& ~ p8(sk89)
& ( p9(X)
| ~ r1(sk89,X) )
& p9(sk89)
& r1(sk0,sk89) )
| ( p8(sk87)
& ( p8(X)
| ~ r1(sk87,X) )
& p8(sk87)
& ~ p9(sk87)
& ~ p8(sk88)
& ( p9(Y)
| ~ r1(sk88,Y) )
& p9(sk88)
& r1(sk87,sk88)
& r1(sk0,sk87) )
| ~ p8(Y)
| ( ~ p8(sk86(Y))
& r1(Y,sk86(Y)) )
| ~ p8(Y)
| p9(Y)
| ~ r1(sk0,Y)
| p8(Y)
| ( ~ p9(sk85(Y))
& r1(Y,sk85(Y)) )
| ~ p9(Y)
| ~ r1(sk0,Y) )
& ( ( p9(sk84)
& ( p9(X)
| ~ r1(sk84,X) )
& p9(sk84)
& ~ p10(sk84)
& ~ p9(sk84)
& ( p10(X)
| ~ r1(sk84,X) )
& p10(sk84)
& r1(sk0,sk84) )
| ( p9(sk83)
& ( p9(Y)
| ~ r1(sk83,Y) )
& p9(sk83)
& ~ p10(sk83)
& r1(sk82,sk83)
& ~ p9(sk82)
& ( p10(X)
| ~ r1(sk82,X) )
& p10(sk82)
& r1(sk0,sk82) )
| ( p9(sk80)
& ( p9(X)
| ~ r1(sk80,X) )
& p9(sk80)
& ~ p10(sk80)
& ~ p9(sk81)
& ( p10(Y)
| ~ r1(sk81,Y) )
& p10(sk81)
& r1(sk80,sk81)
& r1(sk0,sk80) )
| ~ p9(Y)
| ( ~ p9(sk79(Y))
& r1(Y,sk79(Y)) )
| ~ p9(Y)
| p10(Y)
| ~ r1(sk0,Y)
| p9(Y)
| ( ~ p10(sk78(Y))
& r1(Y,sk78(Y)) )
| ~ p10(Y)
| ~ r1(sk0,Y) )
& ( ( p10(sk77)
& ( p10(X)
| ~ r1(sk77,X) )
& p10(sk77)
& ~ p11(sk77)
& ~ p10(sk77)
& ( p11(X)
| ~ r1(sk77,X) )
& p11(sk77)
& r1(sk0,sk77) )
| ( p10(sk76)
& ( p10(Y)
| ~ r1(sk76,Y) )
& p10(sk76)
& ~ p11(sk76)
& r1(sk75,sk76)
& ~ p10(sk75)
& ( p11(X)
| ~ r1(sk75,X) )
& p11(sk75)
& r1(sk0,sk75) )
| ( p10(sk73)
& ( p10(X)
| ~ r1(sk73,X) )
& p10(sk73)
& ~ p11(sk73)
& ~ p10(sk74)
& ( p11(Y)
| ~ r1(sk74,Y) )
& p11(sk74)
& r1(sk73,sk74)
& r1(sk0,sk73) )
| ~ p10(Y)
| ( ~ p10(sk72(Y))
& r1(Y,sk72(Y)) )
| ~ p10(Y)
| p11(Y)
| ~ r1(sk0,Y)
| p10(Y)
| ( ~ p11(sk71(Y))
& r1(Y,sk71(Y)) )
| ~ p11(Y)
| ~ r1(sk0,Y) )
& ( ( p11(sk70)
& ( p11(X)
| ~ r1(sk70,X) )
& p11(sk70)
& ~ p12(sk70)
& ~ p11(sk70)
& ( p12(X)
| ~ r1(sk70,X) )
& p12(sk70)
& r1(sk0,sk70) )
| ( p11(sk69)
& ( p11(Y)
| ~ r1(sk69,Y) )
& p11(sk69)
& ~ p12(sk69)
& r1(sk68,sk69)
& ~ p11(sk68)
& ( p12(X)
| ~ r1(sk68,X) )
& p12(sk68)
& r1(sk0,sk68) )
| ( p11(sk66)
& ( p11(X)
| ~ r1(sk66,X) )
& p11(sk66)
& ~ p12(sk66)
& ~ p11(sk67)
& ( p12(Y)
| ~ r1(sk67,Y) )
& p12(sk67)
& r1(sk66,sk67)
& r1(sk0,sk66) )
| ~ p11(Y)
| ( ~ p11(sk65(Y))
& r1(Y,sk65(Y)) )
| ~ p11(Y)
| p12(Y)
| ~ r1(sk0,Y)
| p11(Y)
| ( ~ p12(sk64(Y))
& r1(Y,sk64(Y)) )
| ~ p12(Y)
| ~ r1(sk0,Y) )
& ( ( p12(sk63)
& ( p12(X)
| ~ r1(sk63,X) )
& p12(sk63)
& ~ p13(sk63)
& ~ p12(sk63)
& ( p13(X)
| ~ r1(sk63,X) )
& p13(sk63)
& r1(sk0,sk63) )
| ( p12(sk62)
& ( p12(Y)
| ~ r1(sk62,Y) )
& p12(sk62)
& ~ p13(sk62)
& r1(sk61,sk62)
& ~ p12(sk61)
& ( p13(X)
| ~ r1(sk61,X) )
& p13(sk61)
& r1(sk0,sk61) )
| ( p12(sk59)
& ( p12(X)
| ~ r1(sk59,X) )
& p12(sk59)
& ~ p13(sk59)
& ~ p12(sk60)
& ( p13(Y)
| ~ r1(sk60,Y) )
& p13(sk60)
& r1(sk59,sk60)
& r1(sk0,sk59) )
| ~ p12(Y)
| ( ~ p12(sk58(Y))
& r1(Y,sk58(Y)) )
| ~ p12(Y)
| p13(Y)
| ~ r1(sk0,Y)
| p12(Y)
| ( ~ p13(sk57(Y))
& r1(Y,sk57(Y)) )
| ~ p13(Y)
| ~ r1(sk0,Y) )
& ( ( p13(sk56)
& ( p13(X)
| ~ r1(sk56,X) )
& p13(sk56)
& ~ p14(sk56)
& ~ p13(sk56)
& ( p14(X)
| ~ r1(sk56,X) )
& p14(sk56)
& r1(sk0,sk56) )
| ( p13(sk55)
& ( p13(Y)
| ~ r1(sk55,Y) )
& p13(sk55)
& ~ p14(sk55)
& r1(sk54,sk55)
& ~ p13(sk54)
& ( p14(X)
| ~ r1(sk54,X) )
& p14(sk54)
& r1(sk0,sk54) )
| ( p13(sk52)
& ( p13(X)
| ~ r1(sk52,X) )
& p13(sk52)
& ~ p14(sk52)
& ~ p13(sk53)
& ( p14(Y)
| ~ r1(sk53,Y) )
& p14(sk53)
& r1(sk52,sk53)
& r1(sk0,sk52) )
| ~ p13(Y)
| ( ~ p13(sk51(Y))
& r1(Y,sk51(Y)) )
| ~ p13(Y)
| p14(Y)
| ~ r1(sk0,Y)
| p13(Y)
| ( ~ p14(sk50(Y))
& r1(Y,sk50(Y)) )
| ~ p14(Y)
| ~ r1(sk0,Y) )
& ( ( p14(sk49)
& ( p14(X)
| ~ r1(sk49,X) )
& p14(sk49)
& ~ p15(sk49)
& ~ p14(sk49)
& ( p15(X)
| ~ r1(sk49,X) )
& p15(sk49)
& r1(sk0,sk49) )
| ( p14(sk48)
& ( p14(Y)
| ~ r1(sk48,Y) )
& p14(sk48)
& ~ p15(sk48)
& r1(sk47,sk48)
& ~ p14(sk47)
& ( p15(X)
| ~ r1(sk47,X) )
& p15(sk47)
& r1(sk0,sk47) )
| ( p14(sk45)
& ( p14(X)
| ~ r1(sk45,X) )
& p14(sk45)
& ~ p15(sk45)
& ~ p14(sk46)
& ( p15(Y)
| ~ r1(sk46,Y) )
& p15(sk46)
& r1(sk45,sk46)
& r1(sk0,sk45) )
| ~ p14(Y)
| ( ~ p14(sk44(Y))
& r1(Y,sk44(Y)) )
| ~ p14(Y)
| p15(Y)
| ~ r1(sk0,Y)
| p14(Y)
| ( ~ p15(sk43(Y))
& r1(Y,sk43(Y)) )
| ~ p15(Y)
| ~ r1(sk0,Y) )
& ( ( p15(sk42)
& ( p15(X)
| ~ r1(sk42,X) )
& p15(sk42)
& ~ p16(sk42)
& ~ p15(sk42)
& ( p16(X)
| ~ r1(sk42,X) )
& p16(sk42)
& r1(sk0,sk42) )
| ( p15(sk41)
& ( p15(Y)
| ~ r1(sk41,Y) )
& p15(sk41)
& ~ p16(sk41)
& r1(sk40,sk41)
& ~ p15(sk40)
& ( p16(X)
| ~ r1(sk40,X) )
& p16(sk40)
& r1(sk0,sk40) )
| ( p15(sk38)
& ( p15(X)
| ~ r1(sk38,X) )
& p15(sk38)
& ~ p16(sk38)
& ~ p15(sk39)
& ( p16(Y)
| ~ r1(sk39,Y) )
& p16(sk39)
& r1(sk38,sk39)
& r1(sk0,sk38) )
| ~ p15(Y)
| ( ~ p15(sk37(Y))
& r1(Y,sk37(Y)) )
| ~ p15(Y)
| p16(Y)
| ~ r1(sk0,Y)
| p15(Y)
| ( ~ p16(sk36(Y))
& r1(Y,sk36(Y)) )
| ~ p16(Y)
| ~ r1(sk0,Y) )
& ( ( p16(sk35)
& ( p16(X)
| ~ r1(sk35,X) )
& p16(sk35)
& ~ p17(sk35)
& ~ p16(sk35)
& ( p17(X)
| ~ r1(sk35,X) )
& p17(sk35)
& r1(sk0,sk35) )
| ( p16(sk34)
& ( p16(Y)
| ~ r1(sk34,Y) )
& p16(sk34)
& ~ p17(sk34)
& r1(sk33,sk34)
& ~ p16(sk33)
& ( p17(X)
| ~ r1(sk33,X) )
& p17(sk33)
& r1(sk0,sk33) )
| ( p16(sk31)
& ( p16(X)
| ~ r1(sk31,X) )
& p16(sk31)
& ~ p17(sk31)
& ~ p16(sk32)
& ( p17(Y)
| ~ r1(sk32,Y) )
& p17(sk32)
& r1(sk31,sk32)
& r1(sk0,sk31) )
| ~ p16(Y)
| ( ~ p16(sk30(Y))
& r1(Y,sk30(Y)) )
| ~ p16(Y)
| p17(Y)
| ~ r1(sk0,Y)
| p16(Y)
| ( ~ p17(sk29(Y))
& r1(Y,sk29(Y)) )
| ~ p17(Y)
| ~ r1(sk0,Y) )
& ( ( p17(sk28)
& ( p17(X)
| ~ r1(sk28,X) )
& p17(sk28)
& ~ p18(sk28)
& ~ p17(sk28)
& ( p18(X)
| ~ r1(sk28,X) )
& p18(sk28)
& r1(sk0,sk28) )
| ( p17(sk27)
& ( p17(Y)
| ~ r1(sk27,Y) )
& p17(sk27)
& ~ p18(sk27)
& r1(sk26,sk27)
& ~ p17(sk26)
& ( p18(X)
| ~ r1(sk26,X) )
& p18(sk26)
& r1(sk0,sk26) )
| ( p17(sk24)
& ( p17(X)
| ~ r1(sk24,X) )
& p17(sk24)
& ~ p18(sk24)
& ~ p17(sk25)
& ( p18(Y)
| ~ r1(sk25,Y) )
& p18(sk25)
& r1(sk24,sk25)
& r1(sk0,sk24) )
| ~ p17(Y)
| ( ~ p17(sk23(Y))
& r1(Y,sk23(Y)) )
| ~ p17(Y)
| p18(Y)
| ~ r1(sk0,Y)
| p17(Y)
| ( ~ p18(sk22(Y))
& r1(Y,sk22(Y)) )
| ~ p18(Y)
| ~ r1(sk0,Y) )
& ( ( p18(sk21)
& ( p18(X)
| ~ r1(sk21,X) )
& p18(sk21)
& ~ p19(sk21)
& ~ p18(sk21)
& ( p19(X)
| ~ r1(sk21,X) )
& p19(sk21)
& r1(sk0,sk21) )
| ( p18(sk20)
& ( p18(Y)
| ~ r1(sk20,Y) )
& p18(sk20)
& ~ p19(sk20)
& r1(sk19,sk20)
& ~ p18(sk19)
& ( p19(X)
| ~ r1(sk19,X) )
& p19(sk19)
& r1(sk0,sk19) )
| ( p18(sk17)
& ( p18(X)
| ~ r1(sk17,X) )
& p18(sk17)
& ~ p19(sk17)
& ~ p18(sk18)
& ( p19(Y)
| ~ r1(sk18,Y) )
& p19(sk18)
& r1(sk17,sk18)
& r1(sk0,sk17) )
| ~ p18(Y)
| ( ~ p18(sk16(Y))
& r1(Y,sk16(Y)) )
| ~ p18(Y)
| p19(Y)
| ~ r1(sk0,Y)
| p18(Y)
| ( ~ p19(sk15(Y))
& r1(Y,sk15(Y)) )
| ~ p19(Y)
| ~ r1(sk0,Y) )
& ( ( p19(sk14)
& ( p19(X)
| ~ r1(sk14,X) )
& p19(sk14)
& ~ p20(sk14)
& ~ p19(sk14)
& ( p20(X)
| ~ r1(sk14,X) )
& p20(sk14)
& r1(sk0,sk14) )
| ( p19(sk13)
& ( p19(Y)
| ~ r1(sk13,Y) )
& p19(sk13)
& ~ p20(sk13)
& r1(sk12,sk13)
& ~ p19(sk12)
& ( p20(X)
| ~ r1(sk12,X) )
& p20(sk12)
& r1(sk0,sk12) )
| ( p19(sk10)
& ( p19(X)
| ~ r1(sk10,X) )
& p19(sk10)
& ~ p20(sk10)
& ~ p19(sk11)
& ( p20(Y)
| ~ r1(sk11,Y) )
& p20(sk11)
& r1(sk10,sk11)
& r1(sk0,sk10) )
| ~ p19(Y)
| ( ~ p19(sk9(Y))
& r1(Y,sk9(Y)) )
| ~ p19(Y)
| p20(Y)
| ~ r1(sk0,Y)
| p19(Y)
| ( ~ p20(sk8(Y))
& r1(Y,sk8(Y)) )
| ~ p20(Y)
| ~ r1(sk0,Y) )
& ( ( p20(sk7)
& ( p20(X)
| ~ r1(sk7,X) )
& p20(sk7)
& ~ p21(sk7)
& ~ p20(sk7)
& ( p21(X)
| ~ r1(sk7,X) )
& p21(sk7)
& r1(sk0,sk7) )
| ( p20(sk6)
& ( p20(Y)
| ~ r1(sk6,Y) )
& p20(sk6)
& ~ p21(sk6)
& r1(sk5,sk6)
& ~ p20(sk5)
& ( p21(X)
| ~ r1(sk5,X) )
& p21(sk5)
& r1(sk0,sk5) )
| ( p20(sk3)
& ( p20(X)
| ~ r1(sk3,X) )
& p20(sk3)
& ~ p21(sk3)
& ~ p20(sk4)
& ( p21(Y)
| ~ r1(sk4,Y) )
& p21(sk4)
& r1(sk3,sk4)
& r1(sk0,sk3) )
| ~ p20(Y)
| ( ~ p20(sk2(Y))
& r1(Y,sk2(Y)) )
| ~ p20(Y)
| p21(Y)
| ~ r1(sk0,Y)
| p20(Y)
| ( ~ p21(sk1(Y))
& r1(Y,sk1(Y)) )
| ~ p21(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,sk108,sk109,sk110,sk111,sk112,sk113,sk114,sk115,sk116,sk117,sk118,sk119,sk120,sk121,sk122,sk123,sk124,sk125,sk126,sk127,sk128,sk129,sk130,sk131,sk132,sk133,sk134,sk135,sk136,sk137,sk138,sk139,sk140,sk141,sk142])],[f0_nnf]) ).
cnf(c2607,plain,
def868(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(c2604,plain,
( def825(X1,X0)
| ~ def868(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p11646,plain,
def825(X0,X1),
inference(resolution,[status(thm)],[c2607,c2604]) ).
cnf(c2475,plain,
( def782(X1,X0)
| ~ def825(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p13366,plain,
def782(X0,X1),
inference(resolution,[status(thm)],[p11646,c2475]) ).
cnf(c2346,plain,
( def739(X1,X0)
| ~ def782(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p14165,plain,
def739(X0,X1),
inference(resolution,[status(thm)],[p13366,c2346]) ).
cnf(c2217,plain,
( def696(X1,X0)
| ~ def739(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p14830,plain,
def696(X0,X1),
inference(resolution,[status(thm)],[p14165,c2217]) ).
cnf(c2088,plain,
( def653(X1,X0)
| ~ def696(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p14911,plain,
def653(X0,X1),
inference(resolution,[status(thm)],[p14830,c2088]) ).
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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15030,plain,
def610(X0,X1),
inference(resolution,[status(thm)],[p14911,c1959]) ).
cnf(c1831,plain,
( def609(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15227,plain,
def609(X0),
inference(resolution,[status(thm)],[p15030,c1831]) ).
cnf(c1828,plain,
( def608(X0)
| ~ def609(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15553,plain,
def608(X0),
inference(resolution,[status(thm)],[p15227,c1828]) ).
cnf(c1825,plain,
( p20(sk100)
| ~ def608(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15933,plain,
p20(sk100),
inference(resolution,[status(thm)],[p15553,c1825]) ).
cnf(c1827,plain,
( def606
| ~ def609(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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15552,plain,
def606,
inference(resolution,[status(thm)],[p15227,c1827]) ).
cnf(c1819,plain,
( ~ p20(sk100)
| ~ def606 ),
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,def654,def655,def656,def657,def658,def659,def660,def661,def662,def663,def664,def665,def666,def667,def668,def669,def670,def671,def672,def673,def674,def675,def676,def677,def678,def679,def680,def681,def682,def683,def684,def685,def686,def687,def688,def689,def690,def691,def692,def693,def694,def695,def696,def697,def698,def699,def700,def701,def702,def703,def704,def705,def706,def707,def708,def709,def710,def711,def712,def713,def714,def715,def716,def717,def718,def719,def720,def721,def722,def723,def724,def725,def726,def727,def728,def729,def730,def731,def732,def733,def734,def735,def736,def737,def738,def739,def740,def741,def742,def743,def744,def745,def746,def747,def748,def749,def750,def751,def752,def753,def754,def755,def756,def757,def758,def759,def760,def761,def762,def763,def764,def765,def766,def767,def768,def769,def770,def771,def772,def773,def774,def775,def776,def777,def778,def779,def780,def781,def782,def783,def784,def785,def786,def787,def788,def789,def790,def791,def792,def793,def794,def795,def796,def797,def798,def799,def800,def801,def802,def803,def804,def805,def806,def807,def808,def809,def810,def811,def812,def813,def814,def815,def816,def817,def818,def819,def820,def821,def822,def823,def824,def825,def826,def827,def828,def829,def830,def831,def832,def833,def834,def835,def836,def837,def838,def839,def840,def841,def842,def843,def844,def845,def846,def847,def848,def849,def850,def851,def852,def853,def854,def855,def856,def857,def858,def859,def860,def861,def862,def863,def864,def865,def866,def867,def868])],[f0_sk]) ).
cnf(p15931,plain,
~ p20(sk100),
inference(resolution,[status(thm)],[p15552,c1819]) ).
cnf(p16658,plain,
$false,
inference(resolution,[status(thm)],[p15933,p15931]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL644+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n001.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Thu Sep 24 00:01:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 70.78/9.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 70.78/9.47 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------