%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:14 AM UTC 2026
% Result : Theorem 255.20s 41.02s
% Output : CNFRefutation 255.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 1
% Syntax : Number of formulae : 148 ( 28 unt; 0 def)
% Number of atoms : 5366 ( 0 equ)
% Maximal formula atoms : 1994 ( 36 avg)
% Number of connectives : 9224 (4006 ~;3541 |;1677 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 341 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 15 ( 14 usr; 1 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 11 con; 0-5 aty)
% Number of variables : 1648 ( 0 sgn1433 !; 63 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) )
& ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ( ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
file('theBenchmark.p',main) ).
fof(main_neg,negated_conjecture,
~ ~ ? [X] :
~ ( ~ ( p100(X)
& ~ p101(X)
& ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) )
& ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ( ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(X,Y) ) )
& ( p2(X)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(X,Y) ) )
& ( p3(X)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(X,Y) ) )
& ( p4(X)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(X,Y) ) )
& ( p5(X)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(X,Y) ) )
& ( p6(X)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(X,Y) ) ) ) )
& ( ~ ( p100(X)
& ~ p101(X) )
| ( ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& p2(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p101(Y)
& ~ p102(Y)
& ~ p2(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p101(X)
& ~ p102(X) )
| ( ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& p3(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p102(Y)
& ~ p103(Y)
& ~ p3(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p102(X)
& ~ p103(X) )
| ( ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& p4(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p103(Y)
& ~ p104(Y)
& ~ p4(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p103(X)
& ~ p104(X) )
| ( ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& p5(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p104(Y)
& ~ p105(Y)
& ~ p5(Y) )
| ~ r1(X,Y) ) ) )
& ( ~ ( p104(X)
& ~ p105(X) )
| ( ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& p6(Y) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p105(Y)
& ~ p106(Y)
& ~ p6(Y) )
| ~ r1(X,Y) ) ) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [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) )
& ( ~ 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) ) ) ) )
& ( ~ ( 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) ) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(nnf_1,plain,
? [X] :
( p100(X)
& ~ p101(X)
& ( ~ p101(X)
| p100(X) )
& ( ~ p102(X)
| p101(X) )
& ( ~ p103(X)
| p102(X) )
& ( ~ p104(X)
| p103(X) )
& ( ~ p105(X)
| p104(X) )
& ( ~ p106(X)
| p105(X) )
& ( ~ p100(X)
| ( ( ~ p1(X)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(X,Y) ) )
& ( p1(X)
| ! [X150] :
( ~ p100(X150)
| ~ p1(X150)
| ~ r1(X,X150) ) ) ) )
& ( ~ p101(X)
| ( ( ~ p2(X)
| ! [X149] :
( ~ p101(X149)
| p2(X149)
| ~ r1(X,X149) ) )
& ( p2(X)
| ! [X148] :
( ~ p101(X148)
| ~ p2(X148)
| ~ r1(X,X148) ) ) ) )
& ( ~ p102(X)
| ( ( ~ p3(X)
| ! [X147] :
( ~ p102(X147)
| p3(X147)
| ~ r1(X,X147) ) )
& ( p3(X)
| ! [X146] :
( ~ p102(X146)
| ~ p3(X146)
| ~ r1(X,X146) ) ) ) )
& ( ~ p103(X)
| ( ( ~ p4(X)
| ! [X145] :
( ~ p103(X145)
| p4(X145)
| ~ r1(X,X145) ) )
& ( p4(X)
| ! [X144] :
( ~ p103(X144)
| ~ p4(X144)
| ~ r1(X,X144) ) ) ) )
& ( ~ p104(X)
| ( ( ~ p5(X)
| ! [X143] :
( ~ p104(X143)
| p5(X143)
| ~ r1(X,X143) ) )
& ( p5(X)
| ! [X142] :
( ~ p104(X142)
| ~ p5(X142)
| ~ r1(X,X142) ) ) ) )
& ( ~ p105(X)
| ( ( ~ p6(X)
| ! [X141] :
( ~ p105(X141)
| p6(X141)
| ~ r1(X,X141) ) )
& ( p6(X)
| ! [X140] :
( ~ p105(X140)
| ~ p6(X140)
| ~ r1(X,X140) ) ) ) )
& ( ~ p100(X)
| p101(X)
| ( ? [X139] :
( p101(X139)
& ~ p102(X139)
& p2(X139)
& r1(X,X139) )
& ? [X138] :
( p101(X138)
& ~ p102(X138)
& ~ p2(X138)
& r1(X,X138) ) ) )
& ( ~ p101(X)
| p102(X)
| ( ? [X137] :
( p102(X137)
& ~ p103(X137)
& p3(X137)
& r1(X,X137) )
& ? [X136] :
( p102(X136)
& ~ p103(X136)
& ~ p3(X136)
& r1(X,X136) ) ) )
& ( ~ p102(X)
| p103(X)
| ( ? [X135] :
( p103(X135)
& ~ p104(X135)
& p4(X135)
& r1(X,X135) )
& ? [X134] :
( p103(X134)
& ~ p104(X134)
& ~ p4(X134)
& r1(X,X134) ) ) )
& ( ~ p103(X)
| p104(X)
| ( ? [X133] :
( p104(X133)
& ~ p105(X133)
& p5(X133)
& r1(X,X133) )
& ? [X132] :
( p104(X132)
& ~ p105(X132)
& ~ p5(X132)
& r1(X,X132) ) ) )
& ( ~ p104(X)
| p105(X)
| ( ? [X131] :
( p105(X131)
& ~ p106(X131)
& p6(X131)
& r1(X,X131) )
& ? [X130] :
( p105(X130)
& ~ p106(X130)
& ~ p6(X130)
& r1(X,X130) ) ) )
& ! [X107] :
( ( ( ~ p101(X107)
| p100(X107) )
& ( ~ p102(X107)
| p101(X107) )
& ( ~ p103(X107)
| p102(X107) )
& ( ~ p104(X107)
| p103(X107) )
& ( ~ p105(X107)
| p104(X107) )
& ( ~ p106(X107)
| p105(X107) )
& ( ~ p100(X107)
| ( ( ~ p1(X107)
| ! [X129] :
( ~ p100(X129)
| p1(X129)
| ~ r1(X107,X129) ) )
& ( p1(X107)
| ! [X128] :
( ~ p100(X128)
| ~ p1(X128)
| ~ r1(X107,X128) ) ) ) )
& ( ~ p101(X107)
| ( ( ~ p2(X107)
| ! [X127] :
( ~ p101(X127)
| p2(X127)
| ~ r1(X107,X127) ) )
& ( p2(X107)
| ! [X126] :
( ~ p101(X126)
| ~ p2(X126)
| ~ r1(X107,X126) ) ) ) )
& ( ~ p102(X107)
| ( ( ~ p3(X107)
| ! [X125] :
( ~ p102(X125)
| p3(X125)
| ~ r1(X107,X125) ) )
& ( p3(X107)
| ! [X124] :
( ~ p102(X124)
| ~ p3(X124)
| ~ r1(X107,X124) ) ) ) )
& ( ~ p103(X107)
| ( ( ~ p4(X107)
| ! [X123] :
( ~ p103(X123)
| p4(X123)
| ~ r1(X107,X123) ) )
& ( p4(X107)
| ! [X122] :
( ~ p103(X122)
| ~ p4(X122)
| ~ r1(X107,X122) ) ) ) )
& ( ~ p104(X107)
| ( ( ~ p5(X107)
| ! [X121] :
( ~ p104(X121)
| p5(X121)
| ~ r1(X107,X121) ) )
& ( p5(X107)
| ! [X120] :
( ~ p104(X120)
| ~ p5(X120)
| ~ r1(X107,X120) ) ) ) )
& ( ~ p105(X107)
| ( ( ~ p6(X107)
| ! [X119] :
( ~ p105(X119)
| p6(X119)
| ~ r1(X107,X119) ) )
& ( p6(X107)
| ! [X118] :
( ~ p105(X118)
| ~ p6(X118)
| ~ r1(X107,X118) ) ) ) )
& ( ~ p100(X107)
| p101(X107)
| ( ? [X117] :
( p101(X117)
& ~ p102(X117)
& p2(X117)
& r1(X107,X117) )
& ? [X116] :
( p101(X116)
& ~ p102(X116)
& ~ p2(X116)
& r1(X107,X116) ) ) )
& ( ~ p101(X107)
| p102(X107)
| ( ? [X115] :
( p102(X115)
& ~ p103(X115)
& p3(X115)
& r1(X107,X115) )
& ? [X114] :
( p102(X114)
& ~ p103(X114)
& ~ p3(X114)
& r1(X107,X114) ) ) )
& ( ~ p102(X107)
| p103(X107)
| ( ? [X113] :
( p103(X113)
& ~ p104(X113)
& p4(X113)
& r1(X107,X113) )
& ? [X112] :
( p103(X112)
& ~ p104(X112)
& ~ p4(X112)
& r1(X107,X112) ) ) )
& ( ~ p103(X107)
| p104(X107)
| ( ? [X111] :
( p104(X111)
& ~ p105(X111)
& p5(X111)
& r1(X107,X111) )
& ? [X110] :
( p104(X110)
& ~ p105(X110)
& ~ p5(X110)
& r1(X107,X110) ) ) )
& ( ~ p104(X107)
| p105(X107)
| ( ? [X109] :
( p105(X109)
& ~ p106(X109)
& p6(X109)
& r1(X107,X109) )
& ? [X108] :
( p105(X108)
& ~ p106(X108)
& ~ p6(X108)
& r1(X107,X108) ) ) ) )
| ~ r1(X,X107) )
& ! [X83] :
( ! [X84] :
( ( ( ~ p101(X84)
| p100(X84) )
& ( ~ p102(X84)
| p101(X84) )
& ( ~ p103(X84)
| p102(X84) )
& ( ~ p104(X84)
| p103(X84) )
& ( ~ p105(X84)
| p104(X84) )
& ( ~ p106(X84)
| p105(X84) )
& ( ~ p100(X84)
| ( ( ~ p1(X84)
| ! [X106] :
( ~ p100(X106)
| p1(X106)
| ~ r1(X84,X106) ) )
& ( p1(X84)
| ! [X105] :
( ~ p100(X105)
| ~ p1(X105)
| ~ r1(X84,X105) ) ) ) )
& ( ~ p101(X84)
| ( ( ~ p2(X84)
| ! [X104] :
( ~ p101(X104)
| p2(X104)
| ~ r1(X84,X104) ) )
& ( p2(X84)
| ! [X103] :
( ~ p101(X103)
| ~ p2(X103)
| ~ r1(X84,X103) ) ) ) )
& ( ~ p102(X84)
| ( ( ~ p3(X84)
| ! [X102] :
( ~ p102(X102)
| p3(X102)
| ~ r1(X84,X102) ) )
& ( p3(X84)
| ! [X101] :
( ~ p102(X101)
| ~ p3(X101)
| ~ r1(X84,X101) ) ) ) )
& ( ~ p103(X84)
| ( ( ~ p4(X84)
| ! [X100] :
( ~ p103(X100)
| p4(X100)
| ~ r1(X84,X100) ) )
& ( p4(X84)
| ! [X99] :
( ~ p103(X99)
| ~ p4(X99)
| ~ r1(X84,X99) ) ) ) )
& ( ~ p104(X84)
| ( ( ~ p5(X84)
| ! [X98] :
( ~ p104(X98)
| p5(X98)
| ~ r1(X84,X98) ) )
& ( p5(X84)
| ! [X97] :
( ~ p104(X97)
| ~ p5(X97)
| ~ r1(X84,X97) ) ) ) )
& ( ~ p105(X84)
| ( ( ~ p6(X84)
| ! [X96] :
( ~ p105(X96)
| p6(X96)
| ~ r1(X84,X96) ) )
& ( p6(X84)
| ! [X95] :
( ~ p105(X95)
| ~ p6(X95)
| ~ r1(X84,X95) ) ) ) )
& ( ~ p100(X84)
| p101(X84)
| ( ? [X94] :
( p101(X94)
& ~ p102(X94)
& p2(X94)
& r1(X84,X94) )
& ? [X93] :
( p101(X93)
& ~ p102(X93)
& ~ p2(X93)
& r1(X84,X93) ) ) )
& ( ~ p101(X84)
| p102(X84)
| ( ? [X92] :
( p102(X92)
& ~ p103(X92)
& p3(X92)
& r1(X84,X92) )
& ? [X91] :
( p102(X91)
& ~ p103(X91)
& ~ p3(X91)
& r1(X84,X91) ) ) )
& ( ~ p102(X84)
| p103(X84)
| ( ? [X90] :
( p103(X90)
& ~ p104(X90)
& p4(X90)
& r1(X84,X90) )
& ? [X89] :
( p103(X89)
& ~ p104(X89)
& ~ p4(X89)
& r1(X84,X89) ) ) )
& ( ~ p103(X84)
| p104(X84)
| ( ? [X88] :
( p104(X88)
& ~ p105(X88)
& p5(X88)
& r1(X84,X88) )
& ? [X87] :
( p104(X87)
& ~ p105(X87)
& ~ p5(X87)
& r1(X84,X87) ) ) )
& ( ~ p104(X84)
| p105(X84)
| ( ? [X86] :
( p105(X86)
& ~ p106(X86)
& p6(X86)
& r1(X84,X86) )
& ? [X85] :
( p105(X85)
& ~ p106(X85)
& ~ p6(X85)
& r1(X84,X85) ) ) ) )
| ~ r1(X83,X84) )
| ~ r1(X,X83) )
& ! [X58] :
( ! [X59] :
( ! [X60] :
( ( ( ~ p101(X60)
| p100(X60) )
& ( ~ p102(X60)
| p101(X60) )
& ( ~ p103(X60)
| p102(X60) )
& ( ~ p104(X60)
| p103(X60) )
& ( ~ p105(X60)
| p104(X60) )
& ( ~ p106(X60)
| p105(X60) )
& ( ~ p100(X60)
| ( ( ~ p1(X60)
| ! [X82] :
( ~ p100(X82)
| p1(X82)
| ~ r1(X60,X82) ) )
& ( p1(X60)
| ! [X81] :
( ~ p100(X81)
| ~ p1(X81)
| ~ r1(X60,X81) ) ) ) )
& ( ~ p101(X60)
| ( ( ~ p2(X60)
| ! [X80] :
( ~ p101(X80)
| p2(X80)
| ~ r1(X60,X80) ) )
& ( p2(X60)
| ! [X79] :
( ~ p101(X79)
| ~ p2(X79)
| ~ r1(X60,X79) ) ) ) )
& ( ~ p102(X60)
| ( ( ~ p3(X60)
| ! [X78] :
( ~ p102(X78)
| p3(X78)
| ~ r1(X60,X78) ) )
& ( p3(X60)
| ! [X77] :
( ~ p102(X77)
| ~ p3(X77)
| ~ r1(X60,X77) ) ) ) )
& ( ~ p103(X60)
| ( ( ~ p4(X60)
| ! [X76] :
( ~ p103(X76)
| p4(X76)
| ~ r1(X60,X76) ) )
& ( p4(X60)
| ! [X75] :
( ~ p103(X75)
| ~ p4(X75)
| ~ r1(X60,X75) ) ) ) )
& ( ~ p104(X60)
| ( ( ~ p5(X60)
| ! [X74] :
( ~ p104(X74)
| p5(X74)
| ~ r1(X60,X74) ) )
& ( p5(X60)
| ! [X73] :
( ~ p104(X73)
| ~ p5(X73)
| ~ r1(X60,X73) ) ) ) )
& ( ~ p105(X60)
| ( ( ~ p6(X60)
| ! [X72] :
( ~ p105(X72)
| p6(X72)
| ~ r1(X60,X72) ) )
& ( p6(X60)
| ! [X71] :
( ~ p105(X71)
| ~ p6(X71)
| ~ r1(X60,X71) ) ) ) )
& ( ~ p100(X60)
| p101(X60)
| ( ? [X70] :
( p101(X70)
& ~ p102(X70)
& p2(X70)
& r1(X60,X70) )
& ? [X69] :
( p101(X69)
& ~ p102(X69)
& ~ p2(X69)
& r1(X60,X69) ) ) )
& ( ~ p101(X60)
| p102(X60)
| ( ? [X68] :
( p102(X68)
& ~ p103(X68)
& p3(X68)
& r1(X60,X68) )
& ? [X67] :
( p102(X67)
& ~ p103(X67)
& ~ p3(X67)
& r1(X60,X67) ) ) )
& ( ~ p102(X60)
| p103(X60)
| ( ? [X66] :
( p103(X66)
& ~ p104(X66)
& p4(X66)
& r1(X60,X66) )
& ? [X65] :
( p103(X65)
& ~ p104(X65)
& ~ p4(X65)
& r1(X60,X65) ) ) )
& ( ~ p103(X60)
| p104(X60)
| ( ? [X64] :
( p104(X64)
& ~ p105(X64)
& p5(X64)
& r1(X60,X64) )
& ? [X63] :
( p104(X63)
& ~ p105(X63)
& ~ p5(X63)
& r1(X60,X63) ) ) )
& ( ~ p104(X60)
| p105(X60)
| ( ? [X62] :
( p105(X62)
& ~ p106(X62)
& p6(X62)
& r1(X60,X62) )
& ? [X61] :
( p105(X61)
& ~ p106(X61)
& ~ p6(X61)
& r1(X60,X61) ) ) ) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X,X58) )
& ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [X35] :
( ( ( ~ p101(X35)
| p100(X35) )
& ( ~ p102(X35)
| p101(X35) )
& ( ~ p103(X35)
| p102(X35) )
& ( ~ p104(X35)
| p103(X35) )
& ( ~ p105(X35)
| p104(X35) )
& ( ~ p106(X35)
| p105(X35) )
& ( ~ p100(X35)
| ( ( ~ p1(X35)
| ! [X57] :
( ~ p100(X57)
| p1(X57)
| ~ r1(X35,X57) ) )
& ( p1(X35)
| ! [X56] :
( ~ p100(X56)
| ~ p1(X56)
| ~ r1(X35,X56) ) ) ) )
& ( ~ p101(X35)
| ( ( ~ p2(X35)
| ! [X55] :
( ~ p101(X55)
| p2(X55)
| ~ r1(X35,X55) ) )
& ( p2(X35)
| ! [X54] :
( ~ p101(X54)
| ~ p2(X54)
| ~ r1(X35,X54) ) ) ) )
& ( ~ p102(X35)
| ( ( ~ p3(X35)
| ! [X53] :
( ~ p102(X53)
| p3(X53)
| ~ r1(X35,X53) ) )
& ( p3(X35)
| ! [X52] :
( ~ p102(X52)
| ~ p3(X52)
| ~ r1(X35,X52) ) ) ) )
& ( ~ p103(X35)
| ( ( ~ p4(X35)
| ! [X51] :
( ~ p103(X51)
| p4(X51)
| ~ r1(X35,X51) ) )
& ( p4(X35)
| ! [X50] :
( ~ p103(X50)
| ~ p4(X50)
| ~ r1(X35,X50) ) ) ) )
& ( ~ p104(X35)
| ( ( ~ p5(X35)
| ! [X49] :
( ~ p104(X49)
| p5(X49)
| ~ r1(X35,X49) ) )
& ( p5(X35)
| ! [X48] :
( ~ p104(X48)
| ~ p5(X48)
| ~ r1(X35,X48) ) ) ) )
& ( ~ p105(X35)
| ( ( ~ p6(X35)
| ! [X47] :
( ~ p105(X47)
| p6(X47)
| ~ r1(X35,X47) ) )
& ( p6(X35)
| ! [X46] :
( ~ p105(X46)
| ~ p6(X46)
| ~ r1(X35,X46) ) ) ) )
& ( ~ p100(X35)
| p101(X35)
| ( ? [X45] :
( p101(X45)
& ~ p102(X45)
& p2(X45)
& r1(X35,X45) )
& ? [X44] :
( p101(X44)
& ~ p102(X44)
& ~ p2(X44)
& r1(X35,X44) ) ) )
& ( ~ p101(X35)
| p102(X35)
| ( ? [X43] :
( p102(X43)
& ~ p103(X43)
& p3(X43)
& r1(X35,X43) )
& ? [X42] :
( p102(X42)
& ~ p103(X42)
& ~ p3(X42)
& r1(X35,X42) ) ) )
& ( ~ p102(X35)
| p103(X35)
| ( ? [X41] :
( p103(X41)
& ~ p104(X41)
& p4(X41)
& r1(X35,X41) )
& ? [X40] :
( p103(X40)
& ~ p104(X40)
& ~ p4(X40)
& r1(X35,X40) ) ) )
& ( ~ p103(X35)
| p104(X35)
| ( ? [X39] :
( p104(X39)
& ~ p105(X39)
& p5(X39)
& r1(X35,X39) )
& ? [X38] :
( p104(X38)
& ~ p105(X38)
& ~ p5(X38)
& r1(X35,X38) ) ) )
& ( ~ p104(X35)
| p105(X35)
| ( ? [X37] :
( p105(X37)
& ~ p106(X37)
& p6(X37)
& r1(X35,X37) )
& ? [X36] :
( p105(X36)
& ~ p106(X36)
& ~ p6(X36)
& r1(X35,X36) ) ) ) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X,X32) )
& ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ( ~ p101(X9)
| p100(X9) )
& ( ~ p102(X9)
| p101(X9) )
& ( ~ p103(X9)
| p102(X9) )
& ( ~ p104(X9)
| p103(X9) )
& ( ~ p105(X9)
| p104(X9) )
& ( ~ p106(X9)
| p105(X9) )
& ( ~ p100(X9)
| ( ( ~ p1(X9)
| ! [X31] :
( ~ p100(X31)
| p1(X31)
| ~ r1(X9,X31) ) )
& ( p1(X9)
| ! [X30] :
( ~ p100(X30)
| ~ p1(X30)
| ~ r1(X9,X30) ) ) ) )
& ( ~ p101(X9)
| ( ( ~ p2(X9)
| ! [X29] :
( ~ p101(X29)
| p2(X29)
| ~ r1(X9,X29) ) )
& ( p2(X9)
| ! [X28] :
( ~ p101(X28)
| ~ p2(X28)
| ~ r1(X9,X28) ) ) ) )
& ( ~ p102(X9)
| ( ( ~ p3(X9)
| ! [X27] :
( ~ p102(X27)
| p3(X27)
| ~ r1(X9,X27) ) )
& ( p3(X9)
| ! [X26] :
( ~ p102(X26)
| ~ p3(X26)
| ~ r1(X9,X26) ) ) ) )
& ( ~ p103(X9)
| ( ( ~ p4(X9)
| ! [X25] :
( ~ p103(X25)
| p4(X25)
| ~ r1(X9,X25) ) )
& ( p4(X9)
| ! [X24] :
( ~ p103(X24)
| ~ p4(X24)
| ~ r1(X9,X24) ) ) ) )
& ( ~ p104(X9)
| ( ( ~ p5(X9)
| ! [X23] :
( ~ p104(X23)
| p5(X23)
| ~ r1(X9,X23) ) )
& ( p5(X9)
| ! [X22] :
( ~ p104(X22)
| ~ p5(X22)
| ~ r1(X9,X22) ) ) ) )
& ( ~ p105(X9)
| ( ( ~ p6(X9)
| ! [X21] :
( ~ p105(X21)
| p6(X21)
| ~ r1(X9,X21) ) )
& ( p6(X9)
| ! [X20] :
( ~ p105(X20)
| ~ p6(X20)
| ~ r1(X9,X20) ) ) ) )
& ( ~ p100(X9)
| p101(X9)
| ( ? [X19] :
( p101(X19)
& ~ p102(X19)
& p2(X19)
& r1(X9,X19) )
& ? [X18] :
( p101(X18)
& ~ p102(X18)
& ~ p2(X18)
& r1(X9,X18) ) ) )
& ( ~ p101(X9)
| p102(X9)
| ( ? [X17] :
( p102(X17)
& ~ p103(X17)
& p3(X17)
& r1(X9,X17) )
& ? [X16] :
( p102(X16)
& ~ p103(X16)
& ~ p3(X16)
& r1(X9,X16) ) ) )
& ( ~ p102(X9)
| p103(X9)
| ( ? [X15] :
( p103(X15)
& ~ p104(X15)
& p4(X15)
& r1(X9,X15) )
& ? [X14] :
( p103(X14)
& ~ p104(X14)
& ~ p4(X14)
& r1(X9,X14) ) ) )
& ( ~ p103(X9)
| p104(X9)
| ( ? [X13] :
( p104(X13)
& ~ p105(X13)
& p5(X13)
& r1(X9,X13) )
& ? [X12] :
( p104(X12)
& ~ p105(X12)
& ~ p5(X12)
& r1(X9,X12) ) ) )
& ( ~ p104(X9)
| p105(X9)
| ( ? [X11] :
( p105(X11)
& ~ p106(X11)
& p6(X11)
& r1(X9,X11) )
& ? [X10] :
( p105(X10)
& ~ p106(X10)
& ~ p6(X10)
& r1(X9,X10) ) ) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X,X5) )
& ! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( p3(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) )
| ~ r1(X,X0) ) ),
inference(fof_nnf,[status(thm)],[main_neg]) ).
fof(sk_main_neg_sk,plain,
( p100(sK0)
& ~ p101(sK0)
& ( ~ p101(sK0)
| p100(sK0) )
& ( ~ p102(sK0)
| p101(sK0) )
& ( ~ p103(sK0)
| p102(sK0) )
& ( ~ p104(sK0)
| p103(sK0) )
& ( ~ p105(sK0)
| p104(sK0) )
& ( ~ p106(sK0)
| p105(sK0) )
& ( ~ p100(sK0)
| ( ( ~ p1(sK0)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(sK0,Y) ) )
& ( p1(sK0)
| ! [X150] :
( ~ p100(X150)
| ~ p1(X150)
| ~ r1(sK0,X150) ) ) ) )
& ( ~ p101(sK0)
| ( ( ~ p2(sK0)
| ! [X149] :
( ~ p101(X149)
| p2(X149)
| ~ r1(sK0,X149) ) )
& ( p2(sK0)
| ! [X148] :
( ~ p101(X148)
| ~ p2(X148)
| ~ r1(sK0,X148) ) ) ) )
& ( ~ p102(sK0)
| ( ( ~ p3(sK0)
| ! [X147] :
( ~ p102(X147)
| p3(X147)
| ~ r1(sK0,X147) ) )
& ( p3(sK0)
| ! [X146] :
( ~ p102(X146)
| ~ p3(X146)
| ~ r1(sK0,X146) ) ) ) )
& ( ~ p103(sK0)
| ( ( ~ p4(sK0)
| ! [X145] :
( ~ p103(X145)
| p4(X145)
| ~ r1(sK0,X145) ) )
& ( p4(sK0)
| ! [X144] :
( ~ p103(X144)
| ~ p4(X144)
| ~ r1(sK0,X144) ) ) ) )
& ( ~ p104(sK0)
| ( ( ~ p5(sK0)
| ! [X143] :
( ~ p104(X143)
| p5(X143)
| ~ r1(sK0,X143) ) )
& ( p5(sK0)
| ! [X142] :
( ~ p104(X142)
| ~ p5(X142)
| ~ r1(sK0,X142) ) ) ) )
& ( ~ p105(sK0)
| ( ( ~ p6(sK0)
| ! [X141] :
( ~ p105(X141)
| p6(X141)
| ~ r1(sK0,X141) ) )
& ( p6(sK0)
| ! [X140] :
( ~ p105(X140)
| ~ p6(X140)
| ~ r1(sK0,X140) ) ) ) )
& ( ~ p100(sK0)
| p101(sK0)
| ( p101(sK60)
& ~ p102(sK60)
& p2(sK60)
& r1(sK0,sK60)
& p101(sK1)
& ~ p102(sK1)
& ~ p2(sK1)
& r1(sK0,sK1) ) )
& ( ~ p101(sK0)
| p102(sK0)
| ( p102(sK59)
& ~ p103(sK59)
& p3(sK59)
& r1(sK0,sK59)
& p102(sK58)
& ~ p103(sK58)
& ~ p3(sK58)
& r1(sK0,sK58) ) )
& ( ~ p102(sK0)
| p103(sK0)
| ( p103(sK57)
& ~ p104(sK57)
& p4(sK57)
& r1(sK0,sK57)
& p103(sK56)
& ~ p104(sK56)
& ~ p4(sK56)
& r1(sK0,sK56) ) )
& ( ~ p103(sK0)
| p104(sK0)
| ( p104(sK55)
& ~ p105(sK55)
& p5(sK55)
& r1(sK0,sK55)
& p104(sK54)
& ~ p105(sK54)
& ~ p5(sK54)
& r1(sK0,sK54) ) )
& ( ~ p104(sK0)
| p105(sK0)
| ( p105(sK53)
& ~ p106(sK53)
& p6(sK53)
& r1(sK0,sK53)
& p105(sK52)
& ~ p106(sK52)
& ~ p6(sK52)
& r1(sK0,sK52) ) )
& ! [X107] :
( ( ( ~ p101(X107)
| p100(X107) )
& ( ~ p102(X107)
| p101(X107) )
& ( ~ p103(X107)
| p102(X107) )
& ( ~ p104(X107)
| p103(X107) )
& ( ~ p105(X107)
| p104(X107) )
& ( ~ p106(X107)
| p105(X107) )
& ( ~ p100(X107)
| ( ( ~ p1(X107)
| ! [X129] :
( ~ p100(X129)
| p1(X129)
| ~ r1(X107,X129) ) )
& ( p1(X107)
| ! [X128] :
( ~ p100(X128)
| ~ p1(X128)
| ~ r1(X107,X128) ) ) ) )
& ( ~ p101(X107)
| ( ( ~ p2(X107)
| ! [X127] :
( ~ p101(X127)
| p2(X127)
| ~ r1(X107,X127) ) )
& ( p2(X107)
| ! [X126] :
( ~ p101(X126)
| ~ p2(X126)
| ~ r1(X107,X126) ) ) ) )
& ( ~ p102(X107)
| ( ( ~ p3(X107)
| ! [X125] :
( ~ p102(X125)
| p3(X125)
| ~ r1(X107,X125) ) )
& ( p3(X107)
| ! [X124] :
( ~ p102(X124)
| ~ p3(X124)
| ~ r1(X107,X124) ) ) ) )
& ( ~ p103(X107)
| ( ( ~ p4(X107)
| ! [X123] :
( ~ p103(X123)
| p4(X123)
| ~ r1(X107,X123) ) )
& ( p4(X107)
| ! [X122] :
( ~ p103(X122)
| ~ p4(X122)
| ~ r1(X107,X122) ) ) ) )
& ( ~ p104(X107)
| ( ( ~ p5(X107)
| ! [X121] :
( ~ p104(X121)
| p5(X121)
| ~ r1(X107,X121) ) )
& ( p5(X107)
| ! [X120] :
( ~ p104(X120)
| ~ p5(X120)
| ~ r1(X107,X120) ) ) ) )
& ( ~ p105(X107)
| ( ( ~ p6(X107)
| ! [X119] :
( ~ p105(X119)
| p6(X119)
| ~ r1(X107,X119) ) )
& ( p6(X107)
| ! [X118] :
( ~ p105(X118)
| ~ p6(X118)
| ~ r1(X107,X118) ) ) ) )
& ( ~ p100(X107)
| p101(X107)
| ( p101(sK51(X107))
& ~ p102(sK51(X107))
& p2(sK51(X107))
& r1(X107,sK51(X107))
& p101(sK50(X107))
& ~ p102(sK50(X107))
& ~ p2(sK50(X107))
& r1(X107,sK50(X107)) ) )
& ( ~ p101(X107)
| p102(X107)
| ( p102(sK49(X107))
& ~ p103(sK49(X107))
& p3(sK49(X107))
& r1(X107,sK49(X107))
& p102(sK2(X107))
& ~ p103(sK2(X107))
& ~ p3(sK2(X107))
& r1(X107,sK2(X107)) ) )
& ( ~ p102(X107)
| p103(X107)
| ( p103(sK48(X107))
& ~ p104(sK48(X107))
& p4(sK48(X107))
& r1(X107,sK48(X107))
& p103(sK47(X107))
& ~ p104(sK47(X107))
& ~ p4(sK47(X107))
& r1(X107,sK47(X107)) ) )
& ( ~ p103(X107)
| p104(X107)
| ( p104(sK46(X107))
& ~ p105(sK46(X107))
& p5(sK46(X107))
& r1(X107,sK46(X107))
& p104(sK45(X107))
& ~ p105(sK45(X107))
& ~ p5(sK45(X107))
& r1(X107,sK45(X107)) ) )
& ( ~ p104(X107)
| p105(X107)
| ( p105(sK44(X107))
& ~ p106(sK44(X107))
& p6(sK44(X107))
& r1(X107,sK44(X107))
& p105(sK43(X107))
& ~ p106(sK43(X107))
& ~ p6(sK43(X107))
& r1(X107,sK43(X107)) ) ) )
| ~ r1(sK0,X107) )
& ! [X83] :
( ! [X84] :
( ( ( ~ p101(X84)
| p100(X84) )
& ( ~ p102(X84)
| p101(X84) )
& ( ~ p103(X84)
| p102(X84) )
& ( ~ p104(X84)
| p103(X84) )
& ( ~ p105(X84)
| p104(X84) )
& ( ~ p106(X84)
| p105(X84) )
& ( ~ p100(X84)
| ( ( ~ p1(X84)
| ! [X106] :
( ~ p100(X106)
| p1(X106)
| ~ r1(X84,X106) ) )
& ( p1(X84)
| ! [X105] :
( ~ p100(X105)
| ~ p1(X105)
| ~ r1(X84,X105) ) ) ) )
& ( ~ p101(X84)
| ( ( ~ p2(X84)
| ! [X104] :
( ~ p101(X104)
| p2(X104)
| ~ r1(X84,X104) ) )
& ( p2(X84)
| ! [X103] :
( ~ p101(X103)
| ~ p2(X103)
| ~ r1(X84,X103) ) ) ) )
& ( ~ p102(X84)
| ( ( ~ p3(X84)
| ! [X102] :
( ~ p102(X102)
| p3(X102)
| ~ r1(X84,X102) ) )
& ( p3(X84)
| ! [X101] :
( ~ p102(X101)
| ~ p3(X101)
| ~ r1(X84,X101) ) ) ) )
& ( ~ p103(X84)
| ( ( ~ p4(X84)
| ! [X100] :
( ~ p103(X100)
| p4(X100)
| ~ r1(X84,X100) ) )
& ( p4(X84)
| ! [X99] :
( ~ p103(X99)
| ~ p4(X99)
| ~ r1(X84,X99) ) ) ) )
& ( ~ p104(X84)
| ( ( ~ p5(X84)
| ! [X98] :
( ~ p104(X98)
| p5(X98)
| ~ r1(X84,X98) ) )
& ( p5(X84)
| ! [X97] :
( ~ p104(X97)
| ~ p5(X97)
| ~ r1(X84,X97) ) ) ) )
& ( ~ p105(X84)
| ( ( ~ p6(X84)
| ! [X96] :
( ~ p105(X96)
| p6(X96)
| ~ r1(X84,X96) ) )
& ( p6(X84)
| ! [X95] :
( ~ p105(X95)
| ~ p6(X95)
| ~ r1(X84,X95) ) ) ) )
& ( ~ p100(X84)
| p101(X84)
| ( p101(sK42(X83,X84))
& ~ p102(sK42(X83,X84))
& p2(sK42(X83,X84))
& r1(X84,sK42(X83,X84))
& p101(sK41(X83,X84))
& ~ p102(sK41(X83,X84))
& ~ p2(sK41(X83,X84))
& r1(X84,sK41(X83,X84)) ) )
& ( ~ p101(X84)
| p102(X84)
| ( p102(sK40(X83,X84))
& ~ p103(sK40(X83,X84))
& p3(sK40(X83,X84))
& r1(X84,sK40(X83,X84))
& p102(sK39(X83,X84))
& ~ p103(sK39(X83,X84))
& ~ p3(sK39(X83,X84))
& r1(X84,sK39(X83,X84)) ) )
& ( ~ p102(X84)
| p103(X84)
| ( p103(sK38(X83,X84))
& ~ p104(sK38(X83,X84))
& p4(sK38(X83,X84))
& r1(X84,sK38(X83,X84))
& p103(sK3(X83,X84))
& ~ p104(sK3(X83,X84))
& ~ p4(sK3(X83,X84))
& r1(X84,sK3(X83,X84)) ) )
& ( ~ p103(X84)
| p104(X84)
| ( p104(sK37(X83,X84))
& ~ p105(sK37(X83,X84))
& p5(sK37(X83,X84))
& r1(X84,sK37(X83,X84))
& p104(sK36(X83,X84))
& ~ p105(sK36(X83,X84))
& ~ p5(sK36(X83,X84))
& r1(X84,sK36(X83,X84)) ) )
& ( ~ p104(X84)
| p105(X84)
| ( p105(sK35(X83,X84))
& ~ p106(sK35(X83,X84))
& p6(sK35(X83,X84))
& r1(X84,sK35(X83,X84))
& p105(sK34(X83,X84))
& ~ p106(sK34(X83,X84))
& ~ p6(sK34(X83,X84))
& r1(X84,sK34(X83,X84)) ) ) )
| ~ r1(X83,X84) )
| ~ r1(sK0,X83) )
& ! [X58] :
( ! [X59] :
( ! [X60] :
( ( ( ~ p101(X60)
| p100(X60) )
& ( ~ p102(X60)
| p101(X60) )
& ( ~ p103(X60)
| p102(X60) )
& ( ~ p104(X60)
| p103(X60) )
& ( ~ p105(X60)
| p104(X60) )
& ( ~ p106(X60)
| p105(X60) )
& ( ~ p100(X60)
| ( ( ~ p1(X60)
| ! [X82] :
( ~ p100(X82)
| p1(X82)
| ~ r1(X60,X82) ) )
& ( p1(X60)
| ! [X81] :
( ~ p100(X81)
| ~ p1(X81)
| ~ r1(X60,X81) ) ) ) )
& ( ~ p101(X60)
| ( ( ~ p2(X60)
| ! [X80] :
( ~ p101(X80)
| p2(X80)
| ~ r1(X60,X80) ) )
& ( p2(X60)
| ! [X79] :
( ~ p101(X79)
| ~ p2(X79)
| ~ r1(X60,X79) ) ) ) )
& ( ~ p102(X60)
| ( ( ~ p3(X60)
| ! [X78] :
( ~ p102(X78)
| p3(X78)
| ~ r1(X60,X78) ) )
& ( p3(X60)
| ! [X77] :
( ~ p102(X77)
| ~ p3(X77)
| ~ r1(X60,X77) ) ) ) )
& ( ~ p103(X60)
| ( ( ~ p4(X60)
| ! [X76] :
( ~ p103(X76)
| p4(X76)
| ~ r1(X60,X76) ) )
& ( p4(X60)
| ! [X75] :
( ~ p103(X75)
| ~ p4(X75)
| ~ r1(X60,X75) ) ) ) )
& ( ~ p104(X60)
| ( ( ~ p5(X60)
| ! [X74] :
( ~ p104(X74)
| p5(X74)
| ~ r1(X60,X74) ) )
& ( p5(X60)
| ! [X73] :
( ~ p104(X73)
| ~ p5(X73)
| ~ r1(X60,X73) ) ) ) )
& ( ~ p105(X60)
| ( ( ~ p6(X60)
| ! [X72] :
( ~ p105(X72)
| p6(X72)
| ~ r1(X60,X72) ) )
& ( p6(X60)
| ! [X71] :
( ~ p105(X71)
| ~ p6(X71)
| ~ r1(X60,X71) ) ) ) )
& ( ~ p100(X60)
| p101(X60)
| ( p101(sK33(X58,X59,X60))
& ~ p102(sK33(X58,X59,X60))
& p2(sK33(X58,X59,X60))
& r1(X60,sK33(X58,X59,X60))
& p101(sK32(X58,X59,X60))
& ~ p102(sK32(X58,X59,X60))
& ~ p2(sK32(X58,X59,X60))
& r1(X60,sK32(X58,X59,X60)) ) )
& ( ~ p101(X60)
| p102(X60)
| ( p102(sK31(X58,X59,X60))
& ~ p103(sK31(X58,X59,X60))
& p3(sK31(X58,X59,X60))
& r1(X60,sK31(X58,X59,X60))
& p102(sK30(X58,X59,X60))
& ~ p103(sK30(X58,X59,X60))
& ~ p3(sK30(X58,X59,X60))
& r1(X60,sK30(X58,X59,X60)) ) )
& ( ~ p102(X60)
| p103(X60)
| ( p103(sK29(X58,X59,X60))
& ~ p104(sK29(X58,X59,X60))
& p4(sK29(X58,X59,X60))
& r1(X60,sK29(X58,X59,X60))
& p103(sK28(X58,X59,X60))
& ~ p104(sK28(X58,X59,X60))
& ~ p4(sK28(X58,X59,X60))
& r1(X60,sK28(X58,X59,X60)) ) )
& ( ~ p103(X60)
| p104(X60)
| ( p104(sK27(X58,X59,X60))
& ~ p105(sK27(X58,X59,X60))
& p5(sK27(X58,X59,X60))
& r1(X60,sK27(X58,X59,X60))
& p104(sK4(X58,X59,X60))
& ~ p105(sK4(X58,X59,X60))
& ~ p5(sK4(X58,X59,X60))
& r1(X60,sK4(X58,X59,X60)) ) )
& ( ~ p104(X60)
| p105(X60)
| ( p105(sK26(X58,X59,X60))
& ~ p106(sK26(X58,X59,X60))
& p6(sK26(X58,X59,X60))
& r1(X60,sK26(X58,X59,X60))
& p105(sK25(X58,X59,X60))
& ~ p106(sK25(X58,X59,X60))
& ~ p6(sK25(X58,X59,X60))
& r1(X60,sK25(X58,X59,X60)) ) ) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(sK0,X58) )
& ! [X32] :
( ! [X33] :
( ! [X34] :
( ! [X35] :
( ( ( ~ p101(X35)
| p100(X35) )
& ( ~ p102(X35)
| p101(X35) )
& ( ~ p103(X35)
| p102(X35) )
& ( ~ p104(X35)
| p103(X35) )
& ( ~ p105(X35)
| p104(X35) )
& ( ~ p106(X35)
| p105(X35) )
& ( ~ p100(X35)
| ( ( ~ p1(X35)
| ! [X57] :
( ~ p100(X57)
| p1(X57)
| ~ r1(X35,X57) ) )
& ( p1(X35)
| ! [X56] :
( ~ p100(X56)
| ~ p1(X56)
| ~ r1(X35,X56) ) ) ) )
& ( ~ p101(X35)
| ( ( ~ p2(X35)
| ! [X55] :
( ~ p101(X55)
| p2(X55)
| ~ r1(X35,X55) ) )
& ( p2(X35)
| ! [X54] :
( ~ p101(X54)
| ~ p2(X54)
| ~ r1(X35,X54) ) ) ) )
& ( ~ p102(X35)
| ( ( ~ p3(X35)
| ! [X53] :
( ~ p102(X53)
| p3(X53)
| ~ r1(X35,X53) ) )
& ( p3(X35)
| ! [X52] :
( ~ p102(X52)
| ~ p3(X52)
| ~ r1(X35,X52) ) ) ) )
& ( ~ p103(X35)
| ( ( ~ p4(X35)
| ! [X51] :
( ~ p103(X51)
| p4(X51)
| ~ r1(X35,X51) ) )
& ( p4(X35)
| ! [X50] :
( ~ p103(X50)
| ~ p4(X50)
| ~ r1(X35,X50) ) ) ) )
& ( ~ p104(X35)
| ( ( ~ p5(X35)
| ! [X49] :
( ~ p104(X49)
| p5(X49)
| ~ r1(X35,X49) ) )
& ( p5(X35)
| ! [X48] :
( ~ p104(X48)
| ~ p5(X48)
| ~ r1(X35,X48) ) ) ) )
& ( ~ p105(X35)
| ( ( ~ p6(X35)
| ! [X47] :
( ~ p105(X47)
| p6(X47)
| ~ r1(X35,X47) ) )
& ( p6(X35)
| ! [X46] :
( ~ p105(X46)
| ~ p6(X46)
| ~ r1(X35,X46) ) ) ) )
& ( ~ p100(X35)
| p101(X35)
| ( p101(sK24(X32,X33,X34,X35))
& ~ p102(sK24(X32,X33,X34,X35))
& p2(sK24(X32,X33,X34,X35))
& r1(X35,sK24(X32,X33,X34,X35))
& p101(sK23(X32,X33,X34,X35))
& ~ p102(sK23(X32,X33,X34,X35))
& ~ p2(sK23(X32,X33,X34,X35))
& r1(X35,sK23(X32,X33,X34,X35)) ) )
& ( ~ p101(X35)
| p102(X35)
| ( p102(sK22(X32,X33,X34,X35))
& ~ p103(sK22(X32,X33,X34,X35))
& p3(sK22(X32,X33,X34,X35))
& r1(X35,sK22(X32,X33,X34,X35))
& p102(sK21(X32,X33,X34,X35))
& ~ p103(sK21(X32,X33,X34,X35))
& ~ p3(sK21(X32,X33,X34,X35))
& r1(X35,sK21(X32,X33,X34,X35)) ) )
& ( ~ p102(X35)
| p103(X35)
| ( p103(sK20(X32,X33,X34,X35))
& ~ p104(sK20(X32,X33,X34,X35))
& p4(sK20(X32,X33,X34,X35))
& r1(X35,sK20(X32,X33,X34,X35))
& p103(sK19(X32,X33,X34,X35))
& ~ p104(sK19(X32,X33,X34,X35))
& ~ p4(sK19(X32,X33,X34,X35))
& r1(X35,sK19(X32,X33,X34,X35)) ) )
& ( ~ p103(X35)
| p104(X35)
| ( p104(sK18(X32,X33,X34,X35))
& ~ p105(sK18(X32,X33,X34,X35))
& p5(sK18(X32,X33,X34,X35))
& r1(X35,sK18(X32,X33,X34,X35))
& p104(sK17(X32,X33,X34,X35))
& ~ p105(sK17(X32,X33,X34,X35))
& ~ p5(sK17(X32,X33,X34,X35))
& r1(X35,sK17(X32,X33,X34,X35)) ) )
& ( ~ p104(X35)
| p105(X35)
| ( p105(sK16(X32,X33,X34,X35))
& ~ p106(sK16(X32,X33,X34,X35))
& p6(sK16(X32,X33,X34,X35))
& r1(X35,sK16(X32,X33,X34,X35))
& p105(sK5(X32,X33,X34,X35))
& ~ p106(sK5(X32,X33,X34,X35))
& ~ p6(sK5(X32,X33,X34,X35))
& r1(X35,sK5(X32,X33,X34,X35)) ) ) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(sK0,X32) )
& ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ( ~ p101(X9)
| p100(X9) )
& ( ~ p102(X9)
| p101(X9) )
& ( ~ p103(X9)
| p102(X9) )
& ( ~ p104(X9)
| p103(X9) )
& ( ~ p105(X9)
| p104(X9) )
& ( ~ p106(X9)
| p105(X9) )
& ( ~ p100(X9)
| ( ( ~ p1(X9)
| ! [X31] :
( ~ p100(X31)
| p1(X31)
| ~ r1(X9,X31) ) )
& ( p1(X9)
| ! [X30] :
( ~ p100(X30)
| ~ p1(X30)
| ~ r1(X9,X30) ) ) ) )
& ( ~ p101(X9)
| ( ( ~ p2(X9)
| ! [X29] :
( ~ p101(X29)
| p2(X29)
| ~ r1(X9,X29) ) )
& ( p2(X9)
| ! [X28] :
( ~ p101(X28)
| ~ p2(X28)
| ~ r1(X9,X28) ) ) ) )
& ( ~ p102(X9)
| ( ( ~ p3(X9)
| ! [X27] :
( ~ p102(X27)
| p3(X27)
| ~ r1(X9,X27) ) )
& ( p3(X9)
| ! [X26] :
( ~ p102(X26)
| ~ p3(X26)
| ~ r1(X9,X26) ) ) ) )
& ( ~ p103(X9)
| ( ( ~ p4(X9)
| ! [X25] :
( ~ p103(X25)
| p4(X25)
| ~ r1(X9,X25) ) )
& ( p4(X9)
| ! [X24] :
( ~ p103(X24)
| ~ p4(X24)
| ~ r1(X9,X24) ) ) ) )
& ( ~ p104(X9)
| ( ( ~ p5(X9)
| ! [X23] :
( ~ p104(X23)
| p5(X23)
| ~ r1(X9,X23) ) )
& ( p5(X9)
| ! [X22] :
( ~ p104(X22)
| ~ p5(X22)
| ~ r1(X9,X22) ) ) ) )
& ( ~ p105(X9)
| ( ( ~ p6(X9)
| ! [X21] :
( ~ p105(X21)
| p6(X21)
| ~ r1(X9,X21) ) )
& ( p6(X9)
| ! [X20] :
( ~ p105(X20)
| ~ p6(X20)
| ~ r1(X9,X20) ) ) ) )
& ( ~ p100(X9)
| p101(X9)
| ( p101(sK15(X5,X6,X7,X8,X9))
& ~ p102(sK15(X5,X6,X7,X8,X9))
& p2(sK15(X5,X6,X7,X8,X9))
& r1(X9,sK15(X5,X6,X7,X8,X9))
& p101(sK14(X5,X6,X7,X8,X9))
& ~ p102(sK14(X5,X6,X7,X8,X9))
& ~ p2(sK14(X5,X6,X7,X8,X9))
& r1(X9,sK14(X5,X6,X7,X8,X9)) ) )
& ( ~ p101(X9)
| p102(X9)
| ( p102(sK13(X5,X6,X7,X8,X9))
& ~ p103(sK13(X5,X6,X7,X8,X9))
& p3(sK13(X5,X6,X7,X8,X9))
& r1(X9,sK13(X5,X6,X7,X8,X9))
& p102(sK12(X5,X6,X7,X8,X9))
& ~ p103(sK12(X5,X6,X7,X8,X9))
& ~ p3(sK12(X5,X6,X7,X8,X9))
& r1(X9,sK12(X5,X6,X7,X8,X9)) ) )
& ( ~ p102(X9)
| p103(X9)
| ( p103(sK11(X5,X6,X7,X8,X9))
& ~ p104(sK11(X5,X6,X7,X8,X9))
& p4(sK11(X5,X6,X7,X8,X9))
& r1(X9,sK11(X5,X6,X7,X8,X9))
& p103(sK10(X5,X6,X7,X8,X9))
& ~ p104(sK10(X5,X6,X7,X8,X9))
& ~ p4(sK10(X5,X6,X7,X8,X9))
& r1(X9,sK10(X5,X6,X7,X8,X9)) ) )
& ( ~ p103(X9)
| p104(X9)
| ( p104(sK9(X5,X6,X7,X8,X9))
& ~ p105(sK9(X5,X6,X7,X8,X9))
& p5(sK9(X5,X6,X7,X8,X9))
& r1(X9,sK9(X5,X6,X7,X8,X9))
& p104(sK8(X5,X6,X7,X8,X9))
& ~ p105(sK8(X5,X6,X7,X8,X9))
& ~ p5(sK8(X5,X6,X7,X8,X9))
& r1(X9,sK8(X5,X6,X7,X8,X9)) ) )
& ( ~ p104(X9)
| p105(X9)
| ( p105(sK7(X5,X6,X7,X8,X9))
& ~ p106(sK7(X5,X6,X7,X8,X9))
& p6(sK7(X5,X6,X7,X8,X9))
& r1(X9,sK7(X5,X6,X7,X8,X9))
& p105(sK6(X5,X6,X7,X8,X9))
& ~ p106(sK6(X5,X6,X7,X8,X9))
& ~ p6(sK6(X5,X6,X7,X8,X9))
& r1(X9,sK6(X5,X6,X7,X8,X9)) ) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(sK0,X5) )
& ! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( p3(X4)
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) )
| ~ r1(sK0,X0) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK5,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK4,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK3,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK2,sK49,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK58,sK59,sK1,sK60]),skolemize(X,sK0),skolemize(X10,sK6(X5,X6,X7,X8,X9)),skolemize(X11,sK7(X5,X6,X7,X8,X9)),skolemize(X12,sK8(X5,X6,X7,X8,X9)),skolemize(X13,sK9(X5,X6,X7,X8,X9)),skolemize(X14,sK10(X5,X6,X7,X8,X9)),skolemize(X15,sK11(X5,X6,X7,X8,X9)),skolemize(X16,sK12(X5,X6,X7,X8,X9)),skolemize(X17,sK13(X5,X6,X7,X8,X9)),skolemize(X18,sK14(X5,X6,X7,X8,X9)),skolemize(X19,sK15(X5,X6,X7,X8,X9)),skolemize(X36,sK5(X32,X33,X34,X35)),skolemize(X37,sK16(X32,X33,X34,X35)),skolemize(X38,sK17(X32,X33,X34,X35)),skolemize(X39,sK18(X32,X33,X34,X35)),skolemize(X40,sK19(X32,X33,X34,X35)),skolemize(X41,sK20(X32,X33,X34,X35)),skolemize(X42,sK21(X32,X33,X34,X35)),skolemize(X43,sK22(X32,X33,X34,X35)),skolemize(X44,sK23(X32,X33,X34,X35)),skolemize(X45,sK24(X32,X33,X34,X35)),skolemize(X61,sK25(X58,X59,X60)),skolemize(X62,sK26(X58,X59,X60)),skolemize(X63,sK4(X58,X59,X60)),skolemize(X64,sK27(X58,X59,X60)),skolemize(X65,sK28(X58,X59,X60)),skolemize(X66,sK29(X58,X59,X60)),skolemize(X67,sK30(X58,X59,X60)),skolemize(X68,sK31(X58,X59,X60)),skolemize(X69,sK32(X58,X59,X60)),skolemize(X70,sK33(X58,X59,X60)),skolemize(X85,sK34(X83,X84)),skolemize(X86,sK35(X83,X84)),skolemize(X87,sK36(X83,X84)),skolemize(X88,sK37(X83,X84)),skolemize(X89,sK3(X83,X84)),skolemize(X90,sK38(X83,X84)),skolemize(X91,sK39(X83,X84)),skolemize(X92,sK40(X83,X84)),skolemize(X93,sK41(X83,X84)),skolemize(X94,sK42(X83,X84)),skolemize(X108,sK43(X107)),skolemize(X109,sK44(X107)),skolemize(X110,sK45(X107)),skolemize(X111,sK46(X107)),skolemize(X112,sK47(X107)),skolemize(X113,sK48(X107)),skolemize(X114,sK2(X107)),skolemize(X115,sK49(X107)),skolemize(X116,sK50(X107)),skolemize(X117,sK51(X107)),skolemize(X130,sK52),skolemize(X131,sK53),skolemize(X132,sK54),skolemize(X133,sK55),skolemize(X134,sK56),skolemize(X135,sK57),skolemize(X136,sK58),skolemize(X137,sK59),skolemize(X138,sK1),skolemize(X139,sK60)],[nnf_1]) ).
fof(sk_main_neg,plain,
( p100(sK0)
& ~ p101(sK0)
& ( ~ p102(sK0)
| p101(sK0) )
& ( ~ p103(sK0)
| p102(sK0) )
& ( ~ p104(sK0)
| p103(sK0) )
& ( ~ p105(sK0)
| p104(sK0) )
& ( ~ p106(sK0)
| p105(sK0) )
& ! [VAR_0] :
( ~ p100(sK0)
| ~ p1(sK0)
| ~ p100(VAR_0)
| p1(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(sK0)
| p1(sK0)
| ~ p100(VAR_0)
| ~ p1(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(sK0)
| ~ p3(sK0)
| ~ p102(VAR_0)
| p3(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(sK0)
| p3(sK0)
| ~ p102(VAR_0)
| ~ p3(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(sK0)
| ~ p4(sK0)
| ~ p103(VAR_0)
| p4(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(sK0)
| p4(sK0)
| ~ p103(VAR_0)
| ~ p4(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(sK0)
| ~ p5(sK0)
| ~ p104(VAR_0)
| p5(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(sK0)
| p5(sK0)
| ~ p104(VAR_0)
| ~ p5(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(sK0)
| ~ p6(sK0)
| ~ p105(VAR_0)
| p6(VAR_0)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p105(sK0)
| p6(sK0)
| ~ p105(VAR_0)
| ~ p6(VAR_0)
| ~ r1(sK0,VAR_0) )
& ( ~ p100(sK0)
| p101(sK0)
| p101(sK60) )
& ( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK60) )
& ( ~ p100(sK0)
| p101(sK0)
| p2(sK60) )
& ( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK60) )
& ( ~ p100(sK0)
| p101(sK0)
| p101(sK1) )
& ( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK1) )
& ( ~ p100(sK0)
| p101(sK0)
| ~ p2(sK1) )
& ( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK1) )
& ( ~ p102(sK0)
| p103(sK0)
| p103(sK57) )
& ( ~ p102(sK0)
| p103(sK0)
| ~ p104(sK57) )
& ( ~ p102(sK0)
| p103(sK0)
| p4(sK57) )
& ( ~ p102(sK0)
| p103(sK0)
| r1(sK0,sK57) )
& ( ~ p102(sK0)
| p103(sK0)
| p103(sK56) )
& ( ~ p102(sK0)
| p103(sK0)
| ~ p104(sK56) )
& ( ~ p102(sK0)
| p103(sK0)
| ~ p4(sK56) )
& ( ~ p102(sK0)
| p103(sK0)
| r1(sK0,sK56) )
& ( ~ p103(sK0)
| p104(sK0)
| p104(sK55) )
& ( ~ p103(sK0)
| p104(sK0)
| ~ p105(sK55) )
& ( ~ p103(sK0)
| p104(sK0)
| p5(sK55) )
& ( ~ p103(sK0)
| p104(sK0)
| r1(sK0,sK55) )
& ( ~ p103(sK0)
| p104(sK0)
| p104(sK54) )
& ( ~ p103(sK0)
| p104(sK0)
| ~ p105(sK54) )
& ( ~ p103(sK0)
| p104(sK0)
| ~ p5(sK54) )
& ( ~ p103(sK0)
| p104(sK0)
| r1(sK0,sK54) )
& ( ~ p104(sK0)
| p105(sK0)
| p105(sK53) )
& ( ~ p104(sK0)
| p105(sK0)
| ~ p106(sK53) )
& ( ~ p104(sK0)
| p105(sK0)
| p6(sK53) )
& ( ~ p104(sK0)
| p105(sK0)
| r1(sK0,sK53) )
& ( ~ p104(sK0)
| p105(sK0)
| p105(sK52) )
& ( ~ p104(sK0)
| p105(sK0)
| ~ p106(sK52) )
& ( ~ p104(sK0)
| p105(sK0)
| ~ p6(sK52) )
& ( ~ p104(sK0)
| p105(sK0)
| r1(sK0,sK52) )
& ! [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,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] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p2(sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK51(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| p101(sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p102(sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| ~ p2(sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p100(VAR_0)
| p101(VAR_0)
| r1(VAR_0,sK50(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p102(sK49(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| ~ p103(sK49(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| p3(sK49(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p101(VAR_0)
| p102(VAR_0)
| r1(VAR_0,sK49(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(sK48(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK48(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p4(sK48(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK48(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| p103(sK47(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p104(sK47(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| ~ p4(sK47(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p102(VAR_0)
| p103(VAR_0)
| r1(VAR_0,sK47(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p5(sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK46(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| p104(sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p105(sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| ~ p5(sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p103(VAR_0)
| p104(VAR_0)
| r1(VAR_0,sK45(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK44(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK44(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p6(sK44(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK44(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| p105(sK43(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p106(sK43(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| ~ p6(sK43(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0] :
( ~ p104(VAR_0)
| p105(VAR_0)
| r1(VAR_0,sK43(VAR_0))
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p100(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p101(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p102(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p103(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p105(VAR_1)
| p104(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p106(VAR_1)
| p105(VAR_1)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_1)
| ~ p1(VAR_1)
| ~ p100(VAR_2)
| p1(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_1)
| p1(VAR_1)
| ~ p100(VAR_2)
| ~ p1(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_1)
| ~ p2(VAR_1)
| ~ p101(VAR_2)
| p2(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_1)
| p2(VAR_1)
| ~ p101(VAR_2)
| ~ p2(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_1)
| ~ p3(VAR_1)
| ~ p102(VAR_2)
| p3(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_1)
| p3(VAR_1)
| ~ p102(VAR_2)
| ~ p3(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_1)
| ~ p4(VAR_1)
| ~ p103(VAR_2)
| p4(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_1)
| p4(VAR_1)
| ~ p103(VAR_2)
| ~ p4(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_1)
| ~ p5(VAR_1)
| ~ p104(VAR_2)
| p5(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_1)
| p5(VAR_1)
| ~ p104(VAR_2)
| ~ p5(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p105(VAR_1)
| ~ p6(VAR_1)
| ~ p105(VAR_2)
| p6(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p105(VAR_1)
| p6(VAR_1)
| ~ p105(VAR_2)
| ~ p6(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| p101(sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| ~ p102(sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| p2(sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| r1(VAR_1,sK42(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| p101(sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| ~ p102(sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| ~ p2(sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p100(VAR_1)
| p101(VAR_1)
| r1(VAR_1,sK41(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| p102(sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| ~ p103(sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| p3(sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| r1(VAR_1,sK40(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| p102(sK39(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| ~ p103(sK39(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| ~ p3(sK39(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p101(VAR_1)
| p102(VAR_1)
| r1(VAR_1,sK39(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| p103(sK38(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| ~ p104(sK38(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| p4(sK38(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| r1(VAR_1,sK38(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| p103(sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| ~ p104(sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| ~ p4(sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p102(VAR_1)
| p103(VAR_1)
| r1(VAR_1,sK3(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| p104(sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| ~ p105(sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| p5(sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| r1(VAR_1,sK37(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| p104(sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| ~ p105(sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| ~ p5(sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p103(VAR_1)
| p104(VAR_1)
| r1(VAR_1,sK36(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| p105(sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| ~ p106(sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| p6(sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| r1(VAR_1,sK35(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| p105(sK34(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| ~ p106(sK34(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| ~ p6(sK34(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1] :
( ~ p104(VAR_1)
| p105(VAR_1)
| r1(VAR_1,sK34(VAR_0,VAR_1))
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p100(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p101(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p102(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p103(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p105(VAR_2)
| p104(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p106(VAR_2)
| p105(VAR_2)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_2)
| ~ p1(VAR_2)
| ~ p100(VAR_3)
| p1(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_2)
| p1(VAR_2)
| ~ p100(VAR_3)
| ~ p1(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_2)
| ~ p2(VAR_2)
| ~ p101(VAR_3)
| p2(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_2)
| p2(VAR_2)
| ~ p101(VAR_3)
| ~ p2(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_2)
| ~ p3(VAR_2)
| ~ p102(VAR_3)
| p3(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_2)
| p3(VAR_2)
| ~ p102(VAR_3)
| ~ p3(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_2)
| ~ p4(VAR_2)
| ~ p103(VAR_3)
| p4(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_2)
| p4(VAR_2)
| ~ p103(VAR_3)
| ~ p4(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_2)
| ~ p5(VAR_2)
| ~ p104(VAR_3)
| p5(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_2)
| p5(VAR_2)
| ~ p104(VAR_3)
| ~ p5(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p105(VAR_2)
| ~ p6(VAR_2)
| ~ p105(VAR_3)
| p6(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p105(VAR_2)
| p6(VAR_2)
| ~ p105(VAR_3)
| ~ p6(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| p101(sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| ~ p102(sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| p2(sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| r1(VAR_2,sK33(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| p101(sK32(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| ~ p102(sK32(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| ~ p2(sK32(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p100(VAR_2)
| p101(VAR_2)
| r1(VAR_2,sK32(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| p102(sK31(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| ~ p103(sK31(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| p3(sK31(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| r1(VAR_2,sK31(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| p102(sK30(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| ~ p103(sK30(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| ~ p3(sK30(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p101(VAR_2)
| p102(VAR_2)
| r1(VAR_2,sK30(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| p103(sK29(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| ~ p104(sK29(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| p4(sK29(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| r1(VAR_2,sK29(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| p103(sK28(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| ~ p104(sK28(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| ~ p4(sK28(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p102(VAR_2)
| p103(VAR_2)
| r1(VAR_2,sK28(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| p104(sK27(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| ~ p105(sK27(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| p5(sK27(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| r1(VAR_2,sK27(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| p104(sK4(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| ~ p105(sK4(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| ~ p5(sK4(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p103(VAR_2)
| p104(VAR_2)
| r1(VAR_2,sK4(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| p105(sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| ~ p106(sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| p6(sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| r1(VAR_2,sK26(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| p105(sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| ~ p106(sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| ~ p6(sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2] :
( ~ p104(VAR_2)
| p105(VAR_2)
| r1(VAR_2,sK25(VAR_0,VAR_1,VAR_2))
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p100(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p101(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p102(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p103(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p105(VAR_3)
| p104(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p106(VAR_3)
| p105(VAR_3)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_3)
| ~ p1(VAR_3)
| ~ p100(VAR_4)
| p1(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_3)
| p1(VAR_3)
| ~ p100(VAR_4)
| ~ p1(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_3)
| ~ p2(VAR_3)
| ~ p101(VAR_4)
| p2(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_3)
| p2(VAR_3)
| ~ p101(VAR_4)
| ~ p2(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_3)
| ~ p3(VAR_3)
| ~ p102(VAR_4)
| p3(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_3)
| p3(VAR_3)
| ~ p102(VAR_4)
| ~ p3(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_3)
| ~ p4(VAR_3)
| ~ p103(VAR_4)
| p4(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_3)
| p4(VAR_3)
| ~ p103(VAR_4)
| ~ p4(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_3)
| ~ p5(VAR_3)
| ~ p104(VAR_4)
| p5(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_3)
| p5(VAR_3)
| ~ p104(VAR_4)
| ~ p5(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p105(VAR_3)
| ~ p6(VAR_3)
| ~ p105(VAR_4)
| p6(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p105(VAR_3)
| p6(VAR_3)
| ~ p105(VAR_4)
| ~ p6(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| p101(sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| ~ p102(sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| p2(sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| r1(VAR_3,sK24(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| p101(sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| ~ p102(sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| ~ p2(sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p100(VAR_3)
| p101(VAR_3)
| r1(VAR_3,sK23(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| p102(sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| ~ p103(sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| p3(sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| r1(VAR_3,sK22(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| p102(sK21(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| ~ p103(sK21(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| ~ p3(sK21(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p101(VAR_3)
| p102(VAR_3)
| r1(VAR_3,sK21(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| p103(sK20(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| ~ p104(sK20(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| p4(sK20(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| r1(VAR_3,sK20(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| p103(sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| ~ p104(sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| ~ p4(sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p102(VAR_3)
| p103(VAR_3)
| r1(VAR_3,sK19(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| p104(sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| ~ p105(sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| p5(sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| r1(VAR_3,sK18(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| p104(sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| ~ p105(sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| ~ p5(sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p103(VAR_3)
| p104(VAR_3)
| r1(VAR_3,sK17(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| p105(sK16(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| ~ p106(sK16(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| p6(sK16(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| r1(VAR_3,sK16(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| p105(sK5(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| ~ p106(sK5(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| ~ p6(sK5(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3] :
( ~ p104(VAR_3)
| p105(VAR_3)
| r1(VAR_3,sK5(VAR_0,VAR_1,VAR_2,VAR_3))
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p100(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p101(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p102(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p103(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p105(VAR_4)
| p104(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p106(VAR_4)
| p105(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p100(VAR_4)
| ~ p1(VAR_4)
| ~ p100(VAR_5)
| p1(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p100(VAR_4)
| p1(VAR_4)
| ~ p100(VAR_5)
| ~ p1(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p101(VAR_4)
| ~ p2(VAR_4)
| ~ p101(VAR_5)
| p2(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p101(VAR_4)
| p2(VAR_4)
| ~ p101(VAR_5)
| ~ p2(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p102(VAR_4)
| ~ p3(VAR_4)
| ~ p102(VAR_5)
| p3(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p102(VAR_4)
| p3(VAR_4)
| ~ p102(VAR_5)
| ~ p3(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p103(VAR_4)
| ~ p4(VAR_4)
| ~ p103(VAR_5)
| p4(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p103(VAR_4)
| p4(VAR_4)
| ~ p103(VAR_5)
| ~ p4(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p104(VAR_4)
| ~ p5(VAR_4)
| ~ p104(VAR_5)
| p5(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p104(VAR_4)
| p5(VAR_4)
| ~ p104(VAR_5)
| ~ p5(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p105(VAR_4)
| ~ p6(VAR_4)
| ~ p105(VAR_5)
| p6(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( ~ p105(VAR_4)
| p6(VAR_4)
| ~ p105(VAR_5)
| ~ p6(VAR_5)
| ~ r1(VAR_4,VAR_5)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| p101(sK15(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| ~ p102(sK15(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| p2(sK15(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| r1(VAR_4,sK15(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| p101(sK14(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| ~ p102(sK14(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| ~ p2(sK14(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p100(VAR_4)
| p101(VAR_4)
| r1(VAR_4,sK14(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| p102(sK13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| ~ p103(sK13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| p3(sK13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| r1(VAR_4,sK13(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| p102(sK12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| ~ p103(sK12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| ~ p3(sK12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p101(VAR_4)
| p102(VAR_4)
| r1(VAR_4,sK12(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| p103(sK11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| ~ p104(sK11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| p4(sK11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| r1(VAR_4,sK11(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| p103(sK10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| ~ p104(sK10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| ~ p4(sK10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p102(VAR_4)
| p103(VAR_4)
| r1(VAR_4,sK10(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| p104(sK9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| ~ p105(sK9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| p5(sK9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| r1(VAR_4,sK9(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| p104(sK8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| ~ p105(sK8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| ~ p5(sK8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p103(VAR_4)
| p104(VAR_4)
| r1(VAR_4,sK8(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| p105(sK7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| ~ p106(sK7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| p6(sK7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| r1(VAR_4,sK7(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| p105(sK6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| ~ p106(sK6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| ~ p6(sK6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( ~ p104(VAR_4)
| p105(VAR_4)
| r1(VAR_4,sK6(VAR_0,VAR_1,VAR_2,VAR_3,VAR_4))
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) )
& ! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] :
( p3(VAR_4)
| ~ r1(VAR_3,VAR_4)
| ~ r1(VAR_2,VAR_3)
| ~ r1(VAR_1,VAR_2)
| ~ r1(VAR_0,VAR_1)
| ~ r1(sK0,VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_main_neg_sk]) ).
cnf(c_2,negated_conjecture,
p100(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_3,negated_conjecture,
~ p101(sK0),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_24,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| p101(sK1) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_38950,negated_conjecture,
( ~ p100(sK0)
| p101(sK1) ),
inference(resolve,[status(thm)],[c_3,c_24]) ).
cnf(c_25,negated_conjecture,
p101(sK1),
inference(resolve,[status(thm)],[c_2,c_38950]) ).
cnf(c_26,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| ~ p102(sK1) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_38951,negated_conjecture,
( ~ p100(sK0)
| ~ p102(sK1) ),
inference(resolve,[status(thm)],[c_3,c_26]) ).
cnf(c_27,negated_conjecture,
~ p102(sK1),
inference(resolve,[status(thm)],[c_2,c_38951]) ).
cnf(c_30,negated_conjecture,
( ~ p100(sK0)
| p101(sK0)
| r1(sK0,sK1) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_38952,negated_conjecture,
( ~ p100(sK0)
| r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_3,c_30]) ).
cnf(c_31,negated_conjecture,
r1(sK0,sK1),
inference(resolve,[status(thm)],[c_2,c_38952]) ).
cnf(c_83,negated_conjecture,
( ~ p101(A)
| p102(A)
| p102(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_84,negated_conjecture,
( ~ p101(A)
| p102(A)
| ~ p103(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_85,negated_conjecture,
( ~ p101(A)
| p102(A)
| ~ p3(sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_86,negated_conjecture,
( ~ p101(A)
| p102(A)
| r1(A,sK2(A))
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_119,negated_conjecture,
( ~ p102(B)
| p3(B)
| ~ p102(C)
| ~ p3(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_146,negated_conjecture,
( ~ p102(B)
| p103(B)
| p103(sK3(A,B))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_147,negated_conjecture,
( ~ p102(B)
| p103(B)
| ~ p104(sK3(A,B))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_149,negated_conjecture,
( ~ p102(B)
| p103(B)
| r1(B,sK3(A,B))
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_166,negated_conjecture,
( ~ p103(C)
| p102(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_174,negated_conjecture,
( ~ p102(C)
| p3(C)
| ~ p102(D)
| ~ p3(D)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_209,negated_conjecture,
( ~ p103(C)
| p104(C)
| p104(sK4(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_210,negated_conjecture,
( ~ p103(C)
| p104(C)
| ~ p105(sK4(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_212,negated_conjecture,
( ~ p103(C)
| p104(C)
| r1(C,sK4(A,B,C))
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_221,negated_conjecture,
( ~ p103(D)
| p102(D)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_222,negated_conjecture,
( ~ p104(D)
| p103(D)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_229,negated_conjecture,
( ~ p102(D)
| p3(D)
| ~ p102(E)
| ~ p3(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_271,negated_conjecture,
( ~ p104(D)
| p105(D)
| p105(sK5(A,B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_273,negated_conjecture,
( ~ p104(D)
| p105(D)
| r1(D,sK5(A,B,C,D))
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_276,negated_conjecture,
( ~ p103(E)
| p102(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_277,negated_conjecture,
( ~ p104(E)
| p103(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_278,negated_conjecture,
( ~ p105(E)
| p104(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_329,negated_conjecture,
( p3(E)
| ~ r1(D,E)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK0,A) ),
inference(split_conjunct,[status(thm)],[sk_main_neg]) ).
cnf(c_38953,negated_conjecture,
( ~ p101(sK1)
| p102(sK1)
| p102(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_83,c_31]) ).
cnf(c_38954,negated_conjecture,
( ~ p101(sK1)
| p102(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_27,c_38953]) ).
cnf(c_1783,negated_conjecture,
p102(sK2(sK1)),
inference(resolve,[status(thm)],[c_25,c_38954]) ).
cnf(c_38955,negated_conjecture,
( ~ p101(sK1)
| p102(sK1)
| ~ p103(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_84,c_31]) ).
cnf(c_38956,negated_conjecture,
( ~ p101(sK1)
| ~ p103(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_27,c_38955]) ).
cnf(c_1785,negated_conjecture,
~ p103(sK2(sK1)),
inference(resolve,[status(thm)],[c_25,c_38956]) ).
cnf(c_38957,negated_conjecture,
( ~ p101(sK1)
| p102(sK1)
| ~ p3(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_85,c_31]) ).
cnf(c_38958,negated_conjecture,
( ~ p101(sK1)
| ~ p3(sK2(sK1)) ),
inference(resolve,[status(thm)],[c_27,c_38957]) ).
cnf(c_1787,negated_conjecture,
~ p3(sK2(sK1)),
inference(resolve,[status(thm)],[c_25,c_38958]) ).
cnf(c_38959,negated_conjecture,
( ~ p101(sK1)
| p102(sK1)
| r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_86,c_31]) ).
cnf(c_38960,negated_conjecture,
( ~ p101(sK1)
| r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_27,c_38959]) ).
cnf(c_1789,negated_conjecture,
r1(sK1,sK2(sK1)),
inference(resolve,[status(thm)],[c_25,c_38960]) ).
cnf(c_1935,plain,
( ~ p102(B)
| p3(B)
| ~ p102(C)
| ~ p3(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_174,c_31]) ).
cnf(c_2109,plain,
( ~ p103(B)
| p104(B)
| p104(sK4(sK1,A,B))
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_209,c_31]) ).
cnf(c_2121,plain,
( ~ p103(B)
| p104(B)
| r1(B,sK4(sK1,A,B))
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_212,c_31]) ).
cnf(c_2167,plain,
( ~ p102(C)
| p3(C)
| ~ p102(D)
| ~ p3(D)
| ~ r1(C,D)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_229,c_31]) ).
cnf(c_38961,negated_conjecture,
( p3(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_329]) ).
cnf(c_8478,negated_conjecture,
( p3(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38961]) ).
cnf(c_38962,negated_conjecture,
( ~ p105(C)
| p104(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_278]) ).
cnf(c_8629,negated_conjecture,
( ~ p105(C)
| p104(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38962]) ).
cnf(c_38963,negated_conjecture,
( ~ p104(C)
| p103(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_277]) ).
cnf(c_8632,negated_conjecture,
( ~ p104(C)
| p103(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38963]) ).
cnf(c_38964,negated_conjecture,
( ~ p103(C)
| p102(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_276]) ).
cnf(c_8635,negated_conjecture,
( ~ p103(C)
| p102(C)
| ~ r1(B,C)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38964]) ).
cnf(c_38965,negated_conjecture,
( ~ p104(B)
| p105(B)
| r1(B,sK5(sK1,sK2(sK1),A,B))
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_273]) ).
cnf(c_8644,negated_conjecture,
( ~ p104(B)
| p105(B)
| r1(B,sK5(sK1,sK2(sK1),A,B))
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38965]) ).
cnf(c_38966,negated_conjecture,
( ~ p104(B)
| p105(B)
| p105(sK5(sK1,sK2(sK1),A,B))
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_271]) ).
cnf(c_8650,negated_conjecture,
( ~ p104(B)
| p105(B)
| p105(sK5(sK1,sK2(sK1),A,B))
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38966]) ).
cnf(c_38967,negated_conjecture,
( ~ p104(B)
| p103(B)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_222]) ).
cnf(c_8776,negated_conjecture,
( ~ p104(B)
| p103(B)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38967]) ).
cnf(c_38968,negated_conjecture,
( ~ p103(B)
| p102(B)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_221]) ).
cnf(c_8778,negated_conjecture,
( ~ p103(B)
| p102(B)
| ~ r1(A,B)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38968]) ).
cnf(c_38969,negated_conjecture,
( ~ p103(A)
| p102(A)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_166]) ).
cnf(c_8872,negated_conjecture,
( ~ p103(A)
| p102(A)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38969]) ).
cnf(c_38970,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| r1(sK2(sK1),sK3(sK1,sK2(sK1)))
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_149]) ).
cnf(c_38971,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_31,c_38970]) ).
cnf(c_38972,negated_conjecture,
( ~ p102(sK2(sK1))
| r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_1785,c_38971]) ).
cnf(c_8883,negated_conjecture,
r1(sK2(sK1),sK3(sK1,sK2(sK1))),
inference(resolve,[status(thm)],[c_1783,c_38972]) ).
cnf(c_38973,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| ~ p104(sK3(sK1,sK2(sK1)))
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_147]) ).
cnf(c_38974,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| ~ p104(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_31,c_38973]) ).
cnf(c_38975,negated_conjecture,
( ~ p102(sK2(sK1))
| ~ p104(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_1785,c_38974]) ).
cnf(c_8885,negated_conjecture,
~ p104(sK3(sK1,sK2(sK1))),
inference(resolve,[status(thm)],[c_1783,c_38975]) ).
cnf(c_38976,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| p103(sK3(sK1,sK2(sK1)))
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_146]) ).
cnf(c_38977,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK2(sK1))
| p103(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_31,c_38976]) ).
cnf(c_38978,negated_conjecture,
( ~ p102(sK2(sK1))
| p103(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_1785,c_38977]) ).
cnf(c_8886,negated_conjecture,
p103(sK3(sK1,sK2(sK1))),
inference(resolve,[status(thm)],[c_1783,c_38978]) ).
cnf(c_38979,negated_conjecture,
( ~ p102(sK2(sK1))
| p3(sK2(sK1))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK2(sK1),A)
| ~ r1(sK0,sK1) ),
inference(resolve,[status(thm)],[c_1789,c_119]) ).
cnf(c_38980,negated_conjecture,
( ~ p102(sK2(sK1))
| p3(sK2(sK1))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_31,c_38979]) ).
cnf(c_38981,negated_conjecture,
( ~ p102(sK2(sK1))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_1787,c_38980]) ).
cnf(c_8903,negated_conjecture,
( ~ p102(A)
| ~ p3(A)
| ~ r1(sK2(sK1),A) ),
inference(resolve,[status(thm)],[c_1783,c_38981]) ).
cnf(c_38982,negated_conjecture,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK3(sK1,sK2(sK1)))
| ~ p105(sK4(A,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(A,sK2(sK1))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_8883,c_210]) ).
cnf(c_38983,negated_conjecture,
( ~ p103(sK3(sK1,sK2(sK1)))
| ~ p105(sK4(A,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(A,sK2(sK1))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_8885,c_38982]) ).
cnf(c_10693,negated_conjecture,
( ~ p105(sK4(A,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(A,sK2(sK1))
| ~ r1(sK0,A) ),
inference(resolve,[status(thm)],[c_8886,c_38983]) ).
cnf(c_11313,plain,
( ~ p102(sK3(sK1,sK2(sK1)))
| ~ p3(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8903,c_8883]) ).
cnf(c_38984,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p102(sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8872,c_8883]) ).
cnf(c_11387,plain,
p102(sK3(sK1,sK2(sK1))),
inference(resolve,[status(thm)],[c_8886,c_38984]) ).
cnf(c_11392,plain,
~ p3(sK3(sK1,sK2(sK1))),
inference(resolve,[status(thm)],[c_11387,c_11313]) ).
cnf(c_38985,plain,
( ~ p102(sK3(sK1,sK2(sK1)))
| p3(sK3(sK1,sK2(sK1)))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK3(sK1,sK2(sK1)),A)
| ~ r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_1935,c_8883]) ).
cnf(c_38986,plain,
( ~ p102(sK3(sK1,sK2(sK1)))
| p3(sK3(sK1,sK2(sK1)))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK3(sK1,sK2(sK1)),A) ),
inference(resolve,[status(thm)],[c_1789,c_38985]) ).
cnf(c_38987,plain,
( ~ p102(sK3(sK1,sK2(sK1)))
| ~ p102(A)
| ~ p3(A)
| ~ r1(sK3(sK1,sK2(sK1)),A) ),
inference(resolve,[status(thm)],[c_11392,c_38986]) ).
cnf(c_11635,plain,
( ~ p102(A)
| ~ p3(A)
| ~ r1(sK3(sK1,sK2(sK1)),A) ),
inference(resolve,[status(thm)],[c_11387,c_38987]) ).
cnf(c_11669,plain,
( ~ p104(A)
| p103(A)
| ~ r1(sK3(sK1,sK2(sK1)),A) ),
inference(resolve,[status(thm)],[c_8776,c_8883]) ).
cnf(c_11792,plain,
( p3(B)
| ~ r1(A,B)
| ~ r1(sK3(sK1,sK2(sK1)),A) ),
inference(resolve,[status(thm)],[c_8478,c_8883]) ).
cnf(c_38988,negated_conjecture,
( ~ p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_10693,c_31]) ).
cnf(c_11901,negated_conjecture,
~ p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_1789,c_38988]) ).
cnf(c_38989,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK3(sK1,sK2(sK1)))
| p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_2109,c_8883]) ).
cnf(c_38990,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK3(sK1,sK2(sK1)))
| p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_1789,c_38989]) ).
cnf(c_38991,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_8885,c_38990]) ).
cnf(c_12431,plain,
p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_8886,c_38991]) ).
cnf(c_38992,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK3(sK1,sK2(sK1)))
| r1(sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(sK1,sK2(sK1)) ),
inference(resolve,[status(thm)],[c_2121,c_8883]) ).
cnf(c_38993,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| p104(sK3(sK1,sK2(sK1)))
| r1(sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_1789,c_38992]) ).
cnf(c_38994,plain,
( ~ p103(sK3(sK1,sK2(sK1)))
| r1(sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_8885,c_38993]) ).
cnf(c_13174,plain,
r1(sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_8886,c_38994]) ).
cnf(c_13311,plain,
( p3(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A) ),
inference(resolve,[status(thm)],[c_13174,c_11792]) ).
cnf(c_38995,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p103(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_13174,c_11669]) ).
cnf(c_13322,plain,
p103(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_12431,c_38995]) ).
cnf(c_13324,plain,
( ~ p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ p3(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_13174,c_11635]) ).
cnf(c_38996,plain,
( ~ p103(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_13174,c_8778]) ).
cnf(c_38997,plain,
( ~ p103(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))) ),
inference(resolve,[status(thm)],[c_8883,c_38996]) ).
cnf(c_13343,plain,
p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_13322,c_38997]) ).
cnf(c_13423,plain,
~ p3(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))),
inference(resolve,[status(thm)],[c_13343,c_13324]) ).
cnf(c_38998,plain,
( ~ p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p3(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ p102(B)
| ~ p3(B)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),B)
| ~ r1(A,sK3(sK1,sK2(sK1)))
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_2167,c_13174]) ).
cnf(c_38999,plain,
( ~ p102(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| ~ p102(B)
| ~ p3(B)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),B)
| ~ r1(A,sK3(sK1,sK2(sK1)))
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_13423,c_38998]) ).
cnf(c_14785,plain,
( ~ p102(B)
| ~ p3(B)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),B)
| ~ r1(A,sK3(sK1,sK2(sK1)))
| ~ r1(sK1,A) ),
inference(resolve,[status(thm)],[c_13343,c_38999]) ).
cnf(c_39000,plain,
( ~ p105(A)
| p104(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A)
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8629,c_13174]) ).
cnf(c_14985,plain,
( ~ p105(A)
| p104(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A) ),
inference(resolve,[status(thm)],[c_8883,c_39000]) ).
cnf(c_39001,plain,
( ~ p104(A)
| p103(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A)
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8632,c_13174]) ).
cnf(c_14995,plain,
( ~ p104(A)
| p103(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A) ),
inference(resolve,[status(thm)],[c_8883,c_39001]) ).
cnf(c_39002,plain,
( ~ p103(A)
| p102(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A)
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8635,c_13174]) ).
cnf(c_15005,plain,
( ~ p103(A)
| p102(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A) ),
inference(resolve,[status(thm)],[c_8883,c_39002]) ).
cnf(c_39003,plain,
( ~ p102(A)
| ~ p3(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A)
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_14785,c_1789]) ).
cnf(c_16437,plain,
( ~ p102(A)
| ~ p3(A)
| ~ r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),A) ),
inference(resolve,[status(thm)],[c_8883,c_39003]) ).
cnf(c_39004,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8650,c_13174]) ).
cnf(c_39005,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_8883,c_39004]) ).
cnf(c_39006,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_11901,c_39005]) ).
cnf(c_19097,plain,
p105(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_12431,c_39006]) ).
cnf(c_39007,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| ~ r1(sK2(sK1),sK3(sK1,sK2(sK1))) ),
inference(resolve,[status(thm)],[c_8644,c_13174]) ).
cnf(c_39008,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| p105(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_8883,c_39007]) ).
cnf(c_39009,plain,
( ~ p104(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))
| r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_11901,c_39008]) ).
cnf(c_21923,plain,
r1(sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))),sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_12431,c_39009]) ).
cnf(c_38605,plain,
( ~ p102(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| ~ p3(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_21923,c_16437]) ).
cnf(c_38617,plain,
( ~ p103(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| p102(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_21923,c_15005]) ).
cnf(c_38618,plain,
( ~ p104(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| p103(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_21923,c_14995]) ).
cnf(c_39010,plain,
( ~ p105(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1)))))
| p104(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))) ),
inference(resolve,[status(thm)],[c_21923,c_14985]) ).
cnf(c_38619,plain,
p104(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_19097,c_39010]) ).
cnf(c_38677,plain,
p3(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_21923,c_13311]) ).
cnf(c_38939,plain,
p103(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_38619,c_38618]) ).
cnf(c_38940,plain,
~ p102(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_38677,c_38605]) ).
cnf(c_39011,plain,
~ p103(sK5(sK1,sK2(sK1),sK3(sK1,sK2(sK1)),sK4(sK1,sK2(sK1),sK3(sK1,sK2(sK1))))),
inference(resolve,[status(thm)],[c_38940,c_38617]) ).
cnf(c_38949,plain,
$false,
inference(resolve,[status(thm)],[c_38939,c_39011]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.52 % Computer : n003.cluster.edu
% 0.10/0.52 % Model : x86_64 x86_64
% 0.10/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.52 % Memory : 8046.5625MB
% 0.10/0.52 % OS : Linux 6.8.0-71-generic
% 0.10/0.52 % CPULimit : 300
% 0.10/0.52 % WCLimit : 300
% 0.10/0.52 % DateTime : Fri Sep 25 22:50:41 UTC 2026
% 0.10/0.52 % CPUTime :
% 0.10/0.52 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.52 % Process 1330601 was started by sandbox on n003,
% 0.10/0.52 % Fri Sep 25 22:50:41 2026
% 0.10/0.52 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.31/0.72
% 0.31/0.72 % From the command line: assign(max_seconds, 300).
% 255.20/41.02
% 255.20/41.02 % given #500 (I,wt=19): 539 -r1(c1,A) | -r1(A,A) | -r1(A,B) | -p3(f17(A,A,A,B)) | p102(B) | -p101(B). [factor(250,b,c)].
% 255.20/41.02
% 255.20/41.02 % given #1000 (I,wt=23): 1039 -r1(c1,A) | -r1(A,B) | -r1(B,C) | -r1(C,C) | p105(f1(A,B,C,C,C)) | p105(C) | -p104(C). [factor(326,d,e)].
% 255.20/41.02
% 255.20/41.02 % given #1500 (I,wt=17): 1539 -r1(c1,c1) | -r1(c1,A) | p104(f4(c1,c1,c1,c1,A)) | p104(A) | -p103(A). [factor(920,a,c),merge(b)].
% 255.20/41.02
% 255.20/41.02 % given #2000 (T,wt=5): 11358 p102(f35(c11,f48(c11))). [resolve(8105,a,8116,a),unit_del(b,8119)].
% 255.20/41.02
% 255.20/41.02 % given #2500 (F,wt=6): 11569 -r1(f35(c11,f48(c11)),c11). [resolve(11554,a,8116,a)].
% 255.20/41.02
% 255.20/41.02 % given #3000 (A,wt=15): 1973 -r1(c10,A) | -r1(A,B) | -p2(f29(c10,A,B)) | p101(B) | -p100(B). [resolve(187,a,31,a)].
% 255.20/41.02
% 255.20/41.02 % given #3500 (T,wt=13): 5102 -r1(c1,c1) | -r1(c11,c1) | p102(f7(c1,c1,c11,c1,c11)). [factor(5100,a,b)].
% 255.20/41.02
% 255.20/41.02 % given #4000 (F,wt=9): 13879 -p3(f23(c11,f47(c11),f36(c11,f47(c11)))). [back_unit_del(13777),unit_del(b,13793)].
% 255.20/41.02
% 255.20/41.02 % given #4500 (T,wt=14): 8197 -r1(c1,A) | -r1(A,c11) | -r1(f48(c11),A) | p2(A) | -p101(A). [factor(7989,b,d),unit_del(d,21),unit_del(e,17)].
% 255.20/41.02
% 255.20/41.02 % given #5000 (F,wt=19): 12211 -r1(c1,A) | -r1(A,f35(c10,f47(c10))) | -r1(f24(c10,f47(c10),f35(c10,f47(c10))),A). [resolve(11962,a,1066,c),unit_del(d,11392)].
% 255.20/41.02
% 255.20/41.02 % given #5500 (T,wt=15): 9549 -r1(f47(c11),A) | -r1(A,B) | p6(B) | -p105(B) | -p6(A) | -p105(A). [resolve(1790,a,179,b),unit_del(a,23)].
% 255.20/41.02
% 255.20/41.02 % given #6000 (F,wt=20): 13831 -r1(c10,f36(c11,f47(c11))) | -r1(f23(c11,f47(c11),f36(c11,f47(c11))),A) | -p5(A) | -p104(A). [resolve(13179,a,1943,b),unit_del(e,11938),unit_del(f,12436)].
% 255.20/41.02
% 255.20/41.02 % given #6500 (T,wt=16): 4861 -r1(c10,c1) | -r1(c10,A) | p103(f15(c10,c1,c10,A)) | p103(A) | -p102(A). [resolve(573,a,31,a)].
% 255.20/41.02
% 255.20/41.02 % given #7000 (F,wt=21): 16496 -r1(f48(c10),f35(c11,f47(c11))) | -r1(f24(c11,f47(c11),f35(c11,f47(c11))),A) | -p4(A) | -p103(A). [resolve(14854,a,1781,a)].
% 255.20/41.02
% 255.20/41.02 % given #7500 (A,wt=20): 2795 -r1(c10,A) | -r1(A,B) | -r1(B,C) | r1(C,f11(c10,A,B,C)) | p105(C) | -p104(C). [resolve(273,a,31,a)].
% 255.20/41.02
% 255.20/41.02 % given #8000 (T,wt=17): 8179 -r1(c11,A) | -r1(A,c1) | -r1(f48(c11),B) | p1(B) | -p100(B) | -p1(f48(c11)). [factor(7849,a,d),unit_del(a,23),unit_del(h,8147)].
% 255.20/41.02
% 255.20/41.02 % given #8500 (F,wt=24): 18319 -r1(f48(c11),f36(c10,f48(c10))) | -p6(f11(c11,f48(c11),f36(c10,f48(c10)),f24(c10,f48(c10),f36(c10,f48(c10))))). [resolve(17532,a,1782,a)].
% 255.20/41.02
% 255.20/41.02 % given #9000 (T,wt=17): 18868 p105(f12(c10,f48(c10),f36(c10,f48(c10)),f23(c10,f48(c10),f36(c10,f48(c10))))). [resolve(6426,b,13177,a),unit_del(a,6657),unit_del(c,11883),unit_del(d,12434)].
% 255.20/41.02
% 255.20/41.02 % given #9500 (F,wt=29): 17595 -r1(c1,f47(c11)) | -r1(f36(c11,f47(c11)),A) | -r1(A,f48(c11)) | -p5(f3(f47(c11),f36(c11,f47(c11)),A,f48(c11),f36(c11,f48(c11)))). [resolve(10463,b,9588,a)].
% 255.20/41.02
% 255.20/41.02 % given #10000 (T,wt=18): 14146 -r1(c1,A) | -r1(A,f36(c11,f48(c11))) | p101(f23(c11,f48(c11),f36(c11,f48(c11)))). [resolve(13183,a,165,c),unit_del(d,14066)].
% 255.20/41.02
% 255.20/41.02 % given #10500 (F,wt=25): 21498 -r1(c11,A) | -r1(A,f48(c11)) | -p6(f1(c11,A,f48(c11),f35(c11,f48(c11)),f23(c11,f48(c11),f35(c11,f48(c11))))). [resolve(21480,a,23,a)].
% 255.20/41.02
% 255.20/41.02 % given #11000 (T,wt=19): 7499 -r1(f48(c11),c1) | -r1(c11,A) | p2(f10(c11,f48(c11),c1,c11,A)) | p101(A) | -p100(A). [resolve(1782,a,702,b),unit_del(a,23)].
% 255.20/41.02
% 255.20/41.02 % given #11500 (F,wt=33): 20243 -r1(c1,f48(c11)) | -r1(f36(c11,f48(c11)),f48(c10)) | -p6(f1(f48(c11),f36(c11,f48(c11)),f48(c10),f35(c10,f48(c10)),f24(c10,f48(c10),f35(c10,f48(c10))))). [resolve(20204,b,8120,a)].
% 255.20/41.02
% 255.20/41.02 % given #12000 (A,wt=21): 3770 -r1(c1,A) | -r1(A,c1) | -r1(c11,c1) | r1(A,f7(A,c1,c11,c1,A)) | p102(A) | -p101(A). [factor(3740,a,d)].
% 255.20/41.02
% 255.20/41.02 % given #12500 (T,wt=20): 4539 -r1(c1,c1) | -r1(c10,A) | -r1(A,c10) | p6(f2(c1,c10,A,c10,A)) | p105(A) | -p104(A). [factor(4519,b,d)].
% 255.20/41.02
% 255.20/41.02 % given #13000 (F,wt=37): 16158 -r1(c1,f36(c10,f48(c10))) | -r1(f24(c10,f48(c10),f36(c10,f48(c10))),f47(c11)) | -p105(f14(f36(c10,f48(c10)),f24(c10,f48(c10),f36(c10,f48(c10))),f47(c11),f35(c11,f47(c11)))). [resolve(11050,b,11965,a)].
% 255.20/41.02
% 255.20/41.02 % given #13500 (T,wt=20): 9809 -r1(c1,A) | -r1(A,f48(c10)) | r1(f35(c10,f48(c10)),f24(A,f48(c10),f35(c10,f48(c10)))). [resolve(6653,a,208,c),unit_del(d,6655),unit_del(e,6656)].
% 255.20/41.02
% 255.20/41.02 % given #14000 (F,wt=38): 16847 -r1(c10,f35(c11,f47(c11))) | -r1(f23(c11,f47(c11),f35(c11,f47(c11))),f48(c10)) | -p105(f4(c10,f35(c11,f47(c11)),f23(c11,f47(c11),f35(c11,f47(c11))),f48(c10),f35(c10,f48(c10)))). [resolve(16783,b,13180,a)].
% 255.20/41.02
% 255.20/41.02 % given #14500 (T,wt=20): 14085 -r1(c10,f36(c11,f48(c11))) | -r1(f23(c11,f48(c11),f36(c11,f48(c11))),A) | p102(A) | -p103(A). [resolve(13183,a,2153,b)].
% 255.20/41.02
% 255.20/41.02 % given #15000 (F,wt=41): 16690 -r1(c1,f36(c10,f47(c10))) | -r1(f24(c10,f47(c10),f36(c10,f47(c10))),A) | -r1(A,f48(c10)) | -p105(f3(f36(c10,f47(c10)),f24(c10,f47(c10),f36(c10,f47(c10))),A,f48(c10),f35(c10,f48(c10)))). [resolve(9753,b,11961,a)].
% 255.20/41.02
% 255.20/41.02 % given #15500 (T,wt=21): 6051 -r1(f48(c10),c10) | -r1(f48(c10),A) | -p102(f10(c10,f48(c10),c10,f48(c10),A)) | p101(A) | -p100(A). [resolve(1781,a,695,b),unit_del(a,31)].
% 255.20/41.02
% 255.20/41.02 % given #16000 (F,wt=45): 18641 -r1(c1,f36(c10,f47(c10))) | -r1(f24(c10,f47(c10),f36(c10,f47(c10))),f36(c11,f48(c11))) | -p6(f11(f36(c10,f47(c10)),f24(c10,f47(c10),f36(c10,f47(c10))),f36(c11,f48(c11)),f24(c11,f48(c11),f36(c11,f48(c11))))). [resolve(13001,b,11961,a)].
% 255.20/41.02
% 255.20/41.02 % given #16500 (A,wt=23): 5882 -r1(f48(c10),f48(c10)) | -r1(f48(c10),A) | p3(f8(c10,f48(c10),f48(c10),f48(c10),A)) | p102(A) | -p101(A). [resolve(1781,a,787,b),unit_del(a,31)].
% 255.20/41.02
% 255.20/41.02 % given #17000 (T,wt=21): 13753 -r1(c11,f36(c10,f48(c10))) | p6(f22(c11,f36(c10,f48(c10)),f23(c10,f48(c10),f36(c10,f48(c10))))). [resolve(2130,b,13177,a),unit_del(c,11883),unit_del(d,12434)].
% 255.20/41.02
% 255.20/41.02 % given #17500 (F,wt=47): 18168 -r1(c1,f24(c11,f48(c11),f36(c11,f48(c11)))) | -r1(f24(c11,f48(c11),f36(c11,f48(c11))),f48(c11)) | -p104(f5(f24(c11,f48(c11),f36(c11,f48(c11))),f48(c11),f36(c11,f48(c11)),f24(c11,f48(c11),f36(c11,f48(c11))),f48(c11))). [resolve(10433,c,12123,a)].
% 255.20/41.02
% 255.20/41.02 % given #18000 (T,wt=21): 22975 -r1(c11,A) | -r1(A,B) | -r1(B,f48(c11)) | p104(f4(c11,A,B,f48(c11),f36(c11,f48(c11)))). [resolve(4140,d,8120,a),unit_del(e,8122),unit_del(f,8123)].
% 255.20/41.02
% 255.20/41.02 % given #18500 (F,wt=49): 21106 -r1(c1,f36(c11,f48(c11))) | -r1(f24(c11,f48(c11),f36(c11,f48(c11))),A) | -r1(A,f35(c10,f48(c10))) | -p6(f1(f36(c11,f48(c11)),f24(c11,f48(c11),f36(c11,f48(c11))),A,f35(c10,f48(c10)),f23(c10,f48(c10),f35(c10,f48(c10))))). [resolve(13717,b,12123,a)].
% 255.20/41.02
% 255.20/41.02 % given #19000 (T,wt=22): 9378 -r1(c1,A) | -r1(A,c11) | -r1(f47(c11),B) | r1(B,f15(A,c11,f47(c11),B)) | p103(B) | -p102(B). [resolve(1790,a,259,c)].
% 255.20/41.02
% 255.20/41.02 % given #19500 (T,wt=23): 12568 -r1(c1,A) | -r1(A,f35(c10,f48(c10))) | -r1(f24(c10,f48(c10),f35(c10,f48(c10))),B) | p101(B) | -p102(B). [resolve(11966,a,220,c)].
% 255.20/41.02
% 255.20/41.02 % given #20000 (T,wt=24): 20595 -r1(c1,f48(c11)) | -r1(f36(c11,f48(c11)),A) | -r1(A,c1) | p102(f7(f48(c11),f36(c11,f48(c11)),A,c1,c10)). [resolve(3539,b,8120,a)].
% 255.20/41.02
% 255.20/41.02 % given #20500 (F,wt=21): 31233 -r1(c1,f48(c10)) | -p5(f11(c10,f48(c10),f36(c10,f48(c10)),f23(c10,f48(c10),f36(c10,f48(c10))))). [resolve(21568,a,10092,c),unit_del(b,13177),unit_del(d,31044),unit_del(e,11881),unit_del(f,12434)].
% 255.20/41.02
% 255.20/41.02 % given #21000 (T,wt=23): 36842 -r1(c10,f35(c11,f48(c11))) | p103(f12(c11,f48(c11),f35(c11,f48(c11)),f23(c11,f48(c11),f35(c11,f48(c11))))). [resolve(21885,a,14247,b),unit_del(c,36811)].
% 255.20/41.02
% 255.20/41.02 % SZS status Theorem for theBenchmark
% 255.20/41.02
% 255.20/41.02 % Proof 1 at 26.81 (+ 5.49) seconds.
% 255.20/41.02 % Length of proof is 82.
% 255.20/41.02 % Level of proof is 14.
% 255.20/41.02 % Maximum clause weight is 34.000.
% 255.20/41.02 % Given clauses 21132.
% 255.20/41.02
% 255.20/41.02 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------