%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 01:08:05 PM UTC 2026
% Result : Theorem 75.49s 10.30s
% Output : CNFRefutation 75.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 23
% Syntax : Number of formulae : 153 ( 5 unt; 22 def)
% Number of atoms : 3596 ( 0 equ)
% Maximal formula atoms : 719 ( 23 avg)
% Number of connectives : 6119 (2676 ~;2083 |;1338 &)
% ( 22 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 36 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 37 ( 36 usr; 23 prp; 0-2 aty)
% Number of functors : 61 ( 61 usr; 11 con; 0-5 aty)
% Number of variables : 713 ( 650 !; 63 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,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('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,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(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,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)
| ! [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(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,plain,
( p100(sK0_skl)
& ~ p101(sK0_skl)
& ( ~ p101(sK0_skl)
| p100(sK0_skl) )
& ( ~ p102(sK0_skl)
| p101(sK0_skl) )
& ( ~ p103(sK0_skl)
| p102(sK0_skl) )
& ( ~ p104(sK0_skl)
| p103(sK0_skl) )
& ( ~ p105(sK0_skl)
| p104(sK0_skl) )
& ( ~ p106(sK0_skl)
| p105(sK0_skl) )
& ( ~ p100(sK0_skl)
| ( ( ~ p1(sK0_skl)
| ! [Y] :
( ~ p100(Y)
| p1(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p1(sK0_skl)
| ! [Y] :
( ~ p100(Y)
| ~ p1(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p101(sK0_skl)
| ( ( ~ p2(sK0_skl)
| ! [Y] :
( ~ p101(Y)
| p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p2(sK0_skl)
| ! [Y] :
( ~ p101(Y)
| ~ p2(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p102(sK0_skl)
| ( ( ~ p3(sK0_skl)
| ! [Y] :
( ~ p102(Y)
| p3(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p3(sK0_skl)
| ! [Y] :
( ~ p102(Y)
| ~ p3(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p103(sK0_skl)
| ( ( ~ p4(sK0_skl)
| ! [Y] :
( ~ p103(Y)
| p4(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p4(sK0_skl)
| ! [Y] :
( ~ p103(Y)
| ~ p4(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p104(sK0_skl)
| ( ( ~ p5(sK0_skl)
| ! [Y] :
( ~ p104(Y)
| p5(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p5(sK0_skl)
| ! [Y] :
( ~ p104(Y)
| ~ p5(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p105(sK0_skl)
| ( ( ~ p6(sK0_skl)
| ! [Y] :
( ~ p105(Y)
| p6(Y)
| ~ r1(sK0_skl,Y) ) )
& ( p6(sK0_skl)
| ! [Y] :
( ~ p105(Y)
| ~ p6(Y)
| ~ r1(sK0_skl,Y) ) ) ) )
& ( ~ p100(sK0_skl)
| p101(sK0_skl)
| ( p101(sK60_skl)
& ~ p102(sK60_skl)
& p2(sK60_skl)
& r1(sK0_skl,sK60_skl)
& p101(sK59_skl)
& ~ p102(sK59_skl)
& ~ p2(sK59_skl)
& r1(sK0_skl,sK59_skl) ) )
& ( ~ p101(sK0_skl)
| p102(sK0_skl)
| ( p102(sK58_skl)
& ~ p103(sK58_skl)
& p3(sK58_skl)
& r1(sK0_skl,sK58_skl)
& p102(sK57_skl)
& ~ p103(sK57_skl)
& ~ p3(sK57_skl)
& r1(sK0_skl,sK57_skl) ) )
& ( ~ p102(sK0_skl)
| p103(sK0_skl)
| ( p103(sK56_skl)
& ~ p104(sK56_skl)
& p4(sK56_skl)
& r1(sK0_skl,sK56_skl)
& p103(sK55_skl)
& ~ p104(sK55_skl)
& ~ p4(sK55_skl)
& r1(sK0_skl,sK55_skl) ) )
& ( ~ p103(sK0_skl)
| p104(sK0_skl)
| ( p104(sK54_skl)
& ~ p105(sK54_skl)
& p5(sK54_skl)
& r1(sK0_skl,sK54_skl)
& p104(sK53_skl)
& ~ p105(sK53_skl)
& ~ p5(sK53_skl)
& r1(sK0_skl,sK53_skl) ) )
& ( ~ p104(sK0_skl)
| p105(sK0_skl)
| ( p105(sK52_skl)
& ~ p106(sK52_skl)
& p6(sK52_skl)
& r1(sK0_skl,sK52_skl)
& p105(sK51_skl)
& ~ p106(sK51_skl)
& ~ p6(sK51_skl)
& r1(sK0_skl,sK51_skl) ) )
& ! [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)
| ( p101(sK50_skl(Y))
& ~ p102(sK50_skl(Y))
& p2(sK50_skl(Y))
& r1(Y,sK50_skl(Y))
& p101(sK49_skl(Y))
& ~ p102(sK49_skl(Y))
& ~ p2(sK49_skl(Y))
& r1(Y,sK49_skl(Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK48_skl(Y))
& ~ p103(sK48_skl(Y))
& p3(sK48_skl(Y))
& r1(Y,sK48_skl(Y))
& p102(sK47_skl(Y))
& ~ p103(sK47_skl(Y))
& ~ p3(sK47_skl(Y))
& r1(Y,sK47_skl(Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK46_skl(Y))
& ~ p104(sK46_skl(Y))
& p4(sK46_skl(Y))
& r1(Y,sK46_skl(Y))
& p103(sK45_skl(Y))
& ~ p104(sK45_skl(Y))
& ~ p4(sK45_skl(Y))
& r1(Y,sK45_skl(Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK44_skl(Y))
& ~ p105(sK44_skl(Y))
& p5(sK44_skl(Y))
& r1(Y,sK44_skl(Y))
& p104(sK43_skl(Y))
& ~ p105(sK43_skl(Y))
& ~ p5(sK43_skl(Y))
& r1(Y,sK43_skl(Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK42_skl(Y))
& ~ p106(sK42_skl(Y))
& p6(sK42_skl(Y))
& r1(Y,sK42_skl(Y))
& p105(sK41_skl(Y))
& ~ p106(sK41_skl(Y))
& ~ p6(sK41_skl(Y))
& r1(Y,sK41_skl(Y)) ) ) )
| ~ r1(sK0_skl,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)
| ( p101(sK40_skl(X,Y))
& ~ p102(sK40_skl(X,Y))
& p2(sK40_skl(X,Y))
& r1(X,sK40_skl(X,Y))
& p101(sK39_skl(X,Y))
& ~ p102(sK39_skl(X,Y))
& ~ p2(sK39_skl(X,Y))
& r1(X,sK39_skl(X,Y)) ) )
& ( ~ p101(X)
| p102(X)
| ( p102(sK38_skl(X,Y))
& ~ p103(sK38_skl(X,Y))
& p3(sK38_skl(X,Y))
& r1(X,sK38_skl(X,Y))
& p102(sK37_skl(X,Y))
& ~ p103(sK37_skl(X,Y))
& ~ p3(sK37_skl(X,Y))
& r1(X,sK37_skl(X,Y)) ) )
& ( ~ p102(X)
| p103(X)
| ( p103(sK36_skl(X,Y))
& ~ p104(sK36_skl(X,Y))
& p4(sK36_skl(X,Y))
& r1(X,sK36_skl(X,Y))
& p103(sK35_skl(X,Y))
& ~ p104(sK35_skl(X,Y))
& ~ p4(sK35_skl(X,Y))
& r1(X,sK35_skl(X,Y)) ) )
& ( ~ p103(X)
| p104(X)
| ( p104(sK34_skl(X,Y))
& ~ p105(sK34_skl(X,Y))
& p5(sK34_skl(X,Y))
& r1(X,sK34_skl(X,Y))
& p104(sK33_skl(X,Y))
& ~ p105(sK33_skl(X,Y))
& ~ p5(sK33_skl(X,Y))
& r1(X,sK33_skl(X,Y)) ) )
& ( ~ p104(X)
| p105(X)
| ( p105(sK32_skl(X,Y))
& ~ p106(sK32_skl(X,Y))
& p6(sK32_skl(X,Y))
& r1(X,sK32_skl(X,Y))
& p105(sK31_skl(X,Y))
& ~ p106(sK31_skl(X,Y))
& ~ p6(sK31_skl(X,Y))
& r1(X,sK31_skl(X,Y)) ) ) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,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)
| ( p101(sK30_skl(Y,X,Y))
& ~ p102(sK30_skl(Y,X,Y))
& p2(sK30_skl(Y,X,Y))
& r1(Y,sK30_skl(Y,X,Y))
& p101(sK29_skl(Y,X,Y))
& ~ p102(sK29_skl(Y,X,Y))
& ~ p2(sK29_skl(Y,X,Y))
& r1(Y,sK29_skl(Y,X,Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK28_skl(Y,X,Y))
& ~ p103(sK28_skl(Y,X,Y))
& p3(sK28_skl(Y,X,Y))
& r1(Y,sK28_skl(Y,X,Y))
& p102(sK27_skl(Y,X,Y))
& ~ p103(sK27_skl(Y,X,Y))
& ~ p3(sK27_skl(Y,X,Y))
& r1(Y,sK27_skl(Y,X,Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK26_skl(Y,X,Y))
& ~ p104(sK26_skl(Y,X,Y))
& p4(sK26_skl(Y,X,Y))
& r1(Y,sK26_skl(Y,X,Y))
& p103(sK25_skl(Y,X,Y))
& ~ p104(sK25_skl(Y,X,Y))
& ~ p4(sK25_skl(Y,X,Y))
& r1(Y,sK25_skl(Y,X,Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK24_skl(Y,X,Y))
& ~ p105(sK24_skl(Y,X,Y))
& p5(sK24_skl(Y,X,Y))
& r1(Y,sK24_skl(Y,X,Y))
& p104(sK23_skl(Y,X,Y))
& ~ p105(sK23_skl(Y,X,Y))
& ~ p5(sK23_skl(Y,X,Y))
& r1(Y,sK23_skl(Y,X,Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK22_skl(Y,X,Y))
& ~ p106(sK22_skl(Y,X,Y))
& p6(sK22_skl(Y,X,Y))
& r1(Y,sK22_skl(Y,X,Y))
& p105(sK21_skl(Y,X,Y))
& ~ p106(sK21_skl(Y,X,Y))
& ~ p6(sK21_skl(Y,X,Y))
& r1(Y,sK21_skl(Y,X,Y)) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,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)
| ( p101(sK20_skl(X,Y,X,Y))
& ~ p102(sK20_skl(X,Y,X,Y))
& p2(sK20_skl(X,Y,X,Y))
& r1(X,sK20_skl(X,Y,X,Y))
& p101(sK19_skl(X,Y,X,Y))
& ~ p102(sK19_skl(X,Y,X,Y))
& ~ p2(sK19_skl(X,Y,X,Y))
& r1(X,sK19_skl(X,Y,X,Y)) ) )
& ( ~ p101(X)
| p102(X)
| ( p102(sK18_skl(X,Y,X,Y))
& ~ p103(sK18_skl(X,Y,X,Y))
& p3(sK18_skl(X,Y,X,Y))
& r1(X,sK18_skl(X,Y,X,Y))
& p102(sK17_skl(X,Y,X,Y))
& ~ p103(sK17_skl(X,Y,X,Y))
& ~ p3(sK17_skl(X,Y,X,Y))
& r1(X,sK17_skl(X,Y,X,Y)) ) )
& ( ~ p102(X)
| p103(X)
| ( p103(sK16_skl(X,Y,X,Y))
& ~ p104(sK16_skl(X,Y,X,Y))
& p4(sK16_skl(X,Y,X,Y))
& r1(X,sK16_skl(X,Y,X,Y))
& p103(sK15_skl(X,Y,X,Y))
& ~ p104(sK15_skl(X,Y,X,Y))
& ~ p4(sK15_skl(X,Y,X,Y))
& r1(X,sK15_skl(X,Y,X,Y)) ) )
& ( ~ p103(X)
| p104(X)
| ( p104(sK14_skl(X,Y,X,Y))
& ~ p105(sK14_skl(X,Y,X,Y))
& p5(sK14_skl(X,Y,X,Y))
& r1(X,sK14_skl(X,Y,X,Y))
& p104(sK13_skl(X,Y,X,Y))
& ~ p105(sK13_skl(X,Y,X,Y))
& ~ p5(sK13_skl(X,Y,X,Y))
& r1(X,sK13_skl(X,Y,X,Y)) ) )
& ( ~ p104(X)
| p105(X)
| ( p105(sK12_skl(X,Y,X,Y))
& ~ p106(sK12_skl(X,Y,X,Y))
& p6(sK12_skl(X,Y,X,Y))
& r1(X,sK12_skl(X,Y,X,Y))
& p105(sK11_skl(X,Y,X,Y))
& ~ p106(sK11_skl(X,Y,X,Y))
& ~ p6(sK11_skl(X,Y,X,Y))
& r1(X,sK11_skl(X,Y,X,Y)) ) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,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)
| ( p101(sK10_skl(Y,X,Y,X,Y))
& ~ p102(sK10_skl(Y,X,Y,X,Y))
& p2(sK10_skl(Y,X,Y,X,Y))
& r1(Y,sK10_skl(Y,X,Y,X,Y))
& p101(sK9_skl(Y,X,Y,X,Y))
& ~ p102(sK9_skl(Y,X,Y,X,Y))
& ~ p2(sK9_skl(Y,X,Y,X,Y))
& r1(Y,sK9_skl(Y,X,Y,X,Y)) ) )
& ( ~ p101(Y)
| p102(Y)
| ( p102(sK8_skl(Y,X,Y,X,Y))
& ~ p103(sK8_skl(Y,X,Y,X,Y))
& p3(sK8_skl(Y,X,Y,X,Y))
& r1(Y,sK8_skl(Y,X,Y,X,Y))
& p102(sK7_skl(Y,X,Y,X,Y))
& ~ p103(sK7_skl(Y,X,Y,X,Y))
& ~ p3(sK7_skl(Y,X,Y,X,Y))
& r1(Y,sK7_skl(Y,X,Y,X,Y)) ) )
& ( ~ p102(Y)
| p103(Y)
| ( p103(sK6_skl(Y,X,Y,X,Y))
& ~ p104(sK6_skl(Y,X,Y,X,Y))
& p4(sK6_skl(Y,X,Y,X,Y))
& r1(Y,sK6_skl(Y,X,Y,X,Y))
& p103(sK5_skl(Y,X,Y,X,Y))
& ~ p104(sK5_skl(Y,X,Y,X,Y))
& ~ p4(sK5_skl(Y,X,Y,X,Y))
& r1(Y,sK5_skl(Y,X,Y,X,Y)) ) )
& ( ~ p103(Y)
| p104(Y)
| ( p104(sK4_skl(Y,X,Y,X,Y))
& ~ p105(sK4_skl(Y,X,Y,X,Y))
& p5(sK4_skl(Y,X,Y,X,Y))
& r1(Y,sK4_skl(Y,X,Y,X,Y))
& p104(sK3_skl(Y,X,Y,X,Y))
& ~ p105(sK3_skl(Y,X,Y,X,Y))
& ~ p5(sK3_skl(Y,X,Y,X,Y))
& r1(Y,sK3_skl(Y,X,Y,X,Y)) ) )
& ( ~ p104(Y)
| p105(Y)
| ( p105(sK2_skl(Y,X,Y,X,Y))
& ~ p106(sK2_skl(Y,X,Y,X,Y))
& p6(sK2_skl(Y,X,Y,X,Y))
& r1(Y,sK2_skl(Y,X,Y,X,Y))
& p105(sK1_skl(Y,X,Y,X,Y))
& ~ p106(sK1_skl(Y,X,Y,X,Y))
& ~ p6(sK1_skl(Y,X,Y,X,Y))
& r1(Y,sK1_skl(Y,X,Y,X,Y)) ) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl,sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl,sK30_skl,sK31_skl,sK32_skl,sK33_skl,sK34_skl,sK35_skl,sK36_skl,sK37_skl,sK38_skl,sK39_skl,sK40_skl,sK41_skl,sK42_skl,sK43_skl,sK44_skl,sK45_skl,sK46_skl,sK47_skl,sK48_skl,sK49_skl,sK50_skl,sK51_skl,sK52_skl,sK53_skl,sK54_skl,sK55_skl,sK56_skl,sK57_skl,sK58_skl,sK59_skl,sK60_skl]),skolemize(X,sK0_skl),skolemize(X,sK1_skl(Y,X,Y,X,Y)),skolemize(X,sK2_skl(Y,X,Y,X,Y)),skolemize(X,sK3_skl(Y,X,Y,X,Y)),skolemize(X,sK4_skl(Y,X,Y,X,Y)),skolemize(X,sK5_skl(Y,X,Y,X,Y)),skolemize(X,sK6_skl(Y,X,Y,X,Y)),skolemize(X,sK7_skl(Y,X,Y,X,Y)),skolemize(X,sK8_skl(Y,X,Y,X,Y)),skolemize(X,sK9_skl(Y,X,Y,X,Y)),skolemize(X,sK10_skl(Y,X,Y,X,Y)),skolemize(Y,sK11_skl(X,Y,X,Y)),skolemize(Y,sK12_skl(X,Y,X,Y)),skolemize(Y,sK13_skl(X,Y,X,Y)),skolemize(Y,sK14_skl(X,Y,X,Y)),skolemize(Y,sK15_skl(X,Y,X,Y)),skolemize(Y,sK16_skl(X,Y,X,Y)),skolemize(Y,sK17_skl(X,Y,X,Y)),skolemize(Y,sK18_skl(X,Y,X,Y)),skolemize(Y,sK19_skl(X,Y,X,Y)),skolemize(Y,sK20_skl(X,Y,X,Y)),skolemize(X,sK21_skl(Y,X,Y)),skolemize(X,sK22_skl(Y,X,Y)),skolemize(X,sK23_skl(Y,X,Y)),skolemize(X,sK24_skl(Y,X,Y)),skolemize(X,sK25_skl(Y,X,Y)),skolemize(X,sK26_skl(Y,X,Y)),skolemize(X,sK27_skl(Y,X,Y)),skolemize(X,sK28_skl(Y,X,Y)),skolemize(X,sK29_skl(Y,X,Y)),skolemize(X,sK30_skl(Y,X,Y)),skolemize(Y,sK31_skl(X,Y)),skolemize(Y,sK32_skl(X,Y)),skolemize(Y,sK33_skl(X,Y)),skolemize(Y,sK34_skl(X,Y)),skolemize(Y,sK35_skl(X,Y)),skolemize(Y,sK36_skl(X,Y)),skolemize(Y,sK37_skl(X,Y)),skolemize(Y,sK38_skl(X,Y)),skolemize(Y,sK39_skl(X,Y)),skolemize(Y,sK40_skl(X,Y)),skolemize(X,sK41_skl(Y)),skolemize(X,sK42_skl(Y)),skolemize(X,sK43_skl(Y)),skolemize(X,sK44_skl(Y)),skolemize(X,sK45_skl(Y)),skolemize(X,sK46_skl(Y)),skolemize(X,sK47_skl(Y)),skolemize(X,sK48_skl(Y)),skolemize(X,sK49_skl(Y)),skolemize(X,sK50_skl(Y)),skolemize(Y,sK51_skl),skolemize(Y,sK52_skl),skolemize(Y,sK53_skl),skolemize(Y,sK54_skl),skolemize(Y,sK55_skl),skolemize(Y,sK56_skl),skolemize(Y,sK57_skl),skolemize(Y,sK58_skl),skolemize(Y,sK59_skl),skolemize(Y,sK60_skl)],[f3]) ).
fof(f5,plain,
! [X0,X1,X2,X3,X4] :
( p3(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f59,plain,
! [X0,X1,X2,X3,X4] :
( ~ p105(X4)
| p104(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f60,plain,
! [X0,X1,X2,X3,X4] :
( ~ p104(X4)
| p103(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f61,plain,
! [X0,X1,X2,X3,X4] :
( ~ p103(X4)
| p102(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f64,plain,
! [X0,X1,X2,X3] :
( ~ p104(X3)
| p105(X3)
| r1(X3,sK11_skl(X3,X2,X1,X0))
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f67,plain,
! [X0,X1,X2,X3] :
( ~ p104(X3)
| p105(X3)
| p105(sK11_skl(X3,X2,X1,X0))
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f110,plain,
! [X0,X1,X2,X3,X4] :
( ~ p102(X3)
| p3(X3)
| ~ p102(X4)
| ~ p3(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f118,plain,
! [X0,X1,X2,X3] :
( ~ p104(X3)
| p103(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f119,plain,
! [X0,X1,X2,X3] :
( ~ p103(X3)
| p102(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f134,plain,
! [X0,X1,X2] :
( ~ p103(X2)
| p104(X2)
| r1(X2,sK24_skl(X2,X1,X0))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f136,plain,
! [X0,X1,X2] :
( ~ p103(X2)
| p104(X2)
| ~ p105(sK24_skl(X2,X1,X0))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f137,plain,
! [X0,X1,X2] :
( ~ p103(X2)
| p104(X2)
| p104(sK24_skl(X2,X1,X0))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f168,plain,
! [X0,X1,X2,X3] :
( ~ p102(X2)
| p3(X2)
| ~ p102(X3)
| ~ p3(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f177,plain,
! [X0,X1,X2] :
( ~ p103(X2)
| p102(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f200,plain,
! [X0,X1] :
( ~ p102(X1)
| p103(X1)
| r1(X1,sK36_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f202,plain,
! [X0,X1] :
( ~ p102(X1)
| p103(X1)
| ~ p104(sK36_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f203,plain,
! [X0,X1] :
( ~ p102(X1)
| p103(X1)
| p103(sK36_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f226,plain,
! [X0,X1,X2] :
( ~ p102(X1)
| p3(X1)
| ~ p102(X2)
| ~ p3(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f262,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| r1(X0,sK47_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f263,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| ~ p3(sK47_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f264,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| ~ p103(sK47_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f265,plain,
! [X0] :
( ~ p101(X0)
| p102(X0)
| p102(sK47_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f332,plain,
( ~ p100(sK0_skl)
| p101(sK0_skl)
| r1(sK0_skl,sK60_skl) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f334,plain,
( ~ p100(sK0_skl)
| p101(sK0_skl)
| ~ p102(sK60_skl) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f335,plain,
( ~ p100(sK0_skl)
| p101(sK0_skl)
| p101(sK60_skl) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f354,plain,
~ p101(sK0_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f355,plain,
p100(sK0_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f467,definition,
( sQ29_spl
<=> p101(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f468,plain,
( ~ sQ29_spl
| p101(sK0_skl) ),
inference(component_clause,[status(thm)],[f467]) ).
fof(f502,definition,
( sQ38_spl
<=> p100(sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f504,plain,
( sQ38_spl
| ~ p100(sK0_skl) ),
inference(component_clause,[status(thm)],[f502]) ).
fof(f518,definition,
( sQ42_spl
<=> r1(sK0_skl,sK60_skl) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f519,plain,
( ~ sQ42_spl
| r1(sK0_skl,sK60_skl) ),
inference(component_clause,[status(thm)],[f518]) ).
fof(f521,plain,
( ~ sQ38_spl
| sQ29_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f332,f518,f467,f502]) ).
fof(f526,definition,
( sQ44_spl
<=> p102(sK60_skl) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f529,plain,
( ~ sQ38_spl
| sQ29_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f334,f526,f467,f502]) ).
fof(f530,definition,
( sQ45_spl
<=> p101(sK60_skl) ),
introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition]) ).
fof(f533,plain,
( ~ sQ38_spl
| sQ29_spl
| sQ45_spl ),
inference(split_clause,[status(thm)],[f335,f530,f467,f502]) ).
fof(f609,plain,
( ~ sQ29_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f468,f354]) ).
fof(f610,plain,
~ sQ29_spl,
inference(contradiction_clause,[status(thm)],[f609]) ).
fof(f611,plain,
( sQ38_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f504,f355]) ).
fof(f612,plain,
sQ38_spl,
inference(contradiction_clause,[status(thm)],[f611]) ).
fof(f773,plain,
( ~ sQ42_spl
| ~ p101(sK60_skl)
| p102(sK60_skl)
| r1(sK60_skl,sK47_skl(sK60_skl)) ),
inference(resolution,[status(thm)],[f262,f519]) ).
fof(f775,definition,
( sQ89_spl
<=> r1(sK60_skl,sK47_skl(sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f776,plain,
( ~ sQ89_spl
| r1(sK60_skl,sK47_skl(sK60_skl)) ),
inference(component_clause,[status(thm)],[f775]) ).
fof(f778,plain,
( ~ sQ42_spl
| ~ sQ45_spl
| sQ44_spl
| sQ89_spl ),
inference(split_clause,[status(thm)],[f773,f775,f526,f530,f518]) ).
fof(f833,definition,
( sQ100_spl
<=> p102(sK47_skl(sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition]) ).
fof(f835,plain,
( sQ100_spl
| ~ p102(sK47_skl(sK60_skl)) ),
inference(component_clause,[status(thm)],[f833]) ).
fof(f837,definition,
( sQ101_spl
<=> p103(sK47_skl(sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f838,plain,
( ~ sQ101_spl
| p103(sK47_skl(sK60_skl)) ),
inference(component_clause,[status(thm)],[f837]) ).
fof(f853,plain,
( ~ sQ101_spl
| ~ p101(sK60_skl)
| p102(sK60_skl)
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f838,f264]) ).
fof(f854,plain,
( ~ sQ101_spl
| ~ sQ45_spl
| sQ44_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f853,f518,f526,f530,f837]) ).
fof(f977,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ p103(X1)
| p102(X1)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f177,f519]) ).
fof(f980,plain,
! [X0] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X0)
| p102(X0)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f977,f776]) ).
fof(f1172,plain,
( sQ100_spl
| ~ p101(sK60_skl)
| p102(sK60_skl)
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f835,f265]) ).
fof(f1173,plain,
( sQ100_spl
| ~ sQ45_spl
| sQ44_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1172,f518,f526,f530,f833]) ).
fof(f1461,plain,
! [X0] :
( ~ sQ42_spl
| ~ p102(X0)
| p103(X0)
| r1(X0,sK36_skl(X0,sK60_skl))
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f200,f519]) ).
fof(f1464,plain,
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p102(sK47_skl(sK60_skl))
| p103(sK47_skl(sK60_skl))
| r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f1461,f776]) ).
fof(f1469,definition,
( sQ212_spl
<=> r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ212_spl])],[split_symbol_definition]) ).
fof(f1470,plain,
( ~ sQ212_spl
| r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f1469]) ).
fof(f1472,plain,
( ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ100_spl
| sQ101_spl
| sQ212_spl ),
inference(split_clause,[status(thm)],[f1464,f1469,f837,f833,f518,f775]) ).
fof(f1515,plain,
! [X0,X1,X2,X3] :
( ~ sQ42_spl
| ~ p105(X3)
| p104(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f59,f519]) ).
fof(f1520,plain,
( ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ212_spl
| ~ p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| p102(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f1470,f980]) ).
fof(f1531,definition,
( sQ222_spl
<=> p102(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition]) ).
fof(f1535,definition,
( sQ223_spl
<=> p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ223_spl])],[split_symbol_definition]) ).
fof(f1537,plain,
( sQ223_spl
| ~ p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f1535]) ).
fof(f1538,plain,
( ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ212_spl
| ~ sQ223_spl
| sQ222_spl ),
inference(split_clause,[status(thm)],[f1520,f1531,f1535,f1469,f518,f775]) ).
fof(f1539,definition,
( sQ224_spl
<=> p104(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ224_spl])],[split_symbol_definition]) ).
fof(f1540,plain,
( ~ sQ224_spl
| p104(sK36_skl(sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f1539]) ).
fof(f1551,plain,
( ~ sQ224_spl
| ~ p102(sK47_skl(sK60_skl))
| p103(sK47_skl(sK60_skl))
| ~ r1(sK60_skl,sK47_skl(sK60_skl))
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f1540,f202]) ).
fof(f1552,plain,
( ~ sQ224_spl
| ~ sQ100_spl
| sQ101_spl
| ~ sQ89_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f1551,f518,f775,f837,f833,f1539]) ).
fof(f1553,plain,
! [X0,X1,X2,X3] :
( ~ sQ42_spl
| ~ p104(X3)
| p103(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f60,f519]) ).
fof(f1555,plain,
! [X0,X1,X2,X3] :
( ~ sQ42_spl
| ~ p103(X3)
| p102(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f61,f519]) ).
fof(f1643,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| ~ p104(X2)
| p105(X2)
| r1(X2,sK11_skl(X2,X1,X0,sK60_skl))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f64,f519]) ).
fof(f1763,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| ~ p104(X2)
| p103(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f118,f519]) ).
fof(f1766,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X1)
| p103(X1)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1763,f776]) ).
fof(f1769,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X0)
| p103(X0)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1766,f1470]) ).
fof(f1779,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| ~ p103(X2)
| p102(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f119,f519]) ).
fof(f1782,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X1)
| p102(X1)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1779,f776]) ).
fof(f1785,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X0)
| p102(X0)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1782,f1470]) ).
fof(f1838,plain,
! [X0,X1,X2] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p105(X2)
| p104(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1515,f776]) ).
fof(f1841,plain,
! [X0,X1] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p105(X1)
| p104(X1)
| ~ r1(X0,X1)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1838,f1470]) ).
fof(f1852,plain,
! [X0,X1,X2] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X2)
| p103(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1553,f776]) ).
fof(f1855,plain,
! [X0,X1] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X1)
| p103(X1)
| ~ r1(X0,X1)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1852,f1470]) ).
fof(f1866,plain,
! [X0,X1,X2] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X2)
| p102(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1555,f776]) ).
fof(f1869,plain,
! [X0,X1] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X1)
| p102(X1)
| ~ r1(X0,X1)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1866,f1470]) ).
fof(f2073,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f226,f519]) ).
fof(f2076,plain,
! [X0] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p102(sK47_skl(sK60_skl))
| p3(sK47_skl(sK60_skl))
| ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2073,f776]) ).
fof(f2084,definition,
! [X0] :
( sQ297_spl
<=> ( ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK47_skl(sK60_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ297_spl])],[split_symbol_definition]) ).
fof(f2085,plain,
! [X0] :
( ~ sQ297_spl
| ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(component_clause,[status(thm)],[f2084]) ).
fof(f2087,definition,
( sQ298_spl
<=> p3(sK47_skl(sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ298_spl])],[split_symbol_definition]) ).
fof(f2088,plain,
( ~ sQ298_spl
| p3(sK47_skl(sK60_skl)) ),
inference(component_clause,[status(thm)],[f2087]) ).
fof(f2090,plain,
( ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ100_spl
| sQ298_spl
| sQ297_spl ),
inference(split_clause,[status(thm)],[f2076,f2084,f2087,f833,f518,f775]) ).
fof(f2101,plain,
( sQ223_spl
| ~ p102(sK47_skl(sK60_skl))
| p103(sK47_skl(sK60_skl))
| ~ r1(sK60_skl,sK47_skl(sK60_skl))
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f1537,f203]) ).
fof(f2102,plain,
( sQ223_spl
| ~ sQ100_spl
| sQ101_spl
| ~ sQ89_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f2101,f518,f775,f837,f833,f1535]) ).
fof(f2192,plain,
( ~ sQ298_spl
| ~ p101(sK60_skl)
| p102(sK60_skl)
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f2088,f263]) ).
fof(f2193,plain,
( ~ sQ298_spl
| ~ sQ45_spl
| sQ44_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f2192,f518,f526,f530,f2087]) ).
fof(f2255,plain,
! [X0,X1,X2,X3,X4] :
( ~ p102(X3)
| p3(X3)
| ~ p102(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f110,f5]) ).
fof(f2256,plain,
! [X0,X1,X2,X3] :
( ~ sQ42_spl
| ~ p102(X2)
| p3(X2)
| ~ p102(X3)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f2255,f519]) ).
fof(f2547,plain,
! [X0,X1] :
( ~ sQ42_spl
| ~ p103(X1)
| p104(X1)
| r1(X1,sK24_skl(X1,X0,sK60_skl))
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f134,f519]) ).
fof(f2554,plain,
! [X0] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(X0)
| p104(X0)
| r1(X0,sK24_skl(X0,sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2547,f776]) ).
fof(f2607,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| p104(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f2554,f1470]) ).
fof(f2609,definition,
( sQ369_spl
<=> r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ369_spl])],[split_symbol_definition]) ).
fof(f2610,plain,
( ~ sQ369_spl
| r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f2609]) ).
fof(f2612,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ223_spl
| sQ224_spl
| sQ369_spl ),
inference(split_clause,[status(thm)],[f2607,f2609,f1539,f1535,f518,f775,f1469]) ).
fof(f2868,plain,
! [X0,X1,X2] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p102(X1)
| p3(X1)
| ~ p102(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2256,f776]) ).
fof(f2871,plain,
! [X0,X1] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ r1(X0,X1)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2868,f1470]) ).
fof(f3115,plain,
! [X0,X1,X2] :
( ~ sQ42_spl
| ~ p102(X1)
| p3(X1)
| ~ p102(X2)
| ~ p3(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK60_skl,X0) ),
inference(resolution,[status(thm)],[f168,f519]) ).
fof(f3389,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p102(X0)
| p3(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f3115,f776]) ).
fof(f3390,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ297_spl
| ~ p102(X0)
| ~ p102(X1)
| ~ p3(X1)
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f3389,f2085]) ).
fof(f3391,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ297_spl
| ~ p102(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f3390,f1470]) ).
fof(f3393,definition,
! [X0] :
( sQ505_spl
<=> ( ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ505_spl])],[split_symbol_definition]) ).
fof(f3394,plain,
! [X0] :
( ~ sQ505_spl
| ~ p102(X0)
| ~ p3(X0)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(component_clause,[status(thm)],[f3393]) ).
fof(f3396,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ297_spl
| ~ sQ222_spl
| sQ505_spl ),
inference(split_clause,[status(thm)],[f3391,f3393,f1531,f2084,f518,f775,f1469]) ).
fof(f3401,plain,
! [X0,X1] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ505_spl
| ~ p102(X0)
| ~ p102(X1)
| ~ r1(X0,X1)
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f2871,f3394]) ).
fof(f4080,plain,
! [X0,X1] :
( ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X1)
| p105(X1)
| r1(X1,sK11_skl(X1,X0,sK47_skl(sK60_skl),sK60_skl))
| ~ r1(X0,X1)
| ~ r1(sK47_skl(sK60_skl),X0) ),
inference(resolution,[status(thm)],[f1643,f776]) ).
fof(f4410,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ p104(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| p103(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f2610,f1769]) ).
fof(f4411,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ p103(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| p102(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f2610,f1785]) ).
fof(f4416,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ505_spl
| ~ sQ369_spl
| ~ p102(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| ~ p102(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2610,f3401]) ).
fof(f4420,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ p103(X0)
| p102(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2610,f1869]) ).
fof(f4421,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ p104(X0)
| p103(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2610,f1855]) ).
fof(f4422,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ p105(X0)
| p104(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f2610,f1841]) ).
fof(f4430,definition,
( sQ641_spl
<=> p103(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ641_spl])],[split_symbol_definition]) ).
fof(f4434,definition,
( sQ642_spl
<=> p104(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ642_spl])],[split_symbol_definition]) ).
fof(f4436,plain,
( sQ642_spl
| ~ p104(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f4434]) ).
fof(f4437,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ642_spl
| sQ641_spl ),
inference(split_clause,[status(thm)],[f4410,f4430,f4434,f2609,f518,f775,f1469]) ).
fof(f4438,definition,
( sQ643_spl
<=> p102(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ643_spl])],[split_symbol_definition]) ).
fof(f4441,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ641_spl
| sQ643_spl ),
inference(split_clause,[status(thm)],[f4411,f4438,f4430,f2609,f518,f775,f1469]) ).
fof(f4442,definition,
( sQ644_spl
<=> p105(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ644_spl])],[split_symbol_definition]) ).
fof(f4443,plain,
( ~ sQ644_spl
| p105(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f4442]) ).
fof(f4464,definition,
! [X0] :
( sQ650_spl
<=> ( ~ p102(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ) ),
introduced(definition,[new_symbols(definition,[sQ650_spl])],[split_symbol_definition]) ).
fof(f4465,plain,
! [X0] :
( ~ sQ650_spl
| ~ p102(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(component_clause,[status(thm)],[f4464]) ).
fof(f4467,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ505_spl
| ~ sQ369_spl
| ~ sQ643_spl
| sQ650_spl ),
inference(split_clause,[status(thm)],[f4416,f4464,f4438,f2609,f3393,f518,f775,f1469]) ).
fof(f4476,plain,
( sQ642_spl
| ~ p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| p104(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK60_skl,sK47_skl(sK60_skl))
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f4436,f137]) ).
fof(f4477,plain,
( sQ642_spl
| ~ sQ223_spl
| sQ224_spl
| ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f4476,f518,f775,f1469,f1539,f1535,f4434]) ).
fof(f4482,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ650_spl
| ~ p103(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4420,f4465]) ).
fof(f4483,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ650_spl
| ~ p104(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4421,f4482]) ).
fof(f4484,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ650_spl
| ~ p105(X0)
| ~ r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4422,f4483]) ).
fof(f5380,plain,
( ~ sQ644_spl
| ~ p103(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| p104(sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK60_skl,sK47_skl(sK60_skl))
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f4443,f136]) ).
fof(f5381,plain,
( ~ sQ644_spl
| ~ sQ223_spl
| sQ224_spl
| ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f5380,f518,f775,f1469,f1539,f1535,f4442]) ).
fof(f5952,plain,
! [X0] :
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(X0)
| p105(X0)
| r1(X0,sK11_skl(X0,sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),X0) ),
inference(resolution,[status(thm)],[f4080,f1470]) ).
fof(f6362,plain,
( ~ sQ369_spl
| ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ p104(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| p105(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK11_skl(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f5952,f2610]) ).
fof(f6364,definition,
( sQ870_spl
<=> r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK11_skl(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
introduced(definition,[new_symbols(definition,[sQ870_spl])],[split_symbol_definition]) ).
fof(f6365,plain,
( ~ sQ870_spl
| r1(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK11_skl(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(component_clause,[status(thm)],[f6364]) ).
fof(f6367,plain,
( ~ sQ369_spl
| ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ642_spl
| sQ644_spl
| sQ870_spl ),
inference(split_clause,[status(thm)],[f6362,f6364,f4442,f4434,f518,f775,f1469,f2609]) ).
fof(f7624,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ650_spl
| ~ sQ870_spl
| ~ p105(sK11_skl(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl)) ),
inference(resolution,[status(thm)],[f6365,f4484]) ).
fof(f7847,plain,
( ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl
| ~ sQ369_spl
| ~ sQ650_spl
| ~ sQ870_spl
| ~ p104(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| p105(sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK24_skl(sK36_skl(sK47_skl(sK60_skl),sK60_skl),sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK47_skl(sK60_skl),sK36_skl(sK47_skl(sK60_skl),sK60_skl))
| ~ r1(sK60_skl,sK47_skl(sK60_skl))
| ~ r1(sK0_skl,sK60_skl) ),
inference(resolution,[status(thm)],[f7624,f67]) ).
fof(f7848,plain,
( ~ sQ650_spl
| ~ sQ870_spl
| ~ sQ642_spl
| sQ644_spl
| ~ sQ369_spl
| ~ sQ212_spl
| ~ sQ89_spl
| ~ sQ42_spl ),
inference(split_clause,[status(thm)],[f7847,f518,f775,f1469,f2609,f4442,f4434,f6364,f4464]) ).
fof(f7849,plain,
$false,
inference(sat_refutation,[status(thm)],[f521,f529,f533,f610,f612,f778,f854,f1173,f1472,f1538,f1552,f2090,f2102,f2193,f2612,f3396,f4437,f4441,f4467,f4477,f5381,f6367,f7848]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : LCL636+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.42 % Computer : n010.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 21 00:41:54 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.46 % Drodi V4.1.1
% 75.49/10.30 % Refutation found
% 75.49/10.30 % SZS status Theorem for theBenchmark: Theorem is valid
% 75.49/10.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 7.45/10.37 % Elapsed time: 9.922762 seconds
% 7.45/10.37 % CPU time: 77.993488 seconds
% 7.45/10.37 % Total memory used: 242.552 MB
% 7.45/10.37 % Net memory used: 231.094 MB
%------------------------------------------------------------------------------