%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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 : Tue Sep 29 11:53:43 AM UTC 2026
% Result : Theorem 4.71s 1.67s
% Output : Refutation 6.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 30
% Syntax : Number of formulae : 340 ( 34 unt; 29 def)
% Number of atoms : 3477 ( 0 equ)
% Maximal formula atoms : 239 ( 10 avg)
% Number of connectives : 5652 (2515 ~;2618 |; 494 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 47 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 26 prp; 0-2 aty)
% Number of functors : 46 ( 46 usr; 9 con; 0-1 aty)
% Number of variables : 1800 ( 0 sgn1603 !; 197 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| p1(X11) ) )
| ~ ! [X12] :
( ~ r1(X9,X12)
| p1(X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ~ ! [X18] :
( ~ r1(X15,X18)
| p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X26,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ~ ! [X51] :
( ~ r1(X48,X51)
| p1(X51) ) ) ) ) ) ) ) ) ) )
| ~ ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) )
| ~ p1(X60) ) )
| ~ ! [X62] :
( ~ r1(X57,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p1(X63) )
| ~ p1(X62)
| ~ ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ~ ( ! [X67] :
( ~ r1(X64,X67)
| p1(X67) )
| ~ p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ~ ! [X70] :
( ~ r1(X57,X70)
| p1(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ~ ! [X76] :
( ~ r1(X73,X76)
| p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| p1(X80) )
| ~ p1(X79) ) ) )
| ~ ! [X81] :
( ~ r1(X57,X81)
| p1(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90) )
| ! [X91] :
( ~ r1(X89,X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
| ~ ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p1(X95) )
| ~ p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| p1(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ~ ! [X109] :
( ~ r1(X106,X109)
| p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| p1(X115) ) )
| ~ ! [X116] :
( ~ r1(X113,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ~ ! [X122] :
( ~ r1(X119,X122)
| p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p1(X127) ) )
| ~ ! [X128] :
( ~ r1(X125,X128)
| p1(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ~ ! [X134] :
( ~ r1(X131,X134)
| p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p1(X138) ) )
| ~ ! [X139] :
( ~ r1(X136,X139)
| p1(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ~ ! [X148] :
( ~ r1(X147,X148)
| p1(X148) ) )
| ~ ! [X149] :
( ~ r1(X146,X149)
| p1(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ~ ! [X155] :
( ~ r1(X152,X155)
| p1(X155) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| p1(X11) ) )
| ~ ! [X12] :
( ~ r1(X9,X12)
| p1(X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ~ ! [X18] :
( ~ r1(X15,X18)
| p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X26,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ~ ! [X51] :
( ~ r1(X48,X51)
| p1(X51) ) ) ) ) ) ) ) ) ) )
| ~ ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) )
| ~ p1(X60) ) )
| ~ ! [X62] :
( ~ r1(X57,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p1(X63) )
| ~ p1(X62)
| ~ ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ~ ( ! [X67] :
( ~ r1(X64,X67)
| p1(X67) )
| ~ p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ~ ! [X70] :
( ~ r1(X57,X70)
| p1(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ~ ! [X76] :
( ~ r1(X73,X76)
| p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| p1(X80) )
| ~ p1(X79) ) ) )
| ~ ! [X81] :
( ~ r1(X57,X81)
| p1(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90) )
| ! [X91] :
( ~ r1(X89,X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
| ~ ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p1(X95) )
| ~ p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| p1(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ~ ! [X109] :
( ~ r1(X106,X109)
| p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| p1(X115) ) )
| ~ ! [X116] :
( ~ r1(X113,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ~ ! [X122] :
( ~ r1(X119,X122)
| p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p1(X127) ) )
| ~ ! [X128] :
( ~ r1(X125,X128)
| p1(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ~ ! [X134] :
( ~ r1(X131,X134)
| p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p1(X138) ) )
| ~ ! [X139] :
( ~ r1(X136,X139)
| p1(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ~ ! [X148] :
( ~ r1(X147,X148)
| p1(X148) ) )
| ~ ! [X149] :
( ~ r1(X146,X149)
| p1(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ~ ! [X155] :
( ~ r1(X152,X155)
| p1(X155) ) ) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X57] :
( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ~ sP0(X57) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X57] :
( ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) )
| ~ sP1(X57) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X57] :
( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) )
| ~ sP2(X57) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X57] :
( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| sP1(X57)
| ~ sP3(X57) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( sP0(X57)
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X57] :
( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| sP1(X57)
| ~ sP3(X57) ),
inference(nnf_transformation,[],[f10]) ).
fof(f13,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(rectify,[],[f12]) ).
fof(f14,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ( r1(X2,sK4(X2))
& r1(sK4(X2),sK5(X2))
& ~ p1(sK5(X2))
& p1(sK4(X2)) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f13]) ).
fof(f15,plain,
! [X57] :
( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) )
| ~ sP2(X57) ),
inference(nnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ~ p1(X2) ) )
| ? [X3] :
( r1(X0,X3)
& ~ p1(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f15]) ).
fof(f17,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK6(X1))
& ~ p1(sK6(X1)) ) )
| ( r1(X0,sK7(X0))
& ~ p1(sK7(X0))
& ! [X4] :
( ~ r1(sK7(X0),X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f16]) ).
fof(f18,plain,
! [X57] :
( ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) )
| ~ sP1(X57) ),
inference(nnf_transformation,[],[f8]) ).
fof(f19,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p1(X2) )
& p1(X1)
& ! [X3] :
( ~ r1(X1,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( ? [X6] :
( r1(X3,X6)
& ~ p1(X6) )
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ( r1(X0,sK8(X0))
& r1(sK8(X0),sK9(X0))
& ~ p1(sK9(X0))
& p1(sK8(X0))
& ! [X3] :
( ~ r1(sK8(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( r1(X3,sK10(X3))
& ~ p1(sK10(X3))
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f19]) ).
fof(f21,plain,
! [X57] :
( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ~ sP0(X57) ),
inference(nnf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ( r1(X2,sK11(X2))
& r1(sK11(X2),sK12(X2))
& ~ p1(sK12(X2))
& p1(sK11(X2)) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f22]) ).
fof(f24,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60) ) )
| ? [X61] :
( r1(X58,X61)
& ~ p1(X61) ) )
& ( sP0(X57)
| ? [X62] :
( r1(X57,X62)
& ~ p1(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p1(X64) )
| ~ p1(X63) ) ) ) ) ) ) ) ) ) )
& ? [X65] :
( r1(X0,X65)
& ? [X66] :
( r1(X65,X66)
& ? [X67] :
( r1(X66,X67)
& ? [X68] :
( r1(X67,X68)
& ? [X69] :
( r1(X68,X69)
& ? [X70] :
( r1(X69,X70)
& ? [X71] :
( r1(X70,X71)
& ~ p1(X71) )
& ? [X72] :
( r1(X70,X72)
& ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X70,X74)
| p1(X74)
| ? [X75] :
( r1(X74,X75)
& ? [X76] :
( r1(X75,X76)
& ~ p1(X76) )
& p1(X75) ) ) ) ) ) ) ) )
& ! [X77] :
( ~ r1(X0,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ( ( p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| ? [X83] :
( r1(X82,X83)
& ~ p1(X83) ) )
| ? [X84] :
( r1(X81,X84)
& ~ p1(X84)
& ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) )
| ~ p1(X85) ) ) )
& ! [X87] :
( ~ r1(X81,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| p1(X89) ) )
| ? [X90] :
( r1(X87,X90)
& ~ p1(X90) ) ) ) ) ) ) ) )
& ! [X91] :
( ~ r1(X0,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ( ( p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| ? [X96] :
( r1(X95,X96)
& ~ p1(X96) ) )
| ? [X97] :
( r1(X94,X97)
& ~ p1(X97)
& ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) ) )
& ! [X100] :
( ~ r1(X94,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103) ) ) ) ) ) ) )
& ! [X104] :
( ~ r1(X0,X104)
| ! [X105] :
( ~ r1(X104,X105)
| ! [X106] :
( ~ r1(X105,X106)
| ( ( p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| ? [X108] :
( r1(X107,X108)
& ~ p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109)
& ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| p1(X111) )
| ~ p1(X110) ) ) )
& ! [X112] :
( ~ r1(X106,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| p1(X114) ) )
| ? [X115] :
( r1(X112,X115)
& ~ p1(X115) ) ) ) ) ) )
& ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,X117)
| ( ( p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| ? [X119] :
( r1(X118,X119)
& ~ p1(X119) ) )
| ? [X120] :
( r1(X117,X120)
& ~ p1(X120)
& ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) )
| ~ p1(X121) ) ) )
& ! [X123] :
( ~ r1(X117,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ? [X126] :
( r1(X123,X126)
& ~ p1(X126) ) ) ) ) )
& ! [X127] :
( ~ r1(X0,X127)
| ( ( p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| ? [X129] :
( r1(X128,X129)
& ~ p1(X129) ) )
| ? [X130] :
( r1(X127,X130)
& ~ p1(X130)
& ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131) ) ) )
& ! [X133] :
( ~ r1(X127,X133)
| ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) ) )
| ? [X136] :
( r1(X133,X136)
& ~ p1(X136) ) ) ) ) ),
inference(rectify,[],[f11]) ).
fof(f25,plain,
( ! [X1] :
( ~ r1(sK13,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( r1(X10,sK14(X10))
& ~ p1(sK14(X10)) ) )
| ( r1(X9,sK15(X9))
& ~ p1(sK15(X9))
& ! [X13] :
( ~ r1(sK15(X9),X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ( r1(X15,sK16(X15))
& ~ p1(sK16(X15)) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(sK13,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ( r1(X27,sK17(X27))
& ~ p1(sK17(X27)) ) )
| ( r1(X26,sK18(X26))
& ~ p1(sK18(X26))
& ! [X30] :
( ~ r1(sK18(X26),X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ( r1(X32,sK19(X32))
& ~ p1(sK19(X32)) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(sK13,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ( r1(X43,sK20(X43))
& ~ p1(sK20(X43)) ) )
| ( r1(X42,sK21(X42))
& ~ p1(sK21(X42))
& ! [X46] :
( ~ r1(sK21(X42),X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ( r1(X48,sK22(X48))
& ~ p1(sK22(X48)) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(sK13,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60) ) )
| ( r1(X58,sK23(X58))
& ~ p1(sK23(X58)) ) )
& ( sP0(X57)
| ( r1(X57,sK24(X57))
& ~ p1(sK24(X57))
& ! [X63] :
( ~ r1(sK24(X57),X63)
| ! [X64] :
( ~ r1(X63,X64)
| p1(X64) )
| ~ p1(X63) ) ) ) ) ) ) ) ) ) )
& r1(sK13,sK25)
& r1(sK25,sK26)
& r1(sK26,sK27)
& r1(sK27,sK28)
& r1(sK28,sK29)
& r1(sK29,sK30)
& r1(sK30,sK31)
& ~ p1(sK31)
& r1(sK30,sK32)
& ! [X73] :
( ~ r1(sK32,X73)
| p1(X73) )
& ! [X74] :
( ~ r1(sK30,X74)
| p1(X74)
| ( r1(X74,sK33(X74))
& r1(sK33(X74),sK34(X74))
& ~ p1(sK34(X74))
& p1(sK33(X74)) ) )
& ! [X77] :
( ~ r1(sK13,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ( ( p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| ( r1(X82,sK35(X82))
& ~ p1(sK35(X82)) ) )
| ( r1(X81,sK36(X81))
& ~ p1(sK36(X81))
& ! [X85] :
( ~ r1(sK36(X81),X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) )
| ~ p1(X85) ) ) )
& ! [X87] :
( ~ r1(X81,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| p1(X89) ) )
| ( r1(X87,sK37(X87))
& ~ p1(sK37(X87)) ) ) ) ) ) ) ) )
& ! [X91] :
( ~ r1(sK13,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ( ( p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( r1(X95,sK38(X95))
& ~ p1(sK38(X95)) ) )
| ( r1(X94,sK39(X94))
& ~ p1(sK39(X94))
& ! [X98] :
( ~ r1(sK39(X94),X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) ) )
& ! [X100] :
( ~ r1(X94,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ( r1(X100,sK40(X100))
& ~ p1(sK40(X100)) ) ) ) ) ) ) )
& ! [X104] :
( ~ r1(sK13,X104)
| ! [X105] :
( ~ r1(X104,X105)
| ! [X106] :
( ~ r1(X105,X106)
| ( ( p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| ( r1(X107,sK41(X107))
& ~ p1(sK41(X107)) ) )
| ( r1(X106,sK42(X106))
& ~ p1(sK42(X106))
& ! [X110] :
( ~ r1(sK42(X106),X110)
| ! [X111] :
( ~ r1(X110,X111)
| p1(X111) )
| ~ p1(X110) ) ) )
& ! [X112] :
( ~ r1(X106,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| p1(X114) ) )
| ( r1(X112,sK43(X112))
& ~ p1(sK43(X112)) ) ) ) ) ) )
& ! [X116] :
( ~ r1(sK13,X116)
| ! [X117] :
( ~ r1(X116,X117)
| ( ( p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| ( r1(X118,sK44(X118))
& ~ p1(sK44(X118)) ) )
| ( r1(X117,sK45(X117))
& ~ p1(sK45(X117))
& ! [X121] :
( ~ r1(sK45(X117),X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) )
| ~ p1(X121) ) ) )
& ! [X123] :
( ~ r1(X117,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ( r1(X123,sK46(X123))
& ~ p1(sK46(X123)) ) ) ) ) )
& ! [X127] :
( ~ r1(sK13,X127)
| ( ( p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| ( r1(X128,sK47(X128))
& ~ p1(sK47(X128)) ) )
| ( r1(X127,sK48(X127))
& ~ p1(sK48(X127))
& ! [X131] :
( ~ r1(sK48(X127),X131)
| ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131) ) ) )
& ! [X133] :
( ~ r1(X127,X133)
| ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) ) )
| ( r1(X133,sK49(X133))
& ~ p1(sK49(X133)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49]),skolemize(X0,sK13),skolemize(X11,sK14(X10)),skolemize(X12,sK15(X9)),skolemize(X18,sK16(X15)),skolemize(X28,sK17(X27)),skolemize(X29,sK18(X26)),skolemize(X35,sK19(X32)),skolemize(X44,sK20(X43)),skolemize(X45,sK21(X42)),skolemize(X51,sK22(X48)),skolemize(X61,sK23(X58)),skolemize(X62,sK24(X57)),skolemize(X65,sK25),skolemize(X66,sK26),skolemize(X67,sK27),skolemize(X68,sK28),skolemize(X69,sK29),skolemize(X70,sK30),skolemize(X71,sK31),skolemize(X72,sK32),skolemize(X75,sK33(X74)),skolemize(X76,sK34(X74)),skolemize(X83,sK35(X82)),skolemize(X84,sK36(X81)),skolemize(X90,sK37(X87)),skolemize(X96,sK38(X95)),skolemize(X97,sK39(X94)),skolemize(X103,sK40(X100)),skolemize(X108,sK41(X107)),skolemize(X109,sK42(X106)),skolemize(X115,sK43(X112)),skolemize(X119,sK44(X118)),skolemize(X120,sK45(X117)),skolemize(X126,sK46(X123)),skolemize(X129,sK47(X128)),skolemize(X130,sK48(X127)),skolemize(X136,sK49(X133))],[f24]) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ p1(sK5(X2))
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1)
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(sK4(X2),sK5(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(X2,sK4(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f30,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f31,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0,X1] :
( ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f34,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f35,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
! [X3,X0,X4,X5] :
( ~ r1(sK8(X0),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f40,plain,
! [X0] :
( ~ p1(sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f41,plain,
! [X0] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X0] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| p1(sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ p1(sK12(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f87,plain,
! [X74] :
( ~ r1(sK30,X74)
| p1(X74)
| p1(sK33(X74)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f88,plain,
! [X74] :
( ~ p1(sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f89,plain,
! [X74] :
( r1(sK33(X74),sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f90,plain,
! [X74] :
( r1(X74,sK33(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f91,plain,
! [X73] :
( ~ r1(sK32,X73)
| p1(X73) ),
inference(cnf_transformation,[],[f25]) ).
fof(f92,plain,
r1(sK30,sK32),
inference(cnf_transformation,[],[f25]) ).
fof(f93,plain,
~ p1(sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f94,plain,
r1(sK30,sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f95,plain,
r1(sK29,sK30),
inference(cnf_transformation,[],[f25]) ).
fof(f96,plain,
r1(sK28,sK29),
inference(cnf_transformation,[],[f25]) ).
fof(f97,plain,
r1(sK27,sK28),
inference(cnf_transformation,[],[f25]) ).
fof(f98,plain,
r1(sK26,sK27),
inference(cnf_transformation,[],[f25]) ).
fof(f99,plain,
r1(sK25,sK26),
inference(cnf_transformation,[],[f25]) ).
fof(f100,plain,
r1(sK13,sK25),
inference(cnf_transformation,[],[f25]) ).
fof(f101,plain,
! [X56,X54,X57,X55,X52,X63,X53,X64] :
( ~ r1(sK24(X57),X63)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| ~ r1(sK13,X52)
| ~ r1(X63,X64)
| p1(X64)
| ~ p1(X63) ),
inference(cnf_transformation,[],[f25]) ).
fof(f102,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ p1(sK24(X57))
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f103,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| r1(X57,sK24(X57)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f104,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( ~ p1(sK23(X58))
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f105,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| r1(X58,sK23(X58)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f106,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP2(X57) ),
inference(cnf_transformation,[],[f25]) ).
fof(f107,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP3(X57) ),
inference(cnf_transformation,[],[f25]) ).
fof(f139,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30))
| ~ sP2(sK30) ),
inference(resolution,[],[f35,f92]) ).
fof(f141,definition,
( spl50_1
<=> sP2(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_1])],[avatar_definition]) ).
fof(f142,plain,
( sP2(sK30)
| ~ spl50_1 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f143,plain,
( ~ sP2(sK30)
| spl50_1 ),
inference(avatar_component_clause,[],[f141]) ).
fof(f145,definition,
( spl50_2
<=> r1(sK30,sK7(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_2])],[avatar_definition]) ).
fof(f146,plain,
( ~ r1(sK30,sK7(sK30))
| spl50_2 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f147,plain,
( r1(sK30,sK7(sK30))
| ~ spl50_2 ),
inference(avatar_component_clause,[],[f145]) ).
fof(f149,definition,
( spl50_3
<=> r1(sK32,sK6(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_3])],[avatar_definition]) ).
fof(f150,plain,
( ~ r1(sK32,sK6(sK32))
| spl50_3 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f151,plain,
( r1(sK32,sK6(sK32))
| ~ spl50_3 ),
inference(avatar_component_clause,[],[f149]) ).
fof(f153,definition,
( spl50_4
<=> p1(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_4])],[avatar_definition]) ).
fof(f154,plain,
( ~ p1(sK30)
| spl50_4 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f155,plain,
( p1(sK30)
| ~ spl50_4 ),
inference(avatar_component_clause,[],[f153]) ).
fof(f156,plain,
( ~ spl50_1
| spl50_2
| spl50_3
| spl50_4 ),
inference(avatar_split_clause,[],[f139,f153,f149,f145,f141]) ).
fof(f354,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f45]) ).
fof(f355,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f43]) ).
fof(f356,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f46]) ).
fof(f358,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f356,f40]) ).
fof(f359,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f355,f40]) ).
fof(f360,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f354,f40]) ).
fof(f361,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f36,f41]) ).
fof(f362,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0) ),
inference(duplicate_literal_removal,[],[f361]) ).
fof(f363,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f362,f40]) ).
fof(f374,plain,
! [X0] :
( p1(X0)
| ~ p1(sK30)
| ~ r1(sK30,X0)
| r1(sK32,sK4(sK32))
| sP1(sK30)
| ~ sP3(sK30) ),
inference(resolution,[],[f29,f92]) ).
fof(f375,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK32,sK4(sK32))
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_4 ),
inference(forward_subsumption_resolution,[],[f374,f155]) ).
fof(f400,definition,
( spl50_50
<=> sP3(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_50])],[avatar_definition]) ).
fof(f401,plain,
( sP3(sK30)
| ~ spl50_50 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f402,plain,
( ~ sP3(sK30)
| spl50_50 ),
inference(avatar_component_clause,[],[f400]) ).
fof(f404,definition,
( spl50_51
<=> sP1(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_51])],[avatar_definition]) ).
fof(f405,plain,
( ~ sP1(sK30)
| spl50_51 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f406,plain,
( sP1(sK30)
| ~ spl50_51 ),
inference(avatar_component_clause,[],[f404]) ).
fof(f408,definition,
( spl50_52
<=> r1(sK32,sK4(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_52])],[avatar_definition]) ).
fof(f410,plain,
( r1(sK32,sK4(sK32))
| ~ spl50_52 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f412,definition,
( spl50_53
<=> ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_53])],[avatar_definition]) ).
fof(f413,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| p1(X0) )
| ~ spl50_53 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f414,plain,
( ~ spl50_50
| spl50_51
| spl50_52
| spl50_53
| ~ spl50_4 ),
inference(avatar_split_clause,[],[f375,f153,f412,f408,f404,f400]) ).
fof(f500,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP3(X4) ),
inference(resolution,[],[f107,f100]) ).
fof(f516,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP2(X4) ),
inference(resolution,[],[f106,f100]) ).
fof(f534,plain,
! [X2,X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK33(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0) ),
inference(resolution,[],[f90,f33]) ).
fof(f546,plain,
! [X2,X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK33(sK7(X0)),X2)
| p1(X2)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f534,f87]) ).
fof(f560,plain,
! [X2,X0,X1] :
( ~ r1(sK33(sK7(X0)),X2)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK30,sK7(X0))
| p1(X2)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f546,f34]) ).
fof(f567,plain,
! [X0] :
( ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f359,f42]) ).
fof(f568,plain,
! [X0] :
( p1(sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f567]) ).
fof(f591,plain,
! [X0] :
( p1(X0)
| ~ p1(sK30)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| sP1(sK30)
| ~ sP3(sK30) ),
inference(resolution,[],[f28,f92]) ).
fof(f594,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(sK33(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK30,sK7(X0)) ),
inference(resolution,[],[f30,f90]) ).
fof(f595,plain,
! [X2,X0,X1] :
( ~ r1(sK33(sK7(X0)),X2)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK30,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f594,f31]) ).
fof(f599,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f358,f42]) ).
fof(f600,plain,
! [X0] :
( r1(sK9(X0),sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f599]) ).
fof(f601,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0)))
| ~ sP1(X0) ),
inference(resolution,[],[f600,f363]) ).
fof(f609,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0))) ),
inference(duplicate_literal_removal,[],[f601]) ).
fof(f611,plain,
! [X0,X1] :
( ~ r1(sK11(sK9(X0)),X1)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(X1) ),
inference(forward_subsumption_resolution,[],[f609,f568]) ).
fof(f614,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f360,f42]) ).
fof(f615,plain,
! [X0] :
( r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f614]) ).
fof(f616,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(sK12(sK9(X0))) ),
inference(resolution,[],[f615,f611]) ).
fof(f624,plain,
! [X0] :
( p1(sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(duplicate_literal_removal,[],[f616]) ).
fof(f625,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X1,sK9(X0))
| p1(sK9(X0))
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(resolution,[],[f624,f44]) ).
fof(f626,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK9(X0))
| ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(forward_subsumption_resolution,[],[f625,f40]) ).
fof(f627,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X1,sK8(X0))
| ~ sP0(X1)
| ~ sP1(X0) ),
inference(resolution,[],[f626,f41]) ).
fof(f628,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP0(X0)
| ~ sP1(X0)
| ~ sP0(X1) ),
inference(duplicate_literal_removal,[],[f627]) ).
fof(f629,plain,
! [X0] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f628,f42]) ).
fof(f630,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f629]) ).
fof(f632,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK34(sK7(X0)))
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK30,sK7(X0)) ),
inference(resolution,[],[f89,f595]) ).
fof(f640,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK34(sK7(X0)))
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0) ),
inference(duplicate_literal_removal,[],[f632]) ).
fof(f648,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f640,f88]) ).
fof(f650,plain,
! [X0,X1] :
( p1(sK7(X0))
| ~ r1(sK30,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f648,f87]) ).
fof(f652,plain,
! [X0,X1] :
( ~ r1(sK30,sK7(X0))
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f650,f31]) ).
fof(f653,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| r1(X4,sK24(X4)) ),
inference(resolution,[],[f103,f100]) ).
fof(f663,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP3(X3) ),
inference(resolution,[],[f500,f99]) ).
fof(f670,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP3(X2) ),
inference(resolution,[],[f663,f98]) ).
fof(f677,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP3(X1) ),
inference(resolution,[],[f670,f97]) ).
fof(f684,plain,
! [X0] :
( ~ r1(sK29,X0)
| sP3(X0) ),
inference(resolution,[],[f677,f96]) ).
fof(f691,plain,
sP3(sK30),
inference(resolution,[],[f684,f95]) ).
fof(f699,plain,
( $false
| spl50_50 ),
inference(forward_subsumption_resolution,[],[f691,f402]) ).
fof(f700,plain,
spl50_50,
inference(avatar_contradiction_clause,[],[f699]) ).
fof(f727,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP2(X3) ),
inference(resolution,[],[f516,f99]) ).
fof(f730,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP2(X2) ),
inference(resolution,[],[f727,f98]) ).
fof(f733,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP2(X1) ),
inference(resolution,[],[f730,f97]) ).
fof(f736,plain,
! [X0] :
( ~ r1(sK29,X0)
| sP2(X0) ),
inference(resolution,[],[f733,f96]) ).
fof(f739,plain,
sP2(sK30),
inference(resolution,[],[f736,f95]) ).
fof(f742,plain,
( $false
| spl50_1 ),
inference(forward_subsumption_resolution,[],[f739,f143]) ).
fof(f743,plain,
spl50_1,
inference(avatar_contradiction_clause,[],[f742]) ).
fof(f787,plain,
( p1(sK6(sK32))
| ~ spl50_3 ),
inference(resolution,[],[f151,f91]) ).
fof(f800,definition,
( spl50_97
<=> p1(sK6(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_97])],[avatar_definition]) ).
fof(f802,plain,
( p1(sK6(sK32))
| ~ spl50_97 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f817,plain,
( spl50_97
| ~ spl50_3 ),
inference(avatar_split_clause,[],[f787,f149,f800]) ).
fof(f818,plain,
( ~ sP0(sK30)
| ~ spl50_51 ),
inference(resolution,[],[f406,f630]) ).
fof(f822,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK30,sK7(X0))
| p1(sK34(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK30,sK7(X0)) ),
inference(resolution,[],[f560,f89]) ).
fof(f825,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK30,sK7(X0))
| p1(sK34(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0)) ),
inference(duplicate_literal_removal,[],[f822]) ).
fof(f826,plain,
! [X0,X1] :
( ~ r1(sK30,sK7(X0))
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(sK34(sK7(X0)))
| ~ sP2(X0) ),
inference(forward_subsumption_resolution,[],[f825,f34]) ).
fof(f827,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK23(X5)) ),
inference(resolution,[],[f105,f100]) ).
fof(f1181,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK23(X4)) ),
inference(resolution,[],[f827,f99]) ).
fof(f1184,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK23(X3)) ),
inference(resolution,[],[f1181,f98]) ).
fof(f1187,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK23(X2)) ),
inference(resolution,[],[f1184,f97]) ).
fof(f1190,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK23(X1)) ),
inference(resolution,[],[f1187,f96]) ).
fof(f1193,plain,
! [X2,X0,X1] :
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK23(X0)) ),
inference(resolution,[],[f1190,f95]) ).
fof(f1197,plain,
! [X0,X1] :
( ~ r1(sK32,X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK32,sK23(sK32)) ),
inference(resolution,[],[f1193,f92]) ).
fof(f1202,definition,
( spl50_148
<=> r1(sK32,sK23(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_148])],[avatar_definition]) ).
fof(f1204,plain,
( r1(sK32,sK23(sK32))
| ~ spl50_148 ),
inference(avatar_component_clause,[],[f1202]) ).
fof(f1206,definition,
( spl50_149
<=> ! [X0,X1] :
( ~ r1(sK32,X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl50_149])],[avatar_definition]) ).
fof(f1207,plain,
( ! [X0,X1] :
( ~ r1(sK32,X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl50_149 ),
inference(avatar_component_clause,[],[f1206]) ).
fof(f1208,plain,
( spl50_148
| spl50_149 ),
inference(avatar_split_clause,[],[f1197,f1206,f1202]) ).
fof(f1225,plain,
( p1(sK31)
| ~ spl50_53 ),
inference(resolution,[],[f413,f94]) ).
fof(f1229,plain,
( $false
| ~ spl50_53 ),
inference(forward_subsumption_resolution,[],[f1225,f93]) ).
fof(f1230,plain,
~ spl50_53,
inference(avatar_contradiction_clause,[],[f1229]) ).
fof(f1233,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_4 ),
inference(forward_subsumption_resolution,[],[f591,f155]) ).
fof(f1237,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| ~ sP3(sK30) )
| ~ spl50_4
| spl50_51 ),
inference(forward_subsumption_resolution,[],[f1233,f405]) ).
fof(f1241,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32)) )
| ~ spl50_4
| ~ spl50_50
| spl50_51 ),
inference(forward_subsumption_resolution,[],[f1237,f401]) ).
fof(f1254,definition,
( spl50_156
<=> r1(sK4(sK32),sK5(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_156])],[avatar_definition]) ).
fof(f1256,plain,
( r1(sK4(sK32),sK5(sK32))
| ~ spl50_156 ),
inference(avatar_component_clause,[],[f1254]) ).
fof(f1257,plain,
( spl50_156
| spl50_53
| ~ spl50_4
| ~ spl50_50
| spl50_51 ),
inference(avatar_split_clause,[],[f1241,f404,f400,f153,f412,f1254]) ).
fof(f1405,plain,
( p1(sK23(sK32))
| ~ spl50_148 ),
inference(resolution,[],[f1204,f91]) ).
fof(f1418,definition,
( spl50_179
<=> p1(sK23(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_179])],[avatar_definition]) ).
fof(f1420,plain,
( p1(sK23(sK32))
| ~ spl50_179 ),
inference(avatar_component_clause,[],[f1418]) ).
fof(f1432,plain,
( spl50_179
| ~ spl50_148 ),
inference(avatar_split_clause,[],[f1405,f1202,f1418]) ).
fof(f1690,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| ~ r1(sK13,X0)
| ~ r1(sK33(sK24(X5)),X6)
| p1(X6)
| ~ p1(sK33(sK24(X5)))
| p1(sK24(X5))
| ~ r1(sK30,sK24(X5)) ),
inference(resolution,[],[f101,f90]) ).
fof(f1695,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK33(sK24(X5)),X6)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(X6)
| ~ p1(sK33(sK24(X5)))
| ~ r1(sK30,sK24(X5)) ),
inference(forward_subsumption_resolution,[],[f1690,f102]) ).
fof(f1697,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ p1(sK33(sK24(X4)))
| ~ r1(sK30,sK24(X4))
| p1(sK24(X4))
| ~ r1(sK30,sK24(X4)) ),
inference(resolution,[],[f1695,f89]) ).
fof(f1704,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ p1(sK33(sK24(X4)))
| ~ r1(sK30,sK24(X4))
| p1(sK24(X4)) ),
inference(duplicate_literal_removal,[],[f1697]) ).
fof(f1706,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ p1(sK33(sK24(X4)))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ r1(X0,X1)
| ~ r1(sK30,sK24(X4)) ),
inference(forward_subsumption_resolution,[],[f1704,f102]) ).
fof(f1707,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP0(X3)
| r1(X3,sK24(X3)) ),
inference(resolution,[],[f653,f99]) ).
fof(f1712,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP0(X2)
| r1(X2,sK24(X2)) ),
inference(resolution,[],[f1707,f98]) ).
fof(f1717,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP0(X1)
| r1(X1,sK24(X1)) ),
inference(resolution,[],[f1712,f97]) ).
fof(f1722,plain,
! [X0] :
( r1(X0,sK24(X0))
| sP0(X0)
| ~ r1(sK29,X0) ),
inference(resolution,[],[f1717,f96]) ).
fof(f1788,plain,
( sP0(sK30)
| ~ r1(sK29,sK30)
| p1(sK24(sK30))
| p1(sK33(sK24(sK30))) ),
inference(resolution,[],[f1722,f87]) ).
fof(f2151,definition,
( spl50_273
<=> p1(sK33(sK24(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_273])],[avatar_definition]) ).
fof(f2153,plain,
( p1(sK33(sK24(sK30)))
| ~ spl50_273 ),
inference(avatar_component_clause,[],[f2151]) ).
fof(f2155,definition,
( spl50_274
<=> p1(sK24(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_274])],[avatar_definition]) ).
fof(f2157,plain,
( p1(sK24(sK30))
| ~ spl50_274 ),
inference(avatar_component_clause,[],[f2155]) ).
fof(f2220,definition,
( spl50_278
<=> p1(sK7(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_278])],[avatar_definition]) ).
fof(f2221,plain,
( ~ p1(sK7(sK30))
| spl50_278 ),
inference(avatar_component_clause,[],[f2220]) ).
fof(f2222,plain,
( p1(sK7(sK30))
| ~ spl50_278 ),
inference(avatar_component_clause,[],[f2220]) ).
fof(f2234,plain,
( sP0(sK30)
| p1(sK24(sK30))
| p1(sK33(sK24(sK30))) ),
inference(forward_subsumption_resolution,[],[f1788,f95]) ).
fof(f2240,definition,
( spl50_281
<=> sP0(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_281])],[avatar_definition]) ).
fof(f2241,plain,
( ~ sP0(sK30)
| spl50_281 ),
inference(avatar_component_clause,[],[f2240]) ).
fof(f2242,plain,
( sP0(sK30)
| ~ spl50_281 ),
inference(avatar_component_clause,[],[f2240]) ).
fof(f2243,plain,
( spl50_273
| spl50_274
| spl50_281 ),
inference(avatar_split_clause,[],[f2234,f2240,f2155,f2151]) ).
fof(f2277,plain,
( ! [X0] :
( ~ r1(sK4(sK32),X0)
| p1(X0) )
| ~ spl50_52
| ~ spl50_149 ),
inference(resolution,[],[f410,f1207]) ).
fof(f2301,definition,
( spl50_286
<=> p1(sK5(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_286])],[avatar_definition]) ).
fof(f2302,plain,
( ~ p1(sK5(sK32))
| spl50_286 ),
inference(avatar_component_clause,[],[f2301]) ).
fof(f2303,plain,
( p1(sK5(sK32))
| ~ spl50_286 ),
inference(avatar_component_clause,[],[f2301]) ).
fof(f2376,plain,
( $false
| ~ spl50_51
| ~ spl50_281 ),
inference(forward_subsumption_resolution,[],[f818,f2242]) ).
fof(f2377,plain,
( ~ spl50_51
| ~ spl50_281 ),
inference(avatar_contradiction_clause,[],[f2376]) ).
fof(f2382,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| sP0(sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0)
| ~ r1(sK30,sK24(sK30)) )
| ~ spl50_273 ),
inference(resolution,[],[f2153,f1706]) ).
fof(f2383,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| sP0(sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0) )
| ~ spl50_273 ),
inference(forward_subsumption_resolution,[],[f2382,f103]) ).
fof(f2384,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0) )
| ~ spl50_273
| spl50_281 ),
inference(forward_subsumption_resolution,[],[f2383,f2241]) ).
fof(f2386,definition,
( spl50_301
<=> p1(sK34(sK24(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_301])],[avatar_definition]) ).
fof(f2388,plain,
( p1(sK34(sK24(sK30)))
| ~ spl50_301 ),
inference(avatar_component_clause,[],[f2386]) ).
fof(f2390,definition,
( spl50_302
<=> ! [X2,X4,X0,X3,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X3)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,sK30)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_302])],[avatar_definition]) ).
fof(f2391,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK13,X3)
| ~ r1(X0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,sK30)
| ~ r1(X1,X2) )
| ~ spl50_302 ),
inference(avatar_component_clause,[],[f2390]) ).
fof(f2392,plain,
( spl50_301
| spl50_302
| ~ spl50_273
| spl50_281 ),
inference(avatar_split_clause,[],[f2384,f2240,f2151,f2390,f2386]) ).
fof(f2393,plain,
( p1(sK24(sK30))
| ~ r1(sK30,sK24(sK30))
| ~ spl50_301 ),
inference(resolution,[],[f2388,f88]) ).
fof(f2395,definition,
( spl50_303
<=> r1(sK30,sK24(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_303])],[avatar_definition]) ).
fof(f2397,plain,
( ~ r1(sK30,sK24(sK30))
| spl50_303 ),
inference(avatar_component_clause,[],[f2395]) ).
fof(f2398,plain,
( ~ spl50_303
| spl50_274
| ~ spl50_301 ),
inference(avatar_split_clause,[],[f2393,f2386,f2155,f2395]) ).
fof(f2399,plain,
( ! [X0,X1] :
( ~ r1(X1,sK32)
| ~ p1(X1)
| p1(X0)
| ~ r1(X1,X0)
| sP1(X1)
| ~ sP3(X1) )
| ~ spl50_286 ),
inference(resolution,[],[f2303,f27]) ).
fof(f2437,plain,
( sP0(sK30)
| ~ r1(sK29,sK30)
| spl50_303 ),
inference(resolution,[],[f2397,f1722]) ).
fof(f2438,plain,
( ~ r1(sK29,sK30)
| spl50_281
| spl50_303 ),
inference(forward_subsumption_resolution,[],[f2437,f2241]) ).
fof(f2439,plain,
( $false
| spl50_281
| spl50_303 ),
inference(forward_subsumption_resolution,[],[f2438,f95]) ).
fof(f2440,plain,
( spl50_281
| spl50_303 ),
inference(avatar_contradiction_clause,[],[f2439]) ).
fof(f2441,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK25,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X3,sK30)
| ~ r1(X1,X3) )
| ~ spl50_302 ),
inference(resolution,[],[f2391,f100]) ).
fof(f2446,plain,
( ! [X2,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK30)
| ~ r1(X1,X2) )
| ~ spl50_302 ),
inference(resolution,[],[f2441,f99]) ).
fof(f2451,plain,
( ! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X1,sK30)
| ~ r1(X0,X1) )
| ~ spl50_302 ),
inference(resolution,[],[f2446,f98]) ).
fof(f2456,plain,
( ! [X0] :
( ~ r1(sK28,X0)
| ~ r1(X0,sK30) )
| ~ spl50_302 ),
inference(resolution,[],[f2451,f97]) ).
fof(f2461,plain,
( ~ r1(sK29,sK30)
| ~ spl50_302 ),
inference(resolution,[],[f2456,f96]) ).
fof(f2466,plain,
( $false
| ~ spl50_302 ),
inference(forward_subsumption_resolution,[],[f2461,f95]) ).
fof(f2467,plain,
~ spl50_302,
inference(avatar_contradiction_clause,[],[f2466]) ).
fof(f2480,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK30)
| sP0(sK30)
| ~ r1(sK13,X0) )
| ~ spl50_274 ),
inference(resolution,[],[f2157,f102]) ).
fof(f2481,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK30)
| ~ r1(sK13,X0) )
| ~ spl50_274
| spl50_281 ),
inference(forward_subsumption_resolution,[],[f2480,f2241]) ).
fof(f2482,plain,
( spl50_302
| ~ spl50_274
| spl50_281 ),
inference(avatar_split_clause,[],[f2481,f2240,f2155,f2390]) ).
fof(f2681,plain,
( p1(sK5(sK32))
| ~ spl50_52
| ~ spl50_149
| ~ spl50_156 ),
inference(resolution,[],[f2277,f1256]) ).
fof(f2873,plain,
( ! [X0] :
( ~ p1(sK30)
| p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_286 ),
inference(resolution,[],[f2399,f92]) ).
fof(f2874,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_4
| ~ spl50_286 ),
inference(forward_subsumption_resolution,[],[f2873,f155]) ).
fof(f2875,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| ~ sP3(sK30) )
| ~ spl50_4
| spl50_51
| ~ spl50_286 ),
inference(forward_subsumption_resolution,[],[f2874,f405]) ).
fof(f2876,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) )
| ~ spl50_4
| ~ spl50_50
| spl50_51
| ~ spl50_286 ),
inference(forward_subsumption_resolution,[],[f2875,f401]) ).
fof(f2877,plain,
( spl50_53
| ~ spl50_4
| ~ spl50_50
| spl50_51
| ~ spl50_286 ),
inference(avatar_split_clause,[],[f2876,f2301,f404,f400,f153,f412]) ).
fof(f2878,plain,
( $false
| ~ spl50_52
| ~ spl50_149
| ~ spl50_156
| spl50_286 ),
inference(forward_subsumption_resolution,[],[f2681,f2302]) ).
fof(f2879,plain,
( ~ spl50_52
| ~ spl50_149
| ~ spl50_156
| spl50_286 ),
inference(avatar_contradiction_clause,[],[f2878]) ).
fof(f2920,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK32)
| ~ r1(sK32,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(sK13,X0) )
| ~ spl50_179 ),
inference(resolution,[],[f1420,f104]) ).
fof(f2922,definition,
( spl50_370
<=> ! [X2,X3,X4,X0,X5,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X5,sK32)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_370])],[avatar_definition]) ).
fof(f2923,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X5,sK32)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl50_370 ),
inference(avatar_component_clause,[],[f2922]) ).
fof(f2924,plain,
( spl50_149
| spl50_370
| ~ spl50_179 ),
inference(avatar_split_clause,[],[f2920,f1418,f2922,f1206]) ).
fof(f2925,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X1,sK32)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X0,X4) )
| ~ spl50_370 ),
inference(resolution,[],[f2923,f100]) ).
fof(f2930,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK26,X3)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X0,sK32) )
| ~ spl50_370 ),
inference(resolution,[],[f2925,f99]) ).
fof(f2935,plain,
( ! [X2,X0,X1] :
( ~ r1(sK27,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK32) )
| ~ spl50_370 ),
inference(resolution,[],[f2930,f98]) ).
fof(f2940,plain,
( ! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK32) )
| ~ spl50_370 ),
inference(resolution,[],[f2935,f97]) ).
fof(f2945,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ r1(X0,sK32) )
| ~ spl50_370 ),
inference(resolution,[],[f2940,f96]) ).
fof(f2950,plain,
( ~ r1(sK30,sK32)
| ~ spl50_370 ),
inference(resolution,[],[f2945,f95]) ).
fof(f2955,plain,
( $false
| ~ spl50_370 ),
inference(forward_subsumption_resolution,[],[f2950,f92]) ).
fof(f2956,plain,
~ spl50_370,
inference(avatar_contradiction_clause,[],[f2955]) ).
fof(f2971,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| p1(sK30)
| ~ r1(sK30,X0)
| ~ sP2(sK30) )
| ~ spl50_2 ),
inference(resolution,[],[f147,f652]) ).
fof(f2986,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0)
| ~ sP2(sK30) )
| ~ spl50_2
| spl50_4 ),
inference(forward_subsumption_resolution,[],[f2971,f154]) ).
fof(f2987,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_1
| ~ spl50_2
| spl50_4 ),
inference(forward_subsumption_resolution,[],[f2986,f142]) ).
fof(f2988,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0))
| p1(sK30)
| ~ sP2(sK30) )
| ~ spl50_278 ),
inference(resolution,[],[f2222,f34]) ).
fof(f2990,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK30) )
| spl50_4
| ~ spl50_278 ),
inference(forward_subsumption_resolution,[],[f2988,f154]) ).
fof(f2991,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_1
| spl50_4
| ~ spl50_278 ),
inference(forward_subsumption_resolution,[],[f2990,f142]) ).
fof(f3072,plain,
( ~ r1(sK30,sK32)
| p1(sK6(sK32))
| ~ spl50_1
| spl50_4
| ~ spl50_278 ),
inference(resolution,[],[f2991,f91]) ).
fof(f3098,plain,
( ~ r1(sK30,sK32)
| ~ spl50_1
| ~ spl50_2
| spl50_4
| ~ spl50_278 ),
inference(forward_subsumption_resolution,[],[f3072,f2987]) ).
fof(f3297,plain,
( $false
| ~ spl50_1
| ~ spl50_2
| spl50_4
| ~ spl50_278 ),
inference(forward_subsumption_resolution,[],[f3098,f92]) ).
fof(f3298,plain,
( ~ spl50_1
| ~ spl50_2
| spl50_4
| ~ spl50_278 ),
inference(avatar_contradiction_clause,[],[f3297]) ).
fof(f3355,plain,
( ! [X0] :
( r1(X0,sK7(X0))
| p1(X0)
| ~ r1(X0,sK32)
| ~ sP2(X0) )
| ~ spl50_97 ),
inference(resolution,[],[f802,f32]) ).
fof(f3418,definition,
( spl50_434
<=> ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl50_434])],[avatar_definition]) ).
fof(f3419,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_434 ),
inference(avatar_component_clause,[],[f3418]) ).
fof(f3422,definition,
( spl50_435
<=> ! [X0] :
( ~ r1(sK30,X0)
| ~ p1(sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl50_435])],[avatar_definition]) ).
fof(f3423,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_435 ),
inference(avatar_component_clause,[],[f3422]) ).
fof(f3521,plain,
( p1(sK30)
| ~ r1(sK30,sK32)
| ~ sP2(sK30)
| spl50_2
| ~ spl50_97 ),
inference(resolution,[],[f3355,f146]) ).
fof(f3522,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,sK32)
| ~ sP2(sK30)
| ~ p1(sK6(X0))
| p1(sK30)
| ~ r1(sK30,X0)
| ~ sP2(sK30) )
| ~ spl50_97 ),
inference(resolution,[],[f3355,f652]) ).
fof(f3546,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,sK32)
| ~ sP2(sK30)
| ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_97 ),
inference(duplicate_literal_removal,[],[f3522]) ).
fof(f3551,plain,
( ! [X0] :
( ~ r1(sK30,sK32)
| ~ sP2(sK30)
| ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3546,f154]) ).
fof(f3552,plain,
( ~ r1(sK30,sK32)
| ~ sP2(sK30)
| spl50_2
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3521,f154]) ).
fof(f3561,plain,
( ! [X0] :
( ~ sP2(sK30)
| ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3551,f92]) ).
fof(f3562,plain,
( ~ sP2(sK30)
| spl50_2
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3552,f92]) ).
fof(f3567,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_1
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3561,f142]) ).
fof(f3568,plain,
( $false
| ~ spl50_1
| spl50_2
| spl50_4
| ~ spl50_97 ),
inference(forward_subsumption_resolution,[],[f3562,f142]) ).
fof(f3569,plain,
( ~ spl50_1
| spl50_2
| spl50_4
| ~ spl50_97 ),
inference(avatar_contradiction_clause,[],[f3568]) ).
fof(f3571,plain,
( spl50_435
| ~ spl50_1
| spl50_4
| ~ spl50_97 ),
inference(avatar_split_clause,[],[f3567,f800,f153,f141,f3422]) ).
fof(f3864,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| p1(sK30)
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ sP2(sK30) )
| ~ spl50_2 ),
inference(resolution,[],[f826,f147]) ).
fof(f3865,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ sP2(sK30) )
| ~ spl50_2
| spl50_4 ),
inference(forward_subsumption_resolution,[],[f3864,f154]) ).
fof(f3866,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30))) )
| ~ spl50_1
| ~ spl50_2
| spl50_4 ),
inference(forward_subsumption_resolution,[],[f3865,f142]) ).
fof(f3868,definition,
( spl50_483
<=> p1(sK34(sK7(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_483])],[avatar_definition]) ).
fof(f3870,plain,
( p1(sK34(sK7(sK30)))
| ~ spl50_483 ),
inference(avatar_component_clause,[],[f3868]) ).
fof(f3871,plain,
( spl50_483
| spl50_434
| ~ spl50_1
| ~ spl50_2
| spl50_4 ),
inference(avatar_split_clause,[],[f3866,f153,f145,f141,f3418,f3868]) ).
fof(f3955,plain,
( ~ r1(sK30,sK32)
| spl50_3
| ~ spl50_434 ),
inference(resolution,[],[f3419,f150]) ).
fof(f3960,plain,
( ~ r1(sK30,sK32)
| p1(sK6(sK32))
| ~ spl50_434 ),
inference(resolution,[],[f3419,f91]) ).
fof(f3976,plain,
( ~ r1(sK30,sK32)
| ~ spl50_434
| ~ spl50_435 ),
inference(forward_subsumption_resolution,[],[f3960,f3423]) ).
fof(f3979,plain,
( $false
| spl50_3
| ~ spl50_434 ),
inference(forward_subsumption_resolution,[],[f3955,f92]) ).
fof(f3980,plain,
( spl50_3
| ~ spl50_434 ),
inference(avatar_contradiction_clause,[],[f3979]) ).
fof(f3990,plain,
( $false
| ~ spl50_434
| ~ spl50_435 ),
inference(forward_subsumption_resolution,[],[f3976,f92]) ).
fof(f3991,plain,
( ~ spl50_434
| ~ spl50_435 ),
inference(avatar_contradiction_clause,[],[f3990]) ).
fof(f3992,plain,
( p1(sK7(sK30))
| ~ r1(sK30,sK7(sK30))
| ~ spl50_483 ),
inference(resolution,[],[f3870,f88]) ).
fof(f3993,plain,
( ~ r1(sK30,sK7(sK30))
| spl50_278
| ~ spl50_483 ),
inference(forward_subsumption_resolution,[],[f3992,f2221]) ).
fof(f3994,plain,
( $false
| ~ spl50_2
| spl50_278
| ~ spl50_483 ),
inference(forward_subsumption_resolution,[],[f3993,f147]) ).
fof(f3995,plain,
( ~ spl50_2
| spl50_278
| ~ spl50_483 ),
inference(avatar_contradiction_clause,[],[f3994]) ).
cnf(s1,plain,
( ~ spl50_1
| spl50_2
| spl50_3
| spl50_4 ),
inference(sat_conversion,[],[f156]) ).
cnf(s18,plain,
( ~ spl50_4
| ~ spl50_50
| spl50_51
| spl50_52
| spl50_53 ),
inference(sat_conversion,[],[f414]) ).
cnf(s34,plain,
spl50_50,
inference(sat_conversion,[],[f700]) ).
cnf(s38,plain,
spl50_1,
inference(sat_conversion,[],[f743]) ).
cnf(s46,plain,
( ~ spl50_3
| spl50_97 ),
inference(sat_conversion,[],[f817]) ).
cnf(s72,plain,
( spl50_148
| spl50_149 ),
inference(sat_conversion,[],[f1208]) ).
cnf(s75,plain,
~ spl50_53,
inference(sat_conversion,[],[f1230]) ).
cnf(s78,plain,
( ~ spl50_4
| ~ spl50_50
| spl50_51
| spl50_53
| spl50_156 ),
inference(sat_conversion,[],[f1257]) ).
cnf(s99,plain,
( ~ spl50_148
| spl50_179 ),
inference(sat_conversion,[],[f1432]) ).
cnf(s175,plain,
( spl50_273
| spl50_274
| spl50_281 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s189,plain,
( ~ spl50_51
| ~ spl50_281 ),
inference(sat_conversion,[],[f2377]) ).
cnf(s190,plain,
( ~ spl50_273
| spl50_281
| spl50_301
| spl50_302 ),
inference(sat_conversion,[],[f2392]) ).
cnf(s191,plain,
( spl50_274
| ~ spl50_301
| ~ spl50_303 ),
inference(sat_conversion,[],[f2398]) ).
cnf(s194,plain,
( spl50_281
| spl50_303 ),
inference(sat_conversion,[],[f2440]) ).
cnf(s195,plain,
~ spl50_302,
inference(sat_conversion,[],[f2467]) ).
cnf(s196,plain,
( ~ spl50_274
| spl50_281
| spl50_302 ),
inference(sat_conversion,[],[f2482]) ).
cnf(s232,plain,
( ~ spl50_4
| ~ spl50_50
| spl50_51
| spl50_53
| ~ spl50_286 ),
inference(sat_conversion,[],[f2877]) ).
cnf(s233,plain,
( ~ spl50_52
| ~ spl50_149
| ~ spl50_156
| spl50_286 ),
inference(sat_conversion,[],[f2879]) ).
cnf(s238,plain,
( spl50_149
| ~ spl50_179
| spl50_370 ),
inference(sat_conversion,[],[f2924]) ).
cnf(s239,plain,
~ spl50_370,
inference(sat_conversion,[],[f2956]) ).
cnf(s287,plain,
( ~ spl50_1
| ~ spl50_2
| spl50_4
| ~ spl50_278 ),
inference(sat_conversion,[],[f3298]) ).
cnf(s305,plain,
( ~ spl50_1
| spl50_2
| spl50_4
| ~ spl50_97 ),
inference(sat_conversion,[],[f3569]) ).
cnf(s306,plain,
( ~ spl50_1
| spl50_4
| ~ spl50_97
| spl50_435 ),
inference(sat_conversion,[],[f3571]) ).
cnf(s331,plain,
( ~ spl50_1
| ~ spl50_2
| spl50_4
| spl50_434
| spl50_483 ),
inference(sat_conversion,[],[f3871]) ).
cnf(s332,plain,
( spl50_3
| ~ spl50_434 ),
inference(sat_conversion,[],[f3980]) ).
cnf(s333,plain,
( ~ spl50_434
| ~ spl50_435 ),
inference(sat_conversion,[],[f3991]) ).
cnf(s334,plain,
( ~ spl50_2
| spl50_278
| ~ spl50_483 ),
inference(sat_conversion,[],[f3995]) ).
cnf(s335,plain,
( spl50_149
| ~ spl50_179 ),
inference(rat,[],[s238,s239]) ).
cnf(s337,plain,
( ~ spl50_273
| spl50_281
| spl50_301 ),
inference(rat,[],[s190,s195]) ).
cnf(s348,plain,
( ~ spl50_4
| spl50_51
| spl50_52 ),
inference(rat,[],[s18,s75,s34]) ).
cnf(s350,plain,
( spl50_2
| spl50_3
| spl50_4 ),
inference(rat,[],[s1,s38]) ).
cnf(s351,plain,
spl50_149,
inference(rat,[],[s99,s72,s335]) ).
cnf(s352,plain,
( spl50_51
| ~ spl50_4 ),
inference(rat,[],[s233,s348,s78,s232,s75,s34,s351]) ).
cnf(s353,plain,
spl50_281,
inference(rat,[],[s337,s175,s191,s194,s196,s195]) ).
cnf(s355,plain,
~ spl50_51,
inference(rat,[],[s189,s353]) ).
cnf(s359,plain,
~ spl50_4,
inference(rat,[],[s352,s355]) ).
cnf(s360,plain,
spl50_2,
inference(rat,[],[s46,s350,s305,s359,s38]) ).
cnf(s361,plain,
~ spl50_278,
inference(rat,[],[s287,s359,s38,s360]) ).
cnf(s362,plain,
~ spl50_483,
inference(rat,[],[s334,s360,s361]) ).
cnf(s364,plain,
spl50_434,
inference(rat,[],[s331,s360,s359,s38,s362]) ).
cnf(s365,plain,
~ spl50_435,
inference(rat,[],[s333,s364]) ).
cnf(s366,plain,
spl50_3,
inference(rat,[],[s332,s364]) ).
cnf(s367,plain,
~ spl50_97,
inference(rat,[],[s306,s359,s38,s365]) ).
cnf(s368,plain,
$false,
inference(rat,[],[s46,s367,s366]) ).
fof(f3996,plain,
$false,
inference(avatar_sat_refutation,[],[s368]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.37 % Computer : n005.cluster.edu
% 0.12/0.37 % Model : x86_64 x86_64
% 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.37 % Memory : 8046.5625MB
% 0.12/0.37 % OS : Linux 6.8.0-71-generic
% 0.12/0.37 % CPULimit : 300
% 0.12/0.37 % WCLimit : 300
% 0.12/0.37 % DateTime : Sun Sep 27 16:09:32 UTC 2026
% 0.12/0.37 % CPUTime :
% 0.12/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.41 Running first-order theorem proving
% 0.12/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.71/1.67 % (4177917)Detected formulas, will run a generic FOF schedule.
% 4.71/1.67 % (4177922)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=3133943445:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.71/1.67 % (4177928)dis-21_1_sil=8000:lcm=predicate:random_seed=2282485353:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.71/1.67 % (4177923)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=357706586:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.71/1.67 % (4177925)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1154132956:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.71/1.67 % (4177927)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4198658416:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.71/1.67 % (4177926)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3475166795:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.71/1.67 % (4177924)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=3830164811:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.71/1.67 % (4177926)Instruction limit reached!
% 4.71/1.67 % (4177926)------------------------------
% 4.71/1.67 % (4177926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177926)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177926)Termination reason: Instruction limit
% 4.71/1.67 % (4177926)Termination phase: Saturation
% 4.71/1.67 % (4177926)Time elapsed: 0.059 s
% 4.71/1.67 % (4177926)Peak memory usage: 87 MB
% 4.71/1.67 % (4177926)Instructions burned: 119 (million)
% 4.71/1.67 % (4177925)Instruction limit reached!
% 4.71/1.67 % (4177925)------------------------------
% 4.71/1.67 % (4177925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177925)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177925)Termination reason: Instruction limit
% 4.71/1.67 % (4177925)Termination phase: Saturation
% 4.71/1.67 % (4177925)Time elapsed: 0.061 s
% 4.71/1.67 % (4177925)Peak memory usage: 91 MB
% 4.71/1.67 % (4177925)Instructions burned: 109 (million)
% 4.71/1.67 % (4177927)Instruction limit reached!
% 4.71/1.67 % (4177927)------------------------------
% 4.71/1.67 % (4177927)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177927)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177927)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177927)Termination reason: Instruction limit
% 4.71/1.67 % (4177927)Termination phase: Saturation
% 4.71/1.67 % (4177927)Time elapsed: 0.064 s
% 4.71/1.67 % (4177927)Peak memory usage: 88 MB
% 4.71/1.67 % (4177927)Instructions burned: 141 (million)
% 4.71/1.67 % (4177928)Instruction limit reached!
% 4.71/1.67 % (4177928)------------------------------
% 4.71/1.67 % (4177928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177928)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177928)Termination reason: Instruction limit
% 4.71/1.67 % (4177928)Termination phase: Saturation
% 4.71/1.67 % (4177928)Time elapsed: 0.073 s
% 4.71/1.67 % (4177928)Peak memory usage: 89 MB
% 4.71/1.67 % (4177928)Instructions burned: 130 (million)
% 4.71/1.67 % (4177936)lrs+10_1_sil=8000:sp=occurrence:random_seed=1952348244:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 4.71/1.67 % (4177937)lrs+10_1_sil=32000:urr=on:br=off:random_seed=337275211:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.71/1.67 % (4177938)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1440139920:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.71/1.67 % (4177939)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1495295563:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 4.71/1.67 % (4177937)Refutation not found, incomplete strategy
% 4.71/1.67 % (4177937)------------------------------
% 4.71/1.67 % (4177937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177937)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177937)Termination reason: Refutation not found, incomplete strategy
% 4.71/1.67 % (4177937)Time elapsed: 0.052 s
% 4.71/1.67 % (4177937)Peak memory usage: 89 MB
% 4.71/1.67 % (4177937)Instructions burned: 109 (million)
% 4.71/1.67 % (4177939)Refutation not found, incomplete strategy
% 4.71/1.67 % (4177939)------------------------------
% 4.71/1.67 % (4177939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177939)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177939)Termination reason: Refutation not found, incomplete strategy
% 4.71/1.67 % (4177939)Time elapsed: 0.096 s
% 4.71/1.67 % (4177939)Peak memory usage: 89 MB
% 4.71/1.67 % (4177939)Instructions burned: 201 (million)
% 4.71/1.67 % (4177936)Instruction limit reached!
% 4.71/1.67 % (4177936)------------------------------
% 4.71/1.67 % (4177936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177936)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177936)Termination reason: Instruction limit
% 4.71/1.67 % (4177936)Termination phase: Saturation
% 4.71/1.67 % (4177936)Time elapsed: 0.137 s
% 4.71/1.67 % (4177936)Peak memory usage: 90 MB
% 4.71/1.67 % (4177936)Instructions burned: 285 (million)
% 4.71/1.67 % (4177938)Instruction limit reached!
% 4.71/1.67 % (4177938)------------------------------
% 4.71/1.67 % (4177938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.71/1.67 % (4177938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.71/1.67 % (4177938)CaDiCaL version: 2.1.3
% 4.71/1.67 % (4177938)Termination reason: Instruction limit
% 4.71/1.67 % (4177938)Termination phase: Saturation
% 4.71/1.67 % (4177938)Time elapsed: 0.150 s
% 4.71/1.67 % (4177938)Peak memory usage: 89 MB
% 4.71/1.67 % (4177938)Instructions burned: 325 (million)
% 4.71/1.67 % (4177922)First to succeed.
% 4.71/1.67 % (4177922)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4177917"
% 4.71/1.67 % (4177937)------------------------------
% 4.71/1.67 % (4177937)------------------------------
% 4.71/1.67 % (4177944)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2673699547:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 4.71/1.67 % (4177945)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1507104353:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 4.71/1.67 % (4177939)------------------------------
% 4.71/1.67 % (4177939)------------------------------
% 4.71/1.67 % (4177922)Refutation found. Thanks to Tanya!
% 4.71/1.67 % SZS status Theorem for theBenchmark
% 4.71/1.67 % SZS output start Proof for theBenchmark
% See solution above
% 6.33/1.84 % (4177922)------------------------------
% 6.33/1.84 % (4177922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.33/1.84 % (4177922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.33/1.84 % (4177922)CaDiCaL version: 2.1.3
% 6.33/1.84 % (4177922)Termination reason: Refutation
% 6.33/1.84 % (4177922)Time elapsed: 0.502 s
% 6.33/1.84 % (4177922)Peak memory usage: 133 MB
% 6.33/1.84 % (4177922)Instructions burned: 1326 (million)
% 6.33/1.84 % (4177922)------------------------------
% 6.33/1.84 % (4177922)------------------------------
% 6.33/1.84 % (4177917)Success in time 0.813 s
% 6.33/1.84 % Vampire exiting
%------------------------------------------------------------------------------