%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL640+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 10.22s 2.12s
% Output : Refutation 11.10s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 31
% Syntax : Number of formulae : 354 ( 35 unt; 30 def)
% Number of atoms : 4903 ( 0 equ)
% Maximal formula atoms : 381 ( 13 avg)
% Number of connectives : 8278 (3729 ~;3841 |; 682 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 64 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 33 ( 32 usr; 27 prp; 0-2 aty)
% Number of functors : 63 ( 63 usr; 11 con; 0-1 aty)
% Number of variables : 2868 ( 0 sgn2603 !; 265 ?)
% 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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ( ( ! [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)
| ! [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)
| ! [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)
| ( ( 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)
| ( ( 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/sandbox2/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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ! [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)
| ( ( ! [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)
| ! [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)
| ! [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)
| ( ( 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)
| ( ( 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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ~ ! [X17] :
( ~ r1(X14,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ~ ! [X23] :
( ~ r1(X20,X23)
| p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| p1(X38) ) )
| ~ ! [X39] :
( ~ r1(X36,X39)
| p1(X39)
| ~ ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| p1(X59) ) )
| ~ ! [X60] :
( ~ r1(X57,X60)
| p1(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ~ ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| p1(X79) ) )
| ~ ! [X80] :
( ~ r1(X77,X80)
| p1(X80)
| ~ ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ~ ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| p1(X98) ) )
| ~ ! [X99] :
( ~ r1(X96,X99)
| p1(X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ~ ! [X105] :
( ~ r1(X102,X105)
| p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ ! [X116] :
( ~ r1(X115,X116)
| p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| p1(X117)
| ~ ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ~ ! [X123] :
( ~ r1(X120,X123)
| p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( ( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) )
| ~ p1(X134) ) )
| ~ ! [X136] :
( ~ r1(X131,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p1(X137) )
| ~ p1(X136)
| ~ ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ~ ( ! [X141] :
( ~ r1(X138,X141)
| p1(X141) )
| ~ p1(X138) ) ) ) )
& ( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ~ ! [X143] :
( ~ r1(X142,X143)
| p1(X143) ) )
| ~ ! [X144] :
( ~ r1(X131,X144)
| p1(X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) ) )
& ! [X147] :
( ~ r1(X131,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ~ ! [X150] :
( ~ r1(X147,X150)
| p1(X150) ) )
& ( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ~ ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) )
| ~ p1(X153) ) ) )
| ~ ! [X155] :
( ~ r1(X131,X155)
| p1(X155)
| ~ ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| p1(X157) )
| ~ p1(X156) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X158] :
( ~ r1(X0,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| p1(X166) )
| ! [X167] :
( ~ r1(X165,X167)
| ~ ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ~ ! [X169] :
( ~ r1(X165,X169)
| p1(X169)
| ~ ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| p1(X171) )
| ~ p1(X170) ) ) ) ) ) ) ) ) ) )
& ! [X172] :
( ~ r1(X0,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ( ( p1(X178)
| ! [X179] :
( ~ r1(X178,X179)
| ~ ! [X180] :
( ~ r1(X179,X180)
| p1(X180) ) )
| ~ ! [X181] :
( ~ r1(X178,X181)
| p1(X181)
| ~ ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) )
| ~ p1(X182) ) ) )
& ! [X184] :
( ~ r1(X178,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| p1(X186) ) )
| ~ ! [X187] :
( ~ r1(X184,X187)
| p1(X187) ) ) ) ) ) ) ) ) ) )
& ! [X188] :
( ~ r1(X0,X188)
| ! [X189] :
( ~ r1(X188,X189)
| ! [X190] :
( ~ r1(X189,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| ( ( p1(X193)
| ! [X194] :
( ~ r1(X193,X194)
| ~ ! [X195] :
( ~ r1(X194,X195)
| p1(X195) ) )
| ~ ! [X196] :
( ~ r1(X193,X196)
| p1(X196)
| ~ ! [X197] :
( ~ r1(X196,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198) )
| ~ p1(X197) ) ) )
& ! [X199] :
( ~ r1(X193,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| p1(X201) ) )
| ~ ! [X202] :
( ~ r1(X199,X202)
| p1(X202) ) ) ) ) ) ) ) ) )
& ! [X203] :
( ~ r1(X0,X203)
| ! [X204] :
( ~ r1(X203,X204)
| ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ! [X207] :
( ~ r1(X206,X207)
| ( ( p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| ~ ! [X209] :
( ~ r1(X208,X209)
| p1(X209) ) )
| ~ ! [X210] :
( ~ r1(X207,X210)
| p1(X210)
| ~ ! [X211] :
( ~ r1(X210,X211)
| ! [X212] :
( ~ r1(X211,X212)
| p1(X212) )
| ~ p1(X211) ) ) )
& ! [X213] :
( ~ r1(X207,X213)
| ! [X214] :
( ~ r1(X213,X214)
| ! [X215] :
( ~ r1(X214,X215)
| p1(X215) ) )
| ~ ! [X216] :
( ~ r1(X213,X216)
| p1(X216) ) ) ) ) ) ) ) )
& ! [X217] :
( ~ r1(X0,X217)
| ! [X218] :
( ~ r1(X217,X218)
| ! [X219] :
( ~ r1(X218,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ( ( p1(X220)
| ! [X221] :
( ~ r1(X220,X221)
| ~ ! [X222] :
( ~ r1(X221,X222)
| p1(X222) ) )
| ~ ! [X223] :
( ~ r1(X220,X223)
| p1(X223)
| ~ ! [X224] :
( ~ r1(X223,X224)
| ! [X225] :
( ~ r1(X224,X225)
| p1(X225) )
| ~ p1(X224) ) ) )
& ! [X226] :
( ~ r1(X220,X226)
| ! [X227] :
( ~ r1(X226,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228) ) )
| ~ ! [X229] :
( ~ r1(X226,X229)
| p1(X229) ) ) ) ) ) ) )
& ! [X230] :
( ~ r1(X0,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| ( ( p1(X232)
| ! [X233] :
( ~ r1(X232,X233)
| ~ ! [X234] :
( ~ r1(X233,X234)
| p1(X234) ) )
| ~ ! [X235] :
( ~ r1(X232,X235)
| p1(X235)
| ~ ! [X236] :
( ~ r1(X235,X236)
| ! [X237] :
( ~ r1(X236,X237)
| p1(X237) )
| ~ p1(X236) ) ) )
& ! [X238] :
( ~ r1(X232,X238)
| ! [X239] :
( ~ r1(X238,X239)
| ! [X240] :
( ~ r1(X239,X240)
| p1(X240) ) )
| ~ ! [X241] :
( ~ r1(X238,X241)
| p1(X241) ) ) ) ) ) )
& ! [X242] :
( ~ r1(X0,X242)
| ! [X243] :
( ~ r1(X242,X243)
| ( ( p1(X243)
| ! [X244] :
( ~ r1(X243,X244)
| ~ ! [X245] :
( ~ r1(X244,X245)
| p1(X245) ) )
| ~ ! [X246] :
( ~ r1(X243,X246)
| p1(X246)
| ~ ! [X247] :
( ~ r1(X246,X247)
| ! [X248] :
( ~ r1(X247,X248)
| p1(X248) )
| ~ p1(X247) ) ) )
& ! [X249] :
( ~ r1(X243,X249)
| ! [X250] :
( ~ r1(X249,X250)
| ! [X251] :
( ~ r1(X250,X251)
| p1(X251) ) )
| ~ ! [X252] :
( ~ r1(X249,X252)
| p1(X252) ) ) ) ) )
& ! [X253] :
( ~ r1(X0,X253)
| ( ( p1(X253)
| ! [X254] :
( ~ r1(X253,X254)
| ~ ! [X255] :
( ~ r1(X254,X255)
| p1(X255) ) )
| ~ ! [X256] :
( ~ r1(X253,X256)
| p1(X256)
| ~ ! [X257] :
( ~ r1(X256,X257)
| ! [X258] :
( ~ r1(X257,X258)
| p1(X258) )
| ~ p1(X257) ) ) )
& ! [X259] :
( ~ r1(X253,X259)
| ! [X260] :
( ~ r1(X259,X260)
| ! [X261] :
( ~ r1(X260,X261)
| p1(X261) ) )
| ~ ! [X262] :
( ~ r1(X259,X262)
| p1(X262) ) ) ) ) ) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ~ ! [X17] :
( ~ r1(X14,X17)
| p1(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ~ ! [X23] :
( ~ r1(X20,X23)
| p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| p1(X38) ) )
| ~ ! [X39] :
( ~ r1(X36,X39)
| p1(X39)
| ~ ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| p1(X59) ) )
| ~ ! [X60] :
( ~ r1(X57,X60)
| p1(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ~ ! [X66] :
( ~ r1(X63,X66)
| p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| p1(X79) ) )
| ~ ! [X80] :
( ~ r1(X77,X80)
| p1(X80)
| ~ ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ~ ! [X86] :
( ~ r1(X83,X86)
| p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| p1(X98) ) )
| ~ ! [X99] :
( ~ r1(X96,X99)
| p1(X99)
| ~ ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ~ ! [X105] :
( ~ r1(X102,X105)
| p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ ! [X116] :
( ~ r1(X115,X116)
| p1(X116) ) )
| ~ ! [X117] :
( ~ r1(X114,X117)
| p1(X117)
| ~ ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ~ ! [X123] :
( ~ r1(X120,X123)
| p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( ( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) )
| ~ p1(X134) ) )
| ~ ! [X136] :
( ~ r1(X131,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p1(X137) )
| ~ p1(X136)
| ~ ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ~ ( ! [X141] :
( ~ r1(X138,X141)
| p1(X141) )
| ~ p1(X138) ) ) ) )
& ( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ~ ! [X143] :
( ~ r1(X142,X143)
| p1(X143) ) )
| ~ ! [X144] :
( ~ r1(X131,X144)
| p1(X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) ) )
& ! [X147] :
( ~ r1(X131,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ~ ! [X150] :
( ~ r1(X147,X150)
| p1(X150) ) )
& ( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ~ ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) )
| ~ p1(X153) ) ) )
| ~ ! [X155] :
( ~ r1(X131,X155)
| p1(X155)
| ~ ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| p1(X157) )
| ~ p1(X156) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X158] :
( ~ r1(X0,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| p1(X166) )
| ! [X167] :
( ~ r1(X165,X167)
| ~ ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ~ ! [X169] :
( ~ r1(X165,X169)
| p1(X169)
| ~ ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| p1(X171) )
| ~ p1(X170) ) ) ) ) ) ) ) ) ) )
& ! [X172] :
( ~ r1(X0,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ( ( p1(X178)
| ! [X179] :
( ~ r1(X178,X179)
| ~ ! [X180] :
( ~ r1(X179,X180)
| p1(X180) ) )
| ~ ! [X181] :
( ~ r1(X178,X181)
| p1(X181)
| ~ ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) )
| ~ p1(X182) ) ) )
& ! [X184] :
( ~ r1(X178,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| p1(X186) ) )
| ~ ! [X187] :
( ~ r1(X184,X187)
| p1(X187) ) ) ) ) ) ) ) ) ) )
& ! [X188] :
( ~ r1(X0,X188)
| ! [X189] :
( ~ r1(X188,X189)
| ! [X190] :
( ~ r1(X189,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| ( ( p1(X193)
| ! [X194] :
( ~ r1(X193,X194)
| ~ ! [X195] :
( ~ r1(X194,X195)
| p1(X195) ) )
| ~ ! [X196] :
( ~ r1(X193,X196)
| p1(X196)
| ~ ! [X197] :
( ~ r1(X196,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198) )
| ~ p1(X197) ) ) )
& ! [X199] :
( ~ r1(X193,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| p1(X201) ) )
| ~ ! [X202] :
( ~ r1(X199,X202)
| p1(X202) ) ) ) ) ) ) ) ) )
& ! [X203] :
( ~ r1(X0,X203)
| ! [X204] :
( ~ r1(X203,X204)
| ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ! [X207] :
( ~ r1(X206,X207)
| ( ( p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| ~ ! [X209] :
( ~ r1(X208,X209)
| p1(X209) ) )
| ~ ! [X210] :
( ~ r1(X207,X210)
| p1(X210)
| ~ ! [X211] :
( ~ r1(X210,X211)
| ! [X212] :
( ~ r1(X211,X212)
| p1(X212) )
| ~ p1(X211) ) ) )
& ! [X213] :
( ~ r1(X207,X213)
| ! [X214] :
( ~ r1(X213,X214)
| ! [X215] :
( ~ r1(X214,X215)
| p1(X215) ) )
| ~ ! [X216] :
( ~ r1(X213,X216)
| p1(X216) ) ) ) ) ) ) ) )
& ! [X217] :
( ~ r1(X0,X217)
| ! [X218] :
( ~ r1(X217,X218)
| ! [X219] :
( ~ r1(X218,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ( ( p1(X220)
| ! [X221] :
( ~ r1(X220,X221)
| ~ ! [X222] :
( ~ r1(X221,X222)
| p1(X222) ) )
| ~ ! [X223] :
( ~ r1(X220,X223)
| p1(X223)
| ~ ! [X224] :
( ~ r1(X223,X224)
| ! [X225] :
( ~ r1(X224,X225)
| p1(X225) )
| ~ p1(X224) ) ) )
& ! [X226] :
( ~ r1(X220,X226)
| ! [X227] :
( ~ r1(X226,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228) ) )
| ~ ! [X229] :
( ~ r1(X226,X229)
| p1(X229) ) ) ) ) ) ) )
& ! [X230] :
( ~ r1(X0,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| ( ( p1(X232)
| ! [X233] :
( ~ r1(X232,X233)
| ~ ! [X234] :
( ~ r1(X233,X234)
| p1(X234) ) )
| ~ ! [X235] :
( ~ r1(X232,X235)
| p1(X235)
| ~ ! [X236] :
( ~ r1(X235,X236)
| ! [X237] :
( ~ r1(X236,X237)
| p1(X237) )
| ~ p1(X236) ) ) )
& ! [X238] :
( ~ r1(X232,X238)
| ! [X239] :
( ~ r1(X238,X239)
| ! [X240] :
( ~ r1(X239,X240)
| p1(X240) ) )
| ~ ! [X241] :
( ~ r1(X238,X241)
| p1(X241) ) ) ) ) ) )
& ! [X242] :
( ~ r1(X0,X242)
| ! [X243] :
( ~ r1(X242,X243)
| ( ( p1(X243)
| ! [X244] :
( ~ r1(X243,X244)
| ~ ! [X245] :
( ~ r1(X244,X245)
| p1(X245) ) )
| ~ ! [X246] :
( ~ r1(X243,X246)
| p1(X246)
| ~ ! [X247] :
( ~ r1(X246,X247)
| ! [X248] :
( ~ r1(X247,X248)
| p1(X248) )
| ~ p1(X247) ) ) )
& ! [X249] :
( ~ r1(X243,X249)
| ! [X250] :
( ~ r1(X249,X250)
| ! [X251] :
( ~ r1(X250,X251)
| p1(X251) ) )
| ~ ! [X252] :
( ~ r1(X249,X252)
| p1(X252) ) ) ) ) )
& ! [X253] :
( ~ r1(X0,X253)
| ( ( p1(X253)
| ! [X254] :
( ~ r1(X253,X254)
| ~ ! [X255] :
( ~ r1(X254,X255)
| p1(X255) ) )
| ~ ! [X256] :
( ~ r1(X253,X256)
| p1(X256)
| ~ ! [X257] :
( ~ r1(X256,X257)
| ! [X258] :
( ~ r1(X257,X258)
| p1(X258) )
| ~ p1(X257) ) ) )
& ! [X259] :
( ~ r1(X253,X259)
| ! [X260] :
( ~ r1(X259,X260)
| ! [X261] :
( ~ r1(X260,X261)
| p1(X261) ) )
| ~ ! [X262] :
( ~ r1(X259,X262)
| p1(X262) ) ) ) ) ) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ? [X16] :
( r1(X15,X16)
& ~ p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ? [X23] :
( r1(X20,X23)
& ~ p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ~ p1(X38) ) )
| ? [X39] :
( r1(X36,X39)
& ~ p1(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ? [X59] :
( r1(X58,X59)
& ~ p1(X59) ) )
| ? [X60] :
( r1(X57,X60)
& ~ p1(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p1(X79) ) )
| ? [X80] :
( r1(X77,X80)
& ~ p1(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ? [X98] :
( r1(X97,X98)
& ~ p1(X98) ) )
| ? [X99] :
( r1(X96,X99)
& ~ p1(X99)
& ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ? [X105] :
( r1(X102,X105)
& ~ p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ? [X116] :
( r1(X115,X116)
& ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& ~ p1(X117)
& ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ? [X123] :
( r1(X120,X123)
& ~ p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( ( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) )
| ? [X136] :
( r1(X131,X136)
& ? [X137] :
( r1(X136,X137)
& ~ p1(X137) )
& p1(X136)
& ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ( ? [X141] :
( r1(X138,X141)
& ~ p1(X141) )
& p1(X138) ) ) ) )
& ( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ? [X143] :
( r1(X142,X143)
& ~ p1(X143) ) )
| ? [X144] :
( r1(X131,X144)
& ~ p1(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) ) )
& ! [X147] :
( ~ r1(X131,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ? [X150] :
( r1(X147,X150)
& ~ p1(X150) ) )
& ( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ? [X153] :
( r1(X152,X153)
& ? [X154] :
( r1(X153,X154)
& ~ p1(X154) )
& p1(X153) ) ) )
| ? [X155] :
( r1(X131,X155)
& ~ p1(X155)
& ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| p1(X157) )
| ~ p1(X156) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X158] :
( r1(X0,X158)
& ? [X159] :
( r1(X158,X159)
& ? [X160] :
( r1(X159,X160)
& ? [X161] :
( r1(X160,X161)
& ? [X162] :
( r1(X161,X162)
& ? [X163] :
( r1(X162,X163)
& ? [X164] :
( r1(X163,X164)
& ? [X165] :
( r1(X164,X165)
& ? [X166] :
( r1(X165,X166)
& ~ p1(X166) )
& ? [X167] :
( r1(X165,X167)
& ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
& ! [X169] :
( ~ r1(X165,X169)
| p1(X169)
| ? [X170] :
( r1(X169,X170)
& ? [X171] :
( r1(X170,X171)
& ~ p1(X171) )
& p1(X170) ) ) ) ) ) ) ) ) ) )
& ! [X172] :
( ~ r1(X0,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ( ( p1(X178)
| ! [X179] :
( ~ r1(X178,X179)
| ? [X180] :
( r1(X179,X180)
& ~ p1(X180) ) )
| ? [X181] :
( r1(X178,X181)
& ~ p1(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) )
| ~ p1(X182) ) ) )
& ! [X184] :
( ~ r1(X178,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| p1(X186) ) )
| ? [X187] :
( r1(X184,X187)
& ~ p1(X187) ) ) ) ) ) ) ) ) ) )
& ! [X188] :
( ~ r1(X0,X188)
| ! [X189] :
( ~ r1(X188,X189)
| ! [X190] :
( ~ r1(X189,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| ( ( p1(X193)
| ! [X194] :
( ~ r1(X193,X194)
| ? [X195] :
( r1(X194,X195)
& ~ p1(X195) ) )
| ? [X196] :
( r1(X193,X196)
& ~ p1(X196)
& ! [X197] :
( ~ r1(X196,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198) )
| ~ p1(X197) ) ) )
& ! [X199] :
( ~ r1(X193,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| p1(X201) ) )
| ? [X202] :
( r1(X199,X202)
& ~ p1(X202) ) ) ) ) ) ) ) ) )
& ! [X203] :
( ~ r1(X0,X203)
| ! [X204] :
( ~ r1(X203,X204)
| ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ! [X207] :
( ~ r1(X206,X207)
| ( ( p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| ? [X209] :
( r1(X208,X209)
& ~ p1(X209) ) )
| ? [X210] :
( r1(X207,X210)
& ~ p1(X210)
& ! [X211] :
( ~ r1(X210,X211)
| ! [X212] :
( ~ r1(X211,X212)
| p1(X212) )
| ~ p1(X211) ) ) )
& ! [X213] :
( ~ r1(X207,X213)
| ! [X214] :
( ~ r1(X213,X214)
| ! [X215] :
( ~ r1(X214,X215)
| p1(X215) ) )
| ? [X216] :
( r1(X213,X216)
& ~ p1(X216) ) ) ) ) ) ) ) )
& ! [X217] :
( ~ r1(X0,X217)
| ! [X218] :
( ~ r1(X217,X218)
| ! [X219] :
( ~ r1(X218,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ( ( p1(X220)
| ! [X221] :
( ~ r1(X220,X221)
| ? [X222] :
( r1(X221,X222)
& ~ p1(X222) ) )
| ? [X223] :
( r1(X220,X223)
& ~ p1(X223)
& ! [X224] :
( ~ r1(X223,X224)
| ! [X225] :
( ~ r1(X224,X225)
| p1(X225) )
| ~ p1(X224) ) ) )
& ! [X226] :
( ~ r1(X220,X226)
| ! [X227] :
( ~ r1(X226,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228) ) )
| ? [X229] :
( r1(X226,X229)
& ~ p1(X229) ) ) ) ) ) ) )
& ! [X230] :
( ~ r1(X0,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| ( ( p1(X232)
| ! [X233] :
( ~ r1(X232,X233)
| ? [X234] :
( r1(X233,X234)
& ~ p1(X234) ) )
| ? [X235] :
( r1(X232,X235)
& ~ p1(X235)
& ! [X236] :
( ~ r1(X235,X236)
| ! [X237] :
( ~ r1(X236,X237)
| p1(X237) )
| ~ p1(X236) ) ) )
& ! [X238] :
( ~ r1(X232,X238)
| ! [X239] :
( ~ r1(X238,X239)
| ! [X240] :
( ~ r1(X239,X240)
| p1(X240) ) )
| ? [X241] :
( r1(X238,X241)
& ~ p1(X241) ) ) ) ) ) )
& ! [X242] :
( ~ r1(X0,X242)
| ! [X243] :
( ~ r1(X242,X243)
| ( ( p1(X243)
| ! [X244] :
( ~ r1(X243,X244)
| ? [X245] :
( r1(X244,X245)
& ~ p1(X245) ) )
| ? [X246] :
( r1(X243,X246)
& ~ p1(X246)
& ! [X247] :
( ~ r1(X246,X247)
| ! [X248] :
( ~ r1(X247,X248)
| p1(X248) )
| ~ p1(X247) ) ) )
& ! [X249] :
( ~ r1(X243,X249)
| ! [X250] :
( ~ r1(X249,X250)
| ! [X251] :
( ~ r1(X250,X251)
| p1(X251) ) )
| ? [X252] :
( r1(X249,X252)
& ~ p1(X252) ) ) ) ) )
& ! [X253] :
( ~ r1(X0,X253)
| ( ( p1(X253)
| ! [X254] :
( ~ r1(X253,X254)
| ? [X255] :
( r1(X254,X255)
& ~ p1(X255) ) )
| ? [X256] :
( r1(X253,X256)
& ~ p1(X256)
& ! [X257] :
( ~ r1(X256,X257)
| ! [X258] :
( ~ r1(X257,X258)
| p1(X258) )
| ~ p1(X257) ) ) )
& ! [X259] :
( ~ r1(X253,X259)
| ! [X260] :
( ~ r1(X259,X260)
| ! [X261] :
( ~ r1(X260,X261)
| p1(X261) ) )
| ? [X262] :
( r1(X259,X262)
& ~ p1(X262) ) ) ) ) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ? [X16] :
( r1(X15,X16)
& ~ p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ? [X23] :
( r1(X20,X23)
& ~ p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ~ p1(X38) ) )
| ? [X39] :
( r1(X36,X39)
& ~ p1(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ? [X59] :
( r1(X58,X59)
& ~ p1(X59) ) )
| ? [X60] :
( r1(X57,X60)
& ~ p1(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p1(X79) ) )
| ? [X80] :
( r1(X77,X80)
& ~ p1(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ? [X98] :
( r1(X97,X98)
& ~ p1(X98) ) )
| ? [X99] :
( r1(X96,X99)
& ~ p1(X99)
& ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ? [X105] :
( r1(X102,X105)
& ~ p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ? [X116] :
( r1(X115,X116)
& ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& ~ p1(X117)
& ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ? [X123] :
( r1(X120,X123)
& ~ p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( ( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) )
| ? [X136] :
( r1(X131,X136)
& ? [X137] :
( r1(X136,X137)
& ~ p1(X137) )
& p1(X136)
& ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ( ? [X141] :
( r1(X138,X141)
& ~ p1(X141) )
& p1(X138) ) ) ) )
& ( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ? [X143] :
( r1(X142,X143)
& ~ p1(X143) ) )
| ? [X144] :
( r1(X131,X144)
& ~ p1(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) ) )
& ! [X147] :
( ~ r1(X131,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ? [X150] :
( r1(X147,X150)
& ~ p1(X150) ) )
& ( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ? [X153] :
( r1(X152,X153)
& ? [X154] :
( r1(X153,X154)
& ~ p1(X154) )
& p1(X153) ) ) )
| ? [X155] :
( r1(X131,X155)
& ~ p1(X155)
& ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| p1(X157) )
| ~ p1(X156) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X158] :
( r1(X0,X158)
& ? [X159] :
( r1(X158,X159)
& ? [X160] :
( r1(X159,X160)
& ? [X161] :
( r1(X160,X161)
& ? [X162] :
( r1(X161,X162)
& ? [X163] :
( r1(X162,X163)
& ? [X164] :
( r1(X163,X164)
& ? [X165] :
( r1(X164,X165)
& ? [X166] :
( r1(X165,X166)
& ~ p1(X166) )
& ? [X167] :
( r1(X165,X167)
& ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
& ! [X169] :
( ~ r1(X165,X169)
| p1(X169)
| ? [X170] :
( r1(X169,X170)
& ? [X171] :
( r1(X170,X171)
& ~ p1(X171) )
& p1(X170) ) ) ) ) ) ) ) ) ) )
& ! [X172] :
( ~ r1(X0,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ( ( p1(X178)
| ! [X179] :
( ~ r1(X178,X179)
| ? [X180] :
( r1(X179,X180)
& ~ p1(X180) ) )
| ? [X181] :
( r1(X178,X181)
& ~ p1(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) )
| ~ p1(X182) ) ) )
& ! [X184] :
( ~ r1(X178,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| p1(X186) ) )
| ? [X187] :
( r1(X184,X187)
& ~ p1(X187) ) ) ) ) ) ) ) ) ) )
& ! [X188] :
( ~ r1(X0,X188)
| ! [X189] :
( ~ r1(X188,X189)
| ! [X190] :
( ~ r1(X189,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| ( ( p1(X193)
| ! [X194] :
( ~ r1(X193,X194)
| ? [X195] :
( r1(X194,X195)
& ~ p1(X195) ) )
| ? [X196] :
( r1(X193,X196)
& ~ p1(X196)
& ! [X197] :
( ~ r1(X196,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198) )
| ~ p1(X197) ) ) )
& ! [X199] :
( ~ r1(X193,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| p1(X201) ) )
| ? [X202] :
( r1(X199,X202)
& ~ p1(X202) ) ) ) ) ) ) ) ) )
& ! [X203] :
( ~ r1(X0,X203)
| ! [X204] :
( ~ r1(X203,X204)
| ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ! [X207] :
( ~ r1(X206,X207)
| ( ( p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| ? [X209] :
( r1(X208,X209)
& ~ p1(X209) ) )
| ? [X210] :
( r1(X207,X210)
& ~ p1(X210)
& ! [X211] :
( ~ r1(X210,X211)
| ! [X212] :
( ~ r1(X211,X212)
| p1(X212) )
| ~ p1(X211) ) ) )
& ! [X213] :
( ~ r1(X207,X213)
| ! [X214] :
( ~ r1(X213,X214)
| ! [X215] :
( ~ r1(X214,X215)
| p1(X215) ) )
| ? [X216] :
( r1(X213,X216)
& ~ p1(X216) ) ) ) ) ) ) ) )
& ! [X217] :
( ~ r1(X0,X217)
| ! [X218] :
( ~ r1(X217,X218)
| ! [X219] :
( ~ r1(X218,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ( ( p1(X220)
| ! [X221] :
( ~ r1(X220,X221)
| ? [X222] :
( r1(X221,X222)
& ~ p1(X222) ) )
| ? [X223] :
( r1(X220,X223)
& ~ p1(X223)
& ! [X224] :
( ~ r1(X223,X224)
| ! [X225] :
( ~ r1(X224,X225)
| p1(X225) )
| ~ p1(X224) ) ) )
& ! [X226] :
( ~ r1(X220,X226)
| ! [X227] :
( ~ r1(X226,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228) ) )
| ? [X229] :
( r1(X226,X229)
& ~ p1(X229) ) ) ) ) ) ) )
& ! [X230] :
( ~ r1(X0,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| ( ( p1(X232)
| ! [X233] :
( ~ r1(X232,X233)
| ? [X234] :
( r1(X233,X234)
& ~ p1(X234) ) )
| ? [X235] :
( r1(X232,X235)
& ~ p1(X235)
& ! [X236] :
( ~ r1(X235,X236)
| ! [X237] :
( ~ r1(X236,X237)
| p1(X237) )
| ~ p1(X236) ) ) )
& ! [X238] :
( ~ r1(X232,X238)
| ! [X239] :
( ~ r1(X238,X239)
| ! [X240] :
( ~ r1(X239,X240)
| p1(X240) ) )
| ? [X241] :
( r1(X238,X241)
& ~ p1(X241) ) ) ) ) ) )
& ! [X242] :
( ~ r1(X0,X242)
| ! [X243] :
( ~ r1(X242,X243)
| ( ( p1(X243)
| ! [X244] :
( ~ r1(X243,X244)
| ? [X245] :
( r1(X244,X245)
& ~ p1(X245) ) )
| ? [X246] :
( r1(X243,X246)
& ~ p1(X246)
& ! [X247] :
( ~ r1(X246,X247)
| ! [X248] :
( ~ r1(X247,X248)
| p1(X248) )
| ~ p1(X247) ) ) )
& ! [X249] :
( ~ r1(X243,X249)
| ! [X250] :
( ~ r1(X249,X250)
| ! [X251] :
( ~ r1(X250,X251)
| p1(X251) ) )
| ? [X252] :
( r1(X249,X252)
& ~ p1(X252) ) ) ) ) )
& ! [X253] :
( ~ r1(X0,X253)
| ( ( p1(X253)
| ! [X254] :
( ~ r1(X253,X254)
| ? [X255] :
( r1(X254,X255)
& ~ p1(X255) ) )
| ? [X256] :
( r1(X253,X256)
& ~ p1(X256)
& ! [X257] :
( ~ r1(X256,X257)
| ! [X258] :
( ~ r1(X257,X258)
| p1(X258) )
| ~ p1(X257) ) ) )
& ! [X259] :
( ~ r1(X253,X259)
| ! [X260] :
( ~ r1(X259,X260)
| ! [X261] :
( ~ r1(X260,X261)
| p1(X261) ) )
| ? [X262] :
( r1(X259,X262)
& ~ p1(X262) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X131] :
( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ? [X153] :
( r1(X152,X153)
& ? [X154] :
( r1(X153,X154)
& ~ p1(X154) )
& p1(X153) ) ) )
| ~ sP0(X131) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X131] :
( ? [X136] :
( r1(X131,X136)
& ? [X137] :
( r1(X136,X137)
& ~ p1(X137) )
& p1(X136)
& ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ( ? [X141] :
( r1(X138,X141)
& ~ p1(X141) )
& p1(X138) ) ) )
| ~ sP1(X131) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X131] :
( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ? [X143] :
( r1(X142,X143)
& ~ p1(X143) ) )
| ? [X144] :
( r1(X131,X144)
& ~ p1(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) )
| ~ sP2(X131) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X131] :
( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) )
| sP1(X131)
| ~ sP3(X131) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ? [X16] :
( r1(X15,X16)
& ~ p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ? [X23] :
( r1(X20,X23)
& ~ p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ~ p1(X38) ) )
| ? [X39] :
( r1(X36,X39)
& ~ p1(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ? [X59] :
( r1(X58,X59)
& ~ p1(X59) ) )
| ? [X60] :
( r1(X57,X60)
& ~ p1(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p1(X79) ) )
| ? [X80] :
( r1(X77,X80)
& ~ p1(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ? [X98] :
( r1(X97,X98)
& ~ p1(X98) ) )
| ? [X99] :
( r1(X96,X99)
& ~ p1(X99)
& ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ? [X105] :
( r1(X102,X105)
& ~ p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ? [X116] :
( r1(X115,X116)
& ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& ~ p1(X117)
& ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ? [X123] :
( r1(X120,X123)
& ~ p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( sP3(X131)
& sP2(X131)
& ! [X147] :
( ~ r1(X131,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ? [X150] :
( r1(X147,X150)
& ~ p1(X150) ) )
& ( sP0(X131)
| ? [X155] :
( r1(X131,X155)
& ~ p1(X155)
& ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| p1(X157) )
| ~ p1(X156) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X158] :
( r1(X0,X158)
& ? [X159] :
( r1(X158,X159)
& ? [X160] :
( r1(X159,X160)
& ? [X161] :
( r1(X160,X161)
& ? [X162] :
( r1(X161,X162)
& ? [X163] :
( r1(X162,X163)
& ? [X164] :
( r1(X163,X164)
& ? [X165] :
( r1(X164,X165)
& ? [X166] :
( r1(X165,X166)
& ~ p1(X166) )
& ? [X167] :
( r1(X165,X167)
& ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
& ! [X169] :
( ~ r1(X165,X169)
| p1(X169)
| ? [X170] :
( r1(X169,X170)
& ? [X171] :
( r1(X170,X171)
& ~ p1(X171) )
& p1(X170) ) ) ) ) ) ) ) ) ) )
& ! [X172] :
( ~ r1(X0,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ( ( p1(X178)
| ! [X179] :
( ~ r1(X178,X179)
| ? [X180] :
( r1(X179,X180)
& ~ p1(X180) ) )
| ? [X181] :
( r1(X178,X181)
& ~ p1(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) )
| ~ p1(X182) ) ) )
& ! [X184] :
( ~ r1(X178,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| p1(X186) ) )
| ? [X187] :
( r1(X184,X187)
& ~ p1(X187) ) ) ) ) ) ) ) ) ) )
& ! [X188] :
( ~ r1(X0,X188)
| ! [X189] :
( ~ r1(X188,X189)
| ! [X190] :
( ~ r1(X189,X190)
| ! [X191] :
( ~ r1(X190,X191)
| ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| ( ( p1(X193)
| ! [X194] :
( ~ r1(X193,X194)
| ? [X195] :
( r1(X194,X195)
& ~ p1(X195) ) )
| ? [X196] :
( r1(X193,X196)
& ~ p1(X196)
& ! [X197] :
( ~ r1(X196,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198) )
| ~ p1(X197) ) ) )
& ! [X199] :
( ~ r1(X193,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| p1(X201) ) )
| ? [X202] :
( r1(X199,X202)
& ~ p1(X202) ) ) ) ) ) ) ) ) )
& ! [X203] :
( ~ r1(X0,X203)
| ! [X204] :
( ~ r1(X203,X204)
| ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| ! [X207] :
( ~ r1(X206,X207)
| ( ( p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| ? [X209] :
( r1(X208,X209)
& ~ p1(X209) ) )
| ? [X210] :
( r1(X207,X210)
& ~ p1(X210)
& ! [X211] :
( ~ r1(X210,X211)
| ! [X212] :
( ~ r1(X211,X212)
| p1(X212) )
| ~ p1(X211) ) ) )
& ! [X213] :
( ~ r1(X207,X213)
| ! [X214] :
( ~ r1(X213,X214)
| ! [X215] :
( ~ r1(X214,X215)
| p1(X215) ) )
| ? [X216] :
( r1(X213,X216)
& ~ p1(X216) ) ) ) ) ) ) ) )
& ! [X217] :
( ~ r1(X0,X217)
| ! [X218] :
( ~ r1(X217,X218)
| ! [X219] :
( ~ r1(X218,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ( ( p1(X220)
| ! [X221] :
( ~ r1(X220,X221)
| ? [X222] :
( r1(X221,X222)
& ~ p1(X222) ) )
| ? [X223] :
( r1(X220,X223)
& ~ p1(X223)
& ! [X224] :
( ~ r1(X223,X224)
| ! [X225] :
( ~ r1(X224,X225)
| p1(X225) )
| ~ p1(X224) ) ) )
& ! [X226] :
( ~ r1(X220,X226)
| ! [X227] :
( ~ r1(X226,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228) ) )
| ? [X229] :
( r1(X226,X229)
& ~ p1(X229) ) ) ) ) ) ) )
& ! [X230] :
( ~ r1(X0,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| ( ( p1(X232)
| ! [X233] :
( ~ r1(X232,X233)
| ? [X234] :
( r1(X233,X234)
& ~ p1(X234) ) )
| ? [X235] :
( r1(X232,X235)
& ~ p1(X235)
& ! [X236] :
( ~ r1(X235,X236)
| ! [X237] :
( ~ r1(X236,X237)
| p1(X237) )
| ~ p1(X236) ) ) )
& ! [X238] :
( ~ r1(X232,X238)
| ! [X239] :
( ~ r1(X238,X239)
| ! [X240] :
( ~ r1(X239,X240)
| p1(X240) ) )
| ? [X241] :
( r1(X238,X241)
& ~ p1(X241) ) ) ) ) ) )
& ! [X242] :
( ~ r1(X0,X242)
| ! [X243] :
( ~ r1(X242,X243)
| ( ( p1(X243)
| ! [X244] :
( ~ r1(X243,X244)
| ? [X245] :
( r1(X244,X245)
& ~ p1(X245) ) )
| ? [X246] :
( r1(X243,X246)
& ~ p1(X246)
& ! [X247] :
( ~ r1(X246,X247)
| ! [X248] :
( ~ r1(X247,X248)
| p1(X248) )
| ~ p1(X247) ) ) )
& ! [X249] :
( ~ r1(X243,X249)
| ! [X250] :
( ~ r1(X249,X250)
| ! [X251] :
( ~ r1(X250,X251)
| p1(X251) ) )
| ? [X252] :
( r1(X249,X252)
& ~ p1(X252) ) ) ) ) )
& ! [X253] :
( ~ r1(X0,X253)
| ( ( p1(X253)
| ! [X254] :
( ~ r1(X253,X254)
| ? [X255] :
( r1(X254,X255)
& ~ p1(X255) ) )
| ? [X256] :
( r1(X253,X256)
& ~ p1(X256)
& ! [X257] :
( ~ r1(X256,X257)
| ! [X258] :
( ~ r1(X257,X258)
| p1(X258) )
| ~ p1(X257) ) ) )
& ! [X259] :
( ~ r1(X253,X259)
| ! [X260] :
( ~ r1(X259,X260)
| ! [X261] :
( ~ r1(X260,X261)
| p1(X261) ) )
| ? [X262] :
( r1(X259,X262)
& ~ p1(X262) ) ) ) ) ),
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X131] :
( ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131)
| ! [X133] :
( ~ r1(X131,X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) )
| sP1(X131)
| ~ sP3(X131) ),
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,
! [X131] :
( p1(X131)
| ! [X142] :
( ~ r1(X131,X142)
| ? [X143] :
( r1(X142,X143)
& ~ p1(X143) ) )
| ? [X144] :
( r1(X131,X144)
& ~ p1(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| p1(X146) )
| ~ p1(X145) ) )
| ~ sP2(X131) ),
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,
! [X131] :
( ? [X136] :
( r1(X131,X136)
& ? [X137] :
( r1(X136,X137)
& ~ p1(X137) )
& p1(X136)
& ! [X138] :
( ~ r1(X136,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| p1(X140) )
| ~ p1(X139) )
| ( ? [X141] :
( r1(X138,X141)
& ~ p1(X141) )
& p1(X138) ) ) )
| ~ sP1(X131) ),
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,
! [X131] :
( ! [X151] :
( ~ r1(X131,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ? [X153] :
( r1(X152,X153)
& ? [X154] :
( r1(X153,X154)
& ~ p1(X154) )
& p1(X153) ) ) )
| ~ sP0(X131) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ? [X16] :
( r1(X15,X16)
& ~ p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ? [X23] :
( r1(X20,X23)
& ~ p1(X23) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X24] :
( ~ r1(X0,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ? [X38] :
( r1(X37,X38)
& ~ p1(X38) ) )
| ? [X39] :
( r1(X36,X39)
& ~ p1(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X46] :
( ~ r1(X0,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ? [X59] :
( r1(X58,X59)
& ~ p1(X59) ) )
| ? [X60] :
( r1(X57,X60)
& ~ p1(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ? [X66] :
( r1(X63,X66)
& ~ p1(X66) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X67] :
( ~ r1(X0,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p1(X79) ) )
| ? [X80] :
( r1(X77,X80)
& ~ p1(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ? [X86] :
( r1(X83,X86)
& ~ p1(X86) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X87] :
( ~ r1(X0,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ? [X98] :
( r1(X97,X98)
& ~ p1(X98) ) )
| ? [X99] :
( r1(X96,X99)
& ~ p1(X99)
& ! [X100] :
( ~ r1(X99,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ? [X105] :
( r1(X102,X105)
& ~ p1(X105) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X106] :
( ~ r1(X0,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ? [X116] :
( r1(X115,X116)
& ~ p1(X116) ) )
| ? [X117] :
( r1(X114,X117)
& ~ p1(X117)
& ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ? [X123] :
( r1(X120,X123)
& ~ p1(X123) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X124] :
( ~ r1(X0,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( sP3(X131)
& sP2(X131)
& ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ! [X134] :
( ~ r1(X133,X134)
| p1(X134) ) )
| ? [X135] :
( r1(X132,X135)
& ~ p1(X135) ) )
& ( sP0(X131)
| ? [X136] :
( r1(X131,X136)
& ~ p1(X136)
& ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| p1(X138) )
| ~ p1(X137) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X139] :
( r1(X0,X139)
& ? [X140] :
( r1(X139,X140)
& ? [X141] :
( r1(X140,X141)
& ? [X142] :
( r1(X141,X142)
& ? [X143] :
( r1(X142,X143)
& ? [X144] :
( r1(X143,X144)
& ? [X145] :
( r1(X144,X145)
& ? [X146] :
( r1(X145,X146)
& ? [X147] :
( r1(X146,X147)
& ~ p1(X147) )
& ? [X148] :
( r1(X146,X148)
& ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
& ! [X150] :
( ~ r1(X146,X150)
| p1(X150)
| ? [X151] :
( r1(X150,X151)
& ? [X152] :
( r1(X151,X152)
& ~ p1(X152) )
& p1(X151) ) ) ) ) ) ) ) ) ) )
& ! [X153] :
( ~ r1(X0,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ! [X155] :
( ~ r1(X154,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( ( p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| ? [X161] :
( r1(X160,X161)
& ~ p1(X161) ) )
| ? [X162] :
( r1(X159,X162)
& ~ p1(X162)
& ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| p1(X164) )
| ~ p1(X163) ) ) )
& ! [X165] :
( ~ r1(X159,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| p1(X167) ) )
| ? [X168] :
( r1(X165,X168)
& ~ p1(X168) ) ) ) ) ) ) ) ) ) )
& ! [X169] :
( ~ r1(X0,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ( ( p1(X174)
| ! [X175] :
( ~ r1(X174,X175)
| ? [X176] :
( r1(X175,X176)
& ~ p1(X176) ) )
| ? [X177] :
( r1(X174,X177)
& ~ p1(X177)
& ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) )
| ~ p1(X178) ) ) )
& ! [X180] :
( ~ r1(X174,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| p1(X182) ) )
| ? [X183] :
( r1(X180,X183)
& ~ p1(X183) ) ) ) ) ) ) ) ) )
& ! [X184] :
( ~ r1(X0,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| ! [X187] :
( ~ r1(X186,X187)
| ! [X188] :
( ~ r1(X187,X188)
| ( ( p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| ? [X190] :
( r1(X189,X190)
& ~ p1(X190) ) )
| ? [X191] :
( r1(X188,X191)
& ~ p1(X191)
& ! [X192] :
( ~ r1(X191,X192)
| ! [X193] :
( ~ r1(X192,X193)
| p1(X193) )
| ~ p1(X192) ) ) )
& ! [X194] :
( ~ r1(X188,X194)
| ! [X195] :
( ~ r1(X194,X195)
| ! [X196] :
( ~ r1(X195,X196)
| p1(X196) ) )
| ? [X197] :
( r1(X194,X197)
& ~ p1(X197) ) ) ) ) ) ) ) )
& ! [X198] :
( ~ r1(X0,X198)
| ! [X199] :
( ~ r1(X198,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| ( ( p1(X201)
| ! [X202] :
( ~ r1(X201,X202)
| ? [X203] :
( r1(X202,X203)
& ~ p1(X203) ) )
| ? [X204] :
( r1(X201,X204)
& ~ p1(X204)
& ! [X205] :
( ~ r1(X204,X205)
| ! [X206] :
( ~ r1(X205,X206)
| p1(X206) )
| ~ p1(X205) ) ) )
& ! [X207] :
( ~ r1(X201,X207)
| ! [X208] :
( ~ r1(X207,X208)
| ! [X209] :
( ~ r1(X208,X209)
| p1(X209) ) )
| ? [X210] :
( r1(X207,X210)
& ~ p1(X210) ) ) ) ) ) ) )
& ! [X211] :
( ~ r1(X0,X211)
| ! [X212] :
( ~ r1(X211,X212)
| ! [X213] :
( ~ r1(X212,X213)
| ( ( p1(X213)
| ! [X214] :
( ~ r1(X213,X214)
| ? [X215] :
( r1(X214,X215)
& ~ p1(X215) ) )
| ? [X216] :
( r1(X213,X216)
& ~ p1(X216)
& ! [X217] :
( ~ r1(X216,X217)
| ! [X218] :
( ~ r1(X217,X218)
| p1(X218) )
| ~ p1(X217) ) ) )
& ! [X219] :
( ~ r1(X213,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p1(X221) ) )
| ? [X222] :
( r1(X219,X222)
& ~ p1(X222) ) ) ) ) ) )
& ! [X223] :
( ~ r1(X0,X223)
| ! [X224] :
( ~ r1(X223,X224)
| ( ( p1(X224)
| ! [X225] :
( ~ r1(X224,X225)
| ? [X226] :
( r1(X225,X226)
& ~ p1(X226) ) )
| ? [X227] :
( r1(X224,X227)
& ~ p1(X227)
& ! [X228] :
( ~ r1(X227,X228)
| ! [X229] :
( ~ r1(X228,X229)
| p1(X229) )
| ~ p1(X228) ) ) )
& ! [X230] :
( ~ r1(X224,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| p1(X232) ) )
| ? [X233] :
( r1(X230,X233)
& ~ p1(X233) ) ) ) ) )
& ! [X234] :
( ~ r1(X0,X234)
| ( ( p1(X234)
| ! [X235] :
( ~ r1(X234,X235)
| ? [X236] :
( r1(X235,X236)
& ~ p1(X236) ) )
| ? [X237] :
( r1(X234,X237)
& ~ p1(X237)
& ! [X238] :
( ~ r1(X237,X238)
| ! [X239] :
( ~ r1(X238,X239)
| p1(X239) )
| ~ p1(X238) ) ) )
& ! [X240] :
( ~ r1(X234,X240)
| ! [X241] :
( ~ r1(X240,X241)
| ! [X242] :
( ~ r1(X241,X242)
| p1(X242) ) )
| ? [X243] :
( r1(X240,X243)
& ~ p1(X243) ) ) ) ) ),
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)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ( ( p1(X14)
| ! [X15] :
( ~ r1(X14,X15)
| ( r1(X15,sK14(X15))
& ~ p1(sK14(X15)) ) )
| ( r1(X14,sK15(X14))
& ~ p1(sK15(X14))
& ! [X18] :
( ~ r1(sK15(X14),X18)
| ! [X19] :
( ~ r1(X18,X19)
| p1(X19) )
| ~ p1(X18) ) ) )
& ! [X20] :
( ~ r1(X14,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| p1(X22) ) )
| ( r1(X20,sK16(X20))
& ~ p1(sK16(X20)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X24] :
( ~ r1(sK13,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( ( p1(X36)
| ! [X37] :
( ~ r1(X36,X37)
| ( r1(X37,sK17(X37))
& ~ p1(sK17(X37)) ) )
| ( r1(X36,sK18(X36))
& ~ p1(sK18(X36))
& ! [X40] :
( ~ r1(sK18(X36),X40)
| ! [X41] :
( ~ r1(X40,X41)
| p1(X41) )
| ~ p1(X40) ) ) )
& ! [X42] :
( ~ r1(X36,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ( r1(X42,sK19(X42))
& ~ p1(sK19(X42)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X46] :
( ~ r1(sK13,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| ( r1(X58,sK20(X58))
& ~ p1(sK20(X58)) ) )
| ( r1(X57,sK21(X57))
& ~ p1(sK21(X57))
& ! [X61] :
( ~ r1(sK21(X57),X61)
| ! [X62] :
( ~ r1(X61,X62)
| p1(X62) )
| ~ p1(X61) ) ) )
& ! [X63] :
( ~ r1(X57,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| p1(X65) ) )
| ( r1(X63,sK22(X63))
& ~ p1(sK22(X63)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X67] :
( ~ r1(sK13,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ( ( p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| ( r1(X78,sK23(X78))
& ~ p1(sK23(X78)) ) )
| ( r1(X77,sK24(X77))
& ~ p1(sK24(X77))
& ! [X81] :
( ~ r1(sK24(X77),X81)
| ! [X82] :
( ~ r1(X81,X82)
| p1(X82) )
| ~ p1(X81) ) ) )
& ! [X83] :
( ~ r1(X77,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| p1(X85) ) )
| ( r1(X83,sK25(X83))
& ~ p1(sK25(X83)) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X87] :
( ~ r1(sK13,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ! [X96] :
( ~ r1(X95,X96)
| ( ( p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| ( r1(X97,sK26(X97))
& ~ p1(sK26(X97)) ) )
| ( r1(X96,sK27(X96))
& ~ p1(sK27(X96))
& ! [X100] :
( ~ r1(sK27(X96),X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100) ) ) )
& ! [X102] :
( ~ r1(X96,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) ) )
| ( r1(X102,sK28(X102))
& ~ p1(sK28(X102)) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X106] :
( ~ r1(sK13,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ( ( p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| ( r1(X115,sK29(X115))
& ~ p1(sK29(X115)) ) )
| ( r1(X114,sK30(X114))
& ~ p1(sK30(X114))
& ! [X118] :
( ~ r1(sK30(X114),X118)
| ! [X119] :
( ~ r1(X118,X119)
| p1(X119) )
| ~ p1(X118) ) ) )
& ! [X120] :
( ~ r1(X114,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) ) )
| ( r1(X120,sK31(X120))
& ~ p1(sK31(X120)) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X124] :
( ~ r1(sK13,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ( sP3(X131)
& sP2(X131)
& ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ! [X134] :
( ~ r1(X133,X134)
| p1(X134) ) )
| ( r1(X132,sK32(X132))
& ~ p1(sK32(X132)) ) )
& ( sP0(X131)
| ( r1(X131,sK33(X131))
& ~ p1(sK33(X131))
& ! [X137] :
( ~ r1(sK33(X131),X137)
| ! [X138] :
( ~ r1(X137,X138)
| p1(X138) )
| ~ p1(X137) ) ) ) ) ) ) ) ) ) ) ) )
& r1(sK13,sK34)
& r1(sK34,sK35)
& r1(sK35,sK36)
& r1(sK36,sK37)
& r1(sK37,sK38)
& r1(sK38,sK39)
& r1(sK39,sK40)
& r1(sK40,sK41)
& r1(sK41,sK42)
& ~ p1(sK42)
& r1(sK41,sK43)
& ! [X149] :
( ~ r1(sK43,X149)
| p1(X149) )
& ! [X150] :
( ~ r1(sK41,X150)
| p1(X150)
| ( r1(X150,sK44(X150))
& r1(sK44(X150),sK45(X150))
& ~ p1(sK45(X150))
& p1(sK44(X150)) ) )
& ! [X153] :
( ~ r1(sK13,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ! [X155] :
( ~ r1(X154,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( ( p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| ( r1(X160,sK46(X160))
& ~ p1(sK46(X160)) ) )
| ( r1(X159,sK47(X159))
& ~ p1(sK47(X159))
& ! [X163] :
( ~ r1(sK47(X159),X163)
| ! [X164] :
( ~ r1(X163,X164)
| p1(X164) )
| ~ p1(X163) ) ) )
& ! [X165] :
( ~ r1(X159,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| p1(X167) ) )
| ( r1(X165,sK48(X165))
& ~ p1(sK48(X165)) ) ) ) ) ) ) ) ) ) )
& ! [X169] :
( ~ r1(sK13,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ( ( p1(X174)
| ! [X175] :
( ~ r1(X174,X175)
| ( r1(X175,sK49(X175))
& ~ p1(sK49(X175)) ) )
| ( r1(X174,sK50(X174))
& ~ p1(sK50(X174))
& ! [X178] :
( ~ r1(sK50(X174),X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) )
| ~ p1(X178) ) ) )
& ! [X180] :
( ~ r1(X174,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| p1(X182) ) )
| ( r1(X180,sK51(X180))
& ~ p1(sK51(X180)) ) ) ) ) ) ) ) ) )
& ! [X184] :
( ~ r1(sK13,X184)
| ! [X185] :
( ~ r1(X184,X185)
| ! [X186] :
( ~ r1(X185,X186)
| ! [X187] :
( ~ r1(X186,X187)
| ! [X188] :
( ~ r1(X187,X188)
| ( ( p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| ( r1(X189,sK52(X189))
& ~ p1(sK52(X189)) ) )
| ( r1(X188,sK53(X188))
& ~ p1(sK53(X188))
& ! [X192] :
( ~ r1(sK53(X188),X192)
| ! [X193] :
( ~ r1(X192,X193)
| p1(X193) )
| ~ p1(X192) ) ) )
& ! [X194] :
( ~ r1(X188,X194)
| ! [X195] :
( ~ r1(X194,X195)
| ! [X196] :
( ~ r1(X195,X196)
| p1(X196) ) )
| ( r1(X194,sK54(X194))
& ~ p1(sK54(X194)) ) ) ) ) ) ) ) )
& ! [X198] :
( ~ r1(sK13,X198)
| ! [X199] :
( ~ r1(X198,X199)
| ! [X200] :
( ~ r1(X199,X200)
| ! [X201] :
( ~ r1(X200,X201)
| ( ( p1(X201)
| ! [X202] :
( ~ r1(X201,X202)
| ( r1(X202,sK55(X202))
& ~ p1(sK55(X202)) ) )
| ( r1(X201,sK56(X201))
& ~ p1(sK56(X201))
& ! [X205] :
( ~ r1(sK56(X201),X205)
| ! [X206] :
( ~ r1(X205,X206)
| p1(X206) )
| ~ p1(X205) ) ) )
& ! [X207] :
( ~ r1(X201,X207)
| ! [X208] :
( ~ r1(X207,X208)
| ! [X209] :
( ~ r1(X208,X209)
| p1(X209) ) )
| ( r1(X207,sK57(X207))
& ~ p1(sK57(X207)) ) ) ) ) ) ) )
& ! [X211] :
( ~ r1(sK13,X211)
| ! [X212] :
( ~ r1(X211,X212)
| ! [X213] :
( ~ r1(X212,X213)
| ( ( p1(X213)
| ! [X214] :
( ~ r1(X213,X214)
| ( r1(X214,sK58(X214))
& ~ p1(sK58(X214)) ) )
| ( r1(X213,sK59(X213))
& ~ p1(sK59(X213))
& ! [X217] :
( ~ r1(sK59(X213),X217)
| ! [X218] :
( ~ r1(X217,X218)
| p1(X218) )
| ~ p1(X217) ) ) )
& ! [X219] :
( ~ r1(X213,X219)
| ! [X220] :
( ~ r1(X219,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p1(X221) ) )
| ( r1(X219,sK60(X219))
& ~ p1(sK60(X219)) ) ) ) ) ) )
& ! [X223] :
( ~ r1(sK13,X223)
| ! [X224] :
( ~ r1(X223,X224)
| ( ( p1(X224)
| ! [X225] :
( ~ r1(X224,X225)
| ( r1(X225,sK61(X225))
& ~ p1(sK61(X225)) ) )
| ( r1(X224,sK62(X224))
& ~ p1(sK62(X224))
& ! [X228] :
( ~ r1(sK62(X224),X228)
| ! [X229] :
( ~ r1(X228,X229)
| p1(X229) )
| ~ p1(X228) ) ) )
& ! [X230] :
( ~ r1(X224,X230)
| ! [X231] :
( ~ r1(X230,X231)
| ! [X232] :
( ~ r1(X231,X232)
| p1(X232) ) )
| ( r1(X230,sK63(X230))
& ~ p1(sK63(X230)) ) ) ) ) )
& ! [X234] :
( ~ r1(sK13,X234)
| ( ( p1(X234)
| ! [X235] :
( ~ r1(X234,X235)
| ( r1(X235,sK64(X235))
& ~ p1(sK64(X235)) ) )
| ( r1(X234,sK65(X234))
& ~ p1(sK65(X234))
& ! [X238] :
( ~ r1(sK65(X234),X238)
| ! [X239] :
( ~ r1(X238,X239)
| p1(X239) )
| ~ p1(X238) ) ) )
& ! [X240] :
( ~ r1(X234,X240)
| ! [X241] :
( ~ r1(X240,X241)
| ! [X242] :
( ~ r1(X241,X242)
| p1(X242) ) )
| ( r1(X240,sK66(X240))
& ~ p1(sK66(X240)) ) ) ) ) ),
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,sK50,sK51,sK52,sK53,sK54,sK55,sK56,sK57,sK58,sK59,sK60,sK61,sK62,sK63,sK64,sK65,sK66]),skolemize(X0,sK13),skolemize(X16,sK14(X15)),skolemize(X17,sK15(X14)),skolemize(X23,sK16(X20)),skolemize(X38,sK17(X37)),skolemize(X39,sK18(X36)),skolemize(X45,sK19(X42)),skolemize(X59,sK20(X58)),skolemize(X60,sK21(X57)),skolemize(X66,sK22(X63)),skolemize(X79,sK23(X78)),skolemize(X80,sK24(X77)),skolemize(X86,sK25(X83)),skolemize(X98,sK26(X97)),skolemize(X99,sK27(X96)),skolemize(X105,sK28(X102)),skolemize(X116,sK29(X115)),skolemize(X117,sK30(X114)),skolemize(X123,sK31(X120)),skolemize(X135,sK32(X132)),skolemize(X136,sK33(X131)),skolemize(X139,sK34),skolemize(X140,sK35),skolemize(X141,sK36),skolemize(X142,sK37),skolemize(X143,sK38),skolemize(X144,sK39),skolemize(X145,sK40),skolemize(X146,sK41),skolemize(X147,sK42),skolemize(X148,sK43),skolemize(X151,sK44(X150)),skolemize(X152,sK45(X150)),skolemize(X161,sK46(X160)),skolemize(X162,sK47(X159)),skolemize(X168,sK48(X165)),skolemize(X176,sK49(X175)),skolemize(X177,sK50(X174)),skolemize(X183,sK51(X180)),skolemize(X190,sK52(X189)),skolemize(X191,sK53(X188)),skolemize(X197,sK54(X194)),skolemize(X203,sK55(X202)),skolemize(X204,sK56(X201)),skolemize(X210,sK57(X207)),skolemize(X215,sK58(X214)),skolemize(X216,sK59(X213)),skolemize(X222,sK60(X219)),skolemize(X226,sK61(X225)),skolemize(X227,sK62(X224)),skolemize(X233,sK63(X230)),skolemize(X236,sK64(X235)),skolemize(X237,sK65(X234)),skolemize(X243,sK66(X240))],[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(f103,plain,
! [X150] :
( ~ r1(sK41,X150)
| p1(X150)
| p1(sK44(X150)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f104,plain,
! [X150] :
( ~ p1(sK45(X150))
| p1(X150)
| ~ r1(sK41,X150) ),
inference(cnf_transformation,[],[f25]) ).
fof(f105,plain,
! [X150] :
( r1(sK44(X150),sK45(X150))
| p1(X150)
| ~ r1(sK41,X150) ),
inference(cnf_transformation,[],[f25]) ).
fof(f106,plain,
! [X150] :
( r1(X150,sK44(X150))
| p1(X150)
| ~ r1(sK41,X150) ),
inference(cnf_transformation,[],[f25]) ).
fof(f107,plain,
! [X149] :
( ~ r1(sK43,X149)
| p1(X149) ),
inference(cnf_transformation,[],[f25]) ).
fof(f108,plain,
r1(sK41,sK43),
inference(cnf_transformation,[],[f25]) ).
fof(f109,plain,
~ p1(sK42),
inference(cnf_transformation,[],[f25]) ).
fof(f110,plain,
r1(sK41,sK42),
inference(cnf_transformation,[],[f25]) ).
fof(f111,plain,
r1(sK40,sK41),
inference(cnf_transformation,[],[f25]) ).
fof(f112,plain,
r1(sK39,sK40),
inference(cnf_transformation,[],[f25]) ).
fof(f113,plain,
r1(sK38,sK39),
inference(cnf_transformation,[],[f25]) ).
fof(f114,plain,
r1(sK37,sK38),
inference(cnf_transformation,[],[f25]) ).
fof(f115,plain,
r1(sK36,sK37),
inference(cnf_transformation,[],[f25]) ).
fof(f116,plain,
r1(sK35,sK36),
inference(cnf_transformation,[],[f25]) ).
fof(f117,plain,
r1(sK34,sK35),
inference(cnf_transformation,[],[f25]) ).
fof(f118,plain,
r1(sK13,sK34),
inference(cnf_transformation,[],[f25]) ).
fof(f119,plain,
! [X126,X127,X124,X130,X131,X125,X128,X138,X129,X137] :
( ~ r1(sK33(X131),X137)
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| sP0(X131)
| ~ r1(sK13,X124)
| ~ r1(X137,X138)
| p1(X138)
| ~ p1(X137) ),
inference(cnf_transformation,[],[f25]) ).
fof(f120,plain,
! [X126,X127,X124,X130,X131,X125,X128,X129] :
( ~ p1(sK33(X131))
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| sP0(X131)
| ~ r1(sK13,X124) ),
inference(cnf_transformation,[],[f25]) ).
fof(f121,plain,
! [X126,X127,X124,X130,X125,X131,X128,X129] :
( ~ r1(sK13,X124)
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| sP0(X131)
| r1(X131,sK33(X131)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f122,plain,
! [X132,X133,X126,X127,X124,X130,X125,X131,X128,X129,X134] :
( ~ p1(sK32(X132))
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| ~ r1(X131,X132)
| ~ r1(X132,X133)
| ~ r1(X133,X134)
| p1(X134)
| ~ r1(sK13,X124) ),
inference(cnf_transformation,[],[f25]) ).
fof(f123,plain,
! [X132,X133,X126,X127,X124,X130,X125,X131,X128,X129,X134] :
( ~ r1(sK13,X124)
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| ~ r1(X131,X132)
| ~ r1(X132,X133)
| ~ r1(X133,X134)
| p1(X134)
| r1(X132,sK32(X132)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f124,plain,
! [X126,X127,X124,X130,X125,X131,X128,X129] :
( ~ r1(sK13,X124)
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| sP2(X131) ),
inference(cnf_transformation,[],[f25]) ).
fof(f125,plain,
! [X126,X127,X124,X130,X125,X131,X128,X129] :
( ~ r1(sK13,X124)
| ~ r1(X124,X125)
| ~ r1(X125,X126)
| ~ r1(X126,X127)
| ~ r1(X127,X128)
| ~ r1(X128,X129)
| ~ r1(X129,X130)
| ~ r1(X130,X131)
| sP3(X131) ),
inference(cnf_transformation,[],[f25]) ).
fof(f183,plain,
( p1(sK41)
| r1(sK43,sK6(sK43))
| r1(sK41,sK7(sK41))
| ~ sP2(sK41) ),
inference(resolution,[],[f35,f108]) ).
fof(f185,definition,
( spl67_1
<=> sP2(sK41) ),
introduced(definition,[new_symbols(definition,[spl67_1])],[avatar_definition]) ).
fof(f186,plain,
( sP2(sK41)
| ~ spl67_1 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f187,plain,
( ~ sP2(sK41)
| spl67_1 ),
inference(avatar_component_clause,[],[f185]) ).
fof(f189,definition,
( spl67_2
<=> r1(sK41,sK7(sK41)) ),
introduced(definition,[new_symbols(definition,[spl67_2])],[avatar_definition]) ).
fof(f190,plain,
( ~ r1(sK41,sK7(sK41))
| spl67_2 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f191,plain,
( r1(sK41,sK7(sK41))
| ~ spl67_2 ),
inference(avatar_component_clause,[],[f189]) ).
fof(f193,definition,
( spl67_3
<=> r1(sK43,sK6(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_3])],[avatar_definition]) ).
fof(f195,plain,
( r1(sK43,sK6(sK43))
| ~ spl67_3 ),
inference(avatar_component_clause,[],[f193]) ).
fof(f197,definition,
( spl67_4
<=> p1(sK41) ),
introduced(definition,[new_symbols(definition,[spl67_4])],[avatar_definition]) ).
fof(f198,plain,
( ~ p1(sK41)
| spl67_4 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f199,plain,
( p1(sK41)
| ~ spl67_4 ),
inference(avatar_component_clause,[],[f197]) ).
fof(f200,plain,
( ~ spl67_1
| spl67_2
| spl67_3
| spl67_4 ),
inference(avatar_split_clause,[],[f183,f197,f193,f189,f185]) ).
fof(f454,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(f455,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(f456,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f43]) ).
fof(f458,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f456,f40]) ).
fof(f459,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f455,f40]) ).
fof(f460,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f454,f40]) ).
fof(f466,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(f468,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0) ),
inference(duplicate_literal_removal,[],[f466]) ).
fof(f469,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f468,f40]) ).
fof(f495,plain,
! [X0] :
( p1(X0)
| ~ p1(sK41)
| ~ r1(sK41,X0)
| r1(sK43,sK4(sK43))
| sP1(sK41)
| ~ sP3(sK41) ),
inference(resolution,[],[f29,f108]) ).
fof(f496,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| r1(sK43,sK4(sK43))
| sP1(sK41)
| ~ sP3(sK41) )
| ~ spl67_4 ),
inference(forward_subsumption_resolution,[],[f495,f199]) ).
fof(f523,definition,
( spl67_63
<=> sP3(sK41) ),
introduced(definition,[new_symbols(definition,[spl67_63])],[avatar_definition]) ).
fof(f524,plain,
( sP3(sK41)
| ~ spl67_63 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f525,plain,
( ~ sP3(sK41)
| spl67_63 ),
inference(avatar_component_clause,[],[f523]) ).
fof(f527,definition,
( spl67_64
<=> sP1(sK41) ),
introduced(definition,[new_symbols(definition,[spl67_64])],[avatar_definition]) ).
fof(f528,plain,
( ~ sP1(sK41)
| spl67_64 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f529,plain,
( sP1(sK41)
| ~ spl67_64 ),
inference(avatar_component_clause,[],[f527]) ).
fof(f531,definition,
( spl67_65
<=> r1(sK43,sK4(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_65])],[avatar_definition]) ).
fof(f533,plain,
( r1(sK43,sK4(sK43))
| ~ spl67_65 ),
inference(avatar_component_clause,[],[f531]) ).
fof(f535,definition,
( spl67_66
<=> ! [X0] :
( p1(X0)
| ~ r1(sK41,X0) ) ),
introduced(definition,[new_symbols(definition,[spl67_66])],[avatar_definition]) ).
fof(f536,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| p1(X0) )
| ~ spl67_66 ),
inference(avatar_component_clause,[],[f535]) ).
fof(f537,plain,
( ~ spl67_63
| spl67_64
| spl67_65
| spl67_66
| ~ spl67_4 ),
inference(avatar_split_clause,[],[f496,f197,f535,f531,f527,f523]) ).
fof(f655,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK34,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP3(X6) ),
inference(resolution,[],[f125,f118]) ).
fof(f686,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK34,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP2(X6) ),
inference(resolution,[],[f124,f118]) ).
fof(f689,plain,
! [X0] :
( ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f458,f42]) ).
fof(f690,plain,
! [X0] :
( p1(sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f689]) ).
fof(f696,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK44(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK44(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK41,sK7(X0)) ),
inference(resolution,[],[f33,f106]) ).
fof(f697,plain,
! [X2,X0,X1] :
( ~ r1(sK44(sK7(X0)),X2)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK44(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK41,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f696,f34]) ).
fof(f711,plain,
! [X0] :
( p1(X0)
| ~ p1(sK41)
| ~ r1(sK41,X0)
| r1(sK4(sK43),sK5(sK43))
| sP1(sK41)
| ~ sP3(sK41) ),
inference(resolution,[],[f28,f108]) ).
fof(f713,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f459,f42]) ).
fof(f714,plain,
! [X0] :
( r1(sK9(X0),sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f713]) ).
fof(f715,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0)))
| ~ sP1(X0) ),
inference(resolution,[],[f714,f469]) ).
fof(f722,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0))) ),
inference(duplicate_literal_removal,[],[f715]) ).
fof(f724,plain,
! [X0,X1] :
( ~ r1(sK11(sK9(X0)),X1)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(X1) ),
inference(forward_subsumption_resolution,[],[f722,f690]) ).
fof(f760,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(sK44(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK44(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK41,sK7(X0)) ),
inference(resolution,[],[f30,f106]) ).
fof(f761,plain,
! [X2,X0,X1] :
( ~ r1(sK44(sK7(X0)),X2)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK44(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK41,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f760,f31]) ).
fof(f768,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| ~ p1(sK44(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK41,sK7(X1)) ),
inference(resolution,[],[f761,f105]) ).
fof(f771,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| ~ p1(sK44(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f768]) ).
fof(f772,plain,
! [X0,X1] :
( ~ p1(sK44(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| ~ p1(sK6(X0))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f771,f31]) ).
fof(f773,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f460,f42]) ).
fof(f774,plain,
! [X0] :
( r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f773]) ).
fof(f775,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(sK12(sK9(X0))) ),
inference(resolution,[],[f774,f724]) ).
fof(f783,plain,
! [X0] :
( p1(sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(duplicate_literal_removal,[],[f775]) ).
fof(f784,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X1,sK9(X0))
| p1(sK9(X0))
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(resolution,[],[f783,f44]) ).
fof(f785,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK9(X0))
| ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(forward_subsumption_resolution,[],[f784,f40]) ).
fof(f786,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X1,sK8(X0))
| ~ sP0(X1)
| ~ sP1(X0) ),
inference(resolution,[],[f785,f41]) ).
fof(f787,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP0(X0)
| ~ sP1(X0)
| ~ sP0(X1) ),
inference(duplicate_literal_removal,[],[f786]) ).
fof(f788,plain,
! [X0] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f787,f42]) ).
fof(f789,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f788]) ).
fof(f790,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK35,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP3(X5) ),
inference(resolution,[],[f655,f117]) ).
fof(f797,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK36,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP3(X4) ),
inference(resolution,[],[f790,f116]) ).
fof(f804,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP3(X3) ),
inference(resolution,[],[f797,f115]) ).
fof(f811,plain,
! [X2,X0,X1] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP3(X2) ),
inference(resolution,[],[f804,f114]) ).
fof(f818,plain,
! [X0,X1] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| sP3(X1) ),
inference(resolution,[],[f811,f113]) ).
fof(f825,plain,
! [X0] :
( ~ r1(sK40,X0)
| sP3(X0) ),
inference(resolution,[],[f818,f112]) ).
fof(f832,plain,
sP3(sK41),
inference(resolution,[],[f825,f111]) ).
fof(f840,plain,
( $false
| spl67_63 ),
inference(forward_subsumption_resolution,[],[f832,f525]) ).
fof(f841,plain,
spl67_63,
inference(avatar_contradiction_clause,[],[f840]) ).
fof(f854,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK35,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP2(X5) ),
inference(resolution,[],[f686,f117]) ).
fof(f857,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK36,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP2(X4) ),
inference(resolution,[],[f854,f116]) ).
fof(f860,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP2(X3) ),
inference(resolution,[],[f857,f115]) ).
fof(f863,plain,
! [X2,X0,X1] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP2(X2) ),
inference(resolution,[],[f860,f114]) ).
fof(f866,plain,
! [X0,X1] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| sP2(X1) ),
inference(resolution,[],[f863,f113]) ).
fof(f869,plain,
! [X0] :
( ~ r1(sK40,X0)
| sP2(X0) ),
inference(resolution,[],[f866,f112]) ).
fof(f872,plain,
sP2(sK41),
inference(resolution,[],[f869,f111]) ).
fof(f875,plain,
( $false
| spl67_1 ),
inference(forward_subsumption_resolution,[],[f872,f187]) ).
fof(f876,plain,
spl67_1,
inference(avatar_contradiction_clause,[],[f875]) ).
fof(f920,plain,
( p1(sK6(sK43))
| ~ spl67_3 ),
inference(resolution,[],[f195,f107]) ).
fof(f933,definition,
( spl67_117
<=> p1(sK6(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_117])],[avatar_definition]) ).
fof(f935,plain,
( p1(sK6(sK43))
| ~ spl67_117 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f950,plain,
( spl67_117
| ~ spl67_3 ),
inference(avatar_split_clause,[],[f920,f193,f933]) ).
fof(f951,plain,
( ~ sP0(sK41)
| ~ spl67_64 ),
inference(resolution,[],[f529,f789]) ).
fof(f952,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| ~ p1(sK44(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK41,sK7(X1)) ),
inference(resolution,[],[f697,f105]) ).
fof(f955,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| ~ p1(sK44(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f952]) ).
fof(f956,plain,
! [X0,X1] :
( ~ p1(sK44(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK45(sK7(X1)))
| r1(X0,sK6(X0))
| ~ sP2(X1)
| ~ r1(sK41,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f955,f34]) ).
fof(f957,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK34,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| r1(X6,sK33(X6)) ),
inference(resolution,[],[f121,f118]) ).
fof(f996,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK35,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| r1(X5,sK33(X5)) ),
inference(resolution,[],[f957,f117]) ).
fof(f999,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK36,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| r1(X4,sK33(X4)) ),
inference(resolution,[],[f996,f116]) ).
fof(f1002,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP0(X3)
| r1(X3,sK33(X3)) ),
inference(resolution,[],[f999,f115]) ).
fof(f1005,plain,
! [X2,X0,X1] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP0(X2)
| r1(X2,sK33(X2)) ),
inference(resolution,[],[f1002,f114]) ).
fof(f1008,plain,
! [X0,X1] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| sP0(X1)
| r1(X1,sK33(X1)) ),
inference(resolution,[],[f1005,f113]) ).
fof(f1011,plain,
! [X0] :
( r1(X0,sK33(X0))
| sP0(X0)
| ~ r1(sK40,X0) ),
inference(resolution,[],[f1008,f112]) ).
fof(f1057,plain,
( sP0(sK41)
| ~ r1(sK40,sK41)
| p1(sK33(sK41))
| p1(sK44(sK33(sK41))) ),
inference(resolution,[],[f1011,f103]) ).
fof(f1257,definition,
( spl67_166
<=> p1(sK44(sK33(sK41))) ),
introduced(definition,[new_symbols(definition,[spl67_166])],[avatar_definition]) ).
fof(f1259,plain,
( p1(sK44(sK33(sK41)))
| ~ spl67_166 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1261,definition,
( spl67_167
<=> p1(sK33(sK41)) ),
introduced(definition,[new_symbols(definition,[spl67_167])],[avatar_definition]) ).
fof(f1262,plain,
( ~ p1(sK33(sK41))
| spl67_167 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1263,plain,
( p1(sK33(sK41))
| ~ spl67_167 ),
inference(avatar_component_clause,[],[f1261]) ).
fof(f1265,plain,
( sP0(sK41)
| p1(sK33(sK41))
| p1(sK44(sK33(sK41))) ),
inference(forward_subsumption_resolution,[],[f1057,f111]) ).
fof(f1267,definition,
( spl67_168
<=> sP0(sK41) ),
introduced(definition,[new_symbols(definition,[spl67_168])],[avatar_definition]) ).
fof(f1268,plain,
( ~ sP0(sK41)
| spl67_168 ),
inference(avatar_component_clause,[],[f1267]) ).
fof(f1270,plain,
( spl67_166
| spl67_167
| spl67_168 ),
inference(avatar_split_clause,[],[f1265,f1267,f1261,f1257]) ).
fof(f1271,plain,
( p1(sK42)
| ~ spl67_66 ),
inference(resolution,[],[f536,f110]) ).
fof(f1277,plain,
( $false
| ~ spl67_66 ),
inference(forward_subsumption_resolution,[],[f1271,f109]) ).
fof(f1278,plain,
~ spl67_66,
inference(avatar_contradiction_clause,[],[f1277]) ).
fof(f1280,plain,
( ~ spl67_168
| ~ spl67_64 ),
inference(avatar_split_clause,[],[f951,f527,f1267]) ).
fof(f1287,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK34,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK32(X7)) ),
inference(resolution,[],[f123,f118]) ).
fof(f1606,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP0(X7)
| ~ r1(sK13,X0)
| ~ r1(sK44(sK33(X7)),X8)
| p1(X8)
| ~ p1(sK44(sK33(X7)))
| p1(sK33(X7))
| ~ r1(sK41,sK33(X7)) ),
inference(resolution,[],[f119,f106]) ).
fof(f1608,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK44(sK33(X7)),X8)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP0(X7)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(X8)
| ~ p1(sK44(sK33(X7)))
| ~ r1(sK41,sK33(X7)) ),
inference(forward_subsumption_resolution,[],[f1606,f120]) ).
fof(f1610,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,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK45(sK33(X6)))
| ~ p1(sK44(sK33(X6)))
| ~ r1(sK41,sK33(X6))
| p1(sK33(X6))
| ~ r1(sK41,sK33(X6)) ),
inference(resolution,[],[f1608,f105]) ).
fof(f1616,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,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK45(sK33(X6)))
| ~ p1(sK44(sK33(X6)))
| ~ r1(sK41,sK33(X6))
| p1(sK33(X6)) ),
inference(duplicate_literal_removal,[],[f1610]) ).
fof(f1618,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p1(sK44(sK33(X6)))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK45(sK33(X6)))
| ~ r1(X0,X1)
| ~ r1(sK41,sK33(X6)) ),
inference(forward_subsumption_resolution,[],[f1616,f120]) ).
fof(f1619,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK41)
| sP0(sK41)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK45(sK33(sK41)))
| ~ r1(X6,X0)
| ~ r1(sK41,sK33(sK41)) )
| ~ spl67_166 ),
inference(resolution,[],[f1618,f1259]) ).
fof(f1620,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK41)
| sP0(sK41)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK45(sK33(sK41)))
| ~ r1(X6,X0) )
| ~ spl67_166 ),
inference(forward_subsumption_resolution,[],[f1619,f121]) ).
fof(f1621,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK41)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK45(sK33(sK41)))
| ~ r1(X6,X0) )
| ~ spl67_166
| spl67_168 ),
inference(forward_subsumption_resolution,[],[f1620,f1268]) ).
fof(f1623,definition,
( spl67_190
<=> p1(sK45(sK33(sK41))) ),
introduced(definition,[new_symbols(definition,[spl67_190])],[avatar_definition]) ).
fof(f1625,plain,
( p1(sK45(sK33(sK41)))
| ~ spl67_190 ),
inference(avatar_component_clause,[],[f1623]) ).
fof(f1627,definition,
( spl67_191
<=> ! [X2,X6,X4,X3,X0,X5,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X5)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,sK41)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl67_191])],[avatar_definition]) ).
fof(f1628,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK13,X5)
| ~ r1(X0,X1)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,sK41)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl67_191 ),
inference(avatar_component_clause,[],[f1627]) ).
fof(f1629,plain,
( spl67_190
| spl67_191
| ~ spl67_166
| spl67_168 ),
inference(avatar_split_clause,[],[f1621,f1267,f1257,f1627,f1623]) ).
fof(f1630,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,sK41)
| sP0(sK41)
| ~ r1(sK13,X0) )
| ~ spl67_167 ),
inference(resolution,[],[f1263,f120]) ).
fof(f1631,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,sK41)
| ~ r1(sK13,X0) )
| ~ spl67_167
| spl67_168 ),
inference(forward_subsumption_resolution,[],[f1630,f1268]) ).
fof(f1632,plain,
( spl67_191
| ~ spl67_167
| spl67_168 ),
inference(avatar_split_clause,[],[f1631,f1267,f1261,f1627]) ).
fof(f1633,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| r1(sK4(sK43),sK5(sK43))
| sP1(sK41)
| ~ sP3(sK41) )
| ~ spl67_4 ),
inference(forward_subsumption_resolution,[],[f711,f199]) ).
fof(f1637,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| r1(sK4(sK43),sK5(sK43))
| ~ sP3(sK41) )
| ~ spl67_4
| spl67_64 ),
inference(forward_subsumption_resolution,[],[f1633,f528]) ).
fof(f1641,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| r1(sK4(sK43),sK5(sK43)) )
| ~ spl67_4
| ~ spl67_63
| spl67_64 ),
inference(forward_subsumption_resolution,[],[f1637,f524]) ).
fof(f1646,definition,
( spl67_192
<=> r1(sK4(sK43),sK5(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_192])],[avatar_definition]) ).
fof(f1648,plain,
( r1(sK4(sK43),sK5(sK43))
| ~ spl67_192 ),
inference(avatar_component_clause,[],[f1646]) ).
fof(f1649,plain,
( spl67_192
| spl67_66
| ~ spl67_4
| ~ spl67_63
| spl67_64 ),
inference(avatar_split_clause,[],[f1641,f527,f523,f197,f535,f1646]) ).
fof(f1700,definition,
( spl67_197
<=> p1(sK5(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_197])],[avatar_definition]) ).
fof(f1701,plain,
( ~ p1(sK5(sK43))
| spl67_197 ),
inference(avatar_component_clause,[],[f1700]) ).
fof(f1702,plain,
( p1(sK5(sK43))
| ~ spl67_197 ),
inference(avatar_component_clause,[],[f1700]) ).
fof(f1733,definition,
( spl67_204
<=> ! [X0] :
( p1(X0)
| ~ r1(sK4(sK43),X0) ) ),
introduced(definition,[new_symbols(definition,[spl67_204])],[avatar_definition]) ).
fof(f1734,plain,
( ! [X0] :
( ~ r1(sK4(sK43),X0)
| p1(X0) )
| ~ spl67_204 ),
inference(avatar_component_clause,[],[f1733]) ).
fof(f1774,plain,
( p1(sK7(sK41))
| p1(sK44(sK7(sK41)))
| ~ spl67_2 ),
inference(resolution,[],[f191,f103]) ).
fof(f1783,definition,
( spl67_212
<=> p1(sK44(sK7(sK41))) ),
introduced(definition,[new_symbols(definition,[spl67_212])],[avatar_definition]) ).
fof(f1785,plain,
( p1(sK44(sK7(sK41)))
| ~ spl67_212 ),
inference(avatar_component_clause,[],[f1783]) ).
fof(f1787,definition,
( spl67_213
<=> p1(sK7(sK41)) ),
introduced(definition,[new_symbols(definition,[spl67_213])],[avatar_definition]) ).
fof(f1788,plain,
( ~ p1(sK7(sK41))
| spl67_213 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1789,plain,
( p1(sK7(sK41))
| ~ spl67_213 ),
inference(avatar_component_clause,[],[f1787]) ).
fof(f1790,plain,
( spl67_212
| spl67_213
| ~ spl67_2 ),
inference(avatar_split_clause,[],[f1774,f189,f1787,f1783]) ).
fof(f1849,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| r1(X0,sK6(X0))
| p1(sK41)
| ~ sP2(sK41) )
| ~ spl67_213 ),
inference(resolution,[],[f1789,f34]) ).
fof(f1850,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0))
| p1(sK41)
| ~ sP2(sK41) )
| ~ spl67_213 ),
inference(resolution,[],[f1789,f31]) ).
fof(f1851,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0))
| ~ sP2(sK41) )
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1850,f198]) ).
fof(f1852,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK41) )
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1849,f198]) ).
fof(f1853,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0)) )
| ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1851,f186]) ).
fof(f1854,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK41,X0) )
| ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1852,f186]) ).
fof(f1946,plain,
( ~ r1(sK41,sK43)
| p1(sK6(sK43))
| ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(resolution,[],[f1854,f107]) ).
fof(f1980,plain,
( ~ r1(sK41,sK43)
| ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1946,f1853]) ).
fof(f2222,plain,
( $false
| ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(forward_subsumption_resolution,[],[f1980,f108]) ).
fof(f2223,plain,
( ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(avatar_contradiction_clause,[],[f2222]) ).
fof(f2640,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK35,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK32(X6)) ),
inference(resolution,[],[f1287,f117]) ).
fof(f2644,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK36,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,sK32(X5)) ),
inference(resolution,[],[f2640,f116]) ).
fof(f2648,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK37,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK32(X4)) ),
inference(resolution,[],[f2644,f115]) ).
fof(f2652,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK32(X3)) ),
inference(resolution,[],[f2648,f114]) ).
fof(f2656,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK32(X2)) ),
inference(resolution,[],[f2652,f113]) ).
fof(f2660,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK40,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK32(X1)) ),
inference(resolution,[],[f2656,f112]) ).
fof(f2664,plain,
! [X2,X0,X1] :
( ~ r1(sK41,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK32(X0)) ),
inference(resolution,[],[f2660,f111]) ).
fof(f2670,plain,
! [X0,X1] :
( ~ r1(sK43,X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK43,sK32(sK43)) ),
inference(resolution,[],[f2664,f108]) ).
fof(f2684,definition,
( spl67_336
<=> r1(sK43,sK32(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_336])],[avatar_definition]) ).
fof(f2686,plain,
( r1(sK43,sK32(sK43))
| ~ spl67_336 ),
inference(avatar_component_clause,[],[f2684]) ).
fof(f2688,definition,
( spl67_337
<=> ! [X0,X1] :
( ~ r1(sK43,X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl67_337])],[avatar_definition]) ).
fof(f2689,plain,
( ! [X0,X1] :
( ~ r1(sK43,X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl67_337 ),
inference(avatar_component_clause,[],[f2688]) ).
fof(f2690,plain,
( spl67_336
| spl67_337 ),
inference(avatar_split_clause,[],[f2670,f2688,f2684]) ).
fof(f2717,plain,
( p1(sK32(sK43))
| ~ spl67_336 ),
inference(resolution,[],[f2686,f107]) ).
fof(f2736,definition,
( spl67_343
<=> p1(sK32(sK43)) ),
introduced(definition,[new_symbols(definition,[spl67_343])],[avatar_definition]) ).
fof(f2738,plain,
( p1(sK32(sK43))
| ~ spl67_343 ),
inference(avatar_component_clause,[],[f2736]) ).
fof(f2758,plain,
( spl67_343
| ~ spl67_336 ),
inference(avatar_split_clause,[],[f2717,f2684,f2736]) ).
fof(f2759,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK4(sK43),X0) )
| ~ spl67_65
| ~ spl67_337 ),
inference(resolution,[],[f2689,f533]) ).
fof(f2763,plain,
( spl67_204
| ~ spl67_65
| ~ spl67_337 ),
inference(avatar_split_clause,[],[f2759,f2688,f531,f1733]) ).
fof(f2908,definition,
( spl67_366
<=> ! [X0] :
( ~ r1(sK41,X0)
| r1(X0,sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl67_366])],[avatar_definition]) ).
fof(f2909,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK41,X0) )
| ~ spl67_366 ),
inference(avatar_component_clause,[],[f2908]) ).
fof(f2912,definition,
( spl67_367
<=> ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl67_367])],[avatar_definition]) ).
fof(f2913,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK41,X0) )
| ~ spl67_367 ),
inference(avatar_component_clause,[],[f2912]) ).
fof(f2959,plain,
( ! [X0] :
( r1(X0,sK7(X0))
| p1(X0)
| ~ r1(X0,sK43)
| ~ sP2(X0) )
| ~ spl67_117 ),
inference(resolution,[],[f935,f32]) ).
fof(f3085,plain,
( p1(sK41)
| ~ r1(sK41,sK43)
| ~ sP2(sK41)
| spl67_2
| ~ spl67_117 ),
inference(resolution,[],[f2959,f190]) ).
fof(f3165,plain,
( ~ r1(sK41,sK43)
| ~ sP2(sK41)
| spl67_2
| spl67_4
| ~ spl67_117 ),
inference(forward_subsumption_resolution,[],[f3085,f198]) ).
fof(f3177,plain,
( ~ sP2(sK41)
| spl67_2
| spl67_4
| ~ spl67_117 ),
inference(forward_subsumption_resolution,[],[f3165,f108]) ).
fof(f3185,plain,
( $false
| ~ spl67_1
| spl67_2
| spl67_4
| ~ spl67_117 ),
inference(forward_subsumption_resolution,[],[f3177,f186]) ).
fof(f3186,plain,
( ~ spl67_1
| spl67_2
| spl67_4
| ~ spl67_117 ),
inference(avatar_contradiction_clause,[],[f3185]) ).
fof(f3385,plain,
( ~ r1(sK41,sK43)
| p1(sK6(sK43))
| ~ spl67_366 ),
inference(resolution,[],[f2909,f107]) ).
fof(f3436,plain,
( ~ r1(sK41,sK43)
| ~ spl67_366
| ~ spl67_367 ),
inference(forward_subsumption_resolution,[],[f3385,f2913]) ).
fof(f3620,plain,
( $false
| ~ spl67_366
| ~ spl67_367 ),
inference(forward_subsumption_resolution,[],[f3436,f108]) ).
fof(f3621,plain,
( ~ spl67_366
| ~ spl67_367 ),
inference(avatar_contradiction_clause,[],[f3620]) ).
fof(f4127,plain,
( ! [X0] :
( p1(sK41)
| ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| r1(X0,sK6(X0))
| ~ sP2(sK41)
| ~ r1(sK41,sK7(sK41)) )
| ~ spl67_212 ),
inference(resolution,[],[f956,f1785]) ).
fof(f4128,plain,
( ! [X0] :
( p1(sK41)
| ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| r1(X0,sK6(X0))
| ~ sP2(sK41) )
| ~ spl67_212 ),
inference(forward_subsumption_resolution,[],[f4127,f35]) ).
fof(f4129,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| r1(X0,sK6(X0))
| ~ sP2(sK41) )
| spl67_4
| ~ spl67_212 ),
inference(forward_subsumption_resolution,[],[f4128,f198]) ).
fof(f4130,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| r1(X0,sK6(X0)) )
| ~ spl67_1
| spl67_4
| ~ spl67_212 ),
inference(forward_subsumption_resolution,[],[f4129,f186]) ).
fof(f4132,definition,
( spl67_466
<=> p1(sK45(sK7(sK41))) ),
introduced(definition,[new_symbols(definition,[spl67_466])],[avatar_definition]) ).
fof(f4133,plain,
( ~ p1(sK45(sK7(sK41)))
| spl67_466 ),
inference(avatar_component_clause,[],[f4132]) ).
fof(f4134,plain,
( p1(sK45(sK7(sK41)))
| ~ spl67_466 ),
inference(avatar_component_clause,[],[f4132]) ).
fof(f4135,plain,
( spl67_466
| spl67_366
| ~ spl67_1
| spl67_4
| ~ spl67_212 ),
inference(avatar_split_clause,[],[f4130,f1783,f197,f185,f2908,f4132]) ).
fof(f4136,plain,
( p1(sK7(sK41))
| ~ r1(sK41,sK7(sK41))
| ~ spl67_466 ),
inference(resolution,[],[f4134,f104]) ).
fof(f4137,plain,
( ~ r1(sK41,sK7(sK41))
| spl67_213
| ~ spl67_466 ),
inference(forward_subsumption_resolution,[],[f4136,f1788]) ).
fof(f4138,plain,
( $false
| ~ spl67_2
| spl67_213
| ~ spl67_466 ),
inference(forward_subsumption_resolution,[],[f4137,f191]) ).
fof(f4139,plain,
( ~ spl67_2
| spl67_213
| ~ spl67_466 ),
inference(avatar_contradiction_clause,[],[f4138]) ).
fof(f4523,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,sK43)
| ~ r1(sK43,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(sK13,X0) )
| ~ spl67_343 ),
inference(resolution,[],[f2738,f122]) ).
fof(f4525,definition,
( spl67_474
<=> ! [X5,X3,X4,X2,X0,X6,X1,X7] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X7,sK43)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl67_474])],[avatar_definition]) ).
fof(f4526,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X7,sK43)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl67_474 ),
inference(avatar_component_clause,[],[f4525]) ).
fof(f4527,plain,
( spl67_337
| spl67_474
| ~ spl67_343 ),
inference(avatar_split_clause,[],[f4523,f2736,f4525,f2688]) ).
fof(f4528,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK34,X0)
| ~ r1(X1,sK43)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X6,X5)
| ~ r1(X0,X6) )
| ~ spl67_474 ),
inference(resolution,[],[f4526,f118]) ).
fof(f4535,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK35,X5)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X0,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4528,f117]) ).
fof(f4542,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK36,X4)
| ~ r1(X2,X0)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X0,X1)
| ~ r1(X1,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4535,f116]) ).
fof(f4549,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK37,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X3)
| ~ r1(X3,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4542,f115]) ).
fof(f4556,plain,
( ! [X2,X0,X1] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4549,f114]) ).
fof(f4563,plain,
( ! [X0,X1] :
( ~ r1(sK39,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4556,f113]) ).
fof(f4570,plain,
( ! [X0] :
( ~ r1(sK40,X0)
| ~ r1(X0,sK43) )
| ~ spl67_474 ),
inference(resolution,[],[f4563,f112]) ).
fof(f4577,plain,
( ~ r1(sK41,sK43)
| ~ spl67_474 ),
inference(resolution,[],[f4570,f111]) ).
fof(f4584,plain,
( $false
| ~ spl67_474 ),
inference(forward_subsumption_resolution,[],[f4577,f108]) ).
fof(f4585,plain,
~ spl67_474,
inference(avatar_contradiction_clause,[],[f4584]) ).
fof(f4679,plain,
( ! [X0] :
( p1(sK41)
| ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| ~ p1(sK6(X0))
| ~ sP2(sK41)
| ~ r1(sK41,sK7(sK41)) )
| ~ spl67_212 ),
inference(resolution,[],[f772,f1785]) ).
fof(f4680,plain,
( ! [X0] :
( p1(sK41)
| ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| ~ p1(sK6(X0))
| ~ sP2(sK41) )
| ~ spl67_212 ),
inference(forward_subsumption_resolution,[],[f4679,f32]) ).
fof(f4681,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| p1(sK45(sK7(sK41)))
| ~ p1(sK6(X0))
| ~ sP2(sK41) )
| spl67_4
| ~ spl67_212 ),
inference(forward_subsumption_resolution,[],[f4680,f198]) ).
fof(f4682,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0))
| ~ sP2(sK41) )
| spl67_4
| ~ spl67_212
| spl67_466 ),
inference(forward_subsumption_resolution,[],[f4681,f4133]) ).
fof(f4683,plain,
( ! [X0] :
( ~ r1(sK41,X0)
| ~ p1(sK6(X0)) )
| ~ spl67_1
| spl67_4
| ~ spl67_212
| spl67_466 ),
inference(forward_subsumption_resolution,[],[f4682,f186]) ).
fof(f4684,plain,
( spl67_367
| ~ spl67_1
| spl67_4
| ~ spl67_212
| spl67_466 ),
inference(avatar_split_clause,[],[f4683,f4132,f1783,f197,f185,f2912]) ).
fof(f4733,plain,
( p1(sK5(sK43))
| ~ spl67_192
| ~ spl67_204 ),
inference(resolution,[],[f1648,f1734]) ).
fof(f4818,plain,
( ! [X0,X1] :
( ~ r1(X1,sK43)
| ~ p1(X1)
| p1(X0)
| ~ r1(X1,X0)
| sP1(X1)
| ~ sP3(X1) )
| ~ spl67_197 ),
inference(resolution,[],[f1702,f27]) ).
fof(f4959,plain,
( ! [X0] :
( ~ p1(sK41)
| p1(X0)
| ~ r1(sK41,X0)
| sP1(sK41)
| ~ sP3(sK41) )
| ~ spl67_197 ),
inference(resolution,[],[f4818,f108]) ).
fof(f4960,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| sP1(sK41)
| ~ sP3(sK41) )
| ~ spl67_4
| ~ spl67_197 ),
inference(forward_subsumption_resolution,[],[f4959,f199]) ).
fof(f4961,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0)
| ~ sP3(sK41) )
| ~ spl67_4
| spl67_64
| ~ spl67_197 ),
inference(forward_subsumption_resolution,[],[f4960,f528]) ).
fof(f4962,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK41,X0) )
| ~ spl67_4
| ~ spl67_63
| spl67_64
| ~ spl67_197 ),
inference(forward_subsumption_resolution,[],[f4961,f524]) ).
fof(f4963,plain,
( spl67_66
| ~ spl67_4
| ~ spl67_63
| spl67_64
| ~ spl67_197 ),
inference(avatar_split_clause,[],[f4962,f1700,f527,f523,f197,f535]) ).
fof(f4964,plain,
( $false
| ~ spl67_192
| spl67_197
| ~ spl67_204 ),
inference(forward_subsumption_resolution,[],[f4733,f1701]) ).
fof(f4965,plain,
( ~ spl67_192
| spl67_197
| ~ spl67_204 ),
inference(avatar_contradiction_clause,[],[f4964]) ).
fof(f5023,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK34,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X3,sK41)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X1,X5) )
| ~ spl67_191 ),
inference(resolution,[],[f1628,f118]) ).
fof(f5030,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK35,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK41)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X1,X4) )
| ~ spl67_191 ),
inference(resolution,[],[f5023,f117]) ).
fof(f5037,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK36,X0)
| ~ r1(X1,sK41)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X0,X3) )
| ~ spl67_191 ),
inference(resolution,[],[f5030,f116]) ).
fof(f5044,plain,
( ! [X2,X0,X1] :
( ~ r1(sK37,X2)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X0,sK41) )
| ~ spl67_191 ),
inference(resolution,[],[f5037,f115]) ).
fof(f5051,plain,
( ! [X0,X1] :
( ~ r1(sK38,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK41) )
| ~ spl67_191 ),
inference(resolution,[],[f5044,f114]) ).
fof(f5058,plain,
( ! [X0] :
( ~ r1(sK39,X0)
| ~ r1(X0,sK41) )
| ~ spl67_191 ),
inference(resolution,[],[f5051,f113]) ).
fof(f5065,plain,
( ~ r1(sK40,sK41)
| ~ spl67_191 ),
inference(resolution,[],[f5058,f112]) ).
fof(f5072,plain,
( $false
| ~ spl67_191 ),
inference(forward_subsumption_resolution,[],[f5065,f111]) ).
fof(f5073,plain,
~ spl67_191,
inference(avatar_contradiction_clause,[],[f5072]) ).
fof(f5076,plain,
( p1(sK33(sK41))
| ~ r1(sK41,sK33(sK41))
| ~ spl67_190 ),
inference(resolution,[],[f1625,f104]) ).
fof(f5077,plain,
( ~ r1(sK41,sK33(sK41))
| spl67_167
| ~ spl67_190 ),
inference(forward_subsumption_resolution,[],[f5076,f1262]) ).
fof(f5078,plain,
( sP0(sK41)
| ~ r1(sK40,sK41)
| spl67_167
| ~ spl67_190 ),
inference(resolution,[],[f5077,f1011]) ).
fof(f5079,plain,
( ~ r1(sK40,sK41)
| spl67_167
| spl67_168
| ~ spl67_190 ),
inference(forward_subsumption_resolution,[],[f5078,f1268]) ).
fof(f5080,plain,
( $false
| spl67_167
| spl67_168
| ~ spl67_190 ),
inference(forward_subsumption_resolution,[],[f5079,f111]) ).
fof(f5081,plain,
( spl67_167
| spl67_168
| ~ spl67_190 ),
inference(avatar_contradiction_clause,[],[f5080]) ).
cnf(s1,plain,
( ~ spl67_1
| spl67_2
| spl67_3
| spl67_4 ),
inference(sat_conversion,[],[f200]) ).
cnf(s23,plain,
( ~ spl67_4
| ~ spl67_63
| spl67_64
| spl67_65
| spl67_66 ),
inference(sat_conversion,[],[f537]) ).
cnf(s41,plain,
spl67_63,
inference(sat_conversion,[],[f841]) ).
cnf(s44,plain,
spl67_1,
inference(sat_conversion,[],[f876]) ).
cnf(s52,plain,
( ~ spl67_3
| spl67_117 ),
inference(sat_conversion,[],[f950]) ).
cnf(s83,plain,
( spl67_166
| spl67_167
| spl67_168 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s84,plain,
~ spl67_66,
inference(sat_conversion,[],[f1278]) ).
cnf(s86,plain,
( ~ spl67_64
| ~ spl67_168 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s96,plain,
( ~ spl67_166
| spl67_168
| spl67_190
| spl67_191 ),
inference(sat_conversion,[],[f1629]) ).
cnf(s97,plain,
( ~ spl67_167
| spl67_168
| spl67_191 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s98,plain,
( ~ spl67_4
| ~ spl67_63
| spl67_64
| spl67_66
| spl67_192 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s112,plain,
( ~ spl67_2
| spl67_212
| spl67_213 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s173,plain,
( ~ spl67_1
| spl67_4
| ~ spl67_213 ),
inference(sat_conversion,[],[f2223]) ).
cnf(s205,plain,
( spl67_336
| spl67_337 ),
inference(sat_conversion,[],[f2690]) ).
cnf(s212,plain,
( ~ spl67_336
| spl67_343 ),
inference(sat_conversion,[],[f2758]) ).
cnf(s213,plain,
( ~ spl67_65
| spl67_204
| ~ spl67_337 ),
inference(sat_conversion,[],[f2763]) ).
cnf(s239,plain,
( ~ spl67_1
| spl67_2
| spl67_4
| ~ spl67_117 ),
inference(sat_conversion,[],[f3186]) ).
cnf(s330,plain,
( ~ spl67_366
| ~ spl67_367 ),
inference(sat_conversion,[],[f3621]) ).
cnf(s360,plain,
( ~ spl67_1
| spl67_4
| ~ spl67_212
| spl67_366
| spl67_466 ),
inference(sat_conversion,[],[f4135]) ).
cnf(s361,plain,
( ~ spl67_2
| spl67_213
| ~ spl67_466 ),
inference(sat_conversion,[],[f4139]) ).
cnf(s371,plain,
( spl67_337
| ~ spl67_343
| spl67_474 ),
inference(sat_conversion,[],[f4527]) ).
cnf(s372,plain,
~ spl67_474,
inference(sat_conversion,[],[f4585]) ).
cnf(s378,plain,
( ~ spl67_1
| spl67_4
| ~ spl67_212
| spl67_367
| spl67_466 ),
inference(sat_conversion,[],[f4684]) ).
cnf(s405,plain,
( ~ spl67_4
| ~ spl67_63
| spl67_64
| spl67_66
| ~ spl67_197 ),
inference(sat_conversion,[],[f4963]) ).
cnf(s406,plain,
( ~ spl67_192
| spl67_197
| ~ spl67_204 ),
inference(sat_conversion,[],[f4965]) ).
cnf(s413,plain,
~ spl67_191,
inference(sat_conversion,[],[f5073]) ).
cnf(s414,plain,
( spl67_167
| spl67_168
| ~ spl67_190 ),
inference(sat_conversion,[],[f5081]) ).
cnf(s415,plain,
( spl67_337
| ~ spl67_343 ),
inference(rat,[],[s371,s372]) ).
cnf(s431,plain,
( ~ spl67_167
| spl67_168 ),
inference(rat,[],[s97,s413]) ).
cnf(s432,plain,
( ~ spl67_166
| spl67_168
| spl67_190 ),
inference(rat,[],[s96,s413]) ).
cnf(s434,plain,
( ~ spl67_4
| spl67_64
| spl67_65 ),
inference(rat,[],[s23,s84,s41]) ).
cnf(s436,plain,
( spl67_2
| spl67_3
| spl67_4 ),
inference(rat,[],[s1,s44]) ).
cnf(s437,plain,
spl67_337,
inference(rat,[],[s212,s205,s415]) ).
cnf(s438,plain,
( spl67_64
| ~ spl67_4 ),
inference(rat,[],[s213,s406,s405,s434,s98,s84,s41,s437]) ).
cnf(s439,plain,
( spl67_167
| spl67_168 ),
inference(rat,[],[s432,s83,s414]) ).
cnf(s440,plain,
spl67_168,
inference(rat,[],[s439,s431]) ).
cnf(s442,plain,
~ spl67_64,
inference(rat,[],[s86,s440]) ).
cnf(s446,plain,
~ spl67_4,
inference(rat,[],[s438,s442]) ).
cnf(s447,plain,
~ spl67_213,
inference(rat,[],[s173,s44,s446]) ).
cnf(s448,plain,
spl67_2,
inference(rat,[],[s52,s436,s239,s446,s44]) ).
cnf(s451,plain,
~ spl67_466,
inference(rat,[],[s361,s447,s448]) ).
cnf(s453,plain,
spl67_212,
inference(rat,[],[s112,s447,s448]) ).
cnf(s456,plain,
spl67_367,
inference(rat,[],[s378,s451,s446,s44,s453]) ).
cnf(s457,plain,
spl67_366,
inference(rat,[],[s360,s451,s446,s44,s453]) ).
cnf(s462,plain,
$false,
inference(rat,[],[s330,s456,s457]) ).
fof(f5082,plain,
$false,
inference(avatar_sat_refutation,[],[s462]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL640+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n006.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 16:09:26 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.41 Running first-order theorem proving
% 0.13/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.39/1.90 % (3142979)Detected formulas, will run a generic FOF schedule.
% 7.39/1.90 % (3142990)dis-21_1_sil=8000:lcm=predicate:random_seed=2909455925: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)
% 7.39/1.90 % (3142990)Instruction limit reached!
% 7.39/1.90 % (3142990)------------------------------
% 7.39/1.90 % (3142990)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.39/1.90 % (3142990)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.90 % (3142990)CaDiCaL version: 2.1.3
% 7.39/1.90 % (3142990)Termination reason: Instruction limit
% 7.39/1.90 % (3142990)Termination phase: Saturation
% 7.39/1.90 % (3142990)Time elapsed: 0.039 s
% 7.39/1.90 % (3142990)Peak memory usage: 89 MB
% 7.39/1.90 % (3142990)Instructions burned: 132 (million)
% 7.39/1.90 % (3142989)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2697370611:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.39/1.90 % (3142988)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2261111518:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.39/1.90 % (3142986)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=3131364814:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.39/1.90 % (3142987)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=442527223:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.39/1.90 % (3142985)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=1712553497:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.39/1.90 % (3142984)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=4174993654:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.39/1.90 % (3142987)Instruction limit reached!
% 7.39/1.90 % (3142987)------------------------------
% 7.39/1.90 % (3142987)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.39/1.90 % (3142987)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.90 % (3142987)CaDiCaL version: 2.1.3
% 7.39/1.90 % (3142987)Termination reason: Instruction limit
% 7.39/1.90 % (3142987)Termination phase: Saturation
% 7.39/1.90 % (3142987)Time elapsed: 0.058 s
% 7.39/1.90 % (3142987)Peak memory usage: 90 MB
% 7.39/1.90 % (3142987)Instructions burned: 110 (million)
% 7.39/1.90 % (3142988)Instruction limit reached!
% 7.39/1.90 % (3142988)------------------------------
% 7.39/1.90 % (3142988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.39/1.90 % (3142988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.90 % (3142988)CaDiCaL version: 2.1.3
% 7.39/1.90 % (3142988)Termination reason: Instruction limit
% 7.39/1.90 % (3142988)Termination phase: Saturation
% 7.39/1.90 % (3142988)Time elapsed: 0.060 s
% 7.39/1.90 % (3142988)Peak memory usage: 88 MB
% 7.39/1.90 % (3142988)Instructions burned: 119 (million)
% 7.39/1.90 % (3142989)Instruction limit reached!
% 7.39/1.90 % (3142989)------------------------------
% 7.39/1.90 % (3142989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.39/1.90 % (3142989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.90 % (3142989)CaDiCaL version: 2.1.3
% 7.39/1.90 % (3142989)Termination reason: Instruction limit
% 7.39/1.90 % (3142989)Termination phase: Saturation
% 7.39/1.90 % (3142989)Time elapsed: 0.066 s
% 7.39/1.90 % (3142989)Peak memory usage: 89 MB
% 7.39/1.90 % (3142989)Instructions burned: 140 (million)
% 7.39/1.90 % (3142992)lrs+10_1_sil=8000:sp=occurrence:random_seed=583691228:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 7.39/1.90 % (3142992)Instruction limit reached!
% 7.39/1.90 % (3142992)------------------------------
% 7.39/1.90 % (3142992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.39/1.90 % (3142992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.39/1.90 % (3142992)CaDiCaL version: 2.1.3
% 7.39/1.90 % (3142992)Termination reason: Instruction limit
% 7.39/1.90 % (3142992)Termination phase: Saturation
% 7.39/1.90 % (3142992)Time elapsed: 0.063 s
% 7.39/1.90 % (3142992)Peak memory usage: 90 MB
% 7.39/1.90 % (3142992)Instructions burned: 286 (million)
% 10.22/2.12 % (3142999)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1166836306:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 10.22/2.12 % (3143001)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=3635761642:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 10.22/2.12 % (3143000)lrs+1011_1_sil=32000:sp=occurrence:random_seed=2010494311:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 10.22/2.12 % (3143003)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=904749802:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2997 on theBenchmark for (2997ds/294Mi)
% 10.22/2.12 % (3142999)Instruction limit reached!
% 10.22/2.12 % (3142999)------------------------------
% 10.22/2.12 % (3142999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3142999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3142999)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3142999)Termination reason: Instruction limit
% 10.22/2.12 % (3142999)Termination phase: Saturation
% 10.22/2.12 % (3142999)Time elapsed: 0.067 s
% 10.22/2.12 % (3142999)Peak memory usage: 88 MB
% 10.22/2.12 % (3142999)Instructions burned: 157 (million)
% 10.22/2.12 % (3143003)Instruction limit reached!
% 10.22/2.12 % (3143003)------------------------------
% 10.22/2.12 % (3143003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143003)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143003)Termination reason: Instruction limit
% 10.22/2.12 % (3143003)Termination phase: Saturation
% 10.22/2.12 % (3143003)Time elapsed: 0.077 s
% 10.22/2.12 % (3143003)Peak memory usage: 89 MB
% 10.22/2.12 % (3143003)Instructions burned: 295 (million)
% 10.22/2.12 % (3143001)Instruction limit reached!
% 10.22/2.12 % (3143001)------------------------------
% 10.22/2.12 % (3143001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143001)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143001)Termination reason: Instruction limit
% 10.22/2.12 % (3143001)Termination phase: Saturation
% 10.22/2.12 % (3143001)Time elapsed: 0.113 s
% 10.22/2.12 % (3143001)Peak memory usage: 89 MB
% 10.22/2.12 % (3143001)Instructions burned: 250 (million)
% 10.22/2.12 % (3143000)Instruction limit reached!
% 10.22/2.12 % (3143000)------------------------------
% 10.22/2.12 % (3143000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143000)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143000)Termination reason: Instruction limit
% 10.22/2.12 % (3143000)Termination phase: Saturation
% 10.22/2.12 % (3143000)Time elapsed: 0.137 s
% 10.22/2.12 % (3143000)Peak memory usage: 89 MB
% 10.22/2.12 % (3143000)Instructions burned: 328 (million)
% 10.22/2.12 % (3143008)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1687984490:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 10.22/2.12 % (3143009)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=939123612:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 10.22/2.12 % (3143009)Instruction limit reached!
% 10.22/2.12 % (3143009)------------------------------
% 10.22/2.12 % (3143009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143009)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143009)Termination reason: Instruction limit
% 10.22/2.12 % (3143009)Termination phase: Saturation
% 10.22/2.12 % (3143009)Time elapsed: 0.036 s
% 10.22/2.12 % (3143009)Peak memory usage: 90 MB
% 10.22/2.12 % (3143009)Instructions burned: 117 (million)
% 10.22/2.12 % (3143010)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1306874847:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 10.22/2.12 % (3143011)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1381515809:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2995 on theBenchmark for (2995ds/114Mi)
% 10.22/2.12 % (3143010)Instruction limit reached!
% 10.22/2.12 % (3143010)------------------------------
% 10.22/2.12 % (3143010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143010)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143010)Termination reason: Instruction limit
% 10.22/2.12 % (3143010)Termination phase: Saturation
% 10.22/2.12 % (3143010)Time elapsed: 0.072 s
% 10.22/2.12 % (3143010)Peak memory usage: 89 MB
% 10.22/2.12 % (3143010)Instructions burned: 128 (million)
% 10.22/2.12 % (3143015)lrs+10_1_sil=8000:sp=occurrence:random_seed=1926860597:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 10.22/2.12 % (3143011)Instruction limit reached!
% 10.22/2.12 % (3143011)------------------------------
% 10.22/2.12 % (3143011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143011)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143011)Termination reason: Instruction limit
% 10.22/2.12 % (3143011)Termination phase: Saturation
% 10.22/2.12 % (3143011)Time elapsed: 0.059 s
% 10.22/2.12 % (3143011)Peak memory usage: 89 MB
% 10.22/2.12 % (3143011)Instructions burned: 114 (million)
% 10.22/2.12 % (3143017)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3789422685:i=437:sd=1:aac=none:ss=included_2993 on theBenchmark for (2993ds/437Mi)
% 10.22/2.12 % (3143019)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2814176296:i=5202:ss=axioms:sgt=16_2993 on theBenchmark for (2993ds/5202Mi)
% 10.22/2.12 % (3143015)Instruction limit reached!
% 10.22/2.12 % (3143015)------------------------------
% 10.22/2.12 % (3143015)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143015)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143015)Termination reason: Instruction limit
% 10.22/2.12 % (3143015)Termination phase: Saturation
% 10.22/2.12 % (3143015)Time elapsed: 0.194 s
% 10.22/2.12 % (3143015)Peak memory usage: 92 MB
% 10.22/2.12 % (3143015)Instructions burned: 908 (million)
% 10.22/2.12 % (3143022)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3732788848:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 10.22/2.12 % (3143022)Instruction limit reached!
% 10.22/2.12 % (3143022)------------------------------
% 10.22/2.12 % (3143022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143022)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143022)Termination reason: Instruction limit
% 10.22/2.12 % (3143022)Termination phase: Saturation
% 10.22/2.12 % (3143022)Time elapsed: 0.035 s
% 10.22/2.12 % (3143022)Peak memory usage: 89 MB
% 10.22/2.12 % (3143022)Instructions burned: 136 (million)
% 10.22/2.12 % (3143017)Instruction limit reached!
% 10.22/2.12 % (3143017)------------------------------
% 10.22/2.12 % (3143017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143017)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143017)Termination reason: Instruction limit
% 10.22/2.12 % (3143017)Termination phase: Saturation
% 10.22/2.12 % (3143017)Time elapsed: 0.194 s
% 10.22/2.12 % (3143017)Peak memory usage: 89 MB
% 10.22/2.12 % (3143017)Instructions burned: 439 (million)
% 10.22/2.12 % (3143024)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=151191067:st=8:i=592:sd=3:ep=RST:ss=axioms_2990 on theBenchmark for (2990ds/592Mi)
% 10.22/2.12 % (3143025)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=646254439:st=3:i=13193:sd=3:ss=axioms_2990 on theBenchmark for (2990ds/13193Mi)
% 10.22/2.12 % (3143024)Instruction limit reached!
% 10.22/2.12 % (3143024)------------------------------
% 10.22/2.12 % (3143024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143024)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143024)Termination reason: Instruction limit
% 10.22/2.12 % (3143024)Termination phase: Saturation
% 10.22/2.12 % (3143024)Time elapsed: 0.146 s
% 10.22/2.12 % (3143024)Peak memory usage: 91 MB
% 10.22/2.12 % (3143024)Instructions burned: 594 (million)
% 10.22/2.12 % (3142984)First to succeed.
% 10.22/2.12 % (3142984)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3142979"
% 10.22/2.12 % (3143028)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=387881517:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/125Mi)
% 10.22/2.12 % (3143028)Instruction limit reached!
% 10.22/2.12 % (3143028)------------------------------
% 10.22/2.12 % (3143028)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143028)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143028)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143028)Termination reason: Instruction limit
% 10.22/2.12 % (3143028)Termination phase: Saturation
% 10.22/2.12 % (3143028)Time elapsed: 0.039 s
% 10.22/2.12 % (3143028)Peak memory usage: 92 MB
% 10.22/2.12 % (3143028)Instructions burned: 128 (million)
% 10.22/2.12 % (3143030)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=390297159:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi)
% 10.22/2.12 % (3143030)Instruction limit reached!
% 10.22/2.12 % (3143030)------------------------------
% 10.22/2.12 % (3143030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.22/2.12 % (3143030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.22/2.12 % (3143030)CaDiCaL version: 2.1.3
% 10.22/2.12 % (3143030)Termination reason: Instruction limit
% 10.22/2.12 % (3143030)Termination phase: Saturation
% 10.22/2.12 % (3143030)Time elapsed: 0.031 s
% 10.22/2.12 % (3143030)Peak memory usage: 89 MB
% 10.22/2.12 % (3143030)Instructions burned: 137 (million)
% 10.22/2.12 % (3142984)Refutation found. Thanks to Tanya!
% 10.22/2.12 % SZS status Theorem for theBenchmark
% 10.22/2.12 % SZS output start Proof for theBenchmark
% See solution above
% 11.10/2.32 % (3142984)------------------------------
% 11.10/2.32 % (3142984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.10/2.32 % (3142984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.10/2.32 % (3142984)CaDiCaL version: 2.1.3
% 11.10/2.32 % (3142984)Termination reason: Refutation
% 11.10/2.32 % (3142984)Time elapsed: 1.110 s
% 11.10/2.32 % (3142984)Peak memory usage: 135 MB
% 11.10/2.32 % (3142984)Instructions burned: 1676 (million)
% 11.10/2.32 % (3142984)------------------------------
% 11.10/2.32 % (3142984)------------------------------
% 11.10/2.32 % (3142979)Success in time 1.513 s
% 11.10/2.32 % Vampire exiting
%------------------------------------------------------------------------------