%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL646+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:19 PM UTC 2026
% Result : Theorem 16.55s 2.68s
% Output : CNFRefutation 16.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 17
% Syntax : Number of formulae : 96 ( 11 unt; 16 def)
% Number of atoms : 1874 ( 0 equ)
% Maximal formula atoms : 390 ( 19 avg)
% Number of connectives : 3391 (1613 ~;1356 |; 406 &)
% ( 16 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 81 ( 8 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 17 prp; 0-2 aty)
% Number of functors : 69 ( 69 usr; 5 con; 0-4 aty)
% Number of variables : 1017 ( 946 !; 71 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p3(Y)
| ~ r1(X,Y) )
| ! [Y] :
( p5(Y)
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p3(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p4(Y)
& ! [X] :
( p1(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p3(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p5(Y)
& ! [X] :
( p5(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p3(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p4(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p1(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p3(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p5(X)
& ! [Y] :
( p5(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p2(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p6(Y)
& ! [X] :
( p6(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p4(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p2(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p4(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p6(X)
& ! [Y] :
( p6(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p6(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] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
& ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
& ! [Y] :
( p1(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p1(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p2(Y)
| ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p3(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p3(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p5(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p5(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p4(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p6(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p4(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p6(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p4(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p6(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p5(Y)
| ? [X] :
( ~ p3(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p5(Y)
| ? [X] :
( ~ p5(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ? [X] :
( ~ p2(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ? [X] :
( ~ p4(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p3(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ? [Y] :
( ~ p5(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ? [X] :
( ~ p6(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p4(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ? [Y] :
( ~ p6(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p6(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,
( ~ p1(sK68_skl)
& r1(sK0_skl,sK68_skl)
& ~ p2(sK67_skl)
& r1(sK0_skl,sK67_skl)
& ~ p3(sK66_skl)
& r1(sK0_skl,sK66_skl)
& ~ p5(sK65_skl)
& r1(sK0_skl,sK65_skl)
& ! [Y] :
( p1(Y)
| ( ~ p3(sK64_skl(Y))
& r1(Y,sK64_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p1(Y)
| ( ~ p5(sK63_skl(Y))
& r1(Y,sK63_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p2(Y)
| ( ~ p1(sK62_skl(Y))
& r1(Y,sK62_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p3(Y)
| ( ~ p3(sK61_skl(Y))
& r1(Y,sK61_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p3(Y)
| ( ~ p5(sK60_skl(Y))
& r1(Y,sK60_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p5(Y)
| ( ~ p3(sK59_skl(Y))
& r1(Y,sK59_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p5(Y)
| ( ~ p5(sK58_skl(Y))
& r1(Y,sK58_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p1(sK57_skl(X,Y))
& r1(X,sK57_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p3(sK56_skl(X,Y))
& r1(X,sK56_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p4(sK55_skl(X,Y))
& r1(X,sK55_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p5(sK54_skl(X,Y))
& r1(X,sK54_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p4(Y)
| ( ~ p2(sK53_skl(Y))
& r1(Y,sK53_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p6(Y)
| ( ~ p2(sK52_skl(Y))
& r1(Y,sK52_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p1(sK51_skl(X,Y))
& r1(X,sK51_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p3(sK50_skl(X,Y))
& r1(X,sK50_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p5(sK49_skl(X,Y))
& r1(X,sK49_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p4(Y)
| ( ~ p4(sK48_skl(Y))
& r1(Y,sK48_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p6(Y)
| ( ~ p4(sK47_skl(Y))
& r1(Y,sK47_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p1(sK46_skl(X,Y))
& r1(X,sK46_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p3(sK45_skl(X,Y))
& r1(X,sK45_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p5(sK44_skl(X,Y))
& r1(X,sK44_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p4(Y)
| ( ~ p6(sK43_skl(Y))
& r1(Y,sK43_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p6(Y)
| ( ~ p6(sK42_skl(Y))
& r1(Y,sK42_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ( ~ p3(sK41_skl(Y,X,Y))
& r1(Y,sK41_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ( ~ p5(sK40_skl(Y,X,Y))
& r1(Y,sK40_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p2(sK39_skl(X,Y))
& r1(X,sK39_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p2(sK38_skl(X,Y))
& r1(X,sK38_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p2(sK37_skl(X,Y))
& r1(X,sK37_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ( ~ p3(sK36_skl(Y,X,Y))
& r1(Y,sK36_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p3(Y)
| ( ~ p5(sK35_skl(Y,X,Y))
& r1(Y,sK35_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ( ~ p1(sK34_skl(Y,X,Y))
& r1(Y,sK34_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p4(sK33_skl(X,Y))
& r1(X,sK33_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p4(sK32_skl(X,Y))
& r1(X,sK32_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p4(sK31_skl(X,Y))
& r1(X,sK31_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p5(Y)
| ( ~ p3(sK30_skl(Y,X,Y))
& r1(Y,sK30_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p5(Y)
| ( ~ p5(sK29_skl(Y,X,Y))
& r1(Y,sK29_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p6(sK28_skl(X,Y))
& r1(X,sK28_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p6(sK27_skl(X,Y))
& r1(X,sK27_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p6(sK26_skl(X,Y))
& r1(X,sK26_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p1(sK25_skl(X,Y,X,Y))
& r1(X,sK25_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p3(sK24_skl(X,Y,X,Y))
& r1(X,sK24_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p4(sK23_skl(X,Y,X,Y))
& r1(X,sK23_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ( ~ p5(sK22_skl(X,Y,X,Y))
& r1(X,sK22_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ( ~ p2(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] :
( p6(Y)
| ( ~ p2(sK20_skl(Y,X,Y))
& r1(Y,sK20_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p1(sK19_skl(X,Y,X,Y))
& r1(X,sK19_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p3(sK18_skl(X,Y,X,Y))
& r1(X,sK18_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p3(X)
| ( ~ p5(sK17_skl(X,Y,X,Y))
& r1(X,sK17_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ( ~ p4(sK16_skl(Y,X,Y))
& r1(Y,sK16_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ( ~ p4(sK15_skl(Y,X,Y))
& r1(Y,sK15_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p1(sK14_skl(X,Y,X,Y))
& r1(X,sK14_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p3(sK13_skl(X,Y,X,Y))
& r1(X,sK13_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p5(X)
| ( ~ p5(sK12_skl(X,Y,X,Y))
& r1(X,sK12_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ( ~ p6(sK11_skl(Y,X,Y))
& r1(Y,sK11_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p6(Y)
| ( ~ p6(sK10_skl(Y,X,Y))
& r1(Y,sK10_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p2(sK9_skl(X,Y,X,Y))
& r1(X,sK9_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p2(sK8_skl(X,Y,X,Y))
& r1(X,sK8_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p2(sK7_skl(X,Y,X,Y))
& r1(X,sK7_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p4(sK6_skl(X,Y,X,Y))
& r1(X,sK6_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p4(sK5_skl(X,Y,X,Y))
& r1(X,sK5_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p4(sK4_skl(X,Y,X,Y))
& r1(X,sK4_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p2(X)
| ( ~ p6(sK3_skl(X,Y,X,Y))
& r1(X,sK3_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p4(X)
| ( ~ p6(sK2_skl(X,Y,X,Y))
& r1(X,sK2_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p6(X)
| ( ~ p6(sK1_skl(X,Y,X,Y))
& r1(X,sK1_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p4(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p6(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,sK61_skl,sK62_skl,sK63_skl,sK64_skl,sK65_skl,sK66_skl,sK67_skl,sK68_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y,X,Y)),skolemize(Y,sK2_skl(X,Y,X,Y)),skolemize(Y,sK3_skl(X,Y,X,Y)),skolemize(Y,sK4_skl(X,Y,X,Y)),skolemize(Y,sK5_skl(X,Y,X,Y)),skolemize(Y,sK6_skl(X,Y,X,Y)),skolemize(Y,sK7_skl(X,Y,X,Y)),skolemize(Y,sK8_skl(X,Y,X,Y)),skolemize(Y,sK9_skl(X,Y,X,Y)),skolemize(X,sK10_skl(Y,X,Y)),skolemize(X,sK11_skl(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(X,sK15_skl(Y,X,Y)),skolemize(X,sK16_skl(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(X,sK20_skl(Y,X,Y)),skolemize(X,sK21_skl(Y,X,Y)),skolemize(Y,sK22_skl(X,Y,X,Y)),skolemize(Y,sK23_skl(X,Y,X,Y)),skolemize(Y,sK24_skl(X,Y,X,Y)),skolemize(Y,sK25_skl(X,Y,X,Y)),skolemize(Y,sK26_skl(X,Y)),skolemize(Y,sK27_skl(X,Y)),skolemize(Y,sK28_skl(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(X,sK34_skl(Y,X,Y)),skolemize(X,sK35_skl(Y,X,Y)),skolemize(X,sK36_skl(Y,X,Y)),skolemize(Y,sK37_skl(X,Y)),skolemize(Y,sK38_skl(X,Y)),skolemize(Y,sK39_skl(X,Y)),skolemize(X,sK40_skl(Y,X,Y)),skolemize(X,sK41_skl(Y,X,Y)),skolemize(X,sK42_skl(Y)),skolemize(X,sK43_skl(Y)),skolemize(Y,sK44_skl(X,Y)),skolemize(Y,sK45_skl(X,Y)),skolemize(Y,sK46_skl(X,Y)),skolemize(X,sK47_skl(Y)),skolemize(X,sK48_skl(Y)),skolemize(Y,sK49_skl(X,Y)),skolemize(Y,sK50_skl(X,Y)),skolemize(Y,sK51_skl(X,Y)),skolemize(X,sK52_skl(Y)),skolemize(X,sK53_skl(Y)),skolemize(Y,sK54_skl(X,Y)),skolemize(Y,sK55_skl(X,Y)),skolemize(Y,sK56_skl(X,Y)),skolemize(Y,sK57_skl(X,Y)),skolemize(X,sK58_skl(Y)),skolemize(X,sK59_skl(Y)),skolemize(X,sK60_skl(Y)),skolemize(X,sK61_skl(Y)),skolemize(X,sK62_skl(Y)),skolemize(X,sK63_skl(Y)),skolemize(X,sK64_skl(Y)),skolemize(Y,sK65_skl),skolemize(Y,sK66_skl),skolemize(Y,sK67_skl),skolemize(Y,sK68_skl)],[f3]) ).
fof(f6,plain,
! [X0,X1,X2,X3,X4] :
( p4(X4)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f53,plain,
! [X0,X1,X2,X3] :
( p1(X3)
| r1(X3,sK23_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(f54,plain,
! [X0,X1,X2,X3] :
( p1(X3)
| ~ p4(sK23_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(f75,plain,
! [X0,X1,X2] :
( p4(X2)
| r1(X2,sK34_skl(X2,X1,X0))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f76,plain,
! [X0,X1,X2] :
( p4(X2)
| ~ p1(sK34_skl(X2,X1,X0))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f117,plain,
! [X0,X1] :
( p1(X1)
| r1(X1,sK55_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f118,plain,
! [X0,X1] :
( p1(X1)
| ~ p4(sK55_skl(X1,X0))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f131,plain,
! [X0] :
( p2(X0)
| r1(X0,sK62_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f132,plain,
! [X0] :
( p2(X0)
| ~ p1(sK62_skl(X0))
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f137,plain,
r1(sK0_skl,sK65_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f139,plain,
r1(sK0_skl,sK66_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f141,plain,
r1(sK0_skl,sK67_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f142,plain,
~ p2(sK67_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f143,plain,
r1(sK0_skl,sK68_skl),
inference(cnf_transformation,[status(thm)],[f4]) ).
fof(f172,plain,
! [X0,X1] :
( p2(X1)
| ~ r1(sK0_skl,X1)
| ~ p4(sK55_skl(sK62_skl(X1),X0))
| ~ r1(X0,sK62_skl(X1))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f118,f132]) ).
fof(f208,plain,
! [X0] :
( p2(X0)
| ~ r1(sK0_skl,X0)
| p2(X0)
| ~ r1(sK0_skl,X0)
| ~ p4(sK55_skl(sK62_skl(X0),X0))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f172,f131]) ).
fof(f209,plain,
! [X0] :
( p2(X0)
| ~ p4(sK55_skl(sK62_skl(X0),X0))
| ~ r1(sK0_skl,X0) ),
inference(duplicate_literals_removal,[status(thm)],[f208]) ).
fof(f213,plain,
( ~ p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f209,f142]) ).
fof(f214,definition,
( sQ4_spl
<=> r1(sK0_skl,sK67_skl) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f216,plain,
( sQ4_spl
| ~ r1(sK0_skl,sK67_skl) ),
inference(component_clause,[status(thm)],[f214]) ).
fof(f217,definition,
( sQ5_spl
<=> p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f219,plain,
( sQ5_spl
| ~ p4(sK55_skl(sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f217]) ).
fof(f220,plain,
( ~ sQ5_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f213,f214,f217]) ).
fof(f221,plain,
( sQ4_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f216,f141]) ).
fof(f222,plain,
sQ4_spl,
inference(contradiction_clause,[status(thm)],[f221]) ).
fof(f225,plain,
! [X0,X1] :
( sQ5_spl
| ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),X1,X0))
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f219,f76]) ).
fof(f230,plain,
! [X0,X1] :
( sQ5_spl
| r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),X1,X0))
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f219,f75]) ).
fof(f295,definition,
( sQ15_spl
<=> r1(sK67_skl,sK62_skl(sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f296,plain,
( ~ sQ15_spl
| r1(sK67_skl,sK62_skl(sK67_skl)) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f297,plain,
( sQ15_spl
| ~ r1(sK67_skl,sK62_skl(sK67_skl)) ),
inference(component_clause,[status(thm)],[f295]) ).
fof(f298,definition,
( sQ16_spl
<=> p1(sK62_skl(sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f299,plain,
( ~ sQ16_spl
| p1(sK62_skl(sK67_skl)) ),
inference(component_clause,[status(thm)],[f298]) ).
fof(f302,plain,
( ~ sQ16_spl
| p2(sK67_skl)
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f299,f132]) ).
fof(f303,definition,
( sQ17_spl
<=> p2(sK67_skl) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f304,plain,
( ~ sQ17_spl
| p2(sK67_skl) ),
inference(component_clause,[status(thm)],[f303]) ).
fof(f306,plain,
( ~ sQ16_spl
| sQ17_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f302,f214,f303,f298]) ).
fof(f307,plain,
( ~ sQ17_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f304,f142]) ).
fof(f308,plain,
~ sQ17_spl,
inference(contradiction_clause,[status(thm)],[f307]) ).
fof(f316,plain,
( sQ15_spl
| p2(sK67_skl)
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f297,f131]) ).
fof(f317,plain,
( sQ15_spl
| sQ17_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f316,f214,f303,f295]) ).
fof(f405,definition,
( sQ27_spl
<=> r1(sK0_skl,sK66_skl) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f407,plain,
( sQ27_spl
| ~ r1(sK0_skl,sK66_skl) ),
inference(component_clause,[status(thm)],[f405]) ).
fof(f412,plain,
( sQ27_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f407,f139]) ).
fof(f413,plain,
sQ27_spl,
inference(contradiction_clause,[status(thm)],[f412]) ).
fof(f432,definition,
( sQ30_spl
<=> r1(sK0_skl,sK65_skl) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f434,plain,
( sQ30_spl
| ~ r1(sK0_skl,sK65_skl) ),
inference(component_clause,[status(thm)],[f432]) ).
fof(f439,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f434,f137]) ).
fof(f440,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f439]) ).
fof(f462,definition,
( sQ35_spl
<=> r1(sK0_skl,sK68_skl) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( sQ35_spl
| ~ r1(sK0_skl,sK68_skl) ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f471,plain,
( sQ35_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f143]) ).
fof(f472,plain,
sQ35_spl,
inference(contradiction_clause,[status(thm)],[f471]) ).
fof(f505,plain,
! [X0] :
( sQ5_spl
| p1(sK62_skl(sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl)
| ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),X0))
| ~ r1(X0,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f225,f117]) ).
fof(f506,definition,
! [X0] :
( sQ42_spl
<=> ( ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),X0))
| ~ r1(X0,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition]) ).
fof(f507,plain,
! [X0] :
( ~ sQ42_spl
| ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),X0))
| ~ r1(X0,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f506]) ).
fof(f509,plain,
( sQ5_spl
| sQ16_spl
| ~ sQ15_spl
| ~ sQ4_spl
| sQ42_spl ),
inference(split_clause,[status(thm)],[f505,f506,f214,f295,f298,f217]) ).
fof(f510,plain,
( ~ sQ15_spl
| ~ sQ42_spl
| ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f507,f296]) ).
fof(f512,definition,
( sQ43_spl
<=> p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition]) ).
fof(f514,plain,
( sQ43_spl
| ~ p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f512]) ).
fof(f515,plain,
( ~ sQ15_spl
| ~ sQ42_spl
| ~ sQ43_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f510,f214,f512,f506,f295]) ).
fof(f518,plain,
! [X0,X1,X2] :
( sQ43_spl
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),X2,X1,X0))
| ~ r1(X2,sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f514,f54]) ).
fof(f808,definition,
( sQ77_spl
<=> r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f809,plain,
( ~ sQ77_spl
| r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f810,plain,
( sQ77_spl
| ~ r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f808]) ).
fof(f1372,plain,
! [X0,X1] :
( sQ5_spl
| sQ43_spl
| ~ r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl)
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),X1,X0))
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f518,f230]) ).
fof(f1373,definition,
! [X0,X1] :
( sQ153_spl
<=> ( ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),X1,X0))
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f1374,plain,
! [X0,X1] :
( ~ sQ153_spl
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),X1,X0))
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f1373]) ).
fof(f1376,plain,
( sQ5_spl
| sQ43_spl
| ~ sQ77_spl
| ~ sQ15_spl
| ~ sQ4_spl
| sQ153_spl ),
inference(split_clause,[status(thm)],[f1372,f1373,f214,f295,f808,f512,f217]) ).
fof(f1377,plain,
( sQ77_spl
| p1(sK62_skl(sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f810,f117]) ).
fof(f1378,plain,
( sQ77_spl
| sQ16_spl
| ~ sQ15_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1377,f214,f295,f298,f808]) ).
fof(f1390,plain,
! [X0] :
( ~ sQ77_spl
| ~ sQ153_spl
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),X0))
| ~ r1(X0,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1374,f809]) ).
fof(f1396,plain,
( ~ sQ15_spl
| ~ sQ77_spl
| ~ sQ153_spl
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f1390,f296]) ).
fof(f1398,definition,
( sQ155_spl
<=> p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ155_spl])],[split_symbol_definition]) ).
fof(f1400,plain,
( sQ155_spl
| ~ p4(sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f1398]) ).
fof(f1401,plain,
( ~ sQ15_spl
| ~ sQ77_spl
| ~ sQ153_spl
| ~ sQ155_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1396,f214,f1398,f1373,f808,f295]) ).
fof(f1422,plain,
! [X0,X1,X2,X3] :
( sQ155_spl
| ~ r1(X3,sK23_skl(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1400,f6]) ).
fof(f1456,plain,
! [X0,X1,X2] :
( sQ155_spl
| p1(sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl)
| ~ r1(X2,sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1422,f53]) ).
fof(f1457,definition,
! [X0,X1,X2] :
( sQ164_spl
<=> ( ~ r1(X2,sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ164_spl])],[split_symbol_definition]) ).
fof(f1458,plain,
! [X0,X1,X2] :
( ~ sQ164_spl
| ~ r1(X2,sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f1457]) ).
fof(f1460,definition,
( sQ165_spl
<=> r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
introduced(definition,[new_symbols(definition,[sQ165_spl])],[split_symbol_definition]) ).
fof(f1462,plain,
( sQ165_spl
| ~ r1(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK34_skl(sK55_skl(sK62_skl(sK67_skl),sK67_skl),sK62_skl(sK67_skl),sK67_skl)) ),
inference(component_clause,[status(thm)],[f1460]) ).
fof(f1463,plain,
( sQ155_spl
| sQ43_spl
| ~ sQ165_spl
| ~ sQ77_spl
| ~ sQ15_spl
| ~ sQ4_spl
| sQ164_spl ),
inference(split_clause,[status(thm)],[f1456,f1457,f214,f295,f808,f1460,f512,f1398]) ).
fof(f1464,plain,
! [X0,X1] :
( sQ5_spl
| ~ sQ164_spl
| ~ r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl)
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1458,f230]) ).
fof(f1465,definition,
! [X0,X1] :
( sQ166_spl
<=> ( ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ166_spl])],[split_symbol_definition]) ).
fof(f1466,plain,
! [X0,X1] :
( ~ sQ166_spl
| ~ r1(X1,sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f1465]) ).
fof(f1468,plain,
( sQ5_spl
| ~ sQ164_spl
| ~ sQ77_spl
| ~ sQ15_spl
| ~ sQ4_spl
| sQ166_spl ),
inference(split_clause,[status(thm)],[f1464,f1465,f214,f295,f808,f1457,f217]) ).
fof(f1469,plain,
! [X0] :
( ~ sQ77_spl
| ~ sQ166_spl
| ~ r1(X0,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1466,f809]) ).
fof(f1475,plain,
( ~ sQ15_spl
| ~ sQ77_spl
| ~ sQ166_spl
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f1469,f296]) ).
fof(f1477,plain,
( ~ sQ15_spl
| ~ sQ77_spl
| ~ sQ166_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1475,f214,f1465,f808,f295]) ).
fof(f1505,plain,
( sQ165_spl
| sQ5_spl
| ~ r1(sK62_skl(sK67_skl),sK55_skl(sK62_skl(sK67_skl),sK67_skl))
| ~ r1(sK67_skl,sK62_skl(sK67_skl))
| ~ r1(sK0_skl,sK67_skl) ),
inference(resolution,[status(thm)],[f230,f1462]) ).
fof(f1507,plain,
( sQ165_spl
| sQ5_spl
| ~ sQ77_spl
| ~ sQ15_spl
| ~ sQ4_spl ),
inference(split_clause,[status(thm)],[f1505,f214,f295,f808,f217,f1460]) ).
fof(f1509,plain,
$false,
inference(sat_refutation,[status(thm)],[f220,f222,f306,f308,f317,f413,f440,f472,f509,f515,f1376,f1378,f1401,f1463,f1468,f1477,f1507]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL646+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n001.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 00:50:13 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.19/0.51 % Drodi V4.1.1
% 16.55/2.68 % Refutation found
% 16.55/2.68 % SZS status Theorem for theBenchmark: Theorem is valid
% 16.55/2.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 1.90/2.73 % Elapsed time: 2.251876 seconds
% 1.90/2.73 % CPU time: 17.217395 seconds
% 1.90/2.73 % Total memory used: 88.376 MB
% 1.90/2.73 % Net memory used: 81.123 MB
%------------------------------------------------------------------------------