%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL674+1.015 : 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 : n015.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 12.19s 2.03s
% Output : CNFRefutation 12.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 3
% Syntax : Number of formulae : 92 ( 28 unt; 0 def)
% Number of atoms : 2247 ( 0 equ)
% Maximal formula atoms : 724 ( 24 avg)
% Number of connectives : 3718 (1563 ~;1335 |; 819 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 174 ( 7 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 35 ( 34 usr; 1 prp; 0-2 aty)
% Number of functors : 31 ( 31 usr; 1 con; 0-1 aty)
% Number of variables : 461 ( 0 sgn 401 !; 33 ?)
% 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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p7(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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( p7(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) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X62] :
( ~ p100(X62)
| p1(X62)
| ~ r1(Y,X62) ) )
& ( p1(Y)
| ! [X61] :
( ~ p100(X61)
| ~ p1(X61)
| ~ r1(Y,X61) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X60] :
( ~ p101(X60)
| p2(X60)
| ~ r1(Y,X60) ) )
& ( p2(Y)
| ! [X59] :
( ~ p101(X59)
| ~ p2(X59)
| ~ r1(Y,X59) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X58] :
( ~ p102(X58)
| p3(X58)
| ~ r1(Y,X58) ) )
& ( p3(Y)
| ! [X57] :
( ~ p102(X57)
| ~ p3(X57)
| ~ r1(Y,X57) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X56] :
( ~ p103(X56)
| p4(X56)
| ~ r1(Y,X56) ) )
& ( p4(Y)
| ! [X55] :
( ~ p103(X55)
| ~ p4(X55)
| ~ r1(Y,X55) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X54] :
( ~ p104(X54)
| p5(X54)
| ~ r1(Y,X54) ) )
& ( p5(Y)
| ! [X53] :
( ~ p104(X53)
| ~ p5(X53)
| ~ r1(Y,X53) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X52] :
( ~ p105(X52)
| p6(X52)
| ~ r1(Y,X52) ) )
& ( p6(Y)
| ! [X51] :
( ~ p105(X51)
| ~ p6(X51)
| ~ r1(Y,X51) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X50] :
( ~ p106(X50)
| p7(X50)
| ~ r1(Y,X50) ) )
& ( p7(Y)
| ! [X49] :
( ~ p106(X49)
| ~ p7(X49)
| ~ r1(Y,X49) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X48] :
( ~ p107(X48)
| p8(X48)
| ~ r1(Y,X48) ) )
& ( p8(Y)
| ! [X47] :
( ~ p107(X47)
| ~ p8(X47)
| ~ r1(Y,X47) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X46] :
( ~ p108(X46)
| p9(X46)
| ~ r1(Y,X46) ) )
& ( p9(Y)
| ! [X45] :
( ~ p108(X45)
| ~ p9(X45)
| ~ r1(Y,X45) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X44] :
( ~ p109(X44)
| p10(X44)
| ~ r1(Y,X44) ) )
& ( p10(Y)
| ! [X43] :
( ~ p109(X43)
| ~ p10(X43)
| ~ r1(Y,X43) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X42] :
( ~ p110(X42)
| p11(X42)
| ~ r1(Y,X42) ) )
& ( p11(Y)
| ! [X41] :
( ~ p110(X41)
| ~ p11(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X40] :
( ~ p111(X40)
| p12(X40)
| ~ r1(Y,X40) ) )
& ( p12(Y)
| ! [X39] :
( ~ p111(X39)
| ~ p12(X39)
| ~ r1(Y,X39) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X38] :
( ~ p112(X38)
| p13(X38)
| ~ r1(Y,X38) ) )
& ( p13(Y)
| ! [X37] :
( ~ p112(X37)
| ~ p13(X37)
| ~ r1(Y,X37) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X36] :
( ~ p113(X36)
| p14(X36)
| ~ r1(Y,X36) ) )
& ( p14(Y)
| ! [X35] :
( ~ p113(X35)
| ~ p14(X35)
| ~ r1(Y,X35) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X34] :
( ~ p114(X34)
| p15(X34)
| ~ r1(Y,X34) ) )
& ( p15(Y)
| ! [X33] :
( ~ p114(X33)
| ~ p15(X33)
| ~ r1(Y,X33) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X32] :
( ~ p115(X32)
| p16(X32)
| ~ r1(Y,X32) ) )
& ( p16(Y)
| ! [X31] :
( ~ p115(X31)
| ~ p16(X31)
| ~ r1(Y,X31) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( ? [X30] :
( p101(X30)
& ~ p102(X30)
& p2(X30)
& r1(Y,X30) )
& ? [X29] :
( p101(X29)
& ~ p102(X29)
& ~ p2(X29)
& r1(Y,X29) ) ) )
& ( ~ p101(Y)
| p102(Y)
| ( ? [X28] :
( p102(X28)
& ~ p103(X28)
& p3(X28)
& r1(Y,X28) )
& ? [X27] :
( p102(X27)
& ~ p103(X27)
& ~ p3(X27)
& r1(Y,X27) ) ) )
& ( ~ p102(Y)
| p103(Y)
| ( ? [X26] :
( p103(X26)
& ~ p104(X26)
& p4(X26)
& r1(Y,X26) )
& ? [X25] :
( p103(X25)
& ~ p104(X25)
& ~ p4(X25)
& r1(Y,X25) ) ) )
& ( ~ p103(Y)
| p104(Y)
| ( ? [X24] :
( p104(X24)
& ~ p105(X24)
& p5(X24)
& r1(Y,X24) )
& ? [X23] :
( p104(X23)
& ~ p105(X23)
& ~ p5(X23)
& r1(Y,X23) ) ) )
& ( ~ p104(Y)
| p105(Y)
| ( ? [X22] :
( p105(X22)
& ~ p106(X22)
& p6(X22)
& r1(Y,X22) )
& ? [X21] :
( p105(X21)
& ~ p106(X21)
& ~ p6(X21)
& r1(Y,X21) ) ) )
& ( ~ p105(Y)
| p106(Y)
| ( ? [X20] :
( p106(X20)
& ~ p107(X20)
& p7(X20)
& r1(Y,X20) )
& ? [X19] :
( p106(X19)
& ~ p107(X19)
& ~ p7(X19)
& r1(Y,X19) ) ) )
& ( ~ p106(Y)
| p107(Y)
| ( ? [X18] :
( p107(X18)
& ~ p108(X18)
& p8(X18)
& r1(Y,X18) )
& ? [X17] :
( p107(X17)
& ~ p108(X17)
& ~ p8(X17)
& r1(Y,X17) ) ) )
& ( ~ p107(Y)
| p108(Y)
| ( ? [X16] :
( p108(X16)
& ~ p109(X16)
& p9(X16)
& r1(Y,X16) )
& ? [X15] :
( p108(X15)
& ~ p109(X15)
& ~ p9(X15)
& r1(Y,X15) ) ) )
& ( ~ p108(Y)
| p109(Y)
| ( ? [X14] :
( p109(X14)
& ~ p110(X14)
& p10(X14)
& r1(Y,X14) )
& ? [X13] :
( p109(X13)
& ~ p110(X13)
& ~ p10(X13)
& r1(Y,X13) ) ) )
& ( ~ p109(Y)
| p110(Y)
| ( ? [X12] :
( p110(X12)
& ~ p111(X12)
& p11(X12)
& r1(Y,X12) )
& ? [X11] :
( p110(X11)
& ~ p111(X11)
& ~ p11(X11)
& r1(Y,X11) ) ) )
& ( ~ p110(Y)
| p111(Y)
| ( ? [X10] :
( p111(X10)
& ~ p112(X10)
& p12(X10)
& r1(Y,X10) )
& ? [X9] :
( p111(X9)
& ~ p112(X9)
& ~ p12(X9)
& r1(Y,X9) ) ) )
& ( ~ p111(Y)
| p112(Y)
| ( ? [X8] :
( p112(X8)
& ~ p113(X8)
& p13(X8)
& r1(Y,X8) )
& ? [X7] :
( p112(X7)
& ~ p113(X7)
& ~ p13(X7)
& r1(Y,X7) ) ) )
& ( ~ p112(Y)
| p113(Y)
| ( ? [X6] :
( p113(X6)
& ~ p114(X6)
& p14(X6)
& r1(Y,X6) )
& ? [X5] :
( p113(X5)
& ~ p114(X5)
& ~ p14(X5)
& r1(Y,X5) ) ) )
& ( ~ p113(Y)
| p114(Y)
| ( ? [X4] :
( p114(X4)
& ~ p115(X4)
& p15(X4)
& r1(Y,X4) )
& ? [X3] :
( p114(X3)
& ~ p115(X3)
& ~ p15(X3)
& r1(Y,X3) ) ) )
& ( ~ p114(Y)
| p115(Y)
| ( ? [X2] :
( p115(X2)
& ~ p116(X2)
& p16(X2)
& r1(Y,X2) )
& ? [X1] :
( p115(X1)
& ~ p116(X1)
& ~ p16(X1)
& r1(Y,X1) ) ) ) )
| ~ r1(X,Y) )
& ! [X0] :
( p7(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) )
& ( ~ p100(Y)
| ( ( ~ p1(Y)
| ! [X62] :
( ~ p100(X62)
| p1(X62)
| ~ r1(Y,X62) ) )
& ( p1(Y)
| ! [X61] :
( ~ p100(X61)
| ~ p1(X61)
| ~ r1(Y,X61) ) ) ) )
& ( ~ p101(Y)
| ( ( ~ p2(Y)
| ! [X60] :
( ~ p101(X60)
| p2(X60)
| ~ r1(Y,X60) ) )
& ( p2(Y)
| ! [X59] :
( ~ p101(X59)
| ~ p2(X59)
| ~ r1(Y,X59) ) ) ) )
& ( ~ p102(Y)
| ( ( ~ p3(Y)
| ! [X58] :
( ~ p102(X58)
| p3(X58)
| ~ r1(Y,X58) ) )
& ( p3(Y)
| ! [X57] :
( ~ p102(X57)
| ~ p3(X57)
| ~ r1(Y,X57) ) ) ) )
& ( ~ p103(Y)
| ( ( ~ p4(Y)
| ! [X56] :
( ~ p103(X56)
| p4(X56)
| ~ r1(Y,X56) ) )
& ( p4(Y)
| ! [X55] :
( ~ p103(X55)
| ~ p4(X55)
| ~ r1(Y,X55) ) ) ) )
& ( ~ p104(Y)
| ( ( ~ p5(Y)
| ! [X54] :
( ~ p104(X54)
| p5(X54)
| ~ r1(Y,X54) ) )
& ( p5(Y)
| ! [X53] :
( ~ p104(X53)
| ~ p5(X53)
| ~ r1(Y,X53) ) ) ) )
& ( ~ p105(Y)
| ( ( ~ p6(Y)
| ! [X52] :
( ~ p105(X52)
| p6(X52)
| ~ r1(Y,X52) ) )
& ( p6(Y)
| ! [X51] :
( ~ p105(X51)
| ~ p6(X51)
| ~ r1(Y,X51) ) ) ) )
& ( ~ p106(Y)
| ( ( ~ p7(Y)
| ! [X50] :
( ~ p106(X50)
| p7(X50)
| ~ r1(Y,X50) ) )
& ( p7(Y)
| ! [X49] :
( ~ p106(X49)
| ~ p7(X49)
| ~ r1(Y,X49) ) ) ) )
& ( ~ p107(Y)
| ( ( ~ p8(Y)
| ! [X48] :
( ~ p107(X48)
| p8(X48)
| ~ r1(Y,X48) ) )
& ( p8(Y)
| ! [X47] :
( ~ p107(X47)
| ~ p8(X47)
| ~ r1(Y,X47) ) ) ) )
& ( ~ p108(Y)
| ( ( ~ p9(Y)
| ! [X46] :
( ~ p108(X46)
| p9(X46)
| ~ r1(Y,X46) ) )
& ( p9(Y)
| ! [X45] :
( ~ p108(X45)
| ~ p9(X45)
| ~ r1(Y,X45) ) ) ) )
& ( ~ p109(Y)
| ( ( ~ p10(Y)
| ! [X44] :
( ~ p109(X44)
| p10(X44)
| ~ r1(Y,X44) ) )
& ( p10(Y)
| ! [X43] :
( ~ p109(X43)
| ~ p10(X43)
| ~ r1(Y,X43) ) ) ) )
& ( ~ p110(Y)
| ( ( ~ p11(Y)
| ! [X42] :
( ~ p110(X42)
| p11(X42)
| ~ r1(Y,X42) ) )
& ( p11(Y)
| ! [X41] :
( ~ p110(X41)
| ~ p11(X41)
| ~ r1(Y,X41) ) ) ) )
& ( ~ p111(Y)
| ( ( ~ p12(Y)
| ! [X40] :
( ~ p111(X40)
| p12(X40)
| ~ r1(Y,X40) ) )
& ( p12(Y)
| ! [X39] :
( ~ p111(X39)
| ~ p12(X39)
| ~ r1(Y,X39) ) ) ) )
& ( ~ p112(Y)
| ( ( ~ p13(Y)
| ! [X38] :
( ~ p112(X38)
| p13(X38)
| ~ r1(Y,X38) ) )
& ( p13(Y)
| ! [X37] :
( ~ p112(X37)
| ~ p13(X37)
| ~ r1(Y,X37) ) ) ) )
& ( ~ p113(Y)
| ( ( ~ p14(Y)
| ! [X36] :
( ~ p113(X36)
| p14(X36)
| ~ r1(Y,X36) ) )
& ( p14(Y)
| ! [X35] :
( ~ p113(X35)
| ~ p14(X35)
| ~ r1(Y,X35) ) ) ) )
& ( ~ p114(Y)
| ( ( ~ p15(Y)
| ! [X34] :
( ~ p114(X34)
| p15(X34)
| ~ r1(Y,X34) ) )
& ( p15(Y)
| ! [X33] :
( ~ p114(X33)
| ~ p15(X33)
| ~ r1(Y,X33) ) ) ) )
& ( ~ p115(Y)
| ( ( ~ p16(Y)
| ! [X32] :
( ~ p115(X32)
| p16(X32)
| ~ r1(Y,X32) ) )
& ( p16(Y)
| ! [X31] :
( ~ p115(X31)
| ~ p16(X31)
| ~ r1(Y,X31) ) ) ) )
& ( ~ p100(Y)
| p101(Y)
| ( p101(sK30(Y))
& ~ p102(sK30(Y))
& p2(sK30(Y))
& r1(Y,sK30(Y))
& p101(sK1(Y))
& ~ p102(sK1(Y))
& ~ p2(sK1(Y))
& r1(Y,sK1(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK29(Y))
& ~ p103(sK29(Y))
& p3(sK29(Y))
& r1(Y,sK29(Y))
& p102(sK2(Y))
& ~ p103(sK2(Y))
& ~ p3(sK2(Y))
& r1(Y,sK2(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK28(Y))
& ~ p104(sK28(Y))
& p4(sK28(Y))
& r1(Y,sK28(Y))
& p103(sK3(Y))
& ~ p104(sK3(Y))
& ~ p4(sK3(Y))
& r1(Y,sK3(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK27(Y))
& ~ p105(sK27(Y))
& p5(sK27(Y))
& r1(Y,sK27(Y))
& p104(sK4(Y))
& ~ p105(sK4(Y))
& ~ p5(sK4(Y))
& r1(Y,sK4(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK26(Y))
& ~ p106(sK26(Y))
& p6(sK26(Y))
& r1(Y,sK26(Y))
& p105(sK5(Y))
& ~ p106(sK5(Y))
& ~ p6(sK5(Y))
& r1(Y,sK5(Y)) ) )
& ( ~ p105(Y)
| p106(Y)
| ( p106(sK25(Y))
& ~ p107(sK25(Y))
& p7(sK25(Y))
& r1(Y,sK25(Y))
& p106(sK6(Y))
& ~ p107(sK6(Y))
& ~ p7(sK6(Y))
& r1(Y,sK6(Y)) ) )
& ( ~ p106(Y)
| p107(Y)
| ( p107(sK24(Y))
& ~ p108(sK24(Y))
& p8(sK24(Y))
& r1(Y,sK24(Y))
& p107(sK23(Y))
& ~ p108(sK23(Y))
& ~ p8(sK23(Y))
& r1(Y,sK23(Y)) ) )
& ( ~ p107(Y)
| p108(Y)
| ( p108(sK22(Y))
& ~ p109(sK22(Y))
& p9(sK22(Y))
& r1(Y,sK22(Y))
& p108(sK21(Y))
& ~ p109(sK21(Y))
& ~ p9(sK21(Y))
& r1(Y,sK21(Y)) ) )
& ( ~ p108(Y)
| p109(Y)
| ( p109(sK20(Y))
& ~ p110(sK20(Y))
& p10(sK20(Y))
& r1(Y,sK20(Y))
& p109(sK19(Y))
& ~ p110(sK19(Y))
& ~ p10(sK19(Y))
& r1(Y,sK19(Y)) ) )
& ( ~ p109(Y)
| p110(Y)
| ( p110(sK18(Y))
& ~ p111(sK18(Y))
& p11(sK18(Y))
& r1(Y,sK18(Y))
& p110(sK17(Y))
& ~ p111(sK17(Y))
& ~ p11(sK17(Y))
& r1(Y,sK17(Y)) ) )
& ( ~ p110(Y)
| p111(Y)
| ( p111(sK16(Y))
& ~ p112(sK16(Y))
& p12(sK16(Y))
& r1(Y,sK16(Y))
& p111(sK15(Y))
& ~ p112(sK15(Y))
& ~ p12(sK15(Y))
& r1(Y,sK15(Y)) ) )
& ( ~ p111(Y)
| p112(Y)
| ( p112(sK14(Y))
& ~ p113(sK14(Y))
& p13(sK14(Y))
& r1(Y,sK14(Y))
& p112(sK13(Y))
& ~ p113(sK13(Y))
& ~ p13(sK13(Y))
& r1(Y,sK13(Y)) ) )
& ( ~ p112(Y)
| p113(Y)
| ( p113(sK12(Y))
& ~ p114(sK12(Y))
& p14(sK12(Y))
& r1(Y,sK12(Y))
& p113(sK11(Y))
& ~ p114(sK11(Y))
& ~ p14(sK11(Y))
& r1(Y,sK11(Y)) ) )
& ( ~ p113(Y)
| p114(Y)
| ( p114(sK10(Y))
& ~ p115(sK10(Y))
& p15(sK10(Y))
& r1(Y,sK10(Y))
& p114(sK9(Y))
& ~ p115(sK9(Y))
& ~ p15(sK9(Y))
& r1(Y,sK9(Y)) ) )
& ( ~ p114(Y)
| p115(Y)
| ( p115(sK8(Y))
& ~ p116(sK8(Y))
& p16(sK8(Y))
& r1(Y,sK8(Y))
& p115(sK7(Y))
& ~ p116(sK7(Y))
& ~ p16(sK7(Y))
& r1(Y,sK7(Y)) ) ) )
| ~ r1(sK0,Y) )
& ! [X0] :
( p7(X0)
| ~ r1(sK0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK6,sK25,sK5,sK26,sK4,sK27,sK3,sK28,sK2,sK29,sK1,sK30]),skolemize(X,sK0),skolemize(X1,sK7(Y)),skolemize(X2,sK8(Y)),skolemize(X3,sK9(Y)),skolemize(X4,sK10(Y)),skolemize(X5,sK11(Y)),skolemize(X6,sK12(Y)),skolemize(X7,sK13(Y)),skolemize(X8,sK14(Y)),skolemize(X9,sK15(Y)),skolemize(X10,sK16(Y)),skolemize(X11,sK17(Y)),skolemize(X12,sK18(Y)),skolemize(X13,sK19(Y)),skolemize(X14,sK20(Y)),skolemize(X15,sK21(Y)),skolemize(X16,sK22(Y)),skolemize(X17,sK23(Y)),skolemize(X18,sK24(Y)),skolemize(X19,sK6(Y)),skolemize(X20,sK25(Y)),skolemize(X21,sK5(Y)),skolemize(X22,sK26(Y)),skolemize(X23,sK4(Y)),skolemize(X24,sK27(Y)),skolemize(X25,sK3(Y)),skolemize(X26,sK28(Y)),skolemize(X27,sK2(Y)),skolemize(X28,sK29(Y)),skolemize(X29,sK1(Y)),skolemize(X30,sK30(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,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] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p2(sK30(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK30(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(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p3(sK29(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK29(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(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p4(sK28(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK28(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(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p5(sK27(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK27(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(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p6(sK26(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK26(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(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| ~ p107(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| p7(sK25(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(VAR_0)
| p106(VAR_0)
| r1(VAR_0,sK25(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(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p8(sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK24(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| p107(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p108(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| ~ p8(sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p106(VAR_0)
| p107(VAR_0)
| r1(VAR_0,sK23(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p9(sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK22(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| p108(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p109(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| ~ p9(sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p107(VAR_0)
| p108(VAR_0)
| r1(VAR_0,sK21(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p10(sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK20(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| p109(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p110(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| ~ p10(sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p108(VAR_0)
| p109(VAR_0)
| r1(VAR_0,sK19(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p11(sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK18(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| p110(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p111(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| ~ p11(sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p109(VAR_0)
| p110(VAR_0)
| r1(VAR_0,sK17(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p111(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p112(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p12(sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| r1(VAR_0,sK16(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| p111(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p112(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| ~ p12(sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p110(VAR_0)
| p111(VAR_0)
| r1(VAR_0,sK15(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p112(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p113(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p13(sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| r1(VAR_0,sK14(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| p112(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p113(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| ~ p13(sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p111(VAR_0)
| p112(VAR_0)
| r1(VAR_0,sK13(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p113(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p114(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p14(sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| r1(VAR_0,sK12(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| p113(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p114(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| ~ p14(sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p112(VAR_0)
| p113(VAR_0)
| r1(VAR_0,sK11(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p114(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p115(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p15(sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| r1(VAR_0,sK10(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| p114(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p115(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| ~ p15(sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p113(VAR_0)
| p114(VAR_0)
| r1(VAR_0,sK9(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p115(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p116(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p16(sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| r1(VAR_0,sK8(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| p115(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p116(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| ~ p16(sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p114(VAR_0)
| p115(VAR_0)
| r1(VAR_0,sK7(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( p7(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_57,negated_conjecture,
( ~ p100(A)
| p101(A)
| p101(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_58,negated_conjecture,
( ~ p100(A)
| p101(A)
| ~ p102(sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_60,negated_conjecture,
( ~ p100(A)
| p101(A)
| r1(A,sK1(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_65,negated_conjecture,
( ~ p101(A)
| p102(A)
| p102(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_66,negated_conjecture,
( ~ p101(A)
| p102(A)
| ~ p103(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_68,negated_conjecture,
( ~ p101(A)
| p102(A)
| r1(A,sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_73,negated_conjecture,
( ~ p102(A)
| p103(A)
| p103(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_74,negated_conjecture,
( ~ p102(A)
| p103(A)
| ~ p104(sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_76,negated_conjecture,
( ~ p102(A)
| p103(A)
| r1(A,sK3(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_81,negated_conjecture,
( ~ p103(A)
| p104(A)
| p104(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_82,negated_conjecture,
( ~ p103(A)
| p104(A)
| ~ p105(sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_84,negated_conjecture,
( ~ p103(A)
| p104(A)
| r1(A,sK4(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_89,negated_conjecture,
( ~ p104(A)
| p105(A)
| p105(sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_90,negated_conjecture,
( ~ p104(A)
| p105(A)
| ~ p106(sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_92,negated_conjecture,
( ~ p104(A)
| p105(A)
| r1(A,sK5(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_99,negated_conjecture,
( ~ p105(A)
| p106(A)
| ~ p7(sK6(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_100,negated_conjecture,
( ~ p105(A)
| p106(A)
| r1(A,sK6(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_171,negated_conjecture,
( p7(A)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_172,plain,
( r1(A,C)
| ~ r1(B,C)
| ~ r1(A,B) ),
inference(clausify,[status(thm)],[transitivity]) ).
cnf(c_173,plain,
r1(A,A),
inference(clausify,[status(thm)],[reflexivity]) ).
cnf(c_12807,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_173,c_60]) ).
cnf(c_12808,negated_conjecture,
( ~ p100(sK0)
| r1(sK0,sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_12807]) ).
cnf(c_277,negated_conjecture,
r1(sK0,sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_12808]) ).
cnf(c_12809,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_173,c_58]) ).
cnf(c_12810,negated_conjecture,
( ~ p100(sK0)
| ~ p102(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_12809]) ).
cnf(c_279,negated_conjecture,
~ p102(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_12810]) ).
cnf(c_12811,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_173,c_57]) ).
cnf(c_12812,negated_conjecture,
( ~ p100(sK0)
| p101(sK1(sK0)) ),
inference(resolve,[status(thm)],[c_5,c_12811]) ).
cnf(c_280,negated_conjecture,
p101(sK1(sK0)),
inference(resolve,[status(thm)],[c_4,c_12812]) ).
cnf(c_341,plain,
( r1(sK0,A)
| ~ r1(sK1(sK0),A) ),
inference(resolve,[status(thm)],[c_277,c_172]) ).
cnf(c_12813,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_277,c_68]) ).
cnf(c_12814,negated_conjecture,
( ~ p101(sK1(sK0))
| r1(sK1(sK0),sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_279,c_12813]) ).
cnf(c_437,negated_conjecture,
r1(sK1(sK0),sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_280,c_12814]) ).
cnf(c_12815,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_277,c_66]) ).
cnf(c_12816,negated_conjecture,
( ~ p101(sK1(sK0))
| ~ p103(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_279,c_12815]) ).
cnf(c_439,negated_conjecture,
~ p103(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_280,c_12816]) ).
cnf(c_12817,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_277,c_65]) ).
cnf(c_12818,negated_conjecture,
( ~ p101(sK1(sK0))
| p102(sK2(sK1(sK0))) ),
inference(resolve,[status(thm)],[c_279,c_12817]) ).
cnf(c_440,negated_conjecture,
p102(sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_280,c_12818]) ).
cnf(c_670,plain,
r1(sK0,sK2(sK1(sK0))),
inference(resolve,[status(thm)],[c_437,c_341]) ).
cnf(c_685,plain,
( r1(sK0,A)
| ~ r1(sK2(sK1(sK0)),A) ),
inference(resolve,[status(thm)],[c_670,c_172]) ).
cnf(c_12819,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_670,c_76]) ).
cnf(c_12820,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_439,c_12819]) ).
cnf(c_773,negated_conjecture,
r1(sK2(sK1(sK0)),sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_440,c_12820]) ).
cnf(c_12821,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_670,c_74]) ).
cnf(c_12822,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| ~ p104(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_439,c_12821]) ).
cnf(c_775,negated_conjecture,
~ p104(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_440,c_12822]) ).
cnf(c_12823,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_670,c_73]) ).
cnf(c_12824,negated_conjecture,
( ~ p102(sK2(sK1(sK0)))
| p103(sK3(sK2(sK1(sK0)))) ),
inference(resolve,[status(thm)],[c_439,c_12823]) ).
cnf(c_776,negated_conjecture,
p103(sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_440,c_12824]) ).
cnf(c_1366,plain,
r1(sK0,sK3(sK2(sK1(sK0)))),
inference(resolve,[status(thm)],[c_773,c_685]) ).
cnf(c_1409,plain,
( r1(sK0,A)
| ~ r1(sK3(sK2(sK1(sK0))),A) ),
inference(resolve,[status(thm)],[c_1366,c_172]) ).
cnf(c_12825,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_1366,c_84]) ).
cnf(c_12826,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_775,c_12825]) ).
cnf(c_1489,negated_conjecture,
r1(sK3(sK2(sK1(sK0))),sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_776,c_12826]) ).
cnf(c_12827,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| ~ p105(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1366,c_82]) ).
cnf(c_12828,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| ~ p105(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_775,c_12827]) ).
cnf(c_1491,negated_conjecture,
~ p105(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_776,c_12828]) ).
cnf(c_12829,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK3(sK2(sK1(sK0))))
| p104(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_1366,c_81]) ).
cnf(c_12830,negated_conjecture,
( ~ p103(sK3(sK2(sK1(sK0))))
| p104(sK4(sK3(sK2(sK1(sK0))))) ),
inference(resolve,[status(thm)],[c_775,c_12829]) ).
cnf(c_1492,negated_conjecture,
p104(sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_776,c_12830]) ).
cnf(c_2633,plain,
r1(sK0,sK4(sK3(sK2(sK1(sK0))))),
inference(resolve,[status(thm)],[c_1489,c_1409]) ).
cnf(c_2937,plain,
( r1(sK0,A)
| ~ r1(sK4(sK3(sK2(sK1(sK0)))),A) ),
inference(resolve,[status(thm)],[c_2633,c_172]) ).
cnf(c_12831,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_2633,c_92]) ).
cnf(c_12832,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_1491,c_12831]) ).
cnf(c_3009,negated_conjecture,
r1(sK4(sK3(sK2(sK1(sK0)))),sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1492,c_12832]) ).
cnf(c_12833,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_2633,c_90]) ).
cnf(c_12834,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| ~ p106(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_1491,c_12833]) ).
cnf(c_3011,negated_conjecture,
~ p106(sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1492,c_12834]) ).
cnf(c_12835,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_2633,c_89]) ).
cnf(c_12836,negated_conjecture,
( ~ p104(sK4(sK3(sK2(sK1(sK0)))))
| p105(sK5(sK4(sK3(sK2(sK1(sK0)))))) ),
inference(resolve,[status(thm)],[c_1491,c_12835]) ).
cnf(c_3012,negated_conjecture,
p105(sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_1492,c_12836]) ).
cnf(c_5114,plain,
r1(sK0,sK5(sK4(sK3(sK2(sK1(sK0)))))),
inference(resolve,[status(thm)],[c_3009,c_2937]) ).
cnf(c_6117,plain,
( r1(sK0,A)
| ~ r1(sK5(sK4(sK3(sK2(sK1(sK0))))),A) ),
inference(resolve,[status(thm)],[c_5114,c_172]) ).
cnf(c_12837,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_5114,c_100]) ).
cnf(c_12838,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_3011,c_12837]) ).
cnf(c_6181,negated_conjecture,
r1(sK5(sK4(sK3(sK2(sK1(sK0))))),sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_3012,c_12838]) ).
cnf(c_12839,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| p106(sK5(sK4(sK3(sK2(sK1(sK0))))))
| ~ p7(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_5114,c_99]) ).
cnf(c_12840,negated_conjecture,
( ~ p105(sK5(sK4(sK3(sK2(sK1(sK0))))))
| ~ p7(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))) ),
inference(resolve,[status(thm)],[c_3011,c_12839]) ).
cnf(c_6182,negated_conjecture,
~ p7(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_3012,c_12840]) ).
cnf(c_10804,plain,
r1(sK0,sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_6181,c_6117]) ).
cnf(c_12841,negated_conjecture,
p7(sK6(sK5(sK4(sK3(sK2(sK1(sK0))))))),
inference(resolve,[status(thm)],[c_10804,c_171]) ).
cnf(c_12806,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_6182,c_12841]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL674+1.015 : 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.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 23:17:57 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 2524266 was started by sandbox2 on n015,
% 0.09/0.36 % Fri Sep 25 23:17:57 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.47
% 0.13/0.47 % From the command line: assign(max_seconds, 300).
% 12.19/2.03
% 12.19/2.03 % given #500 (F,wt=25): 2109 -p111(f26(f28(f29(c1)))). [back_unit_del(2082),unit_del(a,2108)].
% 12.19/2.03
% 12.19/2.03 % given #1000 (A,wt=38): 2920 -r1(A,f26(f27(f30(c1)))) | r1(A,f23(f26(f27(f30(c1))))). [resolve(2378,a,172,b)].
% 12.19/2.03
% 12.19/2.03 % given #1500 (T,wt=36): 4571 -r1(f23(f25(f27(f30(c1)))),A) | r1(f30(c1),A). [resolve(2894,a,172,a)].
% 12.19/2.03
% 12.19/2.03 % given #2000 (T,wt=37): 8774 p7(f21(f24(f26(f28(f29(c1)))))). [resolve(5999,a,171,a)].
% 12.19/2.03
% 12.19/2.03 % given #2500 (A,wt=40): 6490 r1(f28(f30(c1)),f21(f24(f25(f28(f30(c1)))))). [resolve(5379,a,5829,a)].
% 12.19/2.03
% 12.19/2.03 % given #3000 (T,wt=41): 12143 p1(f21(f23(f26(f28(f30(c1)))))) | -p1(f28(f30(c1))). [resolve(6686,a,1349,a),unit_del(b,11493)].
% 12.19/2.03
% 12.19/2.03 % given #3500 (A,wt=44): 9880 -r1(A,f25(f27(f30(c1)))) | r1(A,f22(f24(f25(f27(f30(c1)))))). [resolve(6059,a,172,b)].
% 12.19/2.03
% 12.19/2.03 % SZS status Theorem for theBenchmark
% 12.19/2.03
% 12.19/2.03 % Proof 1 at 1.16 (+ 0.34) seconds.
% 12.19/2.03 % Length of proof is 53.
% 12.19/2.03 % Level of proof is 13.
% 12.19/2.03 % Maximum clause weight is 49.000.
% 12.19/2.03 % Given clauses 3610.
% 12.19/2.03
% 12.19/2.03 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------