%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL638+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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:08:05 PM UTC 2026
% Result : Theorem 48.21s 6.59s
% Output : CNFRefutation 48.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 6
% Syntax : Number of formulae : 57 ( 9 unt; 5 def)
% Number of atoms : 1767 ( 0 equ)
% Maximal formula atoms : 225 ( 31 avg)
% Number of connectives : 3143 (1433 ~;1240 |; 465 &)
% ( 5 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 13 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 9 ( 7 usr; 2 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 26 con; 0-7 aty)
% Number of variables : 1276 (1050 !; 226 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X] :
~ ( ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ 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] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ! [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) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [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) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
~ ~ ? [X] :
~ ( ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ 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] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ! [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) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ! [Y] :
( $false
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
& ~ ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [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) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ ( ~ p1(X)
& ~ ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) ) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( p1(X)
| ~ r1(Y,X) )
| p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ! [X] :
( $false
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ ( ~ p1(Y)
& ~ ! [X] :
( ~ ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) ) )
| ~ 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] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ! [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) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [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) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f4,definition,
! [Y,X] :
( sP0_prd(X,Y)
<=> ( p1(X)
& r1(Y,X) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f5,definition,
! [X,Y] :
( sP1_prd(Y,X)
<=> ( p1(Y)
& r1(X,Y) ) ),
introduced(definition,[new_symbols(definition,[sP1_prd])],[]) ).
fof(f6,definition,
! [Y,X] :
( sP2_prd(X,Y)
<=> ( p1(X)
& r1(Y,X) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f7,definition,
! [X,Y] :
( sP3_prd(Y,X)
<=> ( p1(Y)
& r1(X,Y) ) ),
introduced(definition,[new_symbols(definition,[sP3_prd])],[]) ).
fof(f8,definition,
! [Y,X] :
( sP4_prd(X,Y)
<=> ( p1(X)
& r1(Y,X) ) ),
introduced(definition,[new_symbols(definition,[sP4_prd])],[]) ).
fof(f9,plain,
? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP4_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP3_prd(Y,X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP2_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( $true
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP1_prd(Y,X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( $true
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP0_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
inference(formula_renaming,[status(thm)],[f3,f8,f7,f6,f5,f4]) ).
fof(f10,plain,
? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP4_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ( $true
& ? [Y] : r1(X,Y) )
| ~ r1(Y,X) )
| ~ 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] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP3_prd(Y,X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP2_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( $true
& ? [Y] : r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(Y,X) )
& r1(X,Y) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP1_prd(Y,X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
& ~ p1(Y)
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& r1(Y,X) )
& r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ( $true
& ? [X] : r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(X)
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(X,Y) )
& r1(Y,X) )
| ! [X] :
( ! [Y] :
( ? [X] : sP0_prd(X,Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(Y)
& r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f11,plain,
( ! [X] :
( p1(X)
| ~ r1(sK55_skl,X) )
& ~ p1(sK55_skl)
& r1(sK54_skl,sK55_skl)
& r1(sK53_skl,sK54_skl)
& r1(sK52_skl,sK53_skl)
& r1(sK51_skl,sK52_skl)
& r1(sK0_skl,sK51_skl)
& ! [Y] :
( ( $true
& r1(Y,sK50_skl(Y)) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ( ~ p1(sK49_skl(Y))
& r1(Y,sK49_skl(Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ( ! [Y] :
( ~ p1(Y)
| ~ r1(sK48_skl(Y),Y) )
& r1(Y,sK48_skl(Y)) )
| ! [X] :
( ! [Y] :
( sP4_prd(sK47_skl(Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(sK46_skl(X,Y))
& r1(X,sK46_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p1(Y)
| ! [X] :
( ( ~ p1(sK45_skl(X,Y))
& r1(X,sK45_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [X] :
( p1(X)
| ~ r1(sK44_skl,X) )
& ~ p1(sK44_skl)
& r1(sK43_skl,sK44_skl)
& r1(sK42_skl,sK43_skl)
& r1(sK41_skl,sK42_skl)
& r1(sK40_skl,sK41_skl)
& r1(sK0_skl,sK40_skl)
& ! [Y] :
( ! [X] :
( ( $true
& r1(X,sK39_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ( ~ p1(sK38_skl(X,Y))
& r1(X,sK38_skl(X,Y)) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ( ! [X] :
( ~ p1(X)
| ~ r1(sK37_skl(X,Y),X) )
& r1(X,sK37_skl(X,Y)) )
| ! [Y] :
( ! [X] :
( sP3_prd(sK36_skl(X,Y,X,Y),X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ( p1(sK35_skl(Y,X,Y))
& r1(Y,sK35_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ( ~ p1(sK34_skl(Y,X,Y))
& r1(Y,sK34_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [X] :
( p1(X)
| ~ r1(sK33_skl,X) )
& ~ p1(sK33_skl)
& r1(sK32_skl,sK33_skl)
& r1(sK31_skl,sK32_skl)
& r1(sK30_skl,sK31_skl)
& r1(sK29_skl,sK30_skl)
& r1(sK0_skl,sK29_skl)
& ! [Y] :
( ! [X] :
( ! [Y] :
( ( $true
& r1(Y,sK28_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ( ~ p1(sK27_skl(Y,X,Y))
& r1(Y,sK27_skl(Y,X,Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ( ! [Y] :
( ~ p1(Y)
| ~ r1(sK26_skl(Y,X,Y),Y) )
& r1(Y,sK26_skl(Y,X,Y)) )
| ! [X] :
( ! [Y] :
( sP2_prd(sK25_skl(Y,X,Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(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] :
( p1(Y)
| ! [X] :
( ( ~ p1(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) )
& ! [X] :
( p1(X)
| ~ r1(sK22_skl,X) )
& ~ p1(sK22_skl)
& r1(sK21_skl,sK22_skl)
& r1(sK20_skl,sK21_skl)
& r1(sK19_skl,sK20_skl)
& r1(sK18_skl,sK19_skl)
& r1(sK0_skl,sK18_skl)
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( $true
& r1(X,sK17_skl(X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( ~ p1(sK16_skl(X,Y,X,Y))
& r1(X,sK16_skl(X,Y,X,Y)) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ( ! [X] :
( ~ p1(X)
| ~ r1(sK15_skl(X,Y,X,Y),X) )
& r1(X,sK15_skl(X,Y,X,Y)) )
| ! [Y] :
( ! [X] :
( sP1_prd(sK14_skl(X,Y,X,Y,X,Y),X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ( p1(sK13_skl(Y,X,Y,X,Y))
& r1(Y,sK13_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ( ~ p1(sK12_skl(Y,X,Y,X,Y))
& r1(Y,sK12_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [X] :
( p1(X)
| ~ r1(sK11_skl,X) )
& ~ p1(sK11_skl)
& r1(sK10_skl,sK11_skl)
& r1(sK9_skl,sK10_skl)
& r1(sK8_skl,sK9_skl)
& r1(sK7_skl,sK8_skl)
& r1(sK0_skl,sK7_skl)
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ( $true
& r1(Y,sK6_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ( ~ p1(sK5_skl(Y,X,Y,X,Y))
& r1(Y,sK5_skl(Y,X,Y,X,Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ( ! [Y] :
( ~ p1(Y)
| ~ r1(sK4_skl(Y,X,Y,X,Y),Y) )
& r1(Y,sK4_skl(Y,X,Y,X,Y)) )
| ! [X] :
( ! [Y] :
( sP0_prd(sK3_skl(Y,X,Y,X,Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ( p1(sK2_skl(X,Y,X,Y,X,Y))
& r1(X,sK2_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [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) )
| ~ 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]),skolemize(X,sK0_skl),skolemize(Y,sK1_skl(X,Y,X,Y,X,Y)),skolemize(Y,sK2_skl(X,Y,X,Y,X,Y)),skolemize(X,sK3_skl(Y,X,Y,X,Y,X,Y)),skolemize(X,sK4_skl(Y,X,Y,X,Y)),skolemize(X,sK5_skl(Y,X,Y,X,Y)),skolemize(X,sK6_skl(Y,X,Y,X,Y)),skolemize(Y,sK7_skl),skolemize(X,sK8_skl),skolemize(Y,sK9_skl),skolemize(X,sK10_skl),skolemize(Y,sK11_skl),skolemize(X,sK12_skl(Y,X,Y,X,Y)),skolemize(X,sK13_skl(Y,X,Y,X,Y)),skolemize(Y,sK14_skl(X,Y,X,Y,X,Y)),skolemize(Y,sK15_skl(X,Y,X,Y)),skolemize(Y,sK16_skl(X,Y,X,Y)),skolemize(Y,sK17_skl(X,Y,X,Y)),skolemize(Y,sK18_skl),skolemize(X,sK19_skl),skolemize(Y,sK20_skl),skolemize(X,sK21_skl),skolemize(Y,sK22_skl),skolemize(Y,sK23_skl(X,Y,X,Y)),skolemize(Y,sK24_skl(X,Y,X,Y)),skolemize(X,sK25_skl(Y,X,Y,X,Y)),skolemize(X,sK26_skl(Y,X,Y)),skolemize(X,sK27_skl(Y,X,Y)),skolemize(X,sK28_skl(Y,X,Y)),skolemize(Y,sK29_skl),skolemize(X,sK30_skl),skolemize(Y,sK31_skl),skolemize(X,sK32_skl),skolemize(Y,sK33_skl),skolemize(X,sK34_skl(Y,X,Y)),skolemize(X,sK35_skl(Y,X,Y)),skolemize(Y,sK36_skl(X,Y,X,Y)),skolemize(Y,sK37_skl(X,Y)),skolemize(Y,sK38_skl(X,Y)),skolemize(Y,sK39_skl(X,Y)),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)),skolemize(Y,sK46_skl(X,Y)),skolemize(X,sK47_skl(Y,X,Y)),skolemize(X,sK48_skl(Y)),skolemize(X,sK49_skl(Y)),skolemize(X,sK50_skl(Y)),skolemize(Y,sK51_skl),skolemize(X,sK52_skl),skolemize(Y,sK53_skl),skolemize(X,sK54_skl),skolemize(Y,sK55_skl)],[f10]) ).
fof(f12,plain,
? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK55_skl,X) )
& ~ p1(sK55_skl)
& r1(sK54_skl,sK55_skl) )
& r1(sK53_skl,sK54_skl) )
& r1(sK52_skl,sK53_skl) )
& r1(sK51_skl,sK52_skl) )
& r1(sK0_skl,sK51_skl) )
& ! [Y] :
( ? [X] : r1(Y,sK50_skl(Y))
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ? [X] :
( ~ p1(sK49_skl(Y))
& r1(Y,sK49_skl(Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(sK48_skl(Y),Y) )
& r1(Y,sK48_skl(Y)) )
| ! [X] :
( ! [Y] :
( ? [X] : sP4_prd(sK47_skl(Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(sK46_skl(X,Y))
& r1(X,sK46_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(sK45_skl(X,Y))
& r1(X,sK45_skl(X,Y)) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK44_skl,X) )
& ~ p1(sK44_skl)
& r1(sK43_skl,sK44_skl) )
& r1(sK42_skl,sK43_skl) )
& r1(sK41_skl,sK42_skl) )
& r1(sK40_skl,sK41_skl) )
& r1(sK0_skl,sK40_skl) )
& ! [Y] :
( ! [X] :
( ? [Y] : r1(X,sK39_skl(X,Y))
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ? [Y] :
( ~ p1(sK38_skl(X,Y))
& r1(X,sK38_skl(X,Y)) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(sK37_skl(X,Y),X) )
& r1(X,sK37_skl(X,Y)) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP3_prd(sK36_skl(X,Y,X,Y),X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(sK35_skl(Y,X,Y))
& r1(Y,sK35_skl(Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ 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] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK33_skl,X) )
& ~ p1(sK33_skl)
& r1(sK32_skl,sK33_skl) )
& r1(sK31_skl,sK32_skl) )
& r1(sK30_skl,sK31_skl) )
& r1(sK29_skl,sK30_skl) )
& r1(sK0_skl,sK29_skl) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] : r1(Y,sK28_skl(Y,X,Y))
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(sK27_skl(Y,X,Y))
& r1(Y,sK27_skl(Y,X,Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(sK26_skl(Y,X,Y),Y) )
& r1(Y,sK26_skl(Y,X,Y)) )
| ! [X] :
( ! [Y] :
( ? [X] : sP2_prd(sK25_skl(Y,X,Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(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] :
( p1(Y)
| ! [X] :
( ? [Y] :
( ~ p1(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] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK22_skl,X) )
& ~ p1(sK22_skl)
& r1(sK21_skl,sK22_skl) )
& r1(sK20_skl,sK21_skl) )
& r1(sK19_skl,sK20_skl) )
& r1(sK18_skl,sK19_skl) )
& r1(sK0_skl,sK18_skl) )
& ! [Y] :
( ! [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] :
( ! [X] :
( ? [Y] :
( ~ p1(sK16_skl(X,Y,X,Y))
& r1(X,sK16_skl(X,Y,X,Y)) )
| ! [Y] :
( ! [X] :
( p1(X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ? [Y] :
( ! [X] :
( ~ p1(X)
| ~ r1(sK15_skl(X,Y,X,Y),X) )
& r1(X,sK15_skl(X,Y,X,Y)) )
| ! [Y] :
( ! [X] :
( ? [Y] : sP1_prd(sK14_skl(X,Y,X,Y,X,Y),X)
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ~ p1(X)
| ! [Y] :
( ? [X] :
( p1(sK13_skl(Y,X,Y,X,Y))
& r1(Y,sK13_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( p1(X)
| ! [Y] :
( ? [X] :
( ~ p1(sK12_skl(Y,X,Y,X,Y))
& r1(Y,sK12_skl(Y,X,Y,X,Y)) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ? [Y] :
( ? [X] :
( ? [Y] :
( ? [X] :
( ? [Y] :
( ! [X] :
( p1(X)
| ~ r1(sK11_skl,X) )
& ~ p1(sK11_skl)
& r1(sK10_skl,sK11_skl) )
& r1(sK9_skl,sK10_skl) )
& r1(sK8_skl,sK9_skl) )
& r1(sK7_skl,sK8_skl) )
& r1(sK0_skl,sK7_skl) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] : r1(Y,sK6_skl(Y,X,Y,X,Y))
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ~ p1(sK5_skl(Y,X,Y,X,Y))
& r1(Y,sK5_skl(Y,X,Y,X,Y)) )
| ! [X] :
( ! [Y] :
( p1(Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ? [X] :
( ! [Y] :
( ~ p1(Y)
| ~ r1(sK4_skl(Y,X,Y,X,Y),Y) )
& r1(Y,sK4_skl(Y,X,Y,X,Y)) )
| ! [X] :
( ! [Y] :
( ? [X] : sP0_prd(sK3_skl(Y,X,Y,X,Y,X,Y),Y)
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [Y] :
( ~ p1(Y)
| ! [X] :
( ? [Y] :
( p1(sK2_skl(X,Y,X,Y,X,Y))
& r1(X,sK2_skl(X,Y,X,Y,X,Y)) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) )
& ! [Y] :
( ! [X] :
( ! [Y] :
( ! [X] :
( ! [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) )
| ~ r1(Y,X) )
| ~ r1(X,Y) )
| ~ r1(Y,X) )
| ~ r1(sK0_skl,Y) ) ),
inference(true_and_false_simplification,[status(thm)],[f11]) ).
fof(f13,plain,
! [X0,X1,X2,X3,X4,X5] :
( p1(X4)
| r1(X5,sK1_skl(X5,X4,X3,X2,X1,X0))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f14,plain,
! [X0,X1,X2,X3,X4,X5] :
( p1(X4)
| ~ p1(sK1_skl(X5,X4,X3,X2,X1,X0))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f19,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( r1(X4,sK5_skl(X4,X3,X2,X1,X0))
| p1(X6)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f20,plain,
! [X0,X1,X2,X3,X4,X5,X6] :
( ~ p1(sK5_skl(X4,X3,X2,X1,X0))
| p1(X6)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f29,plain,
! [X0,X1,X2,X3,X4] :
( p1(X3)
| r1(X4,sK12_skl(X4,X3,X2,X1,X0))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f30,plain,
! [X0,X1,X2,X3,X4] :
( p1(X3)
| ~ p1(sK12_skl(X4,X3,X2,X1,X0))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f31,plain,
! [X0,X1,X2,X3,X4] :
( ~ p1(X3)
| r1(X4,sK13_skl(X4,X3,X2,X1,X0))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f86,plain,
r1(sK0_skl,sK51_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f87,plain,
r1(sK51_skl,sK52_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f88,plain,
r1(sK52_skl,sK53_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f89,plain,
r1(sK53_skl,sK54_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f90,plain,
r1(sK54_skl,sK55_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f91,plain,
~ p1(sK55_skl),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f92,plain,
! [X0] :
( p1(X0)
| ~ r1(sK55_skl,X0) ),
inference(cnf_transformation,[status(thm)],[f12]) ).
fof(f133,plain,
! [X0,X1,X2,X3,X4,X5] :
( p1(sK5_skl(sK55_skl,X3,X2,X1,X0))
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK55_skl,X4)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f19,f92]) ).
fof(f178,plain,
! [X0,X1,X2,X3] :
( p1(sK12_skl(sK55_skl,X3,X2,X1,X0))
| p1(X3)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f29,f92]) ).
fof(f331,plain,
! [X0,X1,X2,X3,X4,X5] :
( p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK55_skl,X4)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f133,f20]) ).
fof(f332,plain,
! [X0,X1,X2,X3,X4] :
( p1(X4)
| ~ r1(X3,X4)
| ~ r1(sK55_skl,X3)
| ~ r1(X2,sK54_skl)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f331,f90]) ).
fof(f333,plain,
! [X0,X1,X2,X3] :
( p1(X3)
| ~ r1(X2,X3)
| ~ r1(sK55_skl,X2)
| ~ r1(X1,sK53_skl)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f332,f89]) ).
fof(f334,plain,
! [X0,X1,X2] :
( p1(X2)
| ~ r1(X1,X2)
| ~ r1(sK55_skl,X1)
| ~ r1(X0,sK52_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f333,f88]) ).
fof(f335,plain,
! [X0,X1] :
( p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK55_skl,X0)
| ~ r1(sK0_skl,sK51_skl) ),
inference(resolution,[status(thm)],[f334,f87]) ).
fof(f336,plain,
! [X0,X1] :
( p1(X1)
| ~ r1(X0,X1)
| ~ r1(sK55_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f335,f86]) ).
fof(f481,plain,
! [X0,X1,X2,X3] :
( p1(X3)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f178,f30]) ).
fof(f482,plain,
! [X0,X1,X2] :
( p1(sK54_skl)
| ~ r1(X2,sK54_skl)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f481,f90]) ).
fof(f483,plain,
! [X0,X1] :
( p1(sK54_skl)
| ~ r1(X1,sK53_skl)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f482,f89]) ).
fof(f484,plain,
! [X0] :
( p1(sK54_skl)
| ~ r1(X0,sK52_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f483,f88]) ).
fof(f485,plain,
( p1(sK54_skl)
| ~ r1(sK0_skl,sK51_skl) ),
inference(resolution,[status(thm)],[f484,f87]) ).
fof(f486,plain,
p1(sK54_skl),
inference(forward_subsumption_resolution,[status(thm)],[f485,f86]) ).
fof(f497,plain,
! [X0,X1,X2,X3] :
( r1(X3,sK13_skl(X3,sK54_skl,X2,X1,X0))
| ~ r1(sK54_skl,X3)
| ~ r1(X2,sK54_skl)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f486,f31]) ).
fof(f1108,plain,
! [X0,X1,X2] :
( r1(X2,sK13_skl(X2,sK54_skl,sK53_skl,X1,X0))
| ~ r1(sK54_skl,X2)
| ~ r1(X1,sK53_skl)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f497,f89]) ).
fof(f1111,plain,
! [X0,X1] :
( r1(X1,sK13_skl(X1,sK54_skl,sK53_skl,sK52_skl,X0))
| ~ r1(sK54_skl,X1)
| ~ r1(X0,sK52_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1108,f88]) ).
fof(f1112,plain,
! [X0] :
( r1(X0,sK13_skl(X0,sK54_skl,sK53_skl,sK52_skl,sK51_skl))
| ~ r1(sK54_skl,X0)
| ~ r1(sK0_skl,sK51_skl) ),
inference(resolution,[status(thm)],[f1111,f87]) ).
fof(f1113,plain,
! [X0] :
( r1(X0,sK13_skl(X0,sK54_skl,sK53_skl,sK52_skl,sK51_skl))
| ~ r1(sK54_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1112,f86]) ).
fof(f1114,plain,
! [X0] :
( p1(X0)
| ~ r1(sK13_skl(sK55_skl,sK54_skl,sK53_skl,sK52_skl,sK51_skl),X0)
| ~ r1(sK54_skl,sK55_skl) ),
inference(resolution,[status(thm)],[f1113,f336]) ).
fof(f1129,plain,
! [X0] :
( p1(X0)
| ~ r1(sK13_skl(sK55_skl,sK54_skl,sK53_skl,sK52_skl,sK51_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1114,f90]) ).
fof(f1159,plain,
! [X0,X1,X2,X3,X4] :
( p1(X0)
| ~ r1(X0,sK13_skl(sK55_skl,sK54_skl,sK53_skl,sK52_skl,sK51_skl))
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(sK0_skl,X4)
| p1(sK1_skl(sK13_skl(sK55_skl,sK54_skl,sK53_skl,sK52_skl,sK51_skl),X0,X1,X2,X3,X4)) ),
inference(resolution,[status(thm)],[f1129,f13]) ).
fof(f1169,plain,
! [X0,X1,X2,X3,X4] :
( p1(X4)
| ~ r1(X4,sK13_skl(sK55_skl,sK54_skl,sK53_skl,sK52_skl,sK51_skl))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1159,f14]) ).
fof(f1890,plain,
! [X0,X1,X2,X3] :
( ~ r1(sK54_skl,sK55_skl)
| p1(sK55_skl)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1169,f1113]) ).
fof(f1891,plain,
! [X0,X1,X2,X3] :
( ~ r1(sK54_skl,sK55_skl)
| ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1890,f91]) ).
fof(f1892,plain,
! [X0,X1,X2,X3] :
( ~ r1(X3,sK55_skl)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f1891,f90]) ).
fof(f1893,plain,
! [X0,X1,X2] :
( ~ r1(X2,sK54_skl)
| ~ r1(X1,X2)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1892,f90]) ).
fof(f1894,plain,
! [X0,X1] :
( ~ r1(X1,sK53_skl)
| ~ r1(X0,X1)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1893,f89]) ).
fof(f1895,plain,
! [X0] :
( ~ r1(X0,sK52_skl)
| ~ r1(sK0_skl,X0) ),
inference(resolution,[status(thm)],[f1894,f88]) ).
fof(f1896,plain,
~ r1(sK0_skl,sK51_skl),
inference(resolution,[status(thm)],[f1895,f87]) ).
fof(f1897,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f1896,f86]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL638+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n018.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 00:44:28 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 48.21/6.59 % Refutation found
% 48.21/6.59 % SZS status Theorem for theBenchmark: Theorem is valid
% 48.21/6.59 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.19/6.63 % Elapsed time: 6.243744 seconds
% 9.19/6.63 % CPU time: 48.971597 seconds
% 9.19/6.63 % Total memory used: 106.773 MB
% 9.19/6.63 % Net memory used: 88.703 MB
%------------------------------------------------------------------------------