%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n006.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 : Sun Sep 27 07:59:24 AM UTC 2026
% Result : Theorem 133.03s 20.13s
% Output : CNFRefutation 133.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 1
% Syntax : Number of formulae : 71 ( 7 unt; 0 def)
% Number of atoms : 2680 ( 0 equ)
% Maximal formula atoms : 620 ( 37 avg)
% Number of connectives : 4896 (2287 ~;2064 |; 545 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 141 ( 14 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 1 prp; 0-2 aty)
% Number of functors : 69 ( 69 usr; 5 con; 0-4 aty)
% Number of variables : 1584 ( 0 sgn1232 !; 71 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X] :
~ ( ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p11(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p11(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p12(Y)
& ! [X] :
( p21(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p13(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p13(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p15(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p15(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p22(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p22(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p24(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p24(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p26(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p26(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p31(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p31(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p33(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p33(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p34(Y)
& ! [X] :
( p41(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p35(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p35(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p42(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p42(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p44(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p44(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p46(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p46(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p52(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p54(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p54(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p56(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
file('theBenchmark.p',main) ).
fof(main_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ! [Y] :
( p11(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p12(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p13(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p15(Y)
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p11(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p11(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p12(Y)
& ! [X] :
( p21(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p13(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p13(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p15(Y)
& ! [X] :
( p23(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p15(Y)
& ! [X] :
( p25(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p21(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p22(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p22(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p23(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p24(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p24(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p31(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p33(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p25(X)
& ! [Y] :
( p35(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p14(Y)
& ! [X] :
( p26(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p16(Y)
& ! [X] :
( p26(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p31(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p31(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p32(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p33(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p33(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p34(Y)
& ! [X] :
( p41(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p34(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p35(Y)
& ! [X] :
( p43(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p35(Y)
& ! [X] :
( p45(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p22(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p24(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p26(X)
& ! [Y] :
( p36(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p41(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p42(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p42(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p43(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p44(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p44(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p51(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p53(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p45(X)
& ! [Y] :
( p55(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p32(Y)
& ! [X] :
( p46(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p36(Y)
& ! [X] :
( p46(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p52(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p54(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p42(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p44(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p46(X)
& ! [Y] :
( p56(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p52(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p54(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p54(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p56(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(nnf_2,plain,
? [X] :
( ? [Y] :
( ~ p11(Y)
& r1(X,Y) )
& ? [X252] :
( ~ p12(X252)
& r1(X,X252) )
& ? [X251] :
( ~ p13(X251)
& r1(X,X251) )
& ? [X250] :
( ~ p15(X250)
& r1(X,X250) )
& ! [X248] :
( p11(X248)
| ? [X249] :
( ~ p23(X249)
& r1(X248,X249) )
| ~ r1(X,X248) )
& ! [X246] :
( p11(X246)
| ? [X247] :
( ~ p25(X247)
& r1(X246,X247) )
| ~ r1(X,X246) )
& ! [X244] :
( p12(X244)
| ? [X245] :
( ~ p21(X245)
& r1(X244,X245) )
| ~ r1(X,X244) )
& ! [X242] :
( p13(X242)
| ? [X243] :
( ~ p23(X243)
& r1(X242,X243) )
| ~ r1(X,X242) )
& ! [X240] :
( p13(X240)
| ? [X241] :
( ~ p25(X241)
& r1(X240,X241) )
| ~ r1(X,X240) )
& ! [X238] :
( p15(X238)
| ? [X239] :
( ~ p23(X239)
& r1(X238,X239) )
| ~ r1(X,X238) )
& ! [X236] :
( p15(X236)
| ? [X237] :
( ~ p25(X237)
& r1(X236,X237) )
| ~ r1(X,X236) )
& ! [X233] :
( ! [X234] :
( p21(X234)
| ? [X235] :
( ~ p31(X235)
& r1(X234,X235) )
| ~ r1(X233,X234) )
| ~ r1(X,X233) )
& ! [X230] :
( ! [X231] :
( p21(X231)
| ? [X232] :
( ~ p33(X232)
& r1(X231,X232) )
| ~ r1(X230,X231) )
| ~ r1(X,X230) )
& ! [X227] :
( ! [X228] :
( p21(X228)
| ? [X229] :
( ~ p34(X229)
& r1(X228,X229) )
| ~ r1(X227,X228) )
| ~ r1(X,X227) )
& ! [X224] :
( ! [X225] :
( p21(X225)
| ? [X226] :
( ~ p35(X226)
& r1(X225,X226) )
| ~ r1(X224,X225) )
| ~ r1(X,X224) )
& ! [X222] :
( p14(X222)
| ? [X223] :
( ~ p22(X223)
& r1(X222,X223) )
| ~ r1(X,X222) )
& ! [X220] :
( p16(X220)
| ? [X221] :
( ~ p22(X221)
& r1(X220,X221) )
| ~ r1(X,X220) )
& ! [X217] :
( ! [X218] :
( p23(X218)
| ? [X219] :
( ~ p31(X219)
& r1(X218,X219) )
| ~ r1(X217,X218) )
| ~ r1(X,X217) )
& ! [X214] :
( ! [X215] :
( p23(X215)
| ? [X216] :
( ~ p33(X216)
& r1(X215,X216) )
| ~ r1(X214,X215) )
| ~ r1(X,X214) )
& ! [X211] :
( ! [X212] :
( p23(X212)
| ? [X213] :
( ~ p35(X213)
& r1(X212,X213) )
| ~ r1(X211,X212) )
| ~ r1(X,X211) )
& ! [X209] :
( p14(X209)
| ? [X210] :
( ~ p24(X210)
& r1(X209,X210) )
| ~ r1(X,X209) )
& ! [X207] :
( p16(X207)
| ? [X208] :
( ~ p24(X208)
& r1(X207,X208) )
| ~ r1(X,X207) )
& ! [X204] :
( ! [X205] :
( p25(X205)
| ? [X206] :
( ~ p31(X206)
& r1(X205,X206) )
| ~ r1(X204,X205) )
| ~ r1(X,X204) )
& ! [X201] :
( ! [X202] :
( p25(X202)
| ? [X203] :
( ~ p33(X203)
& r1(X202,X203) )
| ~ r1(X201,X202) )
| ~ r1(X,X201) )
& ! [X198] :
( ! [X199] :
( p25(X199)
| ? [X200] :
( ~ p35(X200)
& r1(X199,X200) )
| ~ r1(X198,X199) )
| ~ r1(X,X198) )
& ! [X196] :
( p14(X196)
| ? [X197] :
( ~ p26(X197)
& r1(X196,X197) )
| ~ r1(X,X196) )
& ! [X194] :
( p16(X194)
| ? [X195] :
( ~ p26(X195)
& r1(X194,X195) )
| ~ r1(X,X194) )
& ! [X190] :
( ! [X191] :
( ! [X192] :
( p31(X192)
| ? [X193] :
( ~ p43(X193)
& r1(X192,X193) )
| ~ r1(X191,X192) )
| ~ r1(X190,X191) )
| ~ r1(X,X190) )
& ! [X186] :
( ! [X187] :
( ! [X188] :
( p31(X188)
| ? [X189] :
( ~ p45(X189)
& r1(X188,X189) )
| ~ r1(X187,X188) )
| ~ r1(X186,X187) )
| ~ r1(X,X186) )
& ! [X183] :
( ! [X184] :
( p22(X184)
| ? [X185] :
( ~ p32(X185)
& r1(X184,X185) )
| ~ r1(X183,X184) )
| ~ r1(X,X183) )
& ! [X180] :
( ! [X181] :
( p24(X181)
| ? [X182] :
( ~ p32(X182)
& r1(X181,X182) )
| ~ r1(X180,X181) )
| ~ r1(X,X180) )
& ! [X177] :
( ! [X178] :
( p26(X178)
| ? [X179] :
( ~ p32(X179)
& r1(X178,X179) )
| ~ r1(X177,X178) )
| ~ r1(X,X177) )
& ! [X173] :
( ! [X174] :
( ! [X175] :
( p33(X175)
| ? [X176] :
( ~ p43(X176)
& r1(X175,X176) )
| ~ r1(X174,X175) )
| ~ r1(X173,X174) )
| ~ r1(X,X173) )
& ! [X169] :
( ! [X170] :
( ! [X171] :
( p33(X171)
| ? [X172] :
( ~ p45(X172)
& r1(X171,X172) )
| ~ r1(X170,X171) )
| ~ r1(X169,X170) )
| ~ r1(X,X169) )
& ! [X165] :
( ! [X166] :
( ! [X167] :
( p34(X167)
| ? [X168] :
( ~ p41(X168)
& r1(X167,X168) )
| ~ r1(X166,X167) )
| ~ r1(X165,X166) )
| ~ r1(X,X165) )
& ! [X162] :
( ! [X163] :
( p22(X163)
| ? [X164] :
( ~ p34(X164)
& r1(X163,X164) )
| ~ r1(X162,X163) )
| ~ r1(X,X162) )
& ! [X159] :
( ! [X160] :
( p24(X160)
| ? [X161] :
( ~ p34(X161)
& r1(X160,X161) )
| ~ r1(X159,X160) )
| ~ r1(X,X159) )
& ! [X156] :
( ! [X157] :
( p26(X157)
| ? [X158] :
( ~ p34(X158)
& r1(X157,X158) )
| ~ r1(X156,X157) )
| ~ r1(X,X156) )
& ! [X152] :
( ! [X153] :
( ! [X154] :
( p35(X154)
| ? [X155] :
( ~ p43(X155)
& r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X,X152) )
& ! [X148] :
( ! [X149] :
( ! [X150] :
( p35(X150)
| ? [X151] :
( ~ p45(X151)
& r1(X150,X151) )
| ~ r1(X149,X150) )
| ~ r1(X148,X149) )
| ~ r1(X,X148) )
& ! [X145] :
( ! [X146] :
( p22(X146)
| ? [X147] :
( ~ p36(X147)
& r1(X146,X147) )
| ~ r1(X145,X146) )
| ~ r1(X,X145) )
& ! [X142] :
( ! [X143] :
( p24(X143)
| ? [X144] :
( ~ p36(X144)
& r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X,X142) )
& ! [X139] :
( ! [X140] :
( p26(X140)
| ? [X141] :
( ~ p36(X141)
& r1(X140,X141) )
| ~ r1(X139,X140) )
| ~ r1(X,X139) )
& ! [X134] :
( ! [X135] :
( ! [X136] :
( ! [X137] :
( p41(X137)
| ? [X138] :
( ~ p51(X138)
& r1(X137,X138) )
| ~ r1(X136,X137) )
| ~ r1(X135,X136) )
| ~ r1(X134,X135) )
| ~ r1(X,X134) )
& ! [X129] :
( ! [X130] :
( ! [X131] :
( ! [X132] :
( p41(X132)
| ? [X133] :
( ~ p53(X133)
& r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
| ~ r1(X129,X130) )
| ~ r1(X,X129) )
& ! [X124] :
( ! [X125] :
( ! [X126] :
( ! [X127] :
( p41(X127)
| ? [X128] :
( ~ p54(X128)
& r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X125,X126) )
| ~ r1(X124,X125) )
| ~ r1(X,X124) )
& ! [X119] :
( ! [X120] :
( ! [X121] :
( ! [X122] :
( p41(X122)
| ? [X123] :
( ~ p55(X123)
& r1(X122,X123) )
| ~ r1(X121,X122) )
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X,X119) )
& ! [X115] :
( ! [X116] :
( ! [X117] :
( p32(X117)
| ? [X118] :
( ~ p42(X118)
& r1(X117,X118) )
| ~ r1(X116,X117) )
| ~ r1(X115,X116) )
| ~ r1(X,X115) )
& ! [X111] :
( ! [X112] :
( ! [X113] :
( p36(X113)
| ? [X114] :
( ~ p42(X114)
& r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X,X111) )
& ! [X106] :
( ! [X107] :
( ! [X108] :
( ! [X109] :
( p43(X109)
| ? [X110] :
( ~ p51(X110)
& r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X,X106) )
& ! [X101] :
( ! [X102] :
( ! [X103] :
( ! [X104] :
( p43(X104)
| ? [X105] :
( ~ p53(X105)
& r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X101,X102) )
| ~ r1(X,X101) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( p43(X99)
| ? [X100] :
( ~ p55(X100)
& r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X,X96) )
& ! [X92] :
( ! [X93] :
( ! [X94] :
( p32(X94)
| ? [X95] :
( ~ p44(X95)
& r1(X94,X95) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X,X92) )
& ! [X88] :
( ! [X89] :
( ! [X90] :
( p36(X90)
| ? [X91] :
( ~ p44(X91)
& r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X,X88) )
& ! [X83] :
( ! [X84] :
( ! [X85] :
( ! [X86] :
( p45(X86)
| ? [X87] :
( ~ p51(X87)
& r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(X,X83) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( p45(X81)
| ? [X82] :
( ~ p53(X82)
& r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X,X78) )
& ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( p45(X76)
| ? [X77] :
( ~ p55(X77)
& r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X,X73) )
& ! [X69] :
( ! [X70] :
( ! [X71] :
( p32(X71)
| ? [X72] :
( ~ p46(X72)
& r1(X71,X72) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X,X69) )
& ! [X65] :
( ! [X66] :
( ! [X67] :
( p36(X67)
| ? [X68] :
( ~ p46(X68)
& r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(X,X65) )
& ! [X60] :
( ! [X61] :
( ! [X62] :
( ! [X63] :
( p42(X63)
| ? [X64] :
( ~ p52(X64)
& r1(X63,X64) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X,X60) )
& ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( p44(X58)
| ? [X59] :
( ~ p52(X59)
& r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X,X55) )
& ! [X50] :
( ! [X51] :
( ! [X52] :
( ! [X53] :
( p46(X53)
| ? [X54] :
( ~ p52(X54)
& r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X50,X51) )
| ~ r1(X,X50) )
& ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( p42(X48)
| ? [X49] :
( ~ p54(X49)
& r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X,X45) )
& ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] :
( p44(X43)
| ? [X44] :
( ~ p54(X44)
& r1(X43,X44) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X,X40) )
& ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( p46(X38)
| ? [X39] :
( ~ p54(X39)
& r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X,X35) )
& ! [X30] :
( ! [X31] :
( ! [X32] :
( ! [X33] :
( p42(X33)
| ? [X34] :
( ~ p56(X34)
& r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(X,X30) )
& ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( p44(X28)
| ? [X29] :
( ~ p56(X29)
& r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X,X25) )
& ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( p46(X23)
| ? [X24] :
( ~ p56(X24)
& r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X,X20) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( p52(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X,X15) )
& ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X14] :
( p54(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X,X10) )
& ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( p54(X9)
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X,X5) )
& ! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( p56(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) )
| ~ r1(X,X0) ) ),
inference(fof_nnf,[status(thm)],[main_neg]) ).
fof(sk_main_neg_sk,plain,
( ~ p11(sK68)
& r1(sK0,sK68)
& ~ p12(sK5)
& r1(sK0,sK5)
& ~ p13(sK67)
& r1(sK0,sK67)
& ~ p15(sK66)
& r1(sK0,sK66)
& ! [X248] :
( p11(X248)
| ( ~ p23(sK65(X248))
& r1(X248,sK65(X248)) )
| ~ r1(sK0,X248) )
& ! [X246] :
( p11(X246)
| ( ~ p25(sK64(X246))
& r1(X246,sK64(X246)) )
| ~ r1(sK0,X246) )
& ! [X244] :
( p12(X244)
| ( ~ p21(sK4(X244))
& r1(X244,sK4(X244)) )
| ~ r1(sK0,X244) )
& ! [X242] :
( p13(X242)
| ( ~ p23(sK63(X242))
& r1(X242,sK63(X242)) )
| ~ r1(sK0,X242) )
& ! [X240] :
( p13(X240)
| ( ~ p25(sK62(X240))
& r1(X240,sK62(X240)) )
| ~ r1(sK0,X240) )
& ! [X238] :
( p15(X238)
| ( ~ p23(sK61(X238))
& r1(X238,sK61(X238)) )
| ~ r1(sK0,X238) )
& ! [X236] :
( p15(X236)
| ( ~ p25(sK60(X236))
& r1(X236,sK60(X236)) )
| ~ r1(sK0,X236) )
& ! [X233] :
( ! [X234] :
( p21(X234)
| ( ~ p31(sK59(X233,X234))
& r1(X234,sK59(X233,X234)) )
| ~ r1(X233,X234) )
| ~ r1(sK0,X233) )
& ! [X230] :
( ! [X231] :
( p21(X231)
| ( ~ p33(sK58(X230,X231))
& r1(X231,sK58(X230,X231)) )
| ~ r1(X230,X231) )
| ~ r1(sK0,X230) )
& ! [X227] :
( ! [X228] :
( p21(X228)
| ( ~ p34(sK3(X227,X228))
& r1(X228,sK3(X227,X228)) )
| ~ r1(X227,X228) )
| ~ r1(sK0,X227) )
& ! [X224] :
( ! [X225] :
( p21(X225)
| ( ~ p35(sK57(X224,X225))
& r1(X225,sK57(X224,X225)) )
| ~ r1(X224,X225) )
| ~ r1(sK0,X224) )
& ! [X222] :
( p14(X222)
| ( ~ p22(sK56(X222))
& r1(X222,sK56(X222)) )
| ~ r1(sK0,X222) )
& ! [X220] :
( p16(X220)
| ( ~ p22(sK55(X220))
& r1(X220,sK55(X220)) )
| ~ r1(sK0,X220) )
& ! [X217] :
( ! [X218] :
( p23(X218)
| ( ~ p31(sK54(X217,X218))
& r1(X218,sK54(X217,X218)) )
| ~ r1(X217,X218) )
| ~ r1(sK0,X217) )
& ! [X214] :
( ! [X215] :
( p23(X215)
| ( ~ p33(sK53(X214,X215))
& r1(X215,sK53(X214,X215)) )
| ~ r1(X214,X215) )
| ~ r1(sK0,X214) )
& ! [X211] :
( ! [X212] :
( p23(X212)
| ( ~ p35(sK52(X211,X212))
& r1(X212,sK52(X211,X212)) )
| ~ r1(X211,X212) )
| ~ r1(sK0,X211) )
& ! [X209] :
( p14(X209)
| ( ~ p24(sK51(X209))
& r1(X209,sK51(X209)) )
| ~ r1(sK0,X209) )
& ! [X207] :
( p16(X207)
| ( ~ p24(sK50(X207))
& r1(X207,sK50(X207)) )
| ~ r1(sK0,X207) )
& ! [X204] :
( ! [X205] :
( p25(X205)
| ( ~ p31(sK49(X204,X205))
& r1(X205,sK49(X204,X205)) )
| ~ r1(X204,X205) )
| ~ r1(sK0,X204) )
& ! [X201] :
( ! [X202] :
( p25(X202)
| ( ~ p33(sK48(X201,X202))
& r1(X202,sK48(X201,X202)) )
| ~ r1(X201,X202) )
| ~ r1(sK0,X201) )
& ! [X198] :
( ! [X199] :
( p25(X199)
| ( ~ p35(sK47(X198,X199))
& r1(X199,sK47(X198,X199)) )
| ~ r1(X198,X199) )
| ~ r1(sK0,X198) )
& ! [X196] :
( p14(X196)
| ( ~ p26(sK46(X196))
& r1(X196,sK46(X196)) )
| ~ r1(sK0,X196) )
& ! [X194] :
( p16(X194)
| ( ~ p26(sK45(X194))
& r1(X194,sK45(X194)) )
| ~ r1(sK0,X194) )
& ! [X190] :
( ! [X191] :
( ! [X192] :
( p31(X192)
| ( ~ p43(sK44(X190,X191,X192))
& r1(X192,sK44(X190,X191,X192)) )
| ~ r1(X191,X192) )
| ~ r1(X190,X191) )
| ~ r1(sK0,X190) )
& ! [X186] :
( ! [X187] :
( ! [X188] :
( p31(X188)
| ( ~ p45(sK43(X186,X187,X188))
& r1(X188,sK43(X186,X187,X188)) )
| ~ r1(X187,X188) )
| ~ r1(X186,X187) )
| ~ r1(sK0,X186) )
& ! [X183] :
( ! [X184] :
( p22(X184)
| ( ~ p32(sK42(X183,X184))
& r1(X184,sK42(X183,X184)) )
| ~ r1(X183,X184) )
| ~ r1(sK0,X183) )
& ! [X180] :
( ! [X181] :
( p24(X181)
| ( ~ p32(sK41(X180,X181))
& r1(X181,sK41(X180,X181)) )
| ~ r1(X180,X181) )
| ~ r1(sK0,X180) )
& ! [X177] :
( ! [X178] :
( p26(X178)
| ( ~ p32(sK40(X177,X178))
& r1(X178,sK40(X177,X178)) )
| ~ r1(X177,X178) )
| ~ r1(sK0,X177) )
& ! [X173] :
( ! [X174] :
( ! [X175] :
( p33(X175)
| ( ~ p43(sK39(X173,X174,X175))
& r1(X175,sK39(X173,X174,X175)) )
| ~ r1(X174,X175) )
| ~ r1(X173,X174) )
| ~ r1(sK0,X173) )
& ! [X169] :
( ! [X170] :
( ! [X171] :
( p33(X171)
| ( ~ p45(sK38(X169,X170,X171))
& r1(X171,sK38(X169,X170,X171)) )
| ~ r1(X170,X171) )
| ~ r1(X169,X170) )
| ~ r1(sK0,X169) )
& ! [X165] :
( ! [X166] :
( ! [X167] :
( p34(X167)
| ( ~ p41(sK2(X165,X166,X167))
& r1(X167,sK2(X165,X166,X167)) )
| ~ r1(X166,X167) )
| ~ r1(X165,X166) )
| ~ r1(sK0,X165) )
& ! [X162] :
( ! [X163] :
( p22(X163)
| ( ~ p34(sK37(X162,X163))
& r1(X163,sK37(X162,X163)) )
| ~ r1(X162,X163) )
| ~ r1(sK0,X162) )
& ! [X159] :
( ! [X160] :
( p24(X160)
| ( ~ p34(sK36(X159,X160))
& r1(X160,sK36(X159,X160)) )
| ~ r1(X159,X160) )
| ~ r1(sK0,X159) )
& ! [X156] :
( ! [X157] :
( p26(X157)
| ( ~ p34(sK35(X156,X157))
& r1(X157,sK35(X156,X157)) )
| ~ r1(X156,X157) )
| ~ r1(sK0,X156) )
& ! [X152] :
( ! [X153] :
( ! [X154] :
( p35(X154)
| ( ~ p43(sK34(X152,X153,X154))
& r1(X154,sK34(X152,X153,X154)) )
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(sK0,X152) )
& ! [X148] :
( ! [X149] :
( ! [X150] :
( p35(X150)
| ( ~ p45(sK33(X148,X149,X150))
& r1(X150,sK33(X148,X149,X150)) )
| ~ r1(X149,X150) )
| ~ r1(X148,X149) )
| ~ r1(sK0,X148) )
& ! [X145] :
( ! [X146] :
( p22(X146)
| ( ~ p36(sK32(X145,X146))
& r1(X146,sK32(X145,X146)) )
| ~ r1(X145,X146) )
| ~ r1(sK0,X145) )
& ! [X142] :
( ! [X143] :
( p24(X143)
| ( ~ p36(sK31(X142,X143))
& r1(X143,sK31(X142,X143)) )
| ~ r1(X142,X143) )
| ~ r1(sK0,X142) )
& ! [X139] :
( ! [X140] :
( p26(X140)
| ( ~ p36(sK30(X139,X140))
& r1(X140,sK30(X139,X140)) )
| ~ r1(X139,X140) )
| ~ r1(sK0,X139) )
& ! [X134] :
( ! [X135] :
( ! [X136] :
( ! [X137] :
( p41(X137)
| ( ~ p51(sK29(X134,X135,X136,X137))
& r1(X137,sK29(X134,X135,X136,X137)) )
| ~ r1(X136,X137) )
| ~ r1(X135,X136) )
| ~ r1(X134,X135) )
| ~ r1(sK0,X134) )
& ! [X129] :
( ! [X130] :
( ! [X131] :
( ! [X132] :
( p41(X132)
| ( ~ p53(sK28(X129,X130,X131,X132))
& r1(X132,sK28(X129,X130,X131,X132)) )
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
| ~ r1(X129,X130) )
| ~ r1(sK0,X129) )
& ! [X124] :
( ! [X125] :
( ! [X126] :
( ! [X127] :
( p41(X127)
| ( ~ p54(sK1(X124,X125,X126,X127))
& r1(X127,sK1(X124,X125,X126,X127)) )
| ~ r1(X126,X127) )
| ~ r1(X125,X126) )
| ~ r1(X124,X125) )
| ~ r1(sK0,X124) )
& ! [X119] :
( ! [X120] :
( ! [X121] :
( ! [X122] :
( p41(X122)
| ( ~ p55(sK27(X119,X120,X121,X122))
& r1(X122,sK27(X119,X120,X121,X122)) )
| ~ r1(X121,X122) )
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(sK0,X119) )
& ! [X115] :
( ! [X116] :
( ! [X117] :
( p32(X117)
| ( ~ p42(sK26(X115,X116,X117))
& r1(X117,sK26(X115,X116,X117)) )
| ~ r1(X116,X117) )
| ~ r1(X115,X116) )
| ~ r1(sK0,X115) )
& ! [X111] :
( ! [X112] :
( ! [X113] :
( p36(X113)
| ( ~ p42(sK25(X111,X112,X113))
& r1(X113,sK25(X111,X112,X113)) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(sK0,X111) )
& ! [X106] :
( ! [X107] :
( ! [X108] :
( ! [X109] :
( p43(X109)
| ( ~ p51(sK24(X106,X107,X108,X109))
& r1(X109,sK24(X106,X107,X108,X109)) )
| ~ r1(X108,X109) )
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(sK0,X106) )
& ! [X101] :
( ! [X102] :
( ! [X103] :
( ! [X104] :
( p43(X104)
| ( ~ p53(sK23(X101,X102,X103,X104))
& r1(X104,sK23(X101,X102,X103,X104)) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X101,X102) )
| ~ r1(sK0,X101) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( p43(X99)
| ( ~ p55(sK22(X96,X97,X98,X99))
& r1(X99,sK22(X96,X97,X98,X99)) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(sK0,X96) )
& ! [X92] :
( ! [X93] :
( ! [X94] :
( p32(X94)
| ( ~ p44(sK21(X92,X93,X94))
& r1(X94,sK21(X92,X93,X94)) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(sK0,X92) )
& ! [X88] :
( ! [X89] :
( ! [X90] :
( p36(X90)
| ( ~ p44(sK20(X88,X89,X90))
& r1(X90,sK20(X88,X89,X90)) )
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(sK0,X88) )
& ! [X83] :
( ! [X84] :
( ! [X85] :
( ! [X86] :
( p45(X86)
| ( ~ p51(sK19(X83,X84,X85,X86))
& r1(X86,sK19(X83,X84,X85,X86)) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X83,X84) )
| ~ r1(sK0,X83) )
& ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( p45(X81)
| ( ~ p53(sK18(X78,X79,X80,X81))
& r1(X81,sK18(X78,X79,X80,X81)) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(sK0,X78) )
& ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( p45(X76)
| ( ~ p55(sK17(X73,X74,X75,X76))
& r1(X76,sK17(X73,X74,X75,X76)) )
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(sK0,X73) )
& ! [X69] :
( ! [X70] :
( ! [X71] :
( p32(X71)
| ( ~ p46(sK16(X69,X70,X71))
& r1(X71,sK16(X69,X70,X71)) )
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(sK0,X69) )
& ! [X65] :
( ! [X66] :
( ! [X67] :
( p36(X67)
| ( ~ p46(sK15(X65,X66,X67))
& r1(X67,sK15(X65,X66,X67)) )
| ~ r1(X66,X67) )
| ~ r1(X65,X66) )
| ~ r1(sK0,X65) )
& ! [X60] :
( ! [X61] :
( ! [X62] :
( ! [X63] :
( p42(X63)
| ( ~ p52(sK14(X60,X61,X62,X63))
& r1(X63,sK14(X60,X61,X62,X63)) )
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(sK0,X60) )
& ! [X55] :
( ! [X56] :
( ! [X57] :
( ! [X58] :
( p44(X58)
| ( ~ p52(sK13(X55,X56,X57,X58))
& r1(X58,sK13(X55,X56,X57,X58)) )
| ~ r1(X57,X58) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(sK0,X55) )
& ! [X50] :
( ! [X51] :
( ! [X52] :
( ! [X53] :
( p46(X53)
| ( ~ p52(sK12(X50,X51,X52,X53))
& r1(X53,sK12(X50,X51,X52,X53)) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X50,X51) )
| ~ r1(sK0,X50) )
& ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( p42(X48)
| ( ~ p54(sK11(X45,X46,X47,X48))
& r1(X48,sK11(X45,X46,X47,X48)) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(sK0,X45) )
& ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] :
( p44(X43)
| ( ~ p54(sK10(X40,X41,X42,X43))
& r1(X43,sK10(X40,X41,X42,X43)) )
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(sK0,X40) )
& ! [X35] :
( ! [X36] :
( ! [X37] :
( ! [X38] :
( p46(X38)
| ( ~ p54(sK9(X35,X36,X37,X38))
& r1(X38,sK9(X35,X36,X37,X38)) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(sK0,X35) )
& ! [X30] :
( ! [X31] :
( ! [X32] :
( ! [X33] :
( p42(X33)
| ( ~ p56(sK8(X30,X31,X32,X33))
& r1(X33,sK8(X30,X31,X32,X33)) )
| ~ r1(X32,X33) )
| ~ r1(X31,X32) )
| ~ r1(X30,X31) )
| ~ r1(sK0,X30) )
& ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( p44(X28)
| ( ~ p56(sK7(X25,X26,X27,X28))
& r1(X28,sK7(X25,X26,X27,X28)) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(sK0,X25) )
& ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( p46(X23)
| ( ~ p56(sK6(X20,X21,X22,X23))
& r1(X23,sK6(X20,X21,X22,X23)) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(sK0,X20) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( p52(X19)
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(sK0,X15) )
& ! [X10] :
( ! [X11] :
( ! [X12] :
( ! [X13] :
( ! [X14] :
( p54(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(sK0,X10) )
& ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( p54(X9)
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(sK0,X5) )
& ! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( p56(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) )
| ~ r1(sK0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK1,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK2,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK3,sK58,sK59,sK60,sK61,sK62,sK63,sK4,sK64,sK65,sK66,sK67,sK5,sK68]),skolemize(X,sK0),skolemize(X24,sK6(X20,X21,X22,X23)),skolemize(X29,sK7(X25,X26,X27,X28)),skolemize(X34,sK8(X30,X31,X32,X33)),skolemize(X39,sK9(X35,X36,X37,X38)),skolemize(X44,sK10(X40,X41,X42,X43)),skolemize(X49,sK11(X45,X46,X47,X48)),skolemize(X54,sK12(X50,X51,X52,X53)),skolemize(X59,sK13(X55,X56,X57,X58)),skolemize(X64,sK14(X60,X61,X62,X63)),skolemize(X68,sK15(X65,X66,X67)),skolemize(X72,sK16(X69,X70,X71)),skolemize(X77,sK17(X73,X74,X75,X76)),skolemize(X82,sK18(X78,X79,X80,X81)),skolemize(X87,sK19(X83,X84,X85,X86)),skolemize(X91,sK20(X88,X89,X90)),skolemize(X95,sK21(X92,X93,X94)),skolemize(X100,sK22(X96,X97,X98,X99)),skolemize(X105,sK23(X101,X102,X103,X104)),skolemize(X110,sK24(X106,X107,X108,X109)),skolemize(X114,sK25(X111,X112,X113)),skolemize(X118,sK26(X115,X116,X117)),skolemize(X123,sK27(X119,X120,X121,X122)),skolemize(X128,sK1(X124,X125,X126,X127)),skolemize(X133,sK28(X129,X130,X131,X132)),skolemize(X138,sK29(X134,X135,X136,X137)),skolemize(X141,sK30(X139,X140)),skolemize(X144,sK31(X142,X143)),skolemize(X147,sK32(X145,X146)),skolemize(X151,sK33(X148,X149,X150)),skolemize(X155,sK34(X152,X153,X154)),skolemize(X158,sK35(X156,X157)),skolemize(X161,sK36(X159,X160)),skolemize(X164,sK37(X162,X163)),skolemize(X168,sK2(X165,X166,X167)),skolemize(X172,sK38(X169,X170,X171)),skolemize(X176,sK39(X173,X174,X175)),skolemize(X179,sK40(X177,X178)),skolemize(X182,sK41(X180,X181)),skolemize(X185,sK42(X183,X184)),skolemize(X189,sK43(X186,X187,X188)),skolemize(X193,sK44(X190,X191,X192)),skolemize(X195,sK45(X194)),skolemize(X197,sK46(X196)),skolemize(X200,sK47(X198,X199)),skolemize(X203,sK48(X201,X202)),skolemize(X206,sK49(X204,X205)),skolemize(X208,sK50(X207)),skolemize(X210,sK51(X209)),skolemize(X213,sK52(X211,X212)),skolemize(X216,sK53(X214,X215)),skolemize(X219,sK54(X217,X218)),skolemize(X221,sK55(X220)),skolemize(X223,sK56(X222)),skolemize(X226,sK57(X224,X225)),skolemize(X229,sK3(X227,X228)),skolemize(X232,sK58(X230,X231)),skolemize(X235,sK59(X233,X234)),skolemize(X237,sK60(X236)),skolemize(X239,sK61(X238)),skolemize(X241,sK62(X240)),skolemize(X243,sK63(X242)),skolemize(X245,sK4(X244)),skolemize(X247,sK64(X246)),skolemize(X249,sK65(X248)),skolemize(X250,sK66),skolemize(X251,sK67),skolemize(X252,sK5),skolemize(Y,sK68)],[nnf_2]) ).
fof(sk_main_neg,plain,
( ~ p11(sK68)
& r1(sK0,sK68)
& ~ p12(sK5)
& r1(sK0,sK5)
& ~ p13(sK67)
& r1(sK0,sK67)
& ~ p15(sK66)
& r1(sK0,sK66)
& ! [VAR_0] :
( p11(VAR_0)
| ~ p23(sK65(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p11(VAR_0)
| r1(VAR_0,sK65(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p11(VAR_0)
| ~ p25(sK64(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p11(VAR_0)
| r1(VAR_0,sK64(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p12(VAR_0)
| ~ p21(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p12(VAR_0)
| r1(VAR_0,sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p13(VAR_0)
| ~ p23(sK63(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p13(VAR_0)
| r1(VAR_0,sK63(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p13(VAR_0)
| ~ p25(sK62(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p13(VAR_0)
| r1(VAR_0,sK62(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p15(VAR_0)
| ~ p23(sK61(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p15(VAR_0)
| r1(VAR_0,sK61(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p15(VAR_0)
| ~ p25(sK60(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p15(VAR_0)
| r1(VAR_0,sK60(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| ~ p31(sK59(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| r1(VAR_1,sK59(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| ~ p33(sK58(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| r1(VAR_1,sK58(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| ~ p34(sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| r1(VAR_1,sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| ~ p35(sK57(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p21(VAR_1)
| r1(VAR_1,sK57(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| ~ p22(sK56(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| r1(VAR_0,sK56(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| ~ p22(sK55(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| r1(VAR_0,sK55(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| ~ p31(sK54(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| r1(VAR_1,sK54(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| ~ p33(sK53(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| r1(VAR_1,sK53(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| ~ p35(sK52(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p23(VAR_1)
| r1(VAR_1,sK52(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| ~ p24(sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| r1(VAR_0,sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| ~ p24(sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| r1(VAR_0,sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| ~ p31(sK49(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| r1(VAR_1,sK49(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| ~ p33(sK48(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| r1(VAR_1,sK48(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| ~ p35(sK47(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p25(VAR_1)
| r1(VAR_1,sK47(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| ~ p26(sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p14(VAR_0)
| r1(VAR_0,sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| ~ p26(sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p16(VAR_0)
| r1(VAR_0,sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p31(VAR_2)
| ~ p43(sK44(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p31(VAR_2)
| r1(VAR_2,sK44(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p31(VAR_2)
| ~ p45(sK43(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p31(VAR_2)
| r1(VAR_2,sK43(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| ~ p32(sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| r1(VAR_1,sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| ~ p32(sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| r1(VAR_1,sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| ~ p32(sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| r1(VAR_1,sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p33(VAR_2)
| ~ p43(sK39(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p33(VAR_2)
| r1(VAR_2,sK39(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p33(VAR_2)
| ~ p45(sK38(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p33(VAR_2)
| r1(VAR_2,sK38(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p34(VAR_2)
| ~ p41(sK2(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p34(VAR_2)
| r1(VAR_2,sK2(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| ~ p34(sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| r1(VAR_1,sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| ~ p34(sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| r1(VAR_1,sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| ~ p34(sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| r1(VAR_1,sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p35(VAR_2)
| ~ p43(sK34(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p35(VAR_2)
| r1(VAR_2,sK34(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p35(VAR_2)
| ~ p45(sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p35(VAR_2)
| r1(VAR_2,sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| ~ p36(sK32(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p22(VAR_1)
| r1(VAR_1,sK32(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| ~ p36(sK31(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p24(VAR_1)
| r1(VAR_1,sK31(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| ~ p36(sK30(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( p26(VAR_1)
| r1(VAR_1,sK30(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| ~ p51(sK29(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| r1(VAR_3,sK29(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| ~ p53(sK28(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| r1(VAR_3,sK28(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| ~ p54(sK1(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| r1(VAR_3,sK1(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| ~ p55(sK27(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p41(VAR_3)
| r1(VAR_3,sK27(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| ~ p42(sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| r1(VAR_2,sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| ~ p42(sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| r1(VAR_2,sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| ~ p51(sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| r1(VAR_3,sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| ~ p53(sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| r1(VAR_3,sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| ~ p55(sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p43(VAR_3)
| r1(VAR_3,sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| ~ p44(sK21(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| r1(VAR_2,sK21(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| ~ p44(sK20(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| r1(VAR_2,sK20(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| ~ p51(sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| r1(VAR_3,sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| ~ p53(sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| r1(VAR_3,sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| ~ p55(sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p45(VAR_3)
| r1(VAR_3,sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| ~ p46(sK16(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p32(VAR_2)
| r1(VAR_2,sK16(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| ~ p46(sK15(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( p36(VAR_2)
| r1(VAR_2,sK15(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| ~ p52(sK14(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| r1(VAR_3,sK14(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| ~ p52(sK13(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| r1(VAR_3,sK13(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| ~ p52(sK12(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| r1(VAR_3,sK12(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| ~ p54(sK11(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| r1(VAR_3,sK11(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| ~ p54(sK10(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| r1(VAR_3,sK10(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| ~ p54(sK9(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| r1(VAR_3,sK9(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| ~ p56(sK8(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p42(VAR_3)
| r1(VAR_3,sK8(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| ~ p56(sK7(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p44(VAR_3)
| r1(VAR_3,sK7(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| ~ p56(sK6(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( p46(VAR_3)
| r1(VAR_3,sK6(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p52(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p54(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p54(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p56(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_main_neg_sk]) ).
cnf(c_7,negated_conjecture,
( p54(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_11,negated_conjecture,
( p41(D)
| ~ p54(sK1(A,B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_104,negated_conjecture,
( p34(C)
| ~ p41(sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_106,negated_conjecture,
( p41(D)
| r1(D,sK1(A,B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_108,negated_conjecture,
( p41(V7)
| ~ r1(V6,V7)
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,V7))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_7,c_11]) ).
cnf(c_264,negated_conjecture,
( p34(V9)
| ~ r1(V8,V9)
| ~ r1(V7,V8)
| ~ r1(sK0,V7)
| ~ r1(V6,sK2(V7,V8,V9))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(V7,V8,V9)))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_108,c_104]) ).
cnf(c_268,negated_conjecture,
( p34(F)
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| r1(sK2(D,E,F),sK1(A,B,C,sK2(D,E,F)))
| ~ r1(C,sK2(D,E,F))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_106,c_104]) ).
cnf(c_271,negated_conjecture,
( p34(C)
| r1(C,sK2(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_272,negated_conjecture,
( p21(B)
| ~ p34(sK3(A,B))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_359,negated_conjecture,
( p12(A)
| ~ p21(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_360,negated_conjecture,
( r1(sK3(A,B),sK2(C,D,sK3(A,B)))
| ~ r1(D,sK3(A,B))
| ~ r1(C,D)
| ~ r1(sK0,C)
| p21(B)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_272,c_271]) ).
cnf(c_363,negated_conjecture,
( ~ r1(V6,sK3(A,B))
| ~ r1(F,V6)
| ~ r1(sK0,F)
| r1(sK2(F,V6,sK3(A,B)),sK1(C,D,E,sK2(F,V6,sK3(A,B))))
| ~ r1(E,sK2(F,V6,sK3(A,B)))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| p21(B)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_272,c_268]) ).
cnf(c_365,negated_conjecture,
( ~ r1(V10,sK3(A,B))
| ~ r1(V9,V10)
| ~ r1(sK0,V9)
| ~ r1(V8,sK2(V9,V10,sK3(A,B)))
| ~ r1(V7,V8)
| ~ r1(V6,V7)
| ~ r1(sK0,V6)
| ~ r1(F,sK1(V6,V7,V8,sK2(V9,V10,sK3(A,B))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| p21(B)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_272,c_264]) ).
cnf(c_376,negated_conjecture,
( p21(B)
| r1(B,sK3(A,B))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_508,negated_conjecture,
~ p12(sK5),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_509,negated_conjecture,
( p12(A)
| r1(A,sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_510,negated_conjecture,
( r1(sK3(B,sK4(A)),sK2(C,D,sK3(B,sK4(A))))
| ~ r1(D,sK3(B,sK4(A)))
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK4(A))
| ~ r1(sK0,B)
| p12(A)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_359,c_360]) ).
cnf(c_513,negated_conjecture,
( ~ r1(V6,sK3(B,sK4(A)))
| ~ r1(F,V6)
| ~ r1(sK0,F)
| r1(sK2(F,V6,sK3(B,sK4(A))),sK1(C,D,E,sK2(F,V6,sK3(B,sK4(A)))))
| ~ r1(E,sK2(F,V6,sK3(B,sK4(A))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK4(A))
| ~ r1(sK0,B)
| p12(A)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_359,c_363]) ).
cnf(c_515,negated_conjecture,
( ~ r1(V10,sK3(B,sK4(A)))
| ~ r1(V9,V10)
| ~ r1(sK0,V9)
| ~ r1(V8,sK2(V9,V10,sK3(B,sK4(A))))
| ~ r1(V7,V8)
| ~ r1(V6,V7)
| ~ r1(sK0,V6)
| ~ r1(F,sK1(V6,V7,V8,sK2(V9,V10,sK3(B,sK4(A)))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK4(A))
| ~ r1(sK0,B)
| p12(A)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_359,c_365]) ).
cnf(c_526,negated_conjecture,
( p12(B)
| ~ r1(sK0,B)
| r1(sK4(B),sK3(A,sK4(B)))
| ~ r1(A,sK4(B))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_376,c_359]) ).
cnf(c_716,negated_conjecture,
r1(sK0,sK5),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_830,negated_conjecture,
( r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5) ),
inference(resolve,[status(thm)],[c_508,c_509]) ).
cnf(c_831,negated_conjecture,
r1(sK5,sK4(sK5)),
inference(resolve,[status(thm)],[c_716,c_830]) ).
cnf(c_832,negated_conjecture,
( r1(sK3(A,sK4(sK5)),sK2(B,C,sK3(A,sK4(sK5))))
| ~ r1(C,sK3(A,sK4(sK5)))
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A)
| ~ r1(sK0,sK5) ),
inference(resolve,[status(thm)],[c_508,c_510]) ).
cnf(c_833,negated_conjecture,
( r1(sK3(A,sK4(sK5)),sK2(B,C,sK3(A,sK4(sK5))))
| ~ r1(C,sK3(A,sK4(sK5)))
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_832]) ).
cnf(c_838,negated_conjecture,
( ~ r1(F,sK3(A,sK4(sK5)))
| ~ r1(E,F)
| ~ r1(sK0,E)
| r1(sK2(E,F,sK3(A,sK4(sK5))),sK1(B,C,D,sK2(E,F,sK3(A,sK4(sK5)))))
| ~ r1(D,sK2(E,F,sK3(A,sK4(sK5))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A)
| ~ r1(sK0,sK5) ),
inference(resolve,[status(thm)],[c_508,c_513]) ).
cnf(c_839,negated_conjecture,
( ~ r1(F,sK3(A,sK4(sK5)))
| ~ r1(E,F)
| ~ r1(sK0,E)
| r1(sK2(E,F,sK3(A,sK4(sK5))),sK1(B,C,D,sK2(E,F,sK3(A,sK4(sK5)))))
| ~ r1(D,sK2(E,F,sK3(A,sK4(sK5))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_838]) ).
cnf(c_842,negated_conjecture,
( ~ r1(V9,sK3(A,sK4(sK5)))
| ~ r1(V8,V9)
| ~ r1(sK0,V8)
| ~ r1(V7,sK2(V8,V9,sK3(A,sK4(sK5))))
| ~ r1(V6,V7)
| ~ r1(F,V6)
| ~ r1(sK0,F)
| ~ r1(E,sK1(F,V6,V7,sK2(V8,V9,sK3(A,sK4(sK5)))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A)
| ~ r1(sK0,sK5) ),
inference(resolve,[status(thm)],[c_508,c_515]) ).
cnf(c_843,negated_conjecture,
( ~ r1(V9,sK3(A,sK4(sK5)))
| ~ r1(V8,V9)
| ~ r1(sK0,V8)
| ~ r1(V7,sK2(V8,V9,sK3(A,sK4(sK5))))
| ~ r1(V6,V7)
| ~ r1(F,V6)
| ~ r1(sK0,F)
| ~ r1(E,sK1(F,V6,V7,sK2(V8,V9,sK3(A,sK4(sK5)))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(sK0,B)
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_842]) ).
cnf(c_864,negated_conjecture,
( ~ r1(sK0,sK5)
| r1(sK4(sK5),sK3(A,sK4(sK5)))
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_508,c_526]) ).
cnf(c_865,negated_conjecture,
( r1(sK4(sK5),sK3(A,sK4(sK5)))
| ~ r1(A,sK4(sK5))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_864]) ).
cnf(c_3530,negated_conjecture,
( ~ r1(V8,sK3(sK5,sK4(sK5)))
| ~ r1(V7,V8)
| ~ r1(sK0,V7)
| ~ r1(V6,sK2(V7,V8,sK3(sK5,sK4(sK5))))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(V7,V8,sK3(sK5,sK4(sK5)))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A)
| ~ r1(sK5,sK4(sK5)) ),
inference(resolve,[status(thm)],[c_843,c_716]) ).
cnf(c_1019,negated_conjecture,
( ~ r1(V8,sK3(sK5,sK4(sK5)))
| ~ r1(V7,V8)
| ~ r1(sK0,V7)
| ~ r1(V6,sK2(V7,V8,sK3(sK5,sK4(sK5))))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(V7,V8,sK3(sK5,sK4(sK5)))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_831,c_3530]) ).
cnf(c_3531,negated_conjecture,
( r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5)) ),
inference(resolve,[status(thm)],[c_865,c_716]) ).
cnf(c_1190,negated_conjecture,
r1(sK4(sK5),sK3(sK5,sK4(sK5))),
inference(resolve,[status(thm)],[c_3531,c_831]) ).
cnf(c_3532,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK0,sK5)
| ~ r1(V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5)))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1019,c_831]) ).
cnf(c_3533,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5)))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_3532]) ).
cnf(c_1663,negated_conjecture,
( ~ r1(V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(F,V6)
| ~ r1(E,F)
| ~ r1(sK0,E)
| ~ r1(D,sK1(E,F,V6,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5)))))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1190,c_3533]) ).
cnf(c_3534,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1663,c_839]) ).
cnf(c_3535,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3534]) ).
cnf(c_3536,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3535]) ).
cnf(c_3537,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3536]) ).
cnf(c_3538,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3537]) ).
cnf(c_3539,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3538]) ).
cnf(c_3540,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3539]) ).
cnf(c_3541,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_3540]) ).
cnf(c_3542,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_831,c_3541]) ).
cnf(c_2305,negated_conjecture,
( ~ r1(F,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(E,F)
| ~ r1(D,E)
| ~ r1(sK0,D)
| ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1190,c_3542]) ).
cnf(c_3543,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_2305,c_833]) ).
cnf(c_3544,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3543]) ).
cnf(c_3545,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(sK0,sK5)
| ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(copy,[status(thm)],[c_3544]) ).
cnf(c_3546,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK5,sK4(sK5))
| ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_716,c_3545]) ).
cnf(c_3547,negated_conjecture,
( ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_831,c_3546]) ).
cnf(c_2498,negated_conjecture,
( ~ r1(E,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(sK0,C)
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1190,c_3547]) ).
cnf(c_3548,negated_conjecture,
( ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A)
| ~ r1(sK4(sK5),sK3(sK5,sK4(sK5)))
| ~ r1(sK0,sK5) ),
inference(resolve,[status(thm)],[c_2498,c_831]) ).
cnf(c_3549,negated_conjecture,
( ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A)
| ~ r1(sK4(sK5),sK3(sK5,sK4(sK5))) ),
inference(resolve,[status(thm)],[c_716,c_3548]) ).
cnf(c_2645,negated_conjecture,
( ~ r1(C,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_1190,c_3549]) ).
cnf(c_3550,negated_conjecture,
( r1(sK3(sK5,sK4(sK5)),sK2(A,B,sK3(sK5,sK4(sK5))))
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A)
| ~ r1(sK5,sK4(sK5)) ),
inference(resolve,[status(thm)],[c_833,c_716]) ).
cnf(c_3551,negated_conjecture,
( r1(sK3(sK5,sK4(sK5)),sK2(A,B,sK3(sK5,sK4(sK5))))
| ~ r1(B,sK3(sK5,sK4(sK5)))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_3550,c_831]) ).
cnf(c_3552,negated_conjecture,
( r1(sK3(sK5,sK4(sK5)),sK2(sK5,A,sK3(sK5,sK4(sK5))))
| ~ r1(A,sK3(sK5,sK4(sK5)))
| ~ r1(sK5,A) ),
inference(resolve,[status(thm)],[c_3551,c_716]) ).
cnf(c_3553,negated_conjecture,
( r1(sK3(sK5,sK4(sK5)),sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(sK4(sK5),sK3(sK5,sK4(sK5))) ),
inference(resolve,[status(thm)],[c_3552,c_831]) ).
cnf(c_3528,negated_conjecture,
r1(sK3(sK5,sK4(sK5)),sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5)))),
inference(resolve,[status(thm)],[c_3553,c_1190]) ).
cnf(c_3554,negated_conjecture,
( ~ r1(B,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(A,B)
| ~ r1(sK5,A) ),
inference(resolve,[status(thm)],[c_2645,c_716]) ).
cnf(c_3555,negated_conjecture,
( ~ r1(A,sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5))))
| ~ r1(sK4(sK5),A) ),
inference(resolve,[status(thm)],[c_3554,c_831]) ).
cnf(c_3556,negated_conjecture,
~ r1(sK3(sK5,sK4(sK5)),sK2(sK5,sK4(sK5),sK3(sK5,sK4(sK5)))),
inference(resolve,[status(thm)],[c_3555,c_1190]) ).
cnf(c_3529,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3528,c_3556]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL664+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n006.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Fri Sep 25 23:07:10 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 3984678 was started by sandbox on n006,
% 0.08/0.36 % Fri Sep 25 23:07:10 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 133.03/20.13
% 133.03/20.13 % SZS status Theorem for theBenchmark
% 133.03/20.13
% 133.03/20.13 % Proof 1 at 19.19 (+ 0.08) seconds.
% 133.03/20.13 % Length of proof is 40.
% 133.03/20.13 % Level of proof is 13.
% 133.03/20.13 % Maximum clause weight is 62.000.
% 133.03/20.13 % Given clauses 225.
% 133.03/20.13
% 133.03/20.13 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------