%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL674+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.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:28 AM UTC 2026
% Result : Theorem 24.04s 4.06s
% Output : CNFRefutation 24.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 3
% Syntax : Number of formulae : 106 ( 32 unt; 0 def)
% Number of atoms : 2935 ( 0 equ)
% Maximal formula atoms : 959 ( 27 avg)
% Number of connectives : 4874 (2045 ~;1744 |;1084 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 229 ( 8 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 1 prp; 0-2 aty)
% Number of functors : 41 ( 41 usr; 1 con; 0-1 aty)
% Number of variables : 600 ( 0 sgn 526 !; 43 ?)
% Comments :
%------------------------------------------------------------------------------
fof(reflexivity,axiom,
! [X] : r1(X,X),
file('theBenchmark.p',reflexivity) ).
fof(transitivity,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('theBenchmark.p',transitivity) ).
fof(main,conjecture,
~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(Y) )
& ( ~ p117(Y)
| p116(Y) )
& ( ~ p118(Y)
| p117(Y) )
& ( ~ p119(Y)
| p118(Y) )
& ( ~ p120(Y)
| p119(Y) )
& ( ~ p121(Y)
| p120(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X] :
( ~ p106(X)
| p7(X)
| ~ r1(Y,X) ) )
& ( p7(Y)
| ! [X] :
( ~ p106(X)
| ~ p7(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X] :
( ~ p107(X)
| p8(X)
| ~ r1(Y,X) ) )
& ( p8(Y)
| ! [X] :
( ~ p107(X)
| ~ p8(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X] :
( ~ p108(X)
| p9(X)
| ~ r1(Y,X) ) )
& ( p9(Y)
| ! [X] :
( ~ p108(X)
| ~ p9(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X] :
( ~ p109(X)
| p10(X)
| ~ r1(Y,X) ) )
& ( p10(Y)
| ! [X] :
( ~ p109(X)
| ~ p10(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X] :
( ~ p110(X)
| p11(X)
| ~ r1(Y,X) ) )
& ( p11(Y)
| ! [X] :
( ~ p110(X)
| ~ p11(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p116(Y)
| ( ( ~ p17(Y)
| ! [X] :
( ~ p116(X)
| p17(X)
| ~ r1(Y,X) ) )
& ( p17(Y)
| ! [X] :
( ~ p116(X)
| ~ p17(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p117(Y)
| ( ( ~ p18(Y)
| ! [X] :
( ~ p117(X)
| p18(X)
| ~ r1(Y,X) ) )
& ( p18(Y)
| ! [X] :
( ~ p117(X)
| ~ p18(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p118(Y)
| ( ( ~ p19(Y)
| ! [X] :
( ~ p118(X)
| p19(X)
| ~ r1(Y,X) ) )
& ( p19(Y)
| ! [X] :
( ~ p118(X)
| ~ p19(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p119(Y)
| ( ( ~ p20(Y)
| ! [X] :
( ~ p119(X)
| p20(X)
| ~ r1(Y,X) ) )
& ( p20(Y)
| ! [X] :
( ~ p119(X)
| ~ p20(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p120(Y)
| ( ( ~ p21(Y)
| ! [X] :
( ~ p120(X)
| p21(X)
| ~ r1(Y,X) ) )
& ( p21(Y)
| ! [X] :
( ~ p120(X)
| ~ p21(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p105(Y)
& ~ p106(Y) )
| ( ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& p7(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& ~ p7(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p106(Y)
& ~ p107(Y) )
| ( ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& p8(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& ~ p8(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p107(Y)
& ~ p108(Y) )
| ( ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& p9(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& ~ p9(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p108(Y)
& ~ p109(Y) )
| ( ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& p10(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& ~ p10(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p109(Y)
& ~ p110(Y) )
| ( ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& p11(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& ~ p11(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p110(Y)
& ~ p111(Y) )
| ( ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& p12(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& ~ p12(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p111(Y)
& ~ p112(Y) )
| ( ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& p13(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& ~ p13(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p112(Y)
& ~ p113(Y) )
| ( ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& p14(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& ~ p14(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p113(Y)
& ~ p114(Y) )
| ( ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& p15(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& ~ p15(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p114(Y)
& ~ p115(Y) )
| ( ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& p16(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& ~ p16(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p115(Y)
& ~ p116(Y) )
| ( ~ ! [X] :
( ~ ( p116(X)
& ~ p117(X)
& p17(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p116(X)
& ~ p117(X)
& ~ p17(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p116(Y)
& ~ p117(Y) )
| ( ~ ! [X] :
( ~ ( p117(X)
& ~ p118(X)
& p18(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p117(X)
& ~ p118(X)
& ~ p18(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p117(Y)
& ~ p118(Y) )
| ( ~ ! [X] :
( ~ ( p118(X)
& ~ p119(X)
& p19(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p118(X)
& ~ p119(X)
& ~ p19(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p118(Y)
& ~ p119(Y) )
| ( ~ ! [X] :
( ~ ( p119(X)
& ~ p120(X)
& p20(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p119(X)
& ~ p120(X)
& ~ p20(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p119(Y)
& ~ p120(Y) )
| ( ~ ! [X] :
( ~ ( p120(X)
& ~ p121(X)
& p21(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p120(X)
& ~ p121(X)
& ~ p21(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p8(Y)
| ~ r1(X,Y) ) ),
file('theBenchmark.p',main) ).
fof(main_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(Y) )
& ( ~ p117(Y)
| p116(Y) )
& ( ~ p118(Y)
| p117(Y) )
& ( ~ p119(Y)
| p118(Y) )
& ( ~ p120(Y)
| p119(Y) )
& ( ~ p121(Y)
| p120(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X] :
( ~ p100(X)
| p1(X)
| ~ r1(Y,X) ) )
& ( p1(Y)
| ! [X] :
( ~ p100(X)
| ~ p1(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X] :
( ~ p101(X)
| p2(X)
| ~ r1(Y,X) ) )
& ( p2(Y)
| ! [X] :
( ~ p101(X)
| ~ p2(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X] :
( ~ p102(X)
| p3(X)
| ~ r1(Y,X) ) )
& ( p3(Y)
| ! [X] :
( ~ p102(X)
| ~ p3(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X] :
( ~ p103(X)
| p4(X)
| ~ r1(Y,X) ) )
& ( p4(Y)
| ! [X] :
( ~ p103(X)
| ~ p4(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X] :
( ~ p104(X)
| p5(X)
| ~ r1(Y,X) ) )
& ( p5(Y)
| ! [X] :
( ~ p104(X)
| ~ p5(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X] :
( ~ p105(X)
| p6(X)
| ~ r1(Y,X) ) )
& ( p6(Y)
| ! [X] :
( ~ p105(X)
| ~ p6(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X] :
( ~ p106(X)
| p7(X)
| ~ r1(Y,X) ) )
& ( p7(Y)
| ! [X] :
( ~ p106(X)
| ~ p7(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X] :
( ~ p107(X)
| p8(X)
| ~ r1(Y,X) ) )
& ( p8(Y)
| ! [X] :
( ~ p107(X)
| ~ p8(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X] :
( ~ p108(X)
| p9(X)
| ~ r1(Y,X) ) )
& ( p9(Y)
| ! [X] :
( ~ p108(X)
| ~ p9(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X] :
( ~ p109(X)
| p10(X)
| ~ r1(Y,X) ) )
& ( p10(Y)
| ! [X] :
( ~ p109(X)
| ~ p10(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X] :
( ~ p110(X)
| p11(X)
| ~ r1(Y,X) ) )
& ( p11(Y)
| ! [X] :
( ~ p110(X)
| ~ p11(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X] :
( ~ p111(X)
| p12(X)
| ~ r1(Y,X) ) )
& ( p12(Y)
| ! [X] :
( ~ p111(X)
| ~ p12(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X] :
( ~ p112(X)
| p13(X)
| ~ r1(Y,X) ) )
& ( p13(Y)
| ! [X] :
( ~ p112(X)
| ~ p13(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X] :
( ~ p113(X)
| p14(X)
| ~ r1(Y,X) ) )
& ( p14(Y)
| ! [X] :
( ~ p113(X)
| ~ p14(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X] :
( ~ p114(X)
| p15(X)
| ~ r1(Y,X) ) )
& ( p15(Y)
| ! [X] :
( ~ p114(X)
| ~ p15(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X] :
( ~ p115(X)
| p16(X)
| ~ r1(Y,X) ) )
& ( p16(Y)
| ! [X] :
( ~ p115(X)
| ~ p16(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p116(Y)
| ( ( ~ p17(Y)
| ! [X] :
( ~ p116(X)
| p17(X)
| ~ r1(Y,X) ) )
& ( p17(Y)
| ! [X] :
( ~ p116(X)
| ~ p17(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p117(Y)
| ( ( ~ p18(Y)
| ! [X] :
( ~ p117(X)
| p18(X)
| ~ r1(Y,X) ) )
& ( p18(Y)
| ! [X] :
( ~ p117(X)
| ~ p18(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p118(Y)
| ( ( ~ p19(Y)
| ! [X] :
( ~ p118(X)
| p19(X)
| ~ r1(Y,X) ) )
& ( p19(Y)
| ! [X] :
( ~ p118(X)
| ~ p19(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p119(Y)
| ( ( ~ p20(Y)
| ! [X] :
( ~ p119(X)
| p20(X)
| ~ r1(Y,X) ) )
& ( p20(Y)
| ! [X] :
( ~ p119(X)
| ~ p20(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ p120(Y)
| ( ( ~ p21(Y)
| ! [X] :
( ~ p120(X)
| p21(X)
| ~ r1(Y,X) ) )
& ( p21(Y)
| ! [X] :
( ~ p120(X)
| ~ p21(X)
| ~ r1(Y,X) ) ) ) )
& ( ~ ( p100(Y)
& ~ p101(Y) )
| ( ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& p2(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p101(X)
& ~ p102(X)
& ~ p2(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p101(Y)
& ~ p102(Y) )
| ( ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& p3(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p102(X)
& ~ p103(X)
& ~ p3(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p102(Y)
& ~ p103(Y) )
| ( ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& p4(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p103(X)
& ~ p104(X)
& ~ p4(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p103(Y)
& ~ p104(Y) )
| ( ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& p5(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p104(X)
& ~ p105(X)
& ~ p5(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p104(Y)
& ~ p105(Y) )
| ( ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& p6(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p105(X)
& ~ p106(X)
& ~ p6(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p105(Y)
& ~ p106(Y) )
| ( ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& p7(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p106(X)
& ~ p107(X)
& ~ p7(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p106(Y)
& ~ p107(Y) )
| ( ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& p8(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p107(X)
& ~ p108(X)
& ~ p8(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p107(Y)
& ~ p108(Y) )
| ( ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& p9(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p108(X)
& ~ p109(X)
& ~ p9(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p108(Y)
& ~ p109(Y) )
| ( ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& p10(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p109(X)
& ~ p110(X)
& ~ p10(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p109(Y)
& ~ p110(Y) )
| ( ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& p11(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p110(X)
& ~ p111(X)
& ~ p11(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p110(Y)
& ~ p111(Y) )
| ( ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& p12(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p111(X)
& ~ p112(X)
& ~ p12(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p111(Y)
& ~ p112(Y) )
| ( ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& p13(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p112(X)
& ~ p113(X)
& ~ p13(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p112(Y)
& ~ p113(Y) )
| ( ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& p14(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p113(X)
& ~ p114(X)
& ~ p14(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p113(Y)
& ~ p114(Y) )
| ( ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& p15(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p114(X)
& ~ p115(X)
& ~ p15(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p114(Y)
& ~ p115(Y) )
| ( ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& p16(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p115(X)
& ~ p116(X)
& ~ p16(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p115(Y)
& ~ p116(Y) )
| ( ~ ! [X] :
( ~ ( p116(X)
& ~ p117(X)
& p17(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p116(X)
& ~ p117(X)
& ~ p17(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p116(Y)
& ~ p117(Y) )
| ( ~ ! [X] :
( ~ ( p117(X)
& ~ p118(X)
& p18(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p117(X)
& ~ p118(X)
& ~ p18(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p117(Y)
& ~ p118(Y) )
| ( ~ ! [X] :
( ~ ( p118(X)
& ~ p119(X)
& p19(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p118(X)
& ~ p119(X)
& ~ p19(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p118(Y)
& ~ p119(Y) )
| ( ~ ! [X] :
( ~ ( p119(X)
& ~ p120(X)
& p20(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p119(X)
& ~ p120(X)
& ~ p20(X) )
| ~ r1(Y,X) ) ) )
& ( ~ ( p119(Y)
& ~ p120(Y) )
| ( ~ ! [X] :
( ~ ( p120(X)
& ~ p121(X)
& p21(X) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p120(X)
& ~ p121(X)
& ~ p21(X) )
| ~ r1(Y,X) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p8(Y)
| ~ r1(X,Y) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(nnf_3,plain,
? [X] :
( p100(X)
& ~ p101(X)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(Y) )
& ( ~ p117(Y)
| p116(Y) )
& ( ~ p118(Y)
| p117(Y) )
& ( ~ p119(Y)
| p118(Y) )
& ( ~ p120(Y)
| p119(Y) )
& ( ~ p121(Y)
| p120(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X82] :
( ~ p100(X82)
| p1(X82)
| ~ r1(Y,X82) ) )
& ( p1(Y)
| ! [X81] :
( ~ p100(X81)
| ~ p1(X81)
| ~ r1(Y,X81) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X80] :
( ~ p101(X80)
| p2(X80)
| ~ r1(Y,X80) ) )
& ( p2(Y)
| ! [X79] :
( ~ p101(X79)
| ~ p2(X79)
| ~ r1(Y,X79) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X78] :
( ~ p102(X78)
| p3(X78)
| ~ r1(Y,X78) ) )
& ( p3(Y)
| ! [X77] :
( ~ p102(X77)
| ~ p3(X77)
| ~ r1(Y,X77) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X76] :
( ~ p103(X76)
| p4(X76)
| ~ r1(Y,X76) ) )
& ( p4(Y)
| ! [X75] :
( ~ p103(X75)
| ~ p4(X75)
| ~ r1(Y,X75) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X74] :
( ~ p104(X74)
| p5(X74)
| ~ r1(Y,X74) ) )
& ( p5(Y)
| ! [X73] :
( ~ p104(X73)
| ~ p5(X73)
| ~ r1(Y,X73) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X72] :
( ~ p105(X72)
| p6(X72)
| ~ r1(Y,X72) ) )
& ( p6(Y)
| ! [X71] :
( ~ p105(X71)
| ~ p6(X71)
| ~ r1(Y,X71) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X70] :
( ~ p106(X70)
| p7(X70)
| ~ r1(Y,X70) ) )
& ( p7(Y)
| ! [X69] :
( ~ p106(X69)
| ~ p7(X69)
| ~ r1(Y,X69) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X68] :
( ~ p107(X68)
| p8(X68)
| ~ r1(Y,X68) ) )
& ( p8(Y)
| ! [X67] :
( ~ p107(X67)
| ~ p8(X67)
| ~ r1(Y,X67) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X66] :
( ~ p108(X66)
| p9(X66)
| ~ r1(Y,X66) ) )
& ( p9(Y)
| ! [X65] :
( ~ p108(X65)
| ~ p9(X65)
| ~ r1(Y,X65) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X64] :
( ~ p109(X64)
| p10(X64)
| ~ r1(Y,X64) ) )
& ( p10(Y)
| ! [X63] :
( ~ p109(X63)
| ~ p10(X63)
| ~ r1(Y,X63) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X62] :
( ~ p110(X62)
| p11(X62)
| ~ r1(Y,X62) ) )
& ( p11(Y)
| ! [X61] :
( ~ p110(X61)
| ~ p11(X61)
| ~ r1(Y,X61) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X60] :
( ~ p111(X60)
| p12(X60)
| ~ r1(Y,X60) ) )
& ( p12(Y)
| ! [X59] :
( ~ p111(X59)
| ~ p12(X59)
| ~ r1(Y,X59) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X58] :
( ~ p112(X58)
| p13(X58)
| ~ r1(Y,X58) ) )
& ( p13(Y)
| ! [X57] :
( ~ p112(X57)
| ~ p13(X57)
| ~ r1(Y,X57) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X56] :
( ~ p113(X56)
| p14(X56)
| ~ r1(Y,X56) ) )
& ( p14(Y)
| ! [X55] :
( ~ p113(X55)
| ~ p14(X55)
| ~ r1(Y,X55) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X54] :
( ~ p114(X54)
| p15(X54)
| ~ r1(Y,X54) ) )
& ( p15(Y)
| ! [X53] :
( ~ p114(X53)
| ~ p15(X53)
| ~ r1(Y,X53) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X52] :
( ~ p115(X52)
| p16(X52)
| ~ r1(Y,X52) ) )
& ( p16(Y)
| ! [X51] :
( ~ p115(X51)
| ~ p16(X51)
| ~ r1(Y,X51) ) ) ) )
& ( ~ p116(Y)
| ( ( ~ p17(Y)
| ! [X50] :
( ~ p116(X50)
| p17(X50)
| ~ r1(Y,X50) ) )
& ( p17(Y)
| ! [X49] :
( ~ p116(X49)
| ~ p17(X49)
| ~ r1(Y,X49) ) ) ) )
& ( ~ p117(Y)
| ( ( ~ p18(Y)
| ! [X48] :
( ~ p117(X48)
| p18(X48)
| ~ r1(Y,X48) ) )
& ( p18(Y)
| ! [X47] :
( ~ p117(X47)
| ~ p18(X47)
| ~ r1(Y,X47) ) ) ) )
& ( ~ p118(Y)
| ( ( ~ p19(Y)
| ! [X46] :
( ~ p118(X46)
| p19(X46)
| ~ r1(Y,X46) ) )
& ( p19(Y)
| ! [X45] :
( ~ p118(X45)
| ~ p19(X45)
| ~ r1(Y,X45) ) ) ) )
& ( ~ p119(Y)
| ( ( ~ p20(Y)
| ! [X44] :
( ~ p119(X44)
| p20(X44)
| ~ r1(Y,X44) ) )
& ( p20(Y)
| ! [X43] :
( ~ p119(X43)
| ~ p20(X43)
| ~ r1(Y,X43) ) ) ) )
& ( ~ p120(Y)
| ( ( ~ p21(Y)
| ! [X42] :
( ~ p120(X42)
| p21(X42)
| ~ r1(Y,X42) ) )
& ( p21(Y)
| ! [X41] :
( ~ p120(X41)
| ~ p21(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( ? [X40] :
( p101(X40)
& ~ p102(X40)
& p2(X40)
& r1(Y,X40) )
& ? [X39] :
( p101(X39)
& ~ p102(X39)
& ~ p2(X39)
& r1(Y,X39) ) ) )
& ( ~ p101(Y)
| p102(Y)
| ( ? [X38] :
( p102(X38)
& ~ p103(X38)
& p3(X38)
& r1(Y,X38) )
& ? [X37] :
( p102(X37)
& ~ p103(X37)
& ~ p3(X37)
& r1(Y,X37) ) ) )
& ( ~ p102(Y)
| p103(Y)
| ( ? [X36] :
( p103(X36)
& ~ p104(X36)
& p4(X36)
& r1(Y,X36) )
& ? [X35] :
( p103(X35)
& ~ p104(X35)
& ~ p4(X35)
& r1(Y,X35) ) ) )
& ( ~ p103(Y)
| p104(Y)
| ( ? [X34] :
( p104(X34)
& ~ p105(X34)
& p5(X34)
& r1(Y,X34) )
& ? [X33] :
( p104(X33)
& ~ p105(X33)
& ~ p5(X33)
& r1(Y,X33) ) ) )
& ( ~ p104(Y)
| p105(Y)
| ( ? [X32] :
( p105(X32)
& ~ p106(X32)
& p6(X32)
& r1(Y,X32) )
& ? [X31] :
( p105(X31)
& ~ p106(X31)
& ~ p6(X31)
& r1(Y,X31) ) ) )
& ( ~ p105(Y)
| p106(Y)
| ( ? [X30] :
( p106(X30)
& ~ p107(X30)
& p7(X30)
& r1(Y,X30) )
& ? [X29] :
( p106(X29)
& ~ p107(X29)
& ~ p7(X29)
& r1(Y,X29) ) ) )
& ( ~ p106(Y)
| p107(Y)
| ( ? [X28] :
( p107(X28)
& ~ p108(X28)
& p8(X28)
& r1(Y,X28) )
& ? [X27] :
( p107(X27)
& ~ p108(X27)
& ~ p8(X27)
& r1(Y,X27) ) ) )
& ( ~ p107(Y)
| p108(Y)
| ( ? [X26] :
( p108(X26)
& ~ p109(X26)
& p9(X26)
& r1(Y,X26) )
& ? [X25] :
( p108(X25)
& ~ p109(X25)
& ~ p9(X25)
& r1(Y,X25) ) ) )
& ( ~ p108(Y)
| p109(Y)
| ( ? [X24] :
( p109(X24)
& ~ p110(X24)
& p10(X24)
& r1(Y,X24) )
& ? [X23] :
( p109(X23)
& ~ p110(X23)
& ~ p10(X23)
& r1(Y,X23) ) ) )
& ( ~ p109(Y)
| p110(Y)
| ( ? [X22] :
( p110(X22)
& ~ p111(X22)
& p11(X22)
& r1(Y,X22) )
& ? [X21] :
( p110(X21)
& ~ p111(X21)
& ~ p11(X21)
& r1(Y,X21) ) ) )
& ( ~ p110(Y)
| p111(Y)
| ( ? [X20] :
( p111(X20)
& ~ p112(X20)
& p12(X20)
& r1(Y,X20) )
& ? [X19] :
( p111(X19)
& ~ p112(X19)
& ~ p12(X19)
& r1(Y,X19) ) ) )
& ( ~ p111(Y)
| p112(Y)
| ( ? [X18] :
( p112(X18)
& ~ p113(X18)
& p13(X18)
& r1(Y,X18) )
& ? [X17] :
( p112(X17)
& ~ p113(X17)
& ~ p13(X17)
& r1(Y,X17) ) ) )
& ( ~ p112(Y)
| p113(Y)
| ( ? [X16] :
( p113(X16)
& ~ p114(X16)
& p14(X16)
& r1(Y,X16) )
& ? [X15] :
( p113(X15)
& ~ p114(X15)
& ~ p14(X15)
& r1(Y,X15) ) ) )
& ( ~ p113(Y)
| p114(Y)
| ( ? [X14] :
( p114(X14)
& ~ p115(X14)
& p15(X14)
& r1(Y,X14) )
& ? [X13] :
( p114(X13)
& ~ p115(X13)
& ~ p15(X13)
& r1(Y,X13) ) ) )
& ( ~ p114(Y)
| p115(Y)
| ( ? [X12] :
( p115(X12)
& ~ p116(X12)
& p16(X12)
& r1(Y,X12) )
& ? [X11] :
( p115(X11)
& ~ p116(X11)
& ~ p16(X11)
& r1(Y,X11) ) ) )
& ( ~ p115(Y)
| p116(Y)
| ( ? [X10] :
( p116(X10)
& ~ p117(X10)
& p17(X10)
& r1(Y,X10) )
& ? [X9] :
( p116(X9)
& ~ p117(X9)
& ~ p17(X9)
& r1(Y,X9) ) ) )
& ( ~ p116(Y)
| p117(Y)
| ( ? [X8] :
( p117(X8)
& ~ p118(X8)
& p18(X8)
& r1(Y,X8) )
& ? [X7] :
( p117(X7)
& ~ p118(X7)
& ~ p18(X7)
& r1(Y,X7) ) ) )
& ( ~ p117(Y)
| p118(Y)
| ( ? [X6] :
( p118(X6)
& ~ p119(X6)
& p19(X6)
& r1(Y,X6) )
& ? [X5] :
( p118(X5)
& ~ p119(X5)
& ~ p19(X5)
& r1(Y,X5) ) ) )
& ( ~ p118(Y)
| p119(Y)
| ( ? [X4] :
( p119(X4)
& ~ p120(X4)
& p20(X4)
& r1(Y,X4) )
& ? [X3] :
( p119(X3)
& ~ p120(X3)
& ~ p20(X3)
& r1(Y,X3) ) ) )
& ( ~ p119(Y)
| p120(Y)
| ( ? [X2] :
( p120(X2)
& ~ p121(X2)
& p21(X2)
& r1(Y,X2) )
& ? [X1] :
( p120(X1)
& ~ p121(X1)
& ~ p21(X1)
& r1(Y,X1) ) ) ) )
| ~ r1(X,Y) )
& ! [X0] :
( p8(X0)
| ~ r1(X,X0) ) ),
inference(fof_nnf,[status(thm)],[main_neg]) ).
fof(sk_main_neg_sk,plain,
( p100(sK0)
& ~ p101(sK0)
& ! [Y] :
( ( ( ~ p101(Y)
| p100(Y) )
& ( ~ p102(Y)
| p101(Y) )
& ( ~ p103(Y)
| p102(Y) )
& ( ~ p104(Y)
| p103(Y) )
& ( ~ p105(Y)
| p104(Y) )
& ( ~ p106(Y)
| p105(Y) )
& ( ~ p107(Y)
| p106(Y) )
& ( ~ p108(Y)
| p107(Y) )
& ( ~ p109(Y)
| p108(Y) )
& ( ~ p110(Y)
| p109(Y) )
& ( ~ p111(Y)
| p110(Y) )
& ( ~ p112(Y)
| p111(Y) )
& ( ~ p113(Y)
| p112(Y) )
& ( ~ p114(Y)
| p113(Y) )
& ( ~ p115(Y)
| p114(Y) )
& ( ~ p116(Y)
| p115(Y) )
& ( ~ p117(Y)
| p116(Y) )
& ( ~ p118(Y)
| p117(Y) )
& ( ~ p119(Y)
| p118(Y) )
& ( ~ p120(Y)
| p119(Y) )
& ( ~ p121(Y)
| p120(Y) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X82] :
( ~ p100(X82)
| p1(X82)
| ~ r1(Y,X82) ) )
& ( p1(Y)
| ! [X81] :
( ~ p100(X81)
| ~ p1(X81)
| ~ r1(Y,X81) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X80] :
( ~ p101(X80)
| p2(X80)
| ~ r1(Y,X80) ) )
& ( p2(Y)
| ! [X79] :
( ~ p101(X79)
| ~ p2(X79)
| ~ r1(Y,X79) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X78] :
( ~ p102(X78)
| p3(X78)
| ~ r1(Y,X78) ) )
& ( p3(Y)
| ! [X77] :
( ~ p102(X77)
| ~ p3(X77)
| ~ r1(Y,X77) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X76] :
( ~ p103(X76)
| p4(X76)
| ~ r1(Y,X76) ) )
& ( p4(Y)
| ! [X75] :
( ~ p103(X75)
| ~ p4(X75)
| ~ r1(Y,X75) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X74] :
( ~ p104(X74)
| p5(X74)
| ~ r1(Y,X74) ) )
& ( p5(Y)
| ! [X73] :
( ~ p104(X73)
| ~ p5(X73)
| ~ r1(Y,X73) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X72] :
( ~ p105(X72)
| p6(X72)
| ~ r1(Y,X72) ) )
& ( p6(Y)
| ! [X71] :
( ~ p105(X71)
| ~ p6(X71)
| ~ r1(Y,X71) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X70] :
( ~ p106(X70)
| p7(X70)
| ~ r1(Y,X70) ) )
& ( p7(Y)
| ! [X69] :
( ~ p106(X69)
| ~ p7(X69)
| ~ r1(Y,X69) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X68] :
( ~ p107(X68)
| p8(X68)
| ~ r1(Y,X68) ) )
& ( p8(Y)
| ! [X67] :
( ~ p107(X67)
| ~ p8(X67)
| ~ r1(Y,X67) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X66] :
( ~ p108(X66)
| p9(X66)
| ~ r1(Y,X66) ) )
& ( p9(Y)
| ! [X65] :
( ~ p108(X65)
| ~ p9(X65)
| ~ r1(Y,X65) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X64] :
( ~ p109(X64)
| p10(X64)
| ~ r1(Y,X64) ) )
& ( p10(Y)
| ! [X63] :
( ~ p109(X63)
| ~ p10(X63)
| ~ r1(Y,X63) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X62] :
( ~ p110(X62)
| p11(X62)
| ~ r1(Y,X62) ) )
& ( p11(Y)
| ! [X61] :
( ~ p110(X61)
| ~ p11(X61)
| ~ r1(Y,X61) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X60] :
( ~ p111(X60)
| p12(X60)
| ~ r1(Y,X60) ) )
& ( p12(Y)
| ! [X59] :
( ~ p111(X59)
| ~ p12(X59)
| ~ r1(Y,X59) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X58] :
( ~ p112(X58)
| p13(X58)
| ~ r1(Y,X58) ) )
& ( p13(Y)
| ! [X57] :
( ~ p112(X57)
| ~ p13(X57)
| ~ r1(Y,X57) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X56] :
( ~ p113(X56)
| p14(X56)
| ~ r1(Y,X56) ) )
& ( p14(Y)
| ! [X55] :
( ~ p113(X55)
| ~ p14(X55)
| ~ r1(Y,X55) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X54] :
( ~ p114(X54)
| p15(X54)
| ~ r1(Y,X54) ) )
& ( p15(Y)
| ! [X53] :
( ~ p114(X53)
| ~ p15(X53)
| ~ r1(Y,X53) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X52] :
( ~ p115(X52)
| p16(X52)
| ~ r1(Y,X52) ) )
& ( p16(Y)
| ! [X51] :
( ~ p115(X51)
| ~ p16(X51)
| ~ r1(Y,X51) ) ) ) )
& ( ~ p116(Y)
| ( ( ~ p17(Y)
| ! [X50] :
( ~ p116(X50)
| p17(X50)
| ~ r1(Y,X50) ) )
& ( p17(Y)
| ! [X49] :
( ~ p116(X49)
| ~ p17(X49)
| ~ r1(Y,X49) ) ) ) )
& ( ~ p117(Y)
| ( ( ~ p18(Y)
| ! [X48] :
( ~ p117(X48)
| p18(X48)
| ~ r1(Y,X48) ) )
& ( p18(Y)
| ! [X47] :
( ~ p117(X47)
| ~ p18(X47)
| ~ r1(Y,X47) ) ) ) )
& ( ~ p118(Y)
| ( ( ~ p19(Y)
| ! [X46] :
( ~ p118(X46)
| p19(X46)
| ~ r1(Y,X46) ) )
& ( p19(Y)
| ! [X45] :
( ~ p118(X45)
| ~ p19(X45)
| ~ r1(Y,X45) ) ) ) )
& ( ~ p119(Y)
| ( ( ~ p20(Y)
| ! [X44] :
( ~ p119(X44)
| p20(X44)
| ~ r1(Y,X44) ) )
& ( p20(Y)
| ! [X43] :
( ~ p119(X43)
| ~ p20(X43)
| ~ r1(Y,X43) ) ) ) )
& ( ~ p120(Y)
| ( ( ~ p21(Y)
| ! [X42] :
( ~ p120(X42)
| p21(X42)
| ~ r1(Y,X42) ) )
& ( p21(Y)
| ! [X41] :
( ~ p120(X41)
| ~ p21(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sK40(Y))
& ~ p102(sK40(Y))
& p2(sK40(Y))
& r1(Y,sK40(Y))
& p101(sK1(Y))
& ~ p102(sK1(Y))
& ~ p2(sK1(Y))
& r1(Y,sK1(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK39(Y))
& ~ p103(sK39(Y))
& p3(sK39(Y))
& r1(Y,sK39(Y))
& p102(sK2(Y))
& ~ p103(sK2(Y))
& ~ p3(sK2(Y))
& r1(Y,sK2(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK38(Y))
& ~ p104(sK38(Y))
& p4(sK38(Y))
& r1(Y,sK38(Y))
& p103(sK3(Y))
& ~ p104(sK3(Y))
& ~ p4(sK3(Y))
& r1(Y,sK3(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK37(Y))
& ~ p105(sK37(Y))
& p5(sK37(Y))
& r1(Y,sK37(Y))
& p104(sK4(Y))
& ~ p105(sK4(Y))
& ~ p5(sK4(Y))
& r1(Y,sK4(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK36(Y))
& ~ p106(sK36(Y))
& p6(sK36(Y))
& r1(Y,sK36(Y))
& p105(sK5(Y))
& ~ p106(sK5(Y))
& ~ p6(sK5(Y))
& r1(Y,sK5(Y)) ) )
& ( ~ p105(Y)
| p106(Y)
| ( p106(sK35(Y))
& ~ p107(sK35(Y))
& p7(sK35(Y))
& r1(Y,sK35(Y))
& p106(sK6(Y))
& ~ p107(sK6(Y))
& ~ p7(sK6(Y))
& r1(Y,sK6(Y)) ) )
& ( ~ p106(Y)
| p107(Y)
| ( p107(sK34(Y))
& ~ p108(sK34(Y))
& p8(sK34(Y))
& r1(Y,sK34(Y))
& p107(sK7(Y))
& ~ p108(sK7(Y))
& ~ p8(sK7(Y))
& r1(Y,sK7(Y)) ) )
& ( ~ p107(Y)
| p108(Y)
| ( p108(sK33(Y))
& ~ p109(sK33(Y))
& p9(sK33(Y))
& r1(Y,sK33(Y))
& p108(sK32(Y))
& ~ p109(sK32(Y))
& ~ p9(sK32(Y))
& r1(Y,sK32(Y)) ) )
& ( ~ p108(Y)
| p109(Y)
| ( p109(sK31(Y))
& ~ p110(sK31(Y))
& p10(sK31(Y))
& r1(Y,sK31(Y))
& p109(sK30(Y))
& ~ p110(sK30(Y))
& ~ p10(sK30(Y))
& r1(Y,sK30(Y)) ) )
& ( ~ p109(Y)
| p110(Y)
| ( p110(sK29(Y))
& ~ p111(sK29(Y))
& p11(sK29(Y))
& r1(Y,sK29(Y))
& p110(sK28(Y))
& ~ p111(sK28(Y))
& ~ p11(sK28(Y))
& r1(Y,sK28(Y)) ) )
& ( ~ p110(Y)
| p111(Y)
| ( p111(sK27(Y))
& ~ p112(sK27(Y))
& p12(sK27(Y))
& r1(Y,sK27(Y))
& p111(sK26(Y))
& ~ p112(sK26(Y))
& ~ p12(sK26(Y))
& r1(Y,sK26(Y)) ) )
& ( ~ p111(Y)
| p112(Y)
| ( p112(sK25(Y))
& ~ p113(sK25(Y))
& p13(sK25(Y))
& r1(Y,sK25(Y))
& p112(sK24(Y))
& ~ p113(sK24(Y))
& ~ p13(sK24(Y))
& r1(Y,sK24(Y)) ) )
& ( ~ p112(Y)
| p113(Y)
| ( p113(sK23(Y))
& ~ p114(sK23(Y))
& p14(sK23(Y))
& r1(Y,sK23(Y))
& p113(sK22(Y))
& ~ p114(sK22(Y))
& ~ p14(sK22(Y))
& r1(Y,sK22(Y)) ) )
& ( ~ p113(Y)
| p114(Y)
| ( p114(sK21(Y))
& ~ p115(sK21(Y))
& p15(sK21(Y))
& r1(Y,sK21(Y))
& p114(sK20(Y))
& ~ p115(sK20(Y))
& ~ p15(sK20(Y))
& r1(Y,sK20(Y)) ) )
& ( ~ p114(Y)
| p115(Y)
| ( p115(sK19(Y))
& ~ p116(sK19(Y))
& p16(sK19(Y))
& r1(Y,sK19(Y))
& p115(sK18(Y))
& ~ p116(sK18(Y))
& ~ p16(sK18(Y))
& r1(Y,sK18(Y)) ) )
& ( ~ p115(Y)
| p116(Y)
| ( p116(sK17(Y))
& ~ p117(sK17(Y))
& p17(sK17(Y))
& r1(Y,sK17(Y))
& p116(sK16(Y))
& ~ p117(sK16(Y))
& ~ p17(sK16(Y))
& r1(Y,sK16(Y)) ) )
& ( ~ p116(Y)
| p117(Y)
| ( p117(sK15(Y))
& ~ p118(sK15(Y))
& p18(sK15(Y))
& r1(Y,sK15(Y))
& p117(sK14(Y))
& ~ p118(sK14(Y))
& ~ p18(sK14(Y))
& r1(Y,sK14(Y)) ) )
& ( ~ p117(Y)
| p118(Y)
| ( p118(sK13(Y))
& ~ p119(sK13(Y))
& p19(sK13(Y))
& r1(Y,sK13(Y))
& p118(sK12(Y))
& ~ p119(sK12(Y))
& ~ p19(sK12(Y))
& r1(Y,sK12(Y)) ) )
& ( ~ p118(Y)
| p119(Y)
| ( p119(sK11(Y))
& ~ p120(sK11(Y))
& p20(sK11(Y))
& r1(Y,sK11(Y))
& p119(sK10(Y))
& ~ p120(sK10(Y))
& ~ p20(sK10(Y))
& r1(Y,sK10(Y)) ) )
& ( ~ p119(Y)
| p120(Y)
| ( p120(sK9(Y))
& ~ p121(sK9(Y))
& p21(sK9(Y))
& r1(Y,sK9(Y))
& p120(sK8(Y))
& ~ p121(sK8(Y))
& ~ p21(sK8(Y))
& r1(Y,sK8(Y)) ) ) )
| ~ r1(sK0,Y) )
& ! [X0] :
( p8(X0)
| ~ r1(sK0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,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,sK7,sK34,sK6,sK35,sK5,sK36,sK4,sK37,sK3,sK38,sK2,sK39,sK1,sK40]),skolemize(X,sK0),skolemize(X1,sK8(Y)),skolemize(X2,sK9(Y)),skolemize(X3,sK10(Y)),skolemize(X4,sK11(Y)),skolemize(X5,sK12(Y)),skolemize(X6,sK13(Y)),skolemize(X7,sK14(Y)),skolemize(X8,sK15(Y)),skolemize(X9,sK16(Y)),skolemize(X10,sK17(Y)),skolemize(X11,sK18(Y)),skolemize(X12,sK19(Y)),skolemize(X13,sK20(Y)),skolemize(X14,sK21(Y)),skolemize(X15,sK22(Y)),skolemize(X16,sK23(Y)),skolemize(X17,sK24(Y)),skolemize(X18,sK25(Y)),skolemize(X19,sK26(Y)),skolemize(X20,sK27(Y)),skolemize(X21,sK28(Y)),skolemize(X22,sK29(Y)),skolemize(X23,sK30(Y)),skolemize(X24,sK31(Y)),skolemize(X25,sK32(Y)),skolemize(X26,sK33(Y)),skolemize(X27,sK7(Y)),skolemize(X28,sK34(Y)),skolemize(X29,sK6(Y)),skolemize(X30,sK35(Y)),skolemize(X31,sK5(Y)),skolemize(X32,sK36(Y)),skolemize(X33,sK4(Y)),skolemize(X34,sK37(Y)),skolemize(X35,sK3(Y)),skolemize(X36,sK38(Y)),skolemize(X37,sK2(Y)),skolemize(X38,sK39(Y)),skolemize(X39,sK1(Y)),skolemize(X40,sK40(Y))],[nnf_3]) ).
fof(sk_main_neg,plain,
( p100(sK0)
& ~ p101(sK0)
& ! [VAR_0] :
( ~ p101(VAR_0)
| p100(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p101(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p102(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p103(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p104(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p105(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p106(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p107(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p108(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p109(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p110(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p111(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p112(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p113(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p114(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p115(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p116(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p117(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p118(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p120(VAR_0)
| p119(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p121(VAR_0)
| p120(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_0)
| ~ p1(VAR_0)
| ~ p100(VAR_1)
| p1(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_0)
| p1(VAR_0)
| ~ p100(VAR_1)
| ~ p1(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_0)
| ~ p2(VAR_0)
| ~ p101(VAR_1)
| p2(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_0)
| p2(VAR_0)
| ~ p101(VAR_1)
| ~ p2(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_0)
| ~ p3(VAR_0)
| ~ p102(VAR_1)
| p3(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_0)
| p3(VAR_0)
| ~ p102(VAR_1)
| ~ p3(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_0)
| ~ p4(VAR_0)
| ~ p103(VAR_1)
| p4(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_0)
| p4(VAR_0)
| ~ p103(VAR_1)
| ~ p4(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_0)
| ~ p5(VAR_0)
| ~ p104(VAR_1)
| p5(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_0)
| p5(VAR_0)
| ~ p104(VAR_1)
| ~ p5(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p105(VAR_0)
| ~ p6(VAR_0)
| ~ p105(VAR_1)
| p6(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p105(VAR_0)
| p6(VAR_0)
| ~ p105(VAR_1)
| ~ p6(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p106(VAR_0)
| ~ p7(VAR_0)
| ~ p106(VAR_1)
| p7(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p106(VAR_0)
| p7(VAR_0)
| ~ p106(VAR_1)
| ~ p7(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p107(VAR_0)
| ~ p8(VAR_0)
| ~ p107(VAR_1)
| p8(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p107(VAR_0)
| p8(VAR_0)
| ~ p107(VAR_1)
| ~ p8(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p108(VAR_0)
| ~ p9(VAR_0)
| ~ p108(VAR_1)
| p9(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p108(VAR_0)
| p9(VAR_0)
| ~ p108(VAR_1)
| ~ p9(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p109(VAR_0)
| ~ p10(VAR_0)
| ~ p109(VAR_1)
| p10(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p109(VAR_0)
| p10(VAR_0)
| ~ p109(VAR_1)
| ~ p10(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p110(VAR_0)
| ~ p11(VAR_0)
| ~ p110(VAR_1)
| p11(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p110(VAR_0)
| p11(VAR_0)
| ~ p110(VAR_1)
| ~ p11(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p111(VAR_0)
| ~ p12(VAR_0)
| ~ p111(VAR_1)
| p12(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p111(VAR_0)
| p12(VAR_0)
| ~ p111(VAR_1)
| ~ p12(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p112(VAR_0)
| ~ p13(VAR_0)
| ~ p112(VAR_1)
| p13(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p112(VAR_0)
| p13(VAR_0)
| ~ p112(VAR_1)
| ~ p13(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p113(VAR_0)
| ~ p14(VAR_0)
| ~ p113(VAR_1)
| p14(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p113(VAR_0)
| p14(VAR_0)
| ~ p113(VAR_1)
| ~ p14(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p114(VAR_0)
| ~ p15(VAR_0)
| ~ p114(VAR_1)
| p15(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p114(VAR_0)
| p15(VAR_0)
| ~ p114(VAR_1)
| ~ p15(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p115(VAR_0)
| ~ p16(VAR_0)
| ~ p115(VAR_1)
| p16(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p115(VAR_0)
| p16(VAR_0)
| ~ p115(VAR_1)
| ~ p16(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p116(VAR_0)
| ~ p17(VAR_0)
| ~ p116(VAR_1)
| p17(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p116(VAR_0)
| p17(VAR_0)
| ~ p116(VAR_1)
| ~ p17(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p117(VAR_0)
| ~ p18(VAR_0)
| ~ p117(VAR_1)
| p18(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p117(VAR_0)
| p18(VAR_0)
| ~ p117(VAR_1)
| ~ p18(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p118(VAR_0)
| ~ p19(VAR_0)
| ~ p118(VAR_1)
| p19(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p118(VAR_0)
| p19(VAR_0)
| ~ p118(VAR_1)
| ~ p19(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p119(VAR_0)
| ~ p20(VAR_0)
| ~ p119(VAR_1)
| p20(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p119(VAR_0)
| p20(VAR_0)
| ~ p119(VAR_1)
| ~ p20(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p120(VAR_0)
| ~ p21(VAR_0)
| ~ p120(VAR_1)
| p21(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p120(VAR_0)
| p21(VAR_0)
| ~ p120(VAR_1)
| ~ p21(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK40(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK40(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p2(sK40(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK40(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p2(sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK1(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p102(sK39(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK39(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p3(sK39(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK39(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p102(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p3(sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK2(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p103(sK38(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK38(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p4(sK38(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK38(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p103(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p4(sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK3(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK37(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK37(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p5(sK37(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK37(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p5(sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK4(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK36(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK36(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p6(sK36(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK36(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p6(sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK5(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p106(sK35(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p107(sK35(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p7(sK35(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| r1(VAR_0,sK35(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p106(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p107(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p7(sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| r1(VAR_0,sK6(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p107(sK34(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK34(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p8(sK34(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK34(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p107(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p8(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK33(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK33(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p9(sK33(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK33(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK32(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK32(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p9(sK32(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK32(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK31(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK31(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p10(sK31(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK31(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p10(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p11(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p11(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p111(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p112(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p12(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| r1(VAR_0,sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p111(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p112(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p12(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| r1(VAR_0,sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p112(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p113(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p13(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| r1(VAR_0,sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p112(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p113(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p13(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| r1(VAR_0,sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p113(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p114(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p14(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| r1(VAR_0,sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p113(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p114(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p14(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| r1(VAR_0,sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p114(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p115(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p15(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| r1(VAR_0,sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p114(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p115(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p15(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| r1(VAR_0,sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p115(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p116(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p16(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| r1(VAR_0,sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p115(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p116(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p16(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| r1(VAR_0,sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| p116(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| ~ p117(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| p17(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| r1(VAR_0,sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| p116(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| ~ p117(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| ~ p17(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p115(VAR_0)
| p116(VAR_0)
| r1(VAR_0,sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| p117(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| ~ p118(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| p18(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| r1(VAR_0,sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| p117(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| ~ p118(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| ~ p18(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p116(VAR_0)
| p117(VAR_0)
| r1(VAR_0,sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| p118(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| ~ p119(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| p19(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| r1(VAR_0,sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| p118(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| ~ p119(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| ~ p19(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p117(VAR_0)
| p118(VAR_0)
| r1(VAR_0,sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| p119(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| ~ p120(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| p20(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| r1(VAR_0,sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| p119(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| ~ p120(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| ~ p20(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p118(VAR_0)
| p119(VAR_0)
| r1(VAR_0,sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| p120(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| ~ p121(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| p21(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| r1(VAR_0,sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| p120(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| ~ p121(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| ~ p21(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p119(VAR_0)
| p120(VAR_0)
| r1(VAR_0,sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p8(VAR_0)
| ~ r1(sK0,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_main_neg_sk]) ).
cnf(c_4,negated_conjecture,
p100(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_5,negated_conjecture,
~ p101(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_72,negated_conjecture,
( ~ p100(A)
| p101(A)
| p101(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_73,negated_conjecture,
( ~ p100(A)
| p101(A)
| ~ p102(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_75,negated_conjecture,
( ~ p100(A)
| p101(A)
| r1(A,sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_80,negated_conjecture,
( ~ p101(A)
| p102(A)
| p102(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_81,negated_conjecture,
( ~ p101(A)
| p102(A)
| ~ p103(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_83,negated_conjecture,
( ~ p101(A)
| p102(A)
| r1(A,sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_88,negated_conjecture,
( ~ p102(A)
| p103(A)
| p103(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_89,negated_conjecture,
( ~ p102(A)
| p103(A)
| ~ p104(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_91,negated_conjecture,
( ~ p102(A)
| p103(A)
| r1(A,sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_96,negated_conjecture,
( ~ p103(A)
| p104(A)
| p104(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_97,negated_conjecture,
( ~ p103(A)
| p104(A)
| ~ p105(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_99,negated_conjecture,
( ~ p103(A)
| p104(A)
| r1(A,sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_104,negated_conjecture,
( ~ p104(A)
| p105(A)
| p105(sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_105,negated_conjecture,
( ~ p104(A)
| p105(A)
| ~ p106(sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_107,negated_conjecture,
( ~ p104(A)
| p105(A)
| r1(A,sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_112,negated_conjecture,
( ~ p105(A)
| p106(A)
| p106(sK6(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_113,negated_conjecture,
( ~ p105(A)
| p106(A)
| ~ p107(sK6(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_115,negated_conjecture,
( ~ p105(A)
| p106(A)
| r1(A,sK6(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_122,negated_conjecture,
( ~ p106(A)
| p107(A)
| ~ p8(sK7(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_123,negated_conjecture,
( ~ p106(A)
| p107(A)
| r1(A,sK7(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_226,negated_conjecture,
( p8(A)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_227,plain,
( r1(A,C)
| ~ r1(B,C)
| ~ r1(A,B) ),
inference(clausify,[status(thm)],[transitivity]) ).
cnf(c_228,plain,
r1(A,A),
inference(clausify,[status(thm)],[reflexivity]) ).
cnf(c_34149,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_228,c_75]) ).
cnf(c_34150,negated_conjecture,
( ~ p100(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_34149]) ).
cnf(c_372,negated_conjecture,
r1(sK0,sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_34150]) ).
cnf(c_34151,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_228,c_73]) ).
cnf(c_34152,negated_conjecture,
( ~ p100(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_34151]) ).
cnf(c_374,negated_conjecture,
~ p102(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_34152]) ).
cnf(c_34153,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_228,c_72]) ).
cnf(c_34154,negated_conjecture,
( ~ p100(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_34153]) ).
cnf(c_375,negated_conjecture,
p101(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_34154]) ).
cnf(c_456,plain,
( r1(sK0,A)
| ~ r1(sK1(sK0),A) ),
inference(resolve,[status(thm)],[c_372,c_227]) ).
cnf(c_34155,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_372,c_83]) ).
cnf(c_34156,negated_conjecture,
( ~ p101(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_374,c_34155]) ).
cnf(c_592,negated_conjecture,
r1(sK1(sK0),sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_375,c_34156]) ).
cnf(c_34157,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_372,c_81]) ).
cnf(c_34158,negated_conjecture,
( ~ p101(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_374,c_34157]) ).
cnf(c_594,negated_conjecture,
~ p103(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_375,c_34158]) ).
cnf(c_34159,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_372,c_80]) ).
cnf(c_34160,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_374,c_34159]) ).
cnf(c_595,negated_conjecture,
p102(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_375,c_34160]) ).
cnf(c_905,plain,
r1(sK0,sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_592,c_456]) ).
cnf(c_920,plain,
( r1(sK0,A)
| ~ r1(sK2(sK1(sK0)),A) ),
inference(resolve,[status(thm)],[c_905,c_227]) ).
cnf(c_34161,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_905,c_91]) ).
cnf(c_34162,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_594,c_34161]) ).
cnf(c_1048,negated_conjecture,
r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_595,c_34162]) ).
cnf(c_34163,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_905,c_89]) ).
cnf(c_34164,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_594,c_34163]) ).
cnf(c_1050,negated_conjecture,
~ p104(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_595,c_34164]) ).
cnf(c_34165,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_905,c_88]) ).
cnf(c_34166,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_594,c_34165]) ).
cnf(c_1051,negated_conjecture,
p103(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_595,c_34166]) ).
cnf(c_1841,plain,
r1(sK0,sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_1048,c_920]) ).
cnf(c_1876,plain,
( r1(sK0,A)
| ~ r1(sK3(sK2(sK1(sK0))),A) ),
inference(resolve,[status(thm)],[c_1841,c_227]) ).
cnf(c_34167,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1841,c_99]) ).
cnf(c_34168,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1050,c_34167]) ).
cnf(c_1996,negated_conjecture,
r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1051,c_34168]) ).
cnf(c_34169,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| ~ p105(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1841,c_97]) ).
cnf(c_34170,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| ~ p105(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1050,c_34169]) ).
cnf(c_1998,negated_conjecture,
~ p105(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1051,c_34170]) ).
cnf(c_34171,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| p104(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1841,c_96]) ).
cnf(c_34172,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1050,c_34171]) ).
cnf(c_1999,negated_conjecture,
p104(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1051,c_34172]) ).
cnf(c_3295,plain,
r1(sK0,sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1996,c_1876]) ).
cnf(c_3892,plain,
( r1(sK0,A)
| ~ r1(sK4(sK3(sK2(sK1(sK0)))),A) ),
inference(resolve,[status(thm)],[c_3295,c_227]) ).
cnf(c_34173,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK4(sK3(sK2(sK1(sK0)))))
| r1(sK4(sK3(sK2(sK1(sK0)))),sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_3295,c_107]) ).
cnf(c_34174,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| r1(sK4(sK3(sK2(sK1(sK0)))),sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_1998,c_34173]) ).
cnf(c_4004,negated_conjecture,
r1(sK4(sK3(sK2(sK1(sK0)))),sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1999,c_34174]) ).
cnf(c_34175,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK4(sK3(sK2(sK1(sK0)))))
| ~ p106(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_3295,c_105]) ).
cnf(c_34176,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| ~ p106(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_1998,c_34175]) ).
cnf(c_4006,negated_conjecture,
~ p106(sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1999,c_34176]) ).
cnf(c_34177,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_3295,c_104]) ).
cnf(c_34178,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_1998,c_34177]) ).
cnf(c_4007,negated_conjecture,
p105(sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1999,c_34178]) ).
cnf(c_6789,plain,
r1(sK0,sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_4004,c_3892]) ).
cnf(c_8032,plain,
( r1(sK0,A)
| ~ r1(sK5(sK4(sK3(sK2(sK1(sK0))))),A) ),
inference(resolve,[status(thm)],[c_6789,c_227]) ).
cnf(c_34179,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK5(sK4(sK3(sK2(sK1(sK0))))))
| r1(sK5(sK4(sK3(sK2(sK1(sK0))))),sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_6789,c_115]) ).
cnf(c_34180,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| r1(sK5(sK4(sK3(sK2(sK1(sK0))))),sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_4006,c_34179]) ).
cnf(c_8136,negated_conjecture,
r1(sK5(sK4(sK3(sK2(sK1(sK0))))),sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_4007,c_34180]) ).
cnf(c_34181,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK5(sK4(sK3(sK2(sK1(sK0))))))
| ~ p107(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_6789,c_113]) ).
cnf(c_34182,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| ~ p107(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_4006,c_34181]) ).
cnf(c_8138,negated_conjecture,
~ p107(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_4007,c_34182]) ).
cnf(c_34183,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_6789,c_112]) ).
cnf(c_34184,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_4006,c_34183]) ).
cnf(c_8139,negated_conjecture,
p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_4007,c_34184]) ).
cnf(c_14196,plain,
r1(sK0,sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_8136,c_8032]) ).
cnf(c_16610,plain,
( r1(sK0,A)
| ~ r1(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))),A) ),
inference(resolve,[status(thm)],[c_14196,c_227]) ).
cnf(c_34185,negated_conjecture,
( ~ p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| p107(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| r1(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))),sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))) ),
inference(resolve,[status(thm)],[c_14196,c_123]) ).
cnf(c_34186,negated_conjecture,
( ~ p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| r1(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))),sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))) ),
inference(resolve,[status(thm)],[c_8138,c_34185]) ).
cnf(c_16706,negated_conjecture,
r1(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))),sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))),
inference(resolve,[status(thm)],[c_8139,c_34186]) ).
cnf(c_34187,negated_conjecture,
( ~ p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| p107(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| ~ p8(sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))) ),
inference(resolve,[status(thm)],[c_14196,c_122]) ).
cnf(c_34188,negated_conjecture,
( ~ p106(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))
| ~ p8(sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))) ),
inference(resolve,[status(thm)],[c_8138,c_34187]) ).
cnf(c_16707,negated_conjecture,
~ p8(sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))),
inference(resolve,[status(thm)],[c_8139,c_34188]) ).
cnf(c_29291,plain,
r1(sK0,sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))),
inference(resolve,[status(thm)],[c_16706,c_16610]) ).
cnf(c_34189,negated_conjecture,
p8(sK7(sK6(sK5(sK4(sK3(sK2(sK1(sK0)))))))),
inference(resolve,[status(thm)],[c_29291,c_226]) ).
cnf(c_34148,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_16707,c_34189]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL674+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 23:17:20 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 243018 was started by sandbox2 on n002,
% 0.09/0.37 % Fri Sep 25 23:17:20 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.45
% 0.09/0.45 % From the command line: assign(max_seconds, 300).
% 24.04/4.06
% 24.04/4.06 % given #500 (A,wt=28): 1744 r1(f38(f40(c1)),f35(f38(f40(c1)))). [resolve(1380,a,91,a),unit_del(b,823),unit_del(c,824)].
% 24.04/4.06
% 24.04/4.06 % given #1000 (T,wt=31): 5296 p103(f34(f35(f38(f39(c1))))). [resolve(3814,a,9,a),unit_del(b,2485)].
% 24.04/4.06
% 24.04/4.06 % given #1500 (A,wt=42): 4746 r1(f34(f36(f37(f39(c1)))),f32(f34(f36(f37(f39(c1)))))). [resolve(3796,a,103,a),unit_del(b,2239),unit_del(c,2240)].
% 24.04/4.06
% 24.04/4.06 % given #2000 (T,wt=37): 9743 p103(f31(f34(f36(f37(f39(c1)))))). [resolve(7807,a,9,a),unit_del(b,9742)].
% 24.04/4.06
% 24.04/4.06 % given #2500 (A,wt=49): 8136 r1(f31(f33(f35(f37(f39(c1))))),f29(f31(f33(f35(f37(f39(c1))))))). [resolve(6789,a,115,a),unit_del(b,4006),unit_del(c,4007)].
% 24.04/4.06
% 24.04/4.06 % given #3000 (F,wt=42): 10256 -r1(f31(f33(f35(f38(f39(c1))))),A) | -p2(A) | -p101(A). [back_unit_del(10244),unit_del(d,10245)].
% 24.04/4.06
% 24.04/4.06 % given #3500 (W,wt=42): 12002 p1(f32(f34(f36(f38(f39(c1)))))) | -p1(f36(f38(f39(c1)))). [resolve(7926,a,2799,a),unit_del(b,11961)].
% 24.04/4.06
% 24.04/4.06 % given #4000 (T,wt=43): 17039 p104(f30(f31(f33(f35(f37(f39(c1))))))). [resolve(14207,a,10,a),unit_del(b,17038)].
% 24.04/4.06
% 24.04/4.06 % given #4500 (A,wt=52): 16128 -r1(A,f31(f33(f35(f38(f39(c1)))))) | r1(A,f29(f31(f33(f35(f38(f39(c1))))))). [resolve(10144,a,227,b)].
% 24.04/4.06
% 24.04/4.06 % given #5000 (T,wt=43): 24712 p101(f30(f32(f34(f36(f38(f39(c1))))))). [resolve(16343,a,7,a),unit_del(b,24711)].
% 24.04/4.06
% 24.04/4.06 % given #5500 (A,wt=45): 16566 r1(f40(c1),f30(f32(f34(f36(f37(f40(c1))))))). [resolve(13835,a,13960,a)].
% 24.04/4.06
% 24.04/4.06 % given #6000 (T,wt=43): 31753 p8(f29(f31(f34(f36(f38(f40(c1))))))). [resolve(17941,a,226,a)].
% 24.04/4.06
% 24.04/4.06 % given #6500 (A,wt=50): 18222 -r1(f30(f32(f33(f35(f37(f39(c1)))))),A) | r1(f35(f37(f39(c1))),A). [resolve(15883,a,227,a)].
% 24.04/4.06
% 24.04/4.06 % given #7000 (F,wt=49): 26137 -p108(f27(f30(f31(f34(f35(f37(f40(c1)))))))). [resolve(16433,a,121,a),unit_del(b,12608),unit_del(c,12609)].
% 24.04/4.06
% 24.04/4.06 % given #7500 (W,wt=48): 23754 p1(f29(f31(f33(f36(f38(f39(c1))))))) | -p1(f36(f38(f39(c1)))). [resolve(16294,a,2799,a),unit_del(b,22964)].
% 24.04/4.06
% 24.04/4.06 % given #8000 (A,wt=56): 22728 -r1(f30(f32(f34(f35(f38(f39(c1)))))),A) | -p1(A) | -p100(A) | p1(f30(f32(f34(f35(f38(f39(c1))))))). [back_unit_del(22695),unit_del(e,22715)].
% 24.04/4.06
% 24.04/4.06 % given #8500 (T,wt=49): 32782 p1(f29(f31(f33(f36(f38(f40(c1))))))) | -p1(f33(f36(f38(f40(c1))))). [resolve(17645,a,7477,a),unit_del(b,30952)].
% 24.04/4.06
% 24.04/4.06 % SZS status Theorem for theBenchmark
% 24.04/4.06
% 24.04/4.06 % Proof 1 at 2.89 (+ 0.66) seconds.
% 24.04/4.06 % Length of proof is 61.
% 24.04/4.06 % Level of proof is 15.
% 24.04/4.06 % Maximum clause weight is 56.000.
% 24.04/4.06 % Given clauses 8639.
% 24.04/4.06
% 24.04/4.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------