%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL672+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 : n009.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:30 PM UTC 2026
% Result : Theorem 8.16s 1.66s
% Output : CNFRefutation 8.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 10
% Syntax : Number of formulae : 68 ( 19 unt; 7 def)
% Number of atoms : 3535 ( 0 equ)
% Maximal formula atoms : 545 ( 51 avg)
% Number of connectives : 6054 (2587 ~;2437 |;1022 &)
% ( 7 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 166 ( 13 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 9 prp; 0-2 aty)
% Number of functors : 111 ( 111 usr; 86 con; 0-7 aty)
% Number of variables : 1993 (1658 !; 335 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] : r1(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
! [X,Y,Z] :
( ( r1(Y,Z)
& r1(X,Y) )
=> r1(X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,conjecture,
~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
~ ~ ? [X] :
~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ~ ( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
& ~ ! [X] :
( p2(X)
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
& ~ ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[status(thm)],[f1]) ).
fof(f6,plain,
! [X,Y,Z] :
( r1(X,Z)
| ~ r1(Y,Z)
| ~ r1(X,Y) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f7,plain,
! [X,Z] :
( r1(X,Z)
| ! [Y] :
( ~ r1(Y,Z)
| ~ r1(X,Y) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f9,plain,
? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
inference(pre_NNF_transformation,[status(thm)],[f4]) ).
fof(f10,plain,
? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( $true
& ? [Y] : r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( $true
& ? [Y] : r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
& ? [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& r1(Y,X) )
& ? [X] :
( ~ p2(X)
& r1(Y,X) )
& r1(X,Y) )
& ? [Y] :
( ~ p2(Y)
& r1(X,Y) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) ) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f11,plain,
( ~ p1(sK110_skl)
& r1(sK0_skl,sK110_skl)
& ~ p1(sK109_skl)
& r1(sK95_skl,sK109_skl)
& ~ p1(sK108_skl)
& r1(sK97_skl,sK108_skl)
& ~ p1(sK107_skl)
& r1(sK99_skl,sK107_skl)
& ~ p1(sK106_skl)
& r1(sK101_skl,sK106_skl)
& ~ p1(sK105_skl)
& r1(sK103_skl,sK105_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK104_skl,Y) )
& r1(sK103_skl,sK104_skl)
& r1(sK101_skl,sK103_skl)
& ~ p2(sK102_skl)
& r1(sK101_skl,sK102_skl)
& r1(sK99_skl,sK101_skl)
& ~ p2(sK100_skl)
& r1(sK99_skl,sK100_skl)
& r1(sK97_skl,sK99_skl)
& ~ p2(sK98_skl)
& r1(sK97_skl,sK98_skl)
& r1(sK95_skl,sK97_skl)
& ~ p2(sK96_skl)
& r1(sK95_skl,sK96_skl)
& r1(sK0_skl,sK95_skl)
& ~ p2(sK94_skl)
& r1(sK0_skl,sK94_skl)
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ( $true
& r1(Y,sK93_skl(Y)) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( ( ~ p1(sK92_skl(X,Y))
& r1(X,sK92_skl(X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ( ! [X] :
( p1(X)
| ~ r1(sK91_skl(X,Y),X) )
& r1(X,sK91_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( ~ p1(sK90_skl(Y,X,Y))
& r1(Y,sK90_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(sK89_skl(X,Y))
& r1(X,sK89_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ~ p1(sK88_skl)
& r1(sK0_skl,sK88_skl)
& ~ p1(sK87_skl)
& r1(sK73_skl,sK87_skl)
& ~ p1(sK86_skl)
& r1(sK75_skl,sK86_skl)
& ~ p1(sK85_skl)
& r1(sK77_skl,sK85_skl)
& ~ p1(sK84_skl)
& r1(sK79_skl,sK84_skl)
& ~ p1(sK83_skl)
& r1(sK81_skl,sK83_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK82_skl,Y) )
& r1(sK81_skl,sK82_skl)
& r1(sK79_skl,sK81_skl)
& ~ p2(sK80_skl)
& r1(sK79_skl,sK80_skl)
& r1(sK77_skl,sK79_skl)
& ~ p2(sK78_skl)
& r1(sK77_skl,sK78_skl)
& r1(sK75_skl,sK77_skl)
& ~ p2(sK76_skl)
& r1(sK75_skl,sK76_skl)
& r1(sK73_skl,sK75_skl)
& ~ p2(sK74_skl)
& r1(sK73_skl,sK74_skl)
& r1(sK0_skl,sK73_skl)
& ~ p2(sK72_skl)
& r1(sK0_skl,sK72_skl)
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( $true
& r1(X,sK71_skl(X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ( ~ p1(sK70_skl(Y,X,Y))
& r1(Y,sK70_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( ( ! [Y] :
( p1(Y)
| ~ r1(sK69_skl(Y,X,Y),Y) )
& r1(Y,sK69_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( ~ p1(sK68_skl(X,Y,X,Y))
& r1(X,sK68_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ( p1(sK67_skl(Y,X,Y))
& r1(Y,sK67_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ~ p1(sK66_skl)
& r1(sK0_skl,sK66_skl)
& ~ p1(sK65_skl)
& r1(sK51_skl,sK65_skl)
& ~ p1(sK64_skl)
& r1(sK53_skl,sK64_skl)
& ~ p1(sK63_skl)
& r1(sK55_skl,sK63_skl)
& ~ p1(sK62_skl)
& r1(sK57_skl,sK62_skl)
& ~ p1(sK61_skl)
& r1(sK59_skl,sK61_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK60_skl,Y) )
& r1(sK59_skl,sK60_skl)
& r1(sK57_skl,sK59_skl)
& ~ p2(sK58_skl)
& r1(sK57_skl,sK58_skl)
& r1(sK55_skl,sK57_skl)
& ~ p2(sK56_skl)
& r1(sK55_skl,sK56_skl)
& r1(sK53_skl,sK55_skl)
& ~ p2(sK54_skl)
& r1(sK53_skl,sK54_skl)
& r1(sK51_skl,sK53_skl)
& ~ p2(sK52_skl)
& r1(sK51_skl,sK52_skl)
& r1(sK0_skl,sK51_skl)
& ~ p2(sK50_skl)
& r1(sK0_skl,sK50_skl)
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( $true
& r1(Y,sK49_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ( ~ p1(sK48_skl(X,Y,X,Y))
& r1(X,sK48_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ( ! [X] :
( p1(X)
| ~ r1(sK47_skl(X,Y,X,Y),X) )
& r1(X,sK47_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( ~ p1(sK46_skl(Y,X,Y,X,Y))
& r1(Y,sK46_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(sK45_skl(X,Y,X,Y))
& r1(X,sK45_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ~ p1(sK44_skl)
& r1(sK0_skl,sK44_skl)
& ~ p1(sK43_skl)
& r1(sK29_skl,sK43_skl)
& ~ p1(sK42_skl)
& r1(sK31_skl,sK42_skl)
& ~ p1(sK41_skl)
& r1(sK33_skl,sK41_skl)
& ~ p1(sK40_skl)
& r1(sK35_skl,sK40_skl)
& ~ p1(sK39_skl)
& r1(sK37_skl,sK39_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK38_skl,Y) )
& r1(sK37_skl,sK38_skl)
& r1(sK35_skl,sK37_skl)
& ~ p2(sK36_skl)
& r1(sK35_skl,sK36_skl)
& r1(sK33_skl,sK35_skl)
& ~ p2(sK34_skl)
& r1(sK33_skl,sK34_skl)
& r1(sK31_skl,sK33_skl)
& ~ p2(sK32_skl)
& r1(sK31_skl,sK32_skl)
& r1(sK29_skl,sK31_skl)
& ~ p2(sK30_skl)
& r1(sK29_skl,sK30_skl)
& r1(sK0_skl,sK29_skl)
& ~ p2(sK28_skl)
& r1(sK0_skl,sK28_skl)
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( $true
& r1(X,sK27_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ( ~ p1(sK26_skl(Y,X,Y,X,Y))
& r1(Y,sK26_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( ( ! [Y] :
( p1(Y)
| ~ r1(sK25_skl(Y,X,Y,X,Y),Y) )
& r1(Y,sK25_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ( ~ p1(sK24_skl(X,Y,X,Y,X,Y))
& r1(X,sK24_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ( p1(sK23_skl(Y,X,Y,X,Y))
& r1(Y,sK23_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ~ p1(sK22_skl)
& r1(sK0_skl,sK22_skl)
& ~ p1(sK21_skl)
& r1(sK7_skl,sK21_skl)
& ~ p1(sK20_skl)
& r1(sK9_skl,sK20_skl)
& ~ p1(sK19_skl)
& r1(sK11_skl,sK19_skl)
& ~ p1(sK18_skl)
& r1(sK13_skl,sK18_skl)
& ~ p1(sK17_skl)
& r1(sK15_skl,sK17_skl)
& ! [Y] :
( p1(Y)
| ~ r1(sK16_skl,Y) )
& r1(sK15_skl,sK16_skl)
& r1(sK13_skl,sK15_skl)
& ~ p2(sK14_skl)
& r1(sK13_skl,sK14_skl)
& r1(sK11_skl,sK13_skl)
& ~ p2(sK12_skl)
& r1(sK11_skl,sK12_skl)
& r1(sK9_skl,sK11_skl)
& ~ p2(sK10_skl)
& r1(sK9_skl,sK10_skl)
& r1(sK7_skl,sK9_skl)
& ~ p2(sK8_skl)
& r1(sK7_skl,sK8_skl)
& r1(sK0_skl,sK7_skl)
& ~ p2(sK6_skl)
& r1(sK0_skl,sK6_skl)
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( $true
& r1(Y,sK5_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ( ~ p1(sK4_skl(X,Y,X,Y,X,Y))
& r1(X,sK4_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ( ! [X] :
( p1(X)
| ~ r1(sK3_skl(X,Y,X,Y,X,Y),X) )
& r1(X,sK3_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ( ~ p1(sK2_skl(Y,X,Y,X,Y,X,Y))
& r1(Y,sK2_skl(Y,X,Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(sK1_skl(X,Y,X,Y,X,Y))
& r1(X,sK1_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ 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,sK69_skl,sK70_skl,sK71_skl,sK72_skl,sK73_skl,sK74_skl,sK75_skl,sK76_skl,sK77_skl,sK78_skl,sK79_skl,sK80_skl,sK81_skl,sK82_skl,sK83_skl,sK84_skl,sK85_skl,sK86_skl,sK87_skl,sK88_skl,sK89_skl,sK90_skl,sK91_skl,sK92_skl,sK93_skl,sK94_skl,sK95_skl,sK96_skl,sK97_skl,sK98_skl,sK99_skl,sK100_skl,sK101_skl,sK102_skl,sK103_skl,sK104_skl,sK105_skl,sK106_skl,sK107_skl,sK108_skl,sK109_skl,sK110_skl]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y,X,Y,X,Y)),skolemize(X,sK2_skl(Y,X,Y,X,Y,X,Y)),skolemize(Y,sK3_skl(X,Y,X,Y,X,Y)),skolemize(Y,sK4_skl(X,Y,X,Y,X,Y)),skolemize(X,sK5_skl(Y,X,Y,X,Y)),skolemize(Y,sK6_skl),skolemize(Y,sK7_skl),skolemize(X,sK8_skl),skolemize(X,sK9_skl),skolemize(Y,sK10_skl),skolemize(Y,sK11_skl),skolemize(X,sK12_skl),skolemize(X,sK13_skl),skolemize(Y,sK14_skl),skolemize(Y,sK15_skl),skolemize(X,sK16_skl),skolemize(X,sK17_skl),skolemize(Y,sK18_skl),skolemize(X,sK19_skl),skolemize(Y,sK20_skl),skolemize(X,sK21_skl),skolemize(Y,sK22_skl),skolemize(X,sK23_skl(Y,X,Y,X,Y)),skolemize(Y,sK24_skl(X,Y,X,Y,X,Y)),skolemize(X,sK25_skl(Y,X,Y,X,Y)),skolemize(X,sK26_skl(Y,X,Y,X,Y)),skolemize(Y,sK27_skl(X,Y,X,Y)),skolemize(Y,sK28_skl),skolemize(Y,sK29_skl),skolemize(X,sK30_skl),skolemize(X,sK31_skl),skolemize(Y,sK32_skl),skolemize(Y,sK33_skl),skolemize(X,sK34_skl),skolemize(X,sK35_skl),skolemize(Y,sK36_skl),skolemize(Y,sK37_skl),skolemize(X,sK38_skl),skolemize(X,sK39_skl),skolemize(Y,sK40_skl),skolemize(X,sK41_skl),skolemize(Y,sK42_skl),skolemize(X,sK43_skl),skolemize(Y,sK44_skl),skolemize(Y,sK45_skl(X,Y,X,Y)),skolemize(X,sK46_skl(Y,X,Y,X,Y)),skolemize(Y,sK47_skl(X,Y,X,Y)),skolemize(Y,sK48_skl(X,Y,X,Y)),skolemize(X,sK49_skl(Y,X,Y)),skolemize(Y,sK50_skl),skolemize(Y,sK51_skl),skolemize(X,sK52_skl),skolemize(X,sK53_skl),skolemize(Y,sK54_skl),skolemize(Y,sK55_skl),skolemize(X,sK56_skl),skolemize(X,sK57_skl),skolemize(Y,sK58_skl),skolemize(Y,sK59_skl),skolemize(X,sK60_skl),skolemize(X,sK61_skl),skolemize(Y,sK62_skl),skolemize(X,sK63_skl),skolemize(Y,sK64_skl),skolemize(X,sK65_skl),skolemize(Y,sK66_skl),skolemize(X,sK67_skl(Y,X,Y)),skolemize(Y,sK68_skl(X,Y,X,Y)),skolemize(X,sK69_skl(Y,X,Y)),skolemize(X,sK70_skl(Y,X,Y)),skolemize(Y,sK71_skl(X,Y)),skolemize(Y,sK72_skl),skolemize(Y,sK73_skl),skolemize(X,sK74_skl),skolemize(X,sK75_skl),skolemize(Y,sK76_skl),skolemize(Y,sK77_skl),skolemize(X,sK78_skl),skolemize(X,sK79_skl),skolemize(Y,sK80_skl),skolemize(Y,sK81_skl),skolemize(X,sK82_skl),skolemize(X,sK83_skl),skolemize(Y,sK84_skl),skolemize(X,sK85_skl),skolemize(Y,sK86_skl),skolemize(X,sK87_skl),skolemize(Y,sK88_skl),skolemize(Y,sK89_skl(X,Y)),skolemize(X,sK90_skl(Y,X,Y)),skolemize(Y,sK91_skl(X,Y)),skolemize(Y,sK92_skl(X,Y)),skolemize(X,sK93_skl(Y)),skolemize(Y,sK94_skl),skolemize(Y,sK95_skl),skolemize(X,sK96_skl),skolemize(X,sK97_skl),skolemize(Y,sK98_skl),skolemize(Y,sK99_skl),skolemize(X,sK100_skl),skolemize(X,sK101_skl),skolemize(Y,sK102_skl),skolemize(Y,sK103_skl),skolemize(X,sK104_skl),skolemize(X,sK105_skl),skolemize(Y,sK106_skl),skolemize(X,sK107_skl),skolemize(Y,sK108_skl),skolemize(X,sK109_skl),skolemize(Y,sK110_skl)],[f10]) ).
fof(f12,plain,
? [X] :
( ? [Y] :
( ~ p1(sK110_skl)
& r1(sK0_skl,sK110_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK109_skl)
& r1(sK95_skl,sK109_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK108_skl)
& r1(sK97_skl,sK108_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK107_skl)
& r1(sK99_skl,sK107_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK106_skl)
& r1(sK101_skl,sK106_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK105_skl)
& r1(sK103_skl,sK105_skl) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK104_skl,Y) )
& r1(sK103_skl,sK104_skl) )
& r1(sK101_skl,sK103_skl) )
& ? [Y] :
( ~ p2(sK102_skl)
& r1(sK101_skl,sK102_skl) )
& r1(sK99_skl,sK101_skl) )
& ? [X] :
( ~ p2(sK100_skl)
& r1(sK99_skl,sK100_skl) )
& r1(sK97_skl,sK99_skl) )
& ? [Y] :
( ~ p2(sK98_skl)
& r1(sK97_skl,sK98_skl) )
& r1(sK95_skl,sK97_skl) )
& ? [X] :
( ~ p2(sK96_skl)
& r1(sK95_skl,sK96_skl) )
& r1(sK0_skl,sK95_skl) )
& ? [Y] :
( ~ p2(sK94_skl)
& r1(sK0_skl,sK94_skl) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ? [X] : r1(Y,sK93_skl(Y))
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(sK92_skl(X,Y))
& r1(X,sK92_skl(X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK91_skl(X,Y),X) )
& r1(X,sK91_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(sK90_skl(Y,X,Y))
& r1(Y,sK90_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(sK89_skl(X,Y))
& r1(X,sK89_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ? [Y] :
( ~ p1(sK88_skl)
& r1(sK0_skl,sK88_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK87_skl)
& r1(sK73_skl,sK87_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK86_skl)
& r1(sK75_skl,sK86_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK85_skl)
& r1(sK77_skl,sK85_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK84_skl)
& r1(sK79_skl,sK84_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK83_skl)
& r1(sK81_skl,sK83_skl) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK82_skl,Y) )
& r1(sK81_skl,sK82_skl) )
& r1(sK79_skl,sK81_skl) )
& ? [Y] :
( ~ p2(sK80_skl)
& r1(sK79_skl,sK80_skl) )
& r1(sK77_skl,sK79_skl) )
& ? [X] :
( ~ p2(sK78_skl)
& r1(sK77_skl,sK78_skl) )
& r1(sK75_skl,sK77_skl) )
& ? [Y] :
( ~ p2(sK76_skl)
& r1(sK75_skl,sK76_skl) )
& r1(sK73_skl,sK75_skl) )
& ? [X] :
( ~ p2(sK74_skl)
& r1(sK73_skl,sK74_skl) )
& r1(sK0_skl,sK73_skl) )
& ? [Y] :
( ~ p2(sK72_skl)
& r1(sK0_skl,sK72_skl) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] : r1(X,sK71_skl(X,Y))
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(sK70_skl(Y,X,Y))
& r1(Y,sK70_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK69_skl(Y,X,Y),Y) )
& r1(Y,sK69_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(sK68_skl(X,Y,X,Y))
& r1(X,sK68_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(sK67_skl(Y,X,Y))
& r1(Y,sK67_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ? [Y] :
( ~ p1(sK66_skl)
& r1(sK0_skl,sK66_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK65_skl)
& r1(sK51_skl,sK65_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK64_skl)
& r1(sK53_skl,sK64_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK63_skl)
& r1(sK55_skl,sK63_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK62_skl)
& r1(sK57_skl,sK62_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK61_skl)
& r1(sK59_skl,sK61_skl) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK60_skl,Y) )
& r1(sK59_skl,sK60_skl) )
& r1(sK57_skl,sK59_skl) )
& ? [Y] :
( ~ p2(sK58_skl)
& r1(sK57_skl,sK58_skl) )
& r1(sK55_skl,sK57_skl) )
& ? [X] :
( ~ p2(sK56_skl)
& r1(sK55_skl,sK56_skl) )
& r1(sK53_skl,sK55_skl) )
& ? [Y] :
( ~ p2(sK54_skl)
& r1(sK53_skl,sK54_skl) )
& r1(sK51_skl,sK53_skl) )
& ? [X] :
( ~ p2(sK52_skl)
& r1(sK51_skl,sK52_skl) )
& r1(sK0_skl,sK51_skl) )
& ? [Y] :
( ~ p2(sK50_skl)
& r1(sK0_skl,sK50_skl) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] : r1(Y,sK49_skl(Y,X,Y))
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(sK48_skl(X,Y,X,Y))
& r1(X,sK48_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK47_skl(X,Y,X,Y),X) )
& r1(X,sK47_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(sK46_skl(Y,X,Y,X,Y))
& r1(Y,sK46_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(sK45_skl(X,Y,X,Y))
& r1(X,sK45_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ? [Y] :
( ~ p1(sK44_skl)
& r1(sK0_skl,sK44_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK43_skl)
& r1(sK29_skl,sK43_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK42_skl)
& r1(sK31_skl,sK42_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK41_skl)
& r1(sK33_skl,sK41_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK40_skl)
& r1(sK35_skl,sK40_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK39_skl)
& r1(sK37_skl,sK39_skl) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK38_skl,Y) )
& r1(sK37_skl,sK38_skl) )
& r1(sK35_skl,sK37_skl) )
& ? [Y] :
( ~ p2(sK36_skl)
& r1(sK35_skl,sK36_skl) )
& r1(sK33_skl,sK35_skl) )
& ? [X] :
( ~ p2(sK34_skl)
& r1(sK33_skl,sK34_skl) )
& r1(sK31_skl,sK33_skl) )
& ? [Y] :
( ~ p2(sK32_skl)
& r1(sK31_skl,sK32_skl) )
& r1(sK29_skl,sK31_skl) )
& ? [X] :
( ~ p2(sK30_skl)
& r1(sK29_skl,sK30_skl) )
& r1(sK0_skl,sK29_skl) )
& ? [Y] :
( ~ p2(sK28_skl)
& r1(sK0_skl,sK28_skl) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] : r1(X,sK27_skl(X,Y,X,Y))
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(sK26_skl(Y,X,Y,X,Y))
& r1(Y,sK26_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK25_skl(Y,X,Y,X,Y),Y) )
& r1(Y,sK25_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ~ p1(sK24_skl(X,Y,X,Y,X,Y))
& r1(X,sK24_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(sK23_skl(Y,X,Y,X,Y))
& r1(Y,sK23_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ? [Y] :
( ~ p1(sK22_skl)
& r1(sK0_skl,sK22_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK21_skl)
& r1(sK7_skl,sK21_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK20_skl)
& r1(sK9_skl,sK20_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK19_skl)
& r1(sK11_skl,sK19_skl) )
& ? [X] :
( ? [Y] :
( ~ p1(sK18_skl)
& r1(sK13_skl,sK18_skl) )
& ? [Y] :
( ? [X] :
( ~ p1(sK17_skl)
& r1(sK15_skl,sK17_skl) )
& ? [X] :
( ! [Y] :
( p1(Y)
| ~ r1(sK16_skl,Y) )
& r1(sK15_skl,sK16_skl) )
& r1(sK13_skl,sK15_skl) )
& ? [Y] :
( ~ p2(sK14_skl)
& r1(sK13_skl,sK14_skl) )
& r1(sK11_skl,sK13_skl) )
& ? [X] :
( ~ p2(sK12_skl)
& r1(sK11_skl,sK12_skl) )
& r1(sK9_skl,sK11_skl) )
& ? [Y] :
( ~ p2(sK10_skl)
& r1(sK9_skl,sK10_skl) )
& r1(sK7_skl,sK9_skl) )
& ? [X] :
( ~ p2(sK8_skl)
& r1(sK7_skl,sK8_skl) )
& r1(sK0_skl,sK7_skl) )
& ? [Y] :
( ~ p2(sK6_skl)
& r1(sK0_skl,sK6_skl) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] : r1(Y,sK5_skl(Y,X,Y,X,Y))
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(sK4_skl(X,Y,X,Y,X,Y))
& r1(X,sK4_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ! [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK3_skl(X,Y,X,Y,X,Y),X) )
& r1(X,sK3_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ? [X] :
( ~ p1(sK2_skl(Y,X,Y,X,Y,X,Y))
& r1(Y,sK2_skl(Y,X,Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) )
& ( ! [Y] :
( p1(Y)
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(sK1_skl(X,Y,X,Y,X,Y))
& r1(X,sK1_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ! [X] :
( p2(X)
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
| ! [Y] :
( p2(Y)
| ~ r1(sK0_skl,Y) ) ) ),
inference(true_and_false_simplification,[status(thm)],[f11]) ).
fof(f129,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( p1(X8)
| ~ r1(sK0_skl,X8)
| p1(X7)
| ~ r1(X1,X7)
| p1(X6)
| ~ r1(X4,X6)
| r1(X5,sK68_skl(X5,X4,X3,X1))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X1,X3)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(sK0_skl,X1)
| p2(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f130,plain,
! [X0,X1,X2,X3,X4,X5,X6,X7,X8] :
( p1(X8)
| ~ r1(sK0_skl,X8)
| p1(X7)
| ~ r1(X1,X7)
| p1(X6)
| ~ r1(X4,X6)
| ~ p1(sK68_skl(X5,X4,X3,X1))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X1,X3)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(sK0_skl,X1)
| p2(X0)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f174,plain,
r1(sK0_skl,sK94_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f175,plain,
~ p2(sK94_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f176,plain,
r1(sK0_skl,sK95_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f179,plain,
r1(sK95_skl,sK97_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f182,plain,
r1(sK97_skl,sK99_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f185,plain,
r1(sK99_skl,sK101_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f188,plain,
r1(sK101_skl,sK103_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f189,plain,
r1(sK103_skl,sK104_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f190,plain,
! [X0] :
( p1(X0)
| ~ r1(sK104_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f191,plain,
r1(sK103_skl,sK105_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f192,plain,
~ p1(sK105_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f201,plain,
r1(sK0_skl,sK110_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f202,plain,
~ p1(sK110_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f203,definition,
! [X0] :
( sQ0_spl
<=> ( p2(X0)
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f204,plain,
! [X0] :
( ~ sQ0_spl
| p2(X0)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f203]) ).
fof(f209,definition,
! [X15] :
( sQ2_spl
<=> ( p1(X15)
| ~ r1(sK0_skl,X15) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f210,plain,
! [X0] :
( ~ sQ2_spl
| p1(X0)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f209]) ).
fof(f325,definition,
! [X1,X2,X3,X4,X5,X6,X7] :
( sQ31_spl
<=> ( p1(X7)
| ~ r1(X1,X7)
| p1(X6)
| ~ r1(X4,X6)
| r1(X5,sK68_skl(X5,X4,X3,X1))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X1,X3)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(sK0_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition]) ).
fof(f326,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ31_spl
| p1(X6)
| ~ r1(X0,X6)
| p1(X5)
| ~ r1(X3,X5)
| r1(X4,sK68_skl(X4,X3,X2,X0))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f325]) ).
fof(f328,plain,
( sQ2_spl
| sQ31_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f129,f203,f325,f209]) ).
fof(f329,definition,
! [X1,X2,X3,X4,X5,X6,X7] :
( sQ32_spl
<=> ( p1(X7)
| ~ r1(X1,X7)
| p1(X6)
| ~ r1(X4,X6)
| ~ p1(sK68_skl(X5,X4,X3,X1))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X1,X3)
| p2(X2)
| ~ r1(X1,X2)
| ~ r1(sK0_skl,X1) ) ),
introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition]) ).
fof(f330,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ sQ32_spl
| p1(X6)
| ~ r1(X0,X6)
| p1(X5)
| ~ r1(X3,X5)
| ~ p1(sK68_skl(X4,X3,X2,X0))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f329]) ).
fof(f332,plain,
( sQ2_spl
| sQ32_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f130,f203,f329,f209]) ).
fof(f399,plain,
( ~ sQ2_spl
| p1(sK110_skl) ),
inference(resolution,[status(thm)],[f210,f201]) ).
fof(f416,plain,
( ~ sQ2_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f399,f202]) ).
fof(f417,plain,
~ sQ2_spl,
inference(contradiction_clause,[status(thm)],[f416]) ).
fof(f420,plain,
( ~ sQ0_spl
| p2(sK94_skl) ),
inference(resolution,[status(thm)],[f204,f174]) ).
fof(f435,plain,
( ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f420,f175]) ).
fof(f436,plain,
~ sQ0_spl,
inference(contradiction_clause,[status(thm)],[f435]) ).
fof(f462,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ31_spl
| p1(sK68_skl(sK104_skl,X3,X2,X0))
| p1(X5)
| ~ r1(X0,X5)
| p1(X4)
| ~ r1(X3,X4)
| ~ r1(X3,sK104_skl)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f326,f190]) ).
fof(f467,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ sQ31_spl
| ~ sQ32_spl
| p1(X5)
| ~ r1(X0,X5)
| p1(X4)
| ~ r1(X3,X4)
| ~ r1(X3,sK104_skl)
| ~ r1(X2,X3)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f462,f330]) ).
fof(f472,plain,
! [X0,X1,X2,X3,X4] :
( ~ sQ31_spl
| ~ sQ32_spl
| p1(X4)
| ~ r1(X0,X4)
| p1(X3)
| ~ r1(sK103_skl,X3)
| ~ r1(X2,sK103_skl)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f467,f189]) ).
fof(f475,definition,
! [X0,X1,X2,X4] :
( sQ47_spl
<=> ( p1(X4)
| ~ r1(X0,X4)
| ~ r1(X2,sK103_skl)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f476,plain,
! [X0,X1,X2,X3] :
( ~ sQ47_spl
| p1(X3)
| ~ r1(X0,X3)
| ~ r1(X2,sK103_skl)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f478,definition,
! [X3] :
( sQ48_spl
<=> ( p1(X3)
| ~ r1(sK103_skl,X3) ) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f479,plain,
! [X0] :
( ~ sQ48_spl
| p1(X0)
| ~ r1(sK103_skl,X0) ),
inference(component_clause,[status(thm)],[f478]) ).
fof(f481,plain,
( ~ sQ31_spl
| ~ sQ32_spl
| sQ48_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f472,f475,f478,f329,f325]) ).
fof(f489,plain,
! [X0,X1,X2] :
( ~ sQ47_spl
| p1(X2)
| ~ r1(X0,X2)
| ~ r1(X0,sK101_skl)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f476,f188]) ).
fof(f493,plain,
! [X0,X1,X2,X3] :
( ~ sQ47_spl
| ~ r1(X3,sK101_skl)
| ~ r1(X0,X3)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f489,f8]) ).
fof(f714,plain,
( ~ sQ48_spl
| p1(sK105_skl) ),
inference(resolution,[status(thm)],[f479,f191]) ).
fof(f732,plain,
( ~ sQ48_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f714,f192]) ).
fof(f733,plain,
~ sQ48_spl,
inference(contradiction_clause,[status(thm)],[f732]) ).
fof(f1071,plain,
! [X0,X1,X2] :
( ~ sQ47_spl
| ~ r1(X0,sK99_skl)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f493,f185]) ).
fof(f1075,plain,
! [X0,X1,X2,X3] :
( ~ sQ47_spl
| ~ r1(X3,sK99_skl)
| ~ r1(X0,X3)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1071,f8]) ).
fof(f1111,plain,
! [X0,X1,X2] :
( ~ sQ47_spl
| ~ r1(X0,sK97_skl)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1075,f182]) ).
fof(f1115,plain,
! [X0,X1,X2,X3] :
( ~ sQ47_spl
| ~ r1(X3,sK97_skl)
| ~ r1(X0,X3)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1111,f8]) ).
fof(f1149,plain,
! [X0,X1,X2] :
( ~ sQ47_spl
| ~ r1(X0,sK95_skl)
| p1(X2)
| ~ r1(X0,X2)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1115,f179]) ).
fof(f1152,plain,
! [X0,X1] :
( ~ sQ47_spl
| p1(X1)
| ~ r1(sK0_skl,X1)
| p2(X0)
| ~ r1(sK0_skl,X0)
| ~ r1(sK0_skl,sK0_skl) ),
inference(resolution,[status(thm)],[f1149,f176]) ).
fof(f1155,definition,
( sQ108_spl
<=> r1(sK0_skl,sK0_skl) ),
introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition]) ).
fof(f1157,plain,
( sQ108_spl
| ~ r1(sK0_skl,sK0_skl) ),
inference(component_clause,[status(thm)],[f1155]) ).
fof(f1158,plain,
( ~ sQ47_spl
| sQ2_spl
| sQ0_spl
| ~ sQ108_spl ),
inference(split_clause,[status(thm)],[f1152,f1155,f203,f209,f475]) ).
fof(f1160,plain,
( sQ108_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1157,f5]) ).
fof(f1161,plain,
sQ108_spl,
inference(contradiction_clause,[status(thm)],[f1160]) ).
fof(f1162,plain,
$false,
inference(sat_refutation,[status(thm)],[f328,f332,f417,f436,f481,f733,f1158,f1161]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL672+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.15/0.39 % Computer : n009.cluster.edu
% 0.15/0.39 % Model : x86_64 x86_64
% 0.15/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.39 % Memory : 8046.5625MB
% 0.15/0.39 % OS : Linux 6.8.0-71-generic
% 0.15/0.40 % CPULimit : 300
% 0.15/0.40 % WCLimit : 300
% 0.15/0.40 % DateTime : Mon Sep 21 00:52:57 UTC 2026
% 0.15/0.40 % CPUTime :
% 0.19/0.44 % Drodi V4.1.1
% 8.16/1.66 % Refutation found
% 8.16/1.66 % SZS status Theorem for theBenchmark: Theorem is valid
% 8.16/1.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 8.26/1.70 % Elapsed time: 1.278343 seconds
% 8.26/1.70 % CPU time: 9.552172 seconds
% 8.26/1.70 % Total memory used: 41.567 MB
% 8.26/1.70 % Net memory used: 38.777 MB
%------------------------------------------------------------------------------