%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL680+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:55:49 AM UTC 2026
% Result : Theorem 74.88s 11.46s
% Output : Refutation 75.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 127
% Syntax : Number of formulae : 265 ( 9 unt; 125 def)
% Number of atoms : 3151 ( 0 equ)
% Maximal formula atoms : 344 ( 11 avg)
% Number of connectives : 6197 (3311 ~;2167 |; 713 &)
% ( 6 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 114 ( 9 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 129 ( 128 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 1646 (1526 !; 120 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity) ).
fof(f3,conjecture,
~ ? [X0] :
~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p2(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p2(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p2(X1) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f4,negated_conjecture,
~ ~ ? [X0] :
~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p2(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p2(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p2(X1) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p2(X1) ) ) ) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
~ ~ ? [X0] :
~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ~ ( p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( p2(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ~ ! [X9] :
( ~ r1(X8,X9)
| p2(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ( p2(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ ( p2(X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ ( p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ~ ( p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ~ ( p2(X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ ( p2(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X21] :
( ~ r1(X0,X21)
| ~ ( p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ~ ( p2(X22)
| ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ~ ( p2(X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ ( p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28)
| ~ ! [X29] :
( ~ r1(X28,X29)
| ~ ( p2(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( p2(X30)
| ~ ! [X31] :
( ~ r1(X30,X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| p2(X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ ( p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ~ ( p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ ( ~ ! [X36] :
( ~ r1(X35,X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| p2(X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ~ ( p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ~ ( p2(X39)
| ~ ! [X40] :
( ~ r1(X39,X40)
| ~ ( p2(X40)
| ~ ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) ) ) ) ) ) ) )
& ~ p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X42] :
( ~ r1(X0,X42)
| ~ ( p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ~ ( p2(X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ~ ( p2(X46)
| ~ ! [X47] :
( ~ r1(X46,X47)
| ~ ( p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X48,X49)
| p2(X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ~ ( p2(X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ ( p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ ( p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ~ ( p2(X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ( ~ ! [X57] :
( ~ r1(X56,X57)
| ~ ! [X58] :
( ~ r1(X57,X58)
| p2(X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| ~ ( p2(X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ~ ( p2(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ~ ( p2(X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) ) ) ) )
& ~ p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X63] :
( ~ r1(X0,X63)
| ~ ( p2(X63)
| ~ ! [X64] :
( ~ r1(X63,X64)
| ~ ( p2(X64)
| ~ ! [X65] :
( ~ r1(X64,X65)
| ~ ! [X66] :
( ~ r1(X65,X66)
| p2(X66)
| ~ ! [X67] :
( ~ r1(X66,X67)
| ~ ( p2(X67)
| ~ ! [X68] :
( ~ r1(X67,X68)
| ~ ( p2(X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| ~ ! [X70] :
( ~ r1(X69,X70)
| p2(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ~ ( p2(X71)
| ~ ! [X72] :
( ~ r1(X71,X72)
| ~ ( p2(X72)
| ~ ! [X73] :
( ~ r1(X72,X73)
| ~ ! [X74] :
( ~ r1(X73,X74)
| p2(X74)
| ~ ! [X75] :
( ~ r1(X74,X75)
| ~ ( p2(X75)
| ~ ! [X76] :
( ~ r1(X75,X76)
| ~ ( p2(X76)
| ~ ! [X77] :
( ~ r1(X76,X77)
| ~ ( ~ ! [X78] :
( ~ r1(X77,X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| p2(X79)
| ~ ! [X80] :
( ~ r1(X79,X80)
| ~ ( p2(X80)
| ~ ! [X81] :
( ~ r1(X80,X81)
| ~ ( p2(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ~ ( p2(X82)
| ~ ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) ) ) ) ) ) ) )
& ~ p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X84] :
( ~ r1(X0,X84)
| ~ ( p2(X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| ~ ! [X86] :
( ~ r1(X85,X86)
| p2(X86)
| ~ ! [X87] :
( ~ r1(X86,X87)
| ~ ( p2(X87)
| ~ ! [X88] :
( ~ r1(X87,X88)
| ~ ( p2(X88)
| ~ ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p2(X90)
| ~ ! [X91] :
( ~ r1(X90,X91)
| ~ ( p2(X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| ~ ( p2(X92)
| ~ ! [X93] :
( ~ r1(X92,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| ~ ! [X96] :
( ~ r1(X95,X96)
| ~ ( p2(X96)
| ~ ! [X97] :
( ~ r1(X96,X97)
| ~ ( p2(X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| ~ ( p2(X98)
| ~ ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) ) ) ) )
& ~ p2(X93) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X100] :
( ~ r1(X0,X100)
| ~ ( p2(X100)
| ~ ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p2(X102)
| ~ ! [X103] :
( ~ r1(X102,X103)
| ~ ( p2(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ~ ( p2(X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| ~ ! [X106] :
( ~ r1(X105,X106)
| p2(X106)
| ~ ! [X107] :
( ~ r1(X106,X107)
| ~ ( p2(X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ( p2(X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| ~ ( ~ ! [X110] :
( ~ r1(X109,X110)
| ~ ! [X111] :
( ~ r1(X110,X111)
| p2(X111)
| ~ ! [X112] :
( ~ r1(X111,X112)
| ~ ( p2(X112)
| ~ ! [X113] :
( ~ r1(X112,X113)
| ~ ( p2(X113)
| ~ ! [X114] :
( ~ r1(X113,X114)
| ~ ( p2(X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) ) ) ) )
& ~ p1(X109) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X116] :
( ~ r1(X0,X116)
| ~ ( p2(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ~ ! [X118] :
( ~ r1(X117,X118)
| p2(X118)
| ~ ! [X119] :
( ~ r1(X118,X119)
| ~ ( p2(X119)
| ~ ! [X120] :
( ~ r1(X119,X120)
| ~ ( p2(X120)
| ~ ! [X121] :
( ~ r1(X120,X121)
| ~ ! [X122] :
( ~ r1(X121,X122)
| p2(X122)
| ~ ! [X123] :
( ~ r1(X122,X123)
| ~ ( p2(X123)
| ~ ! [X124] :
( ~ r1(X123,X124)
| ~ ( p2(X124)
| ~ ! [X125] :
( ~ r1(X124,X125)
| ~ ( ~ ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p2(X127)
| ~ ! [X128] :
( ~ r1(X127,X128)
| ~ ( p2(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ~ ( p2(X129)
| ~ ! [X130] :
( ~ r1(X129,X130)
| ~ ( p2(X130)
| ~ ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) ) ) ) )
& ~ p1(X125) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X132] :
( ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X132,X133)
| p2(X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ~ ( p2(X134)
| ~ ! [X135] :
( ~ r1(X134,X135)
| ~ ( p2(X135)
| ~ ! [X136] :
( ~ r1(X135,X136)
| ~ ( ~ ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| ~ ! [X139] :
( ~ r1(X138,X139)
| ~ ( p2(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ~ ( p2(X140)
| ~ ! [X141] :
( ~ r1(X140,X141)
| ~ ( p2(X141)
| ~ ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) ) ) ) ) ) ) )
& ~ p2(X136) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X143] :
( ~ r1(X0,X143)
| ~ ! [X144] :
( ~ r1(X143,X144)
| p2(X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ~ ( p2(X145)
| ~ ! [X146] :
( ~ r1(X145,X146)
| ~ ( p2(X146)
| ~ ! [X147] :
( ~ r1(X146,X147)
| ~ ( ~ ! [X148] :
( ~ r1(X147,X148)
| ~ ! [X149] :
( ~ r1(X148,X149)
| p2(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ~ ( p2(X150)
| ~ ! [X151] :
( ~ r1(X150,X151)
| ~ ( p2(X151)
| ~ ! [X152] :
( ~ r1(X151,X152)
| ~ ( p2(X152)
| ~ ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) ) ) ) ) ) ) )
& ~ p1(X147) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X154] :
( ~ r1(X0,X154)
| ~ ! [X155] :
( ~ r1(X154,X155)
| p2(X155)
| ~ ! [X156] :
( ~ r1(X155,X156)
| ~ ( p2(X156)
| ~ ! [X157] :
( ~ r1(X156,X157)
| ~ ( p2(X157)
| ~ ! [X158] :
( ~ r1(X157,X158)
| ~ ( ~ ! [X159] :
( ~ r1(X158,X159)
| ~ ! [X160] :
( ~ r1(X159,X160)
| p2(X160)
| ~ ! [X161] :
( ~ r1(X160,X161)
| ~ ( p2(X161)
| ~ ! [X162] :
( ~ r1(X161,X162)
| ~ ( p2(X162)
| ~ ! [X163] :
( ~ r1(X162,X163)
| ~ ( p2(X163)
| ~ ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) ) ) ) )
& ~ p1(X158) ) ) ) ) ) ) ) )
| ( ~ ! [X165] :
( ~ r1(X0,X165)
| ~ ! [X166] :
( ~ r1(X165,X166)
| p2(X166)
| ~ ! [X167] :
( ~ r1(X166,X167)
| ~ ( p2(X167)
| ~ ! [X168] :
( ~ r1(X167,X168)
| ~ ( p2(X168)
| ~ ! [X169] :
( ~ r1(X168,X169)
| ~ ( p2(X169)
| ~ ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X171] :
( ~ r1(X0,X171)
| ~ ! [X172] :
( ~ r1(X171,X172)
| p2(X172)
| ~ ! [X173] :
( ~ r1(X172,X173)
| ~ ( p2(X173)
| ~ ! [X174] :
( ~ r1(X173,X174)
| ~ ( p2(X174)
| ~ ! [X175] :
( ~ r1(X174,X175)
| ~ ( p2(X175)
| ~ ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X177] :
( ~ r1(X0,X177)
| ~ ! [X178] :
( ~ r1(X177,X178)
| p2(X178)
| ~ ! [X179] :
( ~ r1(X178,X179)
| ~ ( p2(X179)
| ~ ! [X180] :
( ~ r1(X179,X180)
| ~ ( p2(X180)
| ~ ! [X181] :
( ~ r1(X180,X181)
| ~ ( p2(X181)
| ~ ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
inference(rectify,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ( p2(X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( p2(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ ( p2(X3)
| ~ ! [X4] :
( ~ r1(X3,X4)
| ~ ! [X5] :
( ~ r1(X4,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ~ ( p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ~ ( p2(X7)
| ~ ! [X8] :
( ~ r1(X7,X8)
| ~ ! [X9] :
( ~ r1(X8,X9)
| p2(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ~ ( p2(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ~ ( p2(X11)
| ~ ! [X12] :
( ~ r1(X11,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| p2(X13)
| ~ ! [X14] :
( ~ r1(X13,X14)
| ~ ( p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ~ ( p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ~ ! [X17] :
( ~ r1(X16,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ~ ( p2(X18)
| ~ ! [X19] :
( ~ r1(X18,X19)
| ~ ( p2(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X21] :
( ~ r1(X0,X21)
| ~ ( p2(X21)
| ~ ! [X22] :
( ~ r1(X21,X22)
| ~ ( p2(X22)
| ~ ! [X23] :
( ~ r1(X22,X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ~ ( p2(X25)
| ~ ! [X26] :
( ~ r1(X25,X26)
| ~ ( p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p2(X28)
| ~ ! [X29] :
( ~ r1(X28,X29)
| ~ ( p2(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ~ ( p2(X30)
| ~ ! [X31] :
( ~ r1(X30,X31)
| ~ ! [X32] :
( ~ r1(X31,X32)
| p2(X32)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ~ ( p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ~ ( p2(X34)
| ~ ! [X35] :
( ~ r1(X34,X35)
| ~ ( ~ ! [X36] :
( ~ r1(X35,X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| p2(X37)
| ~ ! [X38] :
( ~ r1(X37,X38)
| ~ ( p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ~ ( p2(X39)
| ~ ! [X40] :
( ~ r1(X39,X40)
| ~ ( p2(X40)
| ~ ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) ) ) ) ) ) ) )
& ~ p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X42] :
( ~ r1(X0,X42)
| ~ ( p2(X42)
| ~ ! [X43] :
( ~ r1(X42,X43)
| ~ ( p2(X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| p2(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ~ ( p2(X46)
| ~ ! [X47] :
( ~ r1(X46,X47)
| ~ ( p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X48,X49)
| p2(X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ~ ( p2(X50)
| ~ ! [X51] :
( ~ r1(X50,X51)
| ~ ( p2(X51)
| ~ ! [X52] :
( ~ r1(X51,X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ~ ( p2(X54)
| ~ ! [X55] :
( ~ r1(X54,X55)
| ~ ( p2(X55)
| ~ ! [X56] :
( ~ r1(X55,X56)
| ~ ( ~ ! [X57] :
( ~ r1(X56,X57)
| ~ ! [X58] :
( ~ r1(X57,X58)
| p2(X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| ~ ( p2(X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ~ ( p2(X60)
| ~ ! [X61] :
( ~ r1(X60,X61)
| ~ ( p2(X61)
| ~ ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) ) ) ) )
& ~ p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X63] :
( ~ r1(X0,X63)
| ~ ( p2(X63)
| ~ ! [X64] :
( ~ r1(X63,X64)
| ~ ( p2(X64)
| ~ ! [X65] :
( ~ r1(X64,X65)
| ~ ! [X66] :
( ~ r1(X65,X66)
| p2(X66)
| ~ ! [X67] :
( ~ r1(X66,X67)
| ~ ( p2(X67)
| ~ ! [X68] :
( ~ r1(X67,X68)
| ~ ( p2(X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| ~ ! [X70] :
( ~ r1(X69,X70)
| p2(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ~ ( p2(X71)
| ~ ! [X72] :
( ~ r1(X71,X72)
| ~ ( p2(X72)
| ~ ! [X73] :
( ~ r1(X72,X73)
| ~ ! [X74] :
( ~ r1(X73,X74)
| p2(X74)
| ~ ! [X75] :
( ~ r1(X74,X75)
| ~ ( p2(X75)
| ~ ! [X76] :
( ~ r1(X75,X76)
| ~ ( p2(X76)
| ~ ! [X77] :
( ~ r1(X76,X77)
| ~ ( ~ ! [X78] :
( ~ r1(X77,X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| p2(X79)
| ~ ! [X80] :
( ~ r1(X79,X80)
| ~ ( p2(X80)
| ~ ! [X81] :
( ~ r1(X80,X81)
| ~ ( p2(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ~ ( p2(X82)
| ~ ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) ) ) ) ) ) ) )
& ~ p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X84] :
( ~ r1(X0,X84)
| ~ ( p2(X84)
| ~ ! [X85] :
( ~ r1(X84,X85)
| ~ ! [X86] :
( ~ r1(X85,X86)
| p2(X86)
| ~ ! [X87] :
( ~ r1(X86,X87)
| ~ ( p2(X87)
| ~ ! [X88] :
( ~ r1(X87,X88)
| ~ ( p2(X88)
| ~ ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| p2(X90)
| ~ ! [X91] :
( ~ r1(X90,X91)
| ~ ( p2(X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| ~ ( p2(X92)
| ~ ! [X93] :
( ~ r1(X92,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| ~ ! [X96] :
( ~ r1(X95,X96)
| ~ ( p2(X96)
| ~ ! [X97] :
( ~ r1(X96,X97)
| ~ ( p2(X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| ~ ( p2(X98)
| ~ ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) ) ) ) )
& ~ p2(X93) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X100] :
( ~ r1(X0,X100)
| ~ ( p2(X100)
| ~ ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p2(X102)
| ~ ! [X103] :
( ~ r1(X102,X103)
| ~ ( p2(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ~ ( p2(X104)
| ~ ! [X105] :
( ~ r1(X104,X105)
| ~ ! [X106] :
( ~ r1(X105,X106)
| p2(X106)
| ~ ! [X107] :
( ~ r1(X106,X107)
| ~ ( p2(X107)
| ~ ! [X108] :
( ~ r1(X107,X108)
| ~ ( p2(X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| ~ ( ~ ! [X110] :
( ~ r1(X109,X110)
| ~ ! [X111] :
( ~ r1(X110,X111)
| p2(X111)
| ~ ! [X112] :
( ~ r1(X111,X112)
| ~ ( p2(X112)
| ~ ! [X113] :
( ~ r1(X112,X113)
| ~ ( p2(X113)
| ~ ! [X114] :
( ~ r1(X113,X114)
| ~ ( p2(X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) ) ) ) )
& ~ p1(X109) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X116] :
( ~ r1(X0,X116)
| ~ ( p2(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ~ ! [X118] :
( ~ r1(X117,X118)
| p2(X118)
| ~ ! [X119] :
( ~ r1(X118,X119)
| ~ ( p2(X119)
| ~ ! [X120] :
( ~ r1(X119,X120)
| ~ ( p2(X120)
| ~ ! [X121] :
( ~ r1(X120,X121)
| ~ ! [X122] :
( ~ r1(X121,X122)
| p2(X122)
| ~ ! [X123] :
( ~ r1(X122,X123)
| ~ ( p2(X123)
| ~ ! [X124] :
( ~ r1(X123,X124)
| ~ ( p2(X124)
| ~ ! [X125] :
( ~ r1(X124,X125)
| ~ ( ~ ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p2(X127)
| ~ ! [X128] :
( ~ r1(X127,X128)
| ~ ( p2(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ~ ( p2(X129)
| ~ ! [X130] :
( ~ r1(X129,X130)
| ~ ( p2(X130)
| ~ ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) ) ) ) )
& ~ p1(X125) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X132] :
( ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X132,X133)
| p2(X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ~ ( p2(X134)
| ~ ! [X135] :
( ~ r1(X134,X135)
| ~ ( p2(X135)
| ~ ! [X136] :
( ~ r1(X135,X136)
| ~ ( ~ ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| ~ ! [X139] :
( ~ r1(X138,X139)
| ~ ( p2(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ~ ( p2(X140)
| ~ ! [X141] :
( ~ r1(X140,X141)
| ~ ( p2(X141)
| ~ ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) ) ) ) ) ) ) )
& ~ p2(X136) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X143] :
( ~ r1(X0,X143)
| ~ ! [X144] :
( ~ r1(X143,X144)
| p2(X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ~ ( p2(X145)
| ~ ! [X146] :
( ~ r1(X145,X146)
| ~ ( p2(X146)
| ~ ! [X147] :
( ~ r1(X146,X147)
| ~ ( ~ ! [X148] :
( ~ r1(X147,X148)
| ~ ! [X149] :
( ~ r1(X148,X149)
| p2(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ~ ( p2(X150)
| ~ ! [X151] :
( ~ r1(X150,X151)
| ~ ( p2(X151)
| ~ ! [X152] :
( ~ r1(X151,X152)
| ~ ( p2(X152)
| ~ ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) ) ) ) ) ) ) )
& ~ p1(X147) ) ) ) ) ) ) ) )
| p2(X0)
| ~ ! [X154] :
( ~ r1(X0,X154)
| ~ ! [X155] :
( ~ r1(X154,X155)
| p2(X155)
| ~ ! [X156] :
( ~ r1(X155,X156)
| ~ ( p2(X156)
| ~ ! [X157] :
( ~ r1(X156,X157)
| ~ ( p2(X157)
| ~ ! [X158] :
( ~ r1(X157,X158)
| ~ ( ~ ! [X159] :
( ~ r1(X158,X159)
| ~ ! [X160] :
( ~ r1(X159,X160)
| p2(X160)
| ~ ! [X161] :
( ~ r1(X160,X161)
| ~ ( p2(X161)
| ~ ! [X162] :
( ~ r1(X161,X162)
| ~ ( p2(X162)
| ~ ! [X163] :
( ~ r1(X162,X163)
| ~ ( p2(X163)
| ~ ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) ) ) ) )
& ~ p1(X158) ) ) ) ) ) ) ) )
| ( ~ ! [X165] :
( ~ r1(X0,X165)
| ~ ! [X166] :
( ~ r1(X165,X166)
| p2(X166)
| ~ ! [X167] :
( ~ r1(X166,X167)
| ~ ( p2(X167)
| ~ ! [X168] :
( ~ r1(X167,X168)
| ~ ( p2(X168)
| ~ ! [X169] :
( ~ r1(X168,X169)
| ~ ( p2(X169)
| ~ ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X171] :
( ~ r1(X0,X171)
| ~ ! [X172] :
( ~ r1(X171,X172)
| p2(X172)
| ~ ! [X173] :
( ~ r1(X172,X173)
| ~ ( p2(X173)
| ~ ! [X174] :
( ~ r1(X173,X174)
| ~ ( p2(X174)
| ~ ! [X175] :
( ~ r1(X174,X175)
| ~ ( p2(X175)
| ~ ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X177] :
( ~ r1(X0,X177)
| ~ ! [X178] :
( ~ r1(X177,X178)
| p2(X178)
| ~ ! [X179] :
( ~ r1(X178,X179)
| ~ ( p2(X179)
| ~ ! [X180] :
( ~ r1(X179,X180)
| ~ ( p2(X180)
| ~ ! [X181] :
( ~ r1(X180,X181)
| ~ ( p2(X181)
| ~ ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
inference(flattening,[],[f5]) ).
fof(f9,plain,
? [X0] :
( ~ p2(X0)
& ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ( ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ( ~ p2(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ? [X5] :
( r1(X4,X5)
& ~ p2(X5)
& ! [X6] :
( ~ r1(X5,X6)
| ( ~ p2(X6)
& ! [X7] :
( ~ r1(X6,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ? [X9] :
( r1(X8,X9)
& ~ p2(X9)
& ! [X10] :
( ~ r1(X9,X10)
| ( ~ p2(X10)
& ! [X11] :
( ~ r1(X10,X11)
| ( ~ p2(X11)
& ! [X12] :
( ~ r1(X11,X12)
| ? [X13] :
( r1(X12,X13)
& ~ p2(X13)
& ! [X14] :
( ~ r1(X13,X14)
| ( ~ p2(X14)
& ! [X15] :
( ~ r1(X14,X15)
| ( ~ p2(X15)
& ! [X16] :
( ~ r1(X15,X16)
| ? [X17] :
( r1(X16,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ( ~ p2(X18)
& ! [X19] :
( ~ r1(X18,X19)
| ( ~ p2(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X21] :
( ~ r1(X0,X21)
| ( ~ p2(X21)
& ! [X22] :
( ~ r1(X21,X22)
| ( ~ p2(X22)
& ! [X23] :
( ~ r1(X22,X23)
| ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ( ~ p2(X25)
& ! [X26] :
( ~ r1(X25,X26)
| ( ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p2(X28)
& ! [X29] :
( ~ r1(X28,X29)
| ( ~ p2(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ( ~ p2(X30)
& ! [X31] :
( ~ r1(X30,X31)
| ? [X32] :
( r1(X31,X32)
& ~ p2(X32)
& ! [X33] :
( ~ r1(X32,X33)
| ( ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ( ~ p2(X34)
& ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ? [X37] :
( r1(X36,X37)
& ~ p2(X37)
& ! [X38] :
( ~ r1(X37,X38)
| ( ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ( ~ p2(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ( ~ p2(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) ) ) ) ) ) ) )
| p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X42] :
( ~ r1(X0,X42)
| ( ~ p2(X42)
& ! [X43] :
( ~ r1(X42,X43)
| ( ~ p2(X43)
& ! [X44] :
( ~ r1(X43,X44)
| ? [X45] :
( r1(X44,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ( ~ p2(X46)
& ! [X47] :
( ~ r1(X46,X47)
| ( ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ? [X49] :
( r1(X48,X49)
& ~ p2(X49)
& ! [X50] :
( ~ r1(X49,X50)
| ( ~ p2(X50)
& ! [X51] :
( ~ r1(X50,X51)
| ( ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ( ~ p2(X54)
& ! [X55] :
( ~ r1(X54,X55)
| ( ~ p2(X55)
& ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ? [X58] :
( r1(X57,X58)
& ~ p2(X58)
& ! [X59] :
( ~ r1(X58,X59)
| ( ~ p2(X59)
& ! [X60] :
( ~ r1(X59,X60)
| ( ~ p2(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ( ~ p2(X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) ) ) ) )
| p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X63] :
( ~ r1(X0,X63)
| ( ~ p2(X63)
& ! [X64] :
( ~ r1(X63,X64)
| ( ~ p2(X64)
& ! [X65] :
( ~ r1(X64,X65)
| ? [X66] :
( r1(X65,X66)
& ~ p2(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ( ~ p2(X67)
& ! [X68] :
( ~ r1(X67,X68)
| ( ~ p2(X68)
& ! [X69] :
( ~ r1(X68,X69)
| ? [X70] :
( r1(X69,X70)
& ~ p2(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ( ~ p2(X71)
& ! [X72] :
( ~ r1(X71,X72)
| ( ~ p2(X72)
& ! [X73] :
( ~ r1(X72,X73)
| ? [X74] :
( r1(X73,X74)
& ~ p2(X74)
& ! [X75] :
( ~ r1(X74,X75)
| ( ~ p2(X75)
& ! [X76] :
( ~ r1(X75,X76)
| ( ~ p2(X76)
& ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p2(X79)
& ! [X80] :
( ~ r1(X79,X80)
| ( ~ p2(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ( ~ p2(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ( ~ p2(X82)
& ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) ) ) ) ) ) ) )
| p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X84] :
( ~ r1(X0,X84)
| ( ~ p2(X84)
& ! [X85] :
( ~ r1(X84,X85)
| ? [X86] :
( r1(X85,X86)
& ~ p2(X86)
& ! [X87] :
( ~ r1(X86,X87)
| ( ~ p2(X87)
& ! [X88] :
( ~ r1(X87,X88)
| ( ~ p2(X88)
& ! [X89] :
( ~ r1(X88,X89)
| ? [X90] :
( r1(X89,X90)
& ~ p2(X90)
& ! [X91] :
( ~ r1(X90,X91)
| ( ~ p2(X91)
& ! [X92] :
( ~ r1(X91,X92)
| ( ~ p2(X92)
& ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ? [X95] :
( r1(X94,X95)
& ~ p2(X95)
& ! [X96] :
( ~ r1(X95,X96)
| ( ~ p2(X96)
& ! [X97] :
( ~ r1(X96,X97)
| ( ~ p2(X97)
& ! [X98] :
( ~ r1(X97,X98)
| ( ~ p2(X98)
& ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) ) ) ) )
| p2(X93) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X100] :
( ~ r1(X0,X100)
| ( ~ p2(X100)
& ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p2(X102)
& ! [X103] :
( ~ r1(X102,X103)
| ( ~ p2(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ( ~ p2(X104)
& ! [X105] :
( ~ r1(X104,X105)
| ? [X106] :
( r1(X105,X106)
& ~ p2(X106)
& ! [X107] :
( ~ r1(X106,X107)
| ( ~ p2(X107)
& ! [X108] :
( ~ r1(X107,X108)
| ( ~ p2(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ? [X111] :
( r1(X110,X111)
& ~ p2(X111)
& ! [X112] :
( ~ r1(X111,X112)
| ( ~ p2(X112)
& ! [X113] :
( ~ r1(X112,X113)
| ( ~ p2(X113)
& ! [X114] :
( ~ r1(X113,X114)
| ( ~ p2(X114)
& ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) ) ) ) )
| p1(X109) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X116] :
( ~ r1(X0,X116)
| ( ~ p2(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ? [X118] :
( r1(X117,X118)
& ~ p2(X118)
& ! [X119] :
( ~ r1(X118,X119)
| ( ~ p2(X119)
& ! [X120] :
( ~ r1(X119,X120)
| ( ~ p2(X120)
& ! [X121] :
( ~ r1(X120,X121)
| ? [X122] :
( r1(X121,X122)
& ~ p2(X122)
& ! [X123] :
( ~ r1(X122,X123)
| ( ~ p2(X123)
& ! [X124] :
( ~ r1(X123,X124)
| ( ~ p2(X124)
& ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p2(X127)
& ! [X128] :
( ~ r1(X127,X128)
| ( ~ p2(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ( ~ p2(X129)
& ! [X130] :
( ~ r1(X129,X130)
| ( ~ p2(X130)
& ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) ) ) ) )
| p1(X125) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X132] :
( ~ r1(X0,X132)
| ? [X133] :
( r1(X132,X133)
& ~ p2(X133)
& ! [X134] :
( ~ r1(X133,X134)
| ( ~ p2(X134)
& ! [X135] :
( ~ r1(X134,X135)
| ( ~ p2(X135)
& ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p2(X138)
& ! [X139] :
( ~ r1(X138,X139)
| ( ~ p2(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ( ~ p2(X140)
& ! [X141] :
( ~ r1(X140,X141)
| ( ~ p2(X141)
& ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) ) ) ) ) ) ) )
| p2(X136) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X143] :
( ~ r1(X0,X143)
| ? [X144] :
( r1(X143,X144)
& ~ p2(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ( ~ p2(X145)
& ! [X146] :
( ~ r1(X145,X146)
| ( ~ p2(X146)
& ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ? [X149] :
( r1(X148,X149)
& ~ p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ( ~ p2(X150)
& ! [X151] :
( ~ r1(X150,X151)
| ( ~ p2(X151)
& ! [X152] :
( ~ r1(X151,X152)
| ( ~ p2(X152)
& ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) ) ) ) ) ) ) )
| p1(X147) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X154] :
( ~ r1(X0,X154)
| ? [X155] :
( r1(X154,X155)
& ~ p2(X155)
& ! [X156] :
( ~ r1(X155,X156)
| ( ~ p2(X156)
& ! [X157] :
( ~ r1(X156,X157)
| ( ~ p2(X157)
& ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ? [X160] :
( r1(X159,X160)
& ~ p2(X160)
& ! [X161] :
( ~ r1(X160,X161)
| ( ~ p2(X161)
& ! [X162] :
( ~ r1(X161,X162)
| ( ~ p2(X162)
& ! [X163] :
( ~ r1(X162,X163)
| ( ~ p2(X163)
& ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) ) ) ) )
| p1(X158) ) ) ) ) ) ) )
& ( ! [X165] :
( ~ r1(X0,X165)
| ? [X166] :
( r1(X165,X166)
& ~ p2(X166)
& ! [X167] :
( ~ r1(X166,X167)
| ( ~ p2(X167)
& ! [X168] :
( ~ r1(X167,X168)
| ( ~ p2(X168)
& ! [X169] :
( ~ r1(X168,X169)
| ( ~ p2(X169)
& ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) ) ) ) )
| p2(X0) )
& ( ! [X171] :
( ~ r1(X0,X171)
| ? [X172] :
( r1(X171,X172)
& ~ p2(X172)
& ! [X173] :
( ~ r1(X172,X173)
| ( ~ p2(X173)
& ! [X174] :
( ~ r1(X173,X174)
| ( ~ p2(X174)
& ! [X175] :
( ~ r1(X174,X175)
| ( ~ p2(X175)
& ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) ) ) ) )
| p1(X0) )
& ( ! [X177] :
( ~ r1(X0,X177)
| ? [X178] :
( r1(X177,X178)
& ~ p2(X178)
& ! [X179] :
( ~ r1(X178,X179)
| ( ~ p2(X179)
& ! [X180] :
( ~ r1(X179,X180)
| ( ~ p2(X180)
& ! [X181] :
( ~ r1(X180,X181)
| ( ~ p2(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) ) ) ) )
| p1(X0) )
& ~ p1(X0) ),
inference(ennf_transformation,[],[f6]) ).
fof(f10,plain,
? [X0] :
( ~ p2(X0)
& ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ( ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ( ~ p2(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ? [X5] :
( r1(X4,X5)
& ~ p2(X5)
& ! [X6] :
( ~ r1(X5,X6)
| ( ~ p2(X6)
& ! [X7] :
( ~ r1(X6,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| ? [X9] :
( r1(X8,X9)
& ~ p2(X9)
& ! [X10] :
( ~ r1(X9,X10)
| ( ~ p2(X10)
& ! [X11] :
( ~ r1(X10,X11)
| ( ~ p2(X11)
& ! [X12] :
( ~ r1(X11,X12)
| ? [X13] :
( r1(X12,X13)
& ~ p2(X13)
& ! [X14] :
( ~ r1(X13,X14)
| ( ~ p2(X14)
& ! [X15] :
( ~ r1(X14,X15)
| ( ~ p2(X15)
& ! [X16] :
( ~ r1(X15,X16)
| ? [X17] :
( r1(X16,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ( ~ p2(X18)
& ! [X19] :
( ~ r1(X18,X19)
| ( ~ p2(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X21] :
( ~ r1(X0,X21)
| ( ~ p2(X21)
& ! [X22] :
( ~ r1(X21,X22)
| ( ~ p2(X22)
& ! [X23] :
( ~ r1(X22,X23)
| ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ( ~ p2(X25)
& ! [X26] :
( ~ r1(X25,X26)
| ( ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p2(X28)
& ! [X29] :
( ~ r1(X28,X29)
| ( ~ p2(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ( ~ p2(X30)
& ! [X31] :
( ~ r1(X30,X31)
| ? [X32] :
( r1(X31,X32)
& ~ p2(X32)
& ! [X33] :
( ~ r1(X32,X33)
| ( ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ( ~ p2(X34)
& ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ? [X37] :
( r1(X36,X37)
& ~ p2(X37)
& ! [X38] :
( ~ r1(X37,X38)
| ( ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ( ~ p2(X39)
& ! [X40] :
( ~ r1(X39,X40)
| ( ~ p2(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) ) ) ) ) ) ) )
| p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X42] :
( ~ r1(X0,X42)
| ( ~ p2(X42)
& ! [X43] :
( ~ r1(X42,X43)
| ( ~ p2(X43)
& ! [X44] :
( ~ r1(X43,X44)
| ? [X45] :
( r1(X44,X45)
& ~ p2(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ( ~ p2(X46)
& ! [X47] :
( ~ r1(X46,X47)
| ( ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ? [X49] :
( r1(X48,X49)
& ~ p2(X49)
& ! [X50] :
( ~ r1(X49,X50)
| ( ~ p2(X50)
& ! [X51] :
( ~ r1(X50,X51)
| ( ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ( ~ p2(X54)
& ! [X55] :
( ~ r1(X54,X55)
| ( ~ p2(X55)
& ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ? [X58] :
( r1(X57,X58)
& ~ p2(X58)
& ! [X59] :
( ~ r1(X58,X59)
| ( ~ p2(X59)
& ! [X60] :
( ~ r1(X59,X60)
| ( ~ p2(X60)
& ! [X61] :
( ~ r1(X60,X61)
| ( ~ p2(X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) ) ) ) )
| p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X63] :
( ~ r1(X0,X63)
| ( ~ p2(X63)
& ! [X64] :
( ~ r1(X63,X64)
| ( ~ p2(X64)
& ! [X65] :
( ~ r1(X64,X65)
| ? [X66] :
( r1(X65,X66)
& ~ p2(X66)
& ! [X67] :
( ~ r1(X66,X67)
| ( ~ p2(X67)
& ! [X68] :
( ~ r1(X67,X68)
| ( ~ p2(X68)
& ! [X69] :
( ~ r1(X68,X69)
| ? [X70] :
( r1(X69,X70)
& ~ p2(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ( ~ p2(X71)
& ! [X72] :
( ~ r1(X71,X72)
| ( ~ p2(X72)
& ! [X73] :
( ~ r1(X72,X73)
| ? [X74] :
( r1(X73,X74)
& ~ p2(X74)
& ! [X75] :
( ~ r1(X74,X75)
| ( ~ p2(X75)
& ! [X76] :
( ~ r1(X75,X76)
| ( ~ p2(X76)
& ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ? [X79] :
( r1(X78,X79)
& ~ p2(X79)
& ! [X80] :
( ~ r1(X79,X80)
| ( ~ p2(X80)
& ! [X81] :
( ~ r1(X80,X81)
| ( ~ p2(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ( ~ p2(X82)
& ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) ) ) ) ) ) ) )
| p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X84] :
( ~ r1(X0,X84)
| ( ~ p2(X84)
& ! [X85] :
( ~ r1(X84,X85)
| ? [X86] :
( r1(X85,X86)
& ~ p2(X86)
& ! [X87] :
( ~ r1(X86,X87)
| ( ~ p2(X87)
& ! [X88] :
( ~ r1(X87,X88)
| ( ~ p2(X88)
& ! [X89] :
( ~ r1(X88,X89)
| ? [X90] :
( r1(X89,X90)
& ~ p2(X90)
& ! [X91] :
( ~ r1(X90,X91)
| ( ~ p2(X91)
& ! [X92] :
( ~ r1(X91,X92)
| ( ~ p2(X92)
& ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ? [X95] :
( r1(X94,X95)
& ~ p2(X95)
& ! [X96] :
( ~ r1(X95,X96)
| ( ~ p2(X96)
& ! [X97] :
( ~ r1(X96,X97)
| ( ~ p2(X97)
& ! [X98] :
( ~ r1(X97,X98)
| ( ~ p2(X98)
& ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) ) ) ) )
| p2(X93) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X100] :
( ~ r1(X0,X100)
| ( ~ p2(X100)
& ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p2(X102)
& ! [X103] :
( ~ r1(X102,X103)
| ( ~ p2(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ( ~ p2(X104)
& ! [X105] :
( ~ r1(X104,X105)
| ? [X106] :
( r1(X105,X106)
& ~ p2(X106)
& ! [X107] :
( ~ r1(X106,X107)
| ( ~ p2(X107)
& ! [X108] :
( ~ r1(X107,X108)
| ( ~ p2(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ? [X111] :
( r1(X110,X111)
& ~ p2(X111)
& ! [X112] :
( ~ r1(X111,X112)
| ( ~ p2(X112)
& ! [X113] :
( ~ r1(X112,X113)
| ( ~ p2(X113)
& ! [X114] :
( ~ r1(X113,X114)
| ( ~ p2(X114)
& ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) ) ) ) )
| p1(X109) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X116] :
( ~ r1(X0,X116)
| ( ~ p2(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ? [X118] :
( r1(X117,X118)
& ~ p2(X118)
& ! [X119] :
( ~ r1(X118,X119)
| ( ~ p2(X119)
& ! [X120] :
( ~ r1(X119,X120)
| ( ~ p2(X120)
& ! [X121] :
( ~ r1(X120,X121)
| ? [X122] :
( r1(X121,X122)
& ~ p2(X122)
& ! [X123] :
( ~ r1(X122,X123)
| ( ~ p2(X123)
& ! [X124] :
( ~ r1(X123,X124)
| ( ~ p2(X124)
& ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p2(X127)
& ! [X128] :
( ~ r1(X127,X128)
| ( ~ p2(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ( ~ p2(X129)
& ! [X130] :
( ~ r1(X129,X130)
| ( ~ p2(X130)
& ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) ) ) ) )
| p1(X125) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X132] :
( ~ r1(X0,X132)
| ? [X133] :
( r1(X132,X133)
& ~ p2(X133)
& ! [X134] :
( ~ r1(X133,X134)
| ( ~ p2(X134)
& ! [X135] :
( ~ r1(X134,X135)
| ( ~ p2(X135)
& ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p2(X138)
& ! [X139] :
( ~ r1(X138,X139)
| ( ~ p2(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ( ~ p2(X140)
& ! [X141] :
( ~ r1(X140,X141)
| ( ~ p2(X141)
& ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) ) ) ) ) ) ) )
| p2(X136) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X143] :
( ~ r1(X0,X143)
| ? [X144] :
( r1(X143,X144)
& ~ p2(X144)
& ! [X145] :
( ~ r1(X144,X145)
| ( ~ p2(X145)
& ! [X146] :
( ~ r1(X145,X146)
| ( ~ p2(X146)
& ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ? [X149] :
( r1(X148,X149)
& ~ p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ( ~ p2(X150)
& ! [X151] :
( ~ r1(X150,X151)
| ( ~ p2(X151)
& ! [X152] :
( ~ r1(X151,X152)
| ( ~ p2(X152)
& ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) ) ) ) ) ) ) )
| p1(X147) ) ) ) ) ) ) )
& ~ p2(X0)
& ! [X154] :
( ~ r1(X0,X154)
| ? [X155] :
( r1(X154,X155)
& ~ p2(X155)
& ! [X156] :
( ~ r1(X155,X156)
| ( ~ p2(X156)
& ! [X157] :
( ~ r1(X156,X157)
| ( ~ p2(X157)
& ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ? [X160] :
( r1(X159,X160)
& ~ p2(X160)
& ! [X161] :
( ~ r1(X160,X161)
| ( ~ p2(X161)
& ! [X162] :
( ~ r1(X161,X162)
| ( ~ p2(X162)
& ! [X163] :
( ~ r1(X162,X163)
| ( ~ p2(X163)
& ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) ) ) ) )
| p1(X158) ) ) ) ) ) ) )
& ( ! [X165] :
( ~ r1(X0,X165)
| ? [X166] :
( r1(X165,X166)
& ~ p2(X166)
& ! [X167] :
( ~ r1(X166,X167)
| ( ~ p2(X167)
& ! [X168] :
( ~ r1(X167,X168)
| ( ~ p2(X168)
& ! [X169] :
( ~ r1(X168,X169)
| ( ~ p2(X169)
& ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) ) ) ) )
| p2(X0) )
& ( ! [X171] :
( ~ r1(X0,X171)
| ? [X172] :
( r1(X171,X172)
& ~ p2(X172)
& ! [X173] :
( ~ r1(X172,X173)
| ( ~ p2(X173)
& ! [X174] :
( ~ r1(X173,X174)
| ( ~ p2(X174)
& ! [X175] :
( ~ r1(X174,X175)
| ( ~ p2(X175)
& ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) ) ) ) )
| p1(X0) )
& ( ! [X177] :
( ~ r1(X0,X177)
| ? [X178] :
( r1(X177,X178)
& ~ p2(X178)
& ! [X179] :
( ~ r1(X178,X179)
| ( ~ p2(X179)
& ! [X180] :
( ~ r1(X179,X180)
| ( ~ p2(X180)
& ! [X181] :
( ~ r1(X180,X181)
| ( ~ p2(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) ) ) ) )
| p1(X0) )
& ~ p1(X0) ),
inference(flattening,[],[f9]) ).
fof(f11,definition,
! [X180] :
( ! [X181] :
( ~ r1(X180,X181)
| ( ~ p2(X181)
& ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) )
| ~ sP0(X180) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X179] :
( ! [X180] :
( ~ r1(X179,X180)
| ( ~ p2(X180)
& sP0(X180) ) )
| ~ sP1(X179) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X178] :
( ! [X179] :
( ~ r1(X178,X179)
| ( ~ p2(X179)
& sP1(X179) ) )
| ~ sP2(X178) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X177] :
( ? [X178] :
( r1(X177,X178)
& ~ p2(X178)
& sP2(X178) )
| ~ sP3(X177) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X174] :
( ! [X175] :
( ~ r1(X174,X175)
| ( ~ p2(X175)
& ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) )
| ~ sP4(X174) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X173] :
( ! [X174] :
( ~ r1(X173,X174)
| ( ~ p2(X174)
& sP4(X174) ) )
| ~ sP5(X173) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X172] :
( ! [X173] :
( ~ r1(X172,X173)
| ( ~ p2(X173)
& sP5(X173) ) )
| ~ sP6(X172) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X171] :
( ? [X172] :
( r1(X171,X172)
& ~ p2(X172)
& sP6(X172) )
| ~ sP7(X171) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X168] :
( ! [X169] :
( ~ r1(X168,X169)
| ( ~ p2(X169)
& ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) )
| ~ sP8(X168) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X167] :
( ! [X168] :
( ~ r1(X167,X168)
| ( ~ p2(X168)
& sP8(X168) ) )
| ~ sP9(X167) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X166] :
( ! [X167] :
( ~ r1(X166,X167)
| ( ~ p2(X167)
& sP9(X167) ) )
| ~ sP10(X166) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X165] :
( ? [X166] :
( r1(X165,X166)
& ~ p2(X166)
& sP10(X166) )
| ~ sP11(X165) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X162] :
( ! [X163] :
( ~ r1(X162,X163)
| ( ~ p2(X163)
& ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) )
| ~ sP12(X162) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X161] :
( ! [X162] :
( ~ r1(X161,X162)
| ( ~ p2(X162)
& sP12(X162) ) )
| ~ sP13(X161) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X160] :
( ! [X161] :
( ~ r1(X160,X161)
| ( ~ p2(X161)
& sP13(X161) ) )
| ~ sP14(X160) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X159] :
( ? [X160] :
( r1(X159,X160)
& ~ p2(X160)
& sP14(X160) )
| ~ sP15(X159) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X156] :
( ! [X157] :
( ~ r1(X156,X157)
| ( ~ p2(X157)
& ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| sP15(X159) )
| p1(X158) ) ) )
| ~ sP16(X156) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X155] :
( ! [X156] :
( ~ r1(X155,X156)
| ( ~ p2(X156)
& sP16(X156) ) )
| ~ sP17(X155) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X154] :
( ? [X155] :
( r1(X154,X155)
& ~ p2(X155)
& sP17(X155) )
| ~ sP18(X154) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f30,definition,
! [X151] :
( ! [X152] :
( ~ r1(X151,X152)
| ( ~ p2(X152)
& ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) )
| ~ sP19(X151) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f31,definition,
! [X150] :
( ! [X151] :
( ~ r1(X150,X151)
| ( ~ p2(X151)
& sP19(X151) ) )
| ~ sP20(X150) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f32,definition,
! [X149] :
( ! [X150] :
( ~ r1(X149,X150)
| ( ~ p2(X150)
& sP20(X150) ) )
| ~ sP21(X149) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f33,definition,
! [X148] :
( ? [X149] :
( r1(X148,X149)
& ~ p2(X149)
& sP21(X149) )
| ~ sP22(X148) ),
introduced(definition,[new_symbols(definition,[sP22])],[predicate_definition_introduction]) ).
fof(f34,definition,
! [X145] :
( ! [X146] :
( ~ r1(X145,X146)
| ( ~ p2(X146)
& ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| sP22(X148) )
| p1(X147) ) ) )
| ~ sP23(X145) ),
introduced(definition,[new_symbols(definition,[sP23])],[predicate_definition_introduction]) ).
fof(f35,definition,
! [X144] :
( ! [X145] :
( ~ r1(X144,X145)
| ( ~ p2(X145)
& sP23(X145) ) )
| ~ sP24(X144) ),
introduced(definition,[new_symbols(definition,[sP24])],[predicate_definition_introduction]) ).
fof(f36,definition,
! [X143] :
( ? [X144] :
( r1(X143,X144)
& ~ p2(X144)
& sP24(X144) )
| ~ sP25(X143) ),
introduced(definition,[new_symbols(definition,[sP25])],[predicate_definition_introduction]) ).
fof(f37,definition,
! [X140] :
( ! [X141] :
( ~ r1(X140,X141)
| ( ~ p2(X141)
& ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) )
| ~ sP26(X140) ),
introduced(definition,[new_symbols(definition,[sP26])],[predicate_definition_introduction]) ).
fof(f38,definition,
! [X139] :
( ! [X140] :
( ~ r1(X139,X140)
| ( ~ p2(X140)
& sP26(X140) ) )
| ~ sP27(X139) ),
introduced(definition,[new_symbols(definition,[sP27])],[predicate_definition_introduction]) ).
fof(f39,definition,
! [X138] :
( ! [X139] :
( ~ r1(X138,X139)
| ( ~ p2(X139)
& sP27(X139) ) )
| ~ sP28(X138) ),
introduced(definition,[new_symbols(definition,[sP28])],[predicate_definition_introduction]) ).
fof(f40,definition,
! [X137] :
( ? [X138] :
( r1(X137,X138)
& ~ p2(X138)
& sP28(X138) )
| ~ sP29(X137) ),
introduced(definition,[new_symbols(definition,[sP29])],[predicate_definition_introduction]) ).
fof(f41,definition,
! [X134] :
( ! [X135] :
( ~ r1(X134,X135)
| ( ~ p2(X135)
& ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| sP29(X137) )
| p2(X136) ) ) )
| ~ sP30(X134) ),
introduced(definition,[new_symbols(definition,[sP30])],[predicate_definition_introduction]) ).
fof(f42,definition,
! [X133] :
( ! [X134] :
( ~ r1(X133,X134)
| ( ~ p2(X134)
& sP30(X134) ) )
| ~ sP31(X133) ),
introduced(definition,[new_symbols(definition,[sP31])],[predicate_definition_introduction]) ).
fof(f43,definition,
! [X132] :
( ? [X133] :
( r1(X132,X133)
& ~ p2(X133)
& sP31(X133) )
| ~ sP32(X132) ),
introduced(definition,[new_symbols(definition,[sP32])],[predicate_definition_introduction]) ).
fof(f44,definition,
! [X129] :
( ! [X130] :
( ~ r1(X129,X130)
| ( ~ p2(X130)
& ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) )
| ~ sP33(X129) ),
introduced(definition,[new_symbols(definition,[sP33])],[predicate_definition_introduction]) ).
fof(f45,definition,
! [X128] :
( ! [X129] :
( ~ r1(X128,X129)
| ( ~ p2(X129)
& sP33(X129) ) )
| ~ sP34(X128) ),
introduced(definition,[new_symbols(definition,[sP34])],[predicate_definition_introduction]) ).
fof(f46,definition,
! [X127] :
( ! [X128] :
( ~ r1(X127,X128)
| ( ~ p2(X128)
& sP34(X128) ) )
| ~ sP35(X127) ),
introduced(definition,[new_symbols(definition,[sP35])],[predicate_definition_introduction]) ).
fof(f47,definition,
! [X126] :
( ? [X127] :
( r1(X126,X127)
& ~ p2(X127)
& sP35(X127) )
| ~ sP36(X126) ),
introduced(definition,[new_symbols(definition,[sP36])],[predicate_definition_introduction]) ).
fof(f48,definition,
! [X123] :
( ! [X124] :
( ~ r1(X123,X124)
| ( ~ p2(X124)
& ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| sP36(X126) )
| p1(X125) ) ) )
| ~ sP37(X123) ),
introduced(definition,[new_symbols(definition,[sP37])],[predicate_definition_introduction]) ).
fof(f49,definition,
! [X122] :
( ! [X123] :
( ~ r1(X122,X123)
| ( ~ p2(X123)
& sP37(X123) ) )
| ~ sP38(X122) ),
introduced(definition,[new_symbols(definition,[sP38])],[predicate_definition_introduction]) ).
fof(f50,definition,
! [X121] :
( ? [X122] :
( r1(X121,X122)
& ~ p2(X122)
& sP38(X122) )
| ~ sP39(X121) ),
introduced(definition,[new_symbols(definition,[sP39])],[predicate_definition_introduction]) ).
fof(f51,definition,
! [X119] :
( ! [X120] :
( ~ r1(X119,X120)
| ( ~ p2(X120)
& ! [X121] :
( ~ r1(X120,X121)
| sP39(X121) ) ) )
| ~ sP40(X119) ),
introduced(definition,[new_symbols(definition,[sP40])],[predicate_definition_introduction]) ).
fof(f52,definition,
! [X118] :
( ! [X119] :
( ~ r1(X118,X119)
| ( ~ p2(X119)
& sP40(X119) ) )
| ~ sP41(X118) ),
introduced(definition,[new_symbols(definition,[sP41])],[predicate_definition_introduction]) ).
fof(f53,definition,
! [X117] :
( ? [X118] :
( r1(X117,X118)
& ~ p2(X118)
& sP41(X118) )
| ~ sP42(X117) ),
introduced(definition,[new_symbols(definition,[sP42])],[predicate_definition_introduction]) ).
fof(f54,definition,
! [X113] :
( ! [X114] :
( ~ r1(X113,X114)
| ( ~ p2(X114)
& ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) )
| ~ sP43(X113) ),
introduced(definition,[new_symbols(definition,[sP43])],[predicate_definition_introduction]) ).
fof(f55,definition,
! [X112] :
( ! [X113] :
( ~ r1(X112,X113)
| ( ~ p2(X113)
& sP43(X113) ) )
| ~ sP44(X112) ),
introduced(definition,[new_symbols(definition,[sP44])],[predicate_definition_introduction]) ).
fof(f56,definition,
! [X111] :
( ! [X112] :
( ~ r1(X111,X112)
| ( ~ p2(X112)
& sP44(X112) ) )
| ~ sP45(X111) ),
introduced(definition,[new_symbols(definition,[sP45])],[predicate_definition_introduction]) ).
fof(f57,definition,
! [X110] :
( ? [X111] :
( r1(X110,X111)
& ~ p2(X111)
& sP45(X111) )
| ~ sP46(X110) ),
introduced(definition,[new_symbols(definition,[sP46])],[predicate_definition_introduction]) ).
fof(f58,definition,
! [X107] :
( ! [X108] :
( ~ r1(X107,X108)
| ( ~ p2(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| sP46(X110) )
| p1(X109) ) ) )
| ~ sP47(X107) ),
introduced(definition,[new_symbols(definition,[sP47])],[predicate_definition_introduction]) ).
fof(f59,definition,
! [X106] :
( ! [X107] :
( ~ r1(X106,X107)
| ( ~ p2(X107)
& sP47(X107) ) )
| ~ sP48(X106) ),
introduced(definition,[new_symbols(definition,[sP48])],[predicate_definition_introduction]) ).
fof(f60,definition,
! [X105] :
( ? [X106] :
( r1(X105,X106)
& ~ p2(X106)
& sP48(X106) )
| ~ sP49(X105) ),
introduced(definition,[new_symbols(definition,[sP49])],[predicate_definition_introduction]) ).
fof(f61,definition,
! [X103] :
( ! [X104] :
( ~ r1(X103,X104)
| ( ~ p2(X104)
& ! [X105] :
( ~ r1(X104,X105)
| sP49(X105) ) ) )
| ~ sP50(X103) ),
introduced(definition,[new_symbols(definition,[sP50])],[predicate_definition_introduction]) ).
fof(f62,definition,
! [X102] :
( ! [X103] :
( ~ r1(X102,X103)
| ( ~ p2(X103)
& sP50(X103) ) )
| ~ sP51(X102) ),
introduced(definition,[new_symbols(definition,[sP51])],[predicate_definition_introduction]) ).
fof(f63,definition,
! [X101] :
( ? [X102] :
( r1(X101,X102)
& ~ p2(X102)
& sP51(X102) )
| ~ sP52(X101) ),
introduced(definition,[new_symbols(definition,[sP52])],[predicate_definition_introduction]) ).
fof(f64,definition,
! [X97] :
( ! [X98] :
( ~ r1(X97,X98)
| ( ~ p2(X98)
& ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) )
| ~ sP53(X97) ),
introduced(definition,[new_symbols(definition,[sP53])],[predicate_definition_introduction]) ).
fof(f65,definition,
! [X96] :
( ! [X97] :
( ~ r1(X96,X97)
| ( ~ p2(X97)
& sP53(X97) ) )
| ~ sP54(X96) ),
introduced(definition,[new_symbols(definition,[sP54])],[predicate_definition_introduction]) ).
fof(f66,definition,
! [X95] :
( ! [X96] :
( ~ r1(X95,X96)
| ( ~ p2(X96)
& sP54(X96) ) )
| ~ sP55(X95) ),
introduced(definition,[new_symbols(definition,[sP55])],[predicate_definition_introduction]) ).
fof(f67,definition,
! [X94] :
( ? [X95] :
( r1(X94,X95)
& ~ p2(X95)
& sP55(X95) )
| ~ sP56(X94) ),
introduced(definition,[new_symbols(definition,[sP56])],[predicate_definition_introduction]) ).
fof(f68,definition,
! [X91] :
( ! [X92] :
( ~ r1(X91,X92)
| ( ~ p2(X92)
& ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| sP56(X94) )
| p2(X93) ) ) )
| ~ sP57(X91) ),
introduced(definition,[new_symbols(definition,[sP57])],[predicate_definition_introduction]) ).
fof(f69,definition,
! [X90] :
( ! [X91] :
( ~ r1(X90,X91)
| ( ~ p2(X91)
& sP57(X91) ) )
| ~ sP58(X90) ),
introduced(definition,[new_symbols(definition,[sP58])],[predicate_definition_introduction]) ).
fof(f70,definition,
! [X89] :
( ? [X90] :
( r1(X89,X90)
& ~ p2(X90)
& sP58(X90) )
| ~ sP59(X89) ),
introduced(definition,[new_symbols(definition,[sP59])],[predicate_definition_introduction]) ).
fof(f71,definition,
! [X87] :
( ! [X88] :
( ~ r1(X87,X88)
| ( ~ p2(X88)
& ! [X89] :
( ~ r1(X88,X89)
| sP59(X89) ) ) )
| ~ sP60(X87) ),
introduced(definition,[new_symbols(definition,[sP60])],[predicate_definition_introduction]) ).
fof(f72,definition,
! [X86] :
( ! [X87] :
( ~ r1(X86,X87)
| ( ~ p2(X87)
& sP60(X87) ) )
| ~ sP61(X86) ),
introduced(definition,[new_symbols(definition,[sP61])],[predicate_definition_introduction]) ).
fof(f73,definition,
! [X85] :
( ? [X86] :
( r1(X85,X86)
& ~ p2(X86)
& sP61(X86) )
| ~ sP62(X85) ),
introduced(definition,[new_symbols(definition,[sP62])],[predicate_definition_introduction]) ).
fof(f74,definition,
! [X81] :
( ! [X82] :
( ~ r1(X81,X82)
| ( ~ p2(X82)
& ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) )
| ~ sP63(X81) ),
introduced(definition,[new_symbols(definition,[sP63])],[predicate_definition_introduction]) ).
fof(f75,definition,
! [X80] :
( ! [X81] :
( ~ r1(X80,X81)
| ( ~ p2(X81)
& sP63(X81) ) )
| ~ sP64(X80) ),
introduced(definition,[new_symbols(definition,[sP64])],[predicate_definition_introduction]) ).
fof(f76,definition,
! [X79] :
( ! [X80] :
( ~ r1(X79,X80)
| ( ~ p2(X80)
& sP64(X80) ) )
| ~ sP65(X79) ),
introduced(definition,[new_symbols(definition,[sP65])],[predicate_definition_introduction]) ).
fof(f77,definition,
! [X78] :
( ? [X79] :
( r1(X78,X79)
& ~ p2(X79)
& sP65(X79) )
| ~ sP66(X78) ),
introduced(definition,[new_symbols(definition,[sP66])],[predicate_definition_introduction]) ).
fof(f78,definition,
! [X75] :
( ! [X76] :
( ~ r1(X75,X76)
| ( ~ p2(X76)
& ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| sP66(X78) )
| p1(X77) ) ) )
| ~ sP67(X75) ),
introduced(definition,[new_symbols(definition,[sP67])],[predicate_definition_introduction]) ).
fof(f79,definition,
! [X74] :
( ! [X75] :
( ~ r1(X74,X75)
| ( ~ p2(X75)
& sP67(X75) ) )
| ~ sP68(X74) ),
introduced(definition,[new_symbols(definition,[sP68])],[predicate_definition_introduction]) ).
fof(f80,definition,
! [X73] :
( ? [X74] :
( r1(X73,X74)
& ~ p2(X74)
& sP68(X74) )
| ~ sP69(X73) ),
introduced(definition,[new_symbols(definition,[sP69])],[predicate_definition_introduction]) ).
fof(f81,definition,
! [X71] :
( ! [X72] :
( ~ r1(X71,X72)
| ( ~ p2(X72)
& ! [X73] :
( ~ r1(X72,X73)
| sP69(X73) ) ) )
| ~ sP70(X71) ),
introduced(definition,[new_symbols(definition,[sP70])],[predicate_definition_introduction]) ).
fof(f82,definition,
! [X70] :
( ! [X71] :
( ~ r1(X70,X71)
| ( ~ p2(X71)
& sP70(X71) ) )
| ~ sP71(X70) ),
introduced(definition,[new_symbols(definition,[sP71])],[predicate_definition_introduction]) ).
fof(f83,definition,
! [X69] :
( ? [X70] :
( r1(X69,X70)
& ~ p2(X70)
& sP71(X70) )
| ~ sP72(X69) ),
introduced(definition,[new_symbols(definition,[sP72])],[predicate_definition_introduction]) ).
fof(f84,definition,
! [X67] :
( ! [X68] :
( ~ r1(X67,X68)
| ( ~ p2(X68)
& ! [X69] :
( ~ r1(X68,X69)
| sP72(X69) ) ) )
| ~ sP73(X67) ),
introduced(definition,[new_symbols(definition,[sP73])],[predicate_definition_introduction]) ).
fof(f85,definition,
! [X66] :
( ! [X67] :
( ~ r1(X66,X67)
| ( ~ p2(X67)
& sP73(X67) ) )
| ~ sP74(X66) ),
introduced(definition,[new_symbols(definition,[sP74])],[predicate_definition_introduction]) ).
fof(f86,definition,
! [X65] :
( ? [X66] :
( r1(X65,X66)
& ~ p2(X66)
& sP74(X66) )
| ~ sP75(X65) ),
introduced(definition,[new_symbols(definition,[sP75])],[predicate_definition_introduction]) ).
fof(f87,definition,
! [X63] :
( ! [X64] :
( ~ r1(X63,X64)
| ( ~ p2(X64)
& ! [X65] :
( ~ r1(X64,X65)
| sP75(X65) ) ) )
| ~ sP76(X63) ),
introduced(definition,[new_symbols(definition,[sP76])],[predicate_definition_introduction]) ).
fof(f88,definition,
! [X60] :
( ! [X61] :
( ~ r1(X60,X61)
| ( ~ p2(X61)
& ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) )
| ~ sP77(X60) ),
introduced(definition,[new_symbols(definition,[sP77])],[predicate_definition_introduction]) ).
fof(f89,definition,
! [X59] :
( ! [X60] :
( ~ r1(X59,X60)
| ( ~ p2(X60)
& sP77(X60) ) )
| ~ sP78(X59) ),
introduced(definition,[new_symbols(definition,[sP78])],[predicate_definition_introduction]) ).
fof(f90,definition,
! [X58] :
( ! [X59] :
( ~ r1(X58,X59)
| ( ~ p2(X59)
& sP78(X59) ) )
| ~ sP79(X58) ),
introduced(definition,[new_symbols(definition,[sP79])],[predicate_definition_introduction]) ).
fof(f91,definition,
! [X57] :
( ? [X58] :
( r1(X57,X58)
& ~ p2(X58)
& sP79(X58) )
| ~ sP80(X57) ),
introduced(definition,[new_symbols(definition,[sP80])],[predicate_definition_introduction]) ).
fof(f92,definition,
! [X54] :
( ! [X55] :
( ~ r1(X54,X55)
| ( ~ p2(X55)
& ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| sP80(X57) )
| p1(X56) ) ) )
| ~ sP81(X54) ),
introduced(definition,[new_symbols(definition,[sP81])],[predicate_definition_introduction]) ).
fof(f93,definition,
! [X53] :
( ! [X54] :
( ~ r1(X53,X54)
| ( ~ p2(X54)
& sP81(X54) ) )
| ~ sP82(X53) ),
introduced(definition,[new_symbols(definition,[sP82])],[predicate_definition_introduction]) ).
fof(f94,definition,
! [X52] :
( ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& sP82(X53) )
| ~ sP83(X52) ),
introduced(definition,[new_symbols(definition,[sP83])],[predicate_definition_introduction]) ).
fof(f95,definition,
! [X50] :
( ! [X51] :
( ~ r1(X50,X51)
| ( ~ p2(X51)
& ! [X52] :
( ~ r1(X51,X52)
| sP83(X52) ) ) )
| ~ sP84(X50) ),
introduced(definition,[new_symbols(definition,[sP84])],[predicate_definition_introduction]) ).
fof(f96,definition,
! [X49] :
( ! [X50] :
( ~ r1(X49,X50)
| ( ~ p2(X50)
& sP84(X50) ) )
| ~ sP85(X49) ),
introduced(definition,[new_symbols(definition,[sP85])],[predicate_definition_introduction]) ).
fof(f97,definition,
! [X48] :
( ? [X49] :
( r1(X48,X49)
& ~ p2(X49)
& sP85(X49) )
| ~ sP86(X48) ),
introduced(definition,[new_symbols(definition,[sP86])],[predicate_definition_introduction]) ).
fof(f98,definition,
! [X46] :
( ! [X47] :
( ~ r1(X46,X47)
| ( ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| sP86(X48) ) ) )
| ~ sP87(X46) ),
introduced(definition,[new_symbols(definition,[sP87])],[predicate_definition_introduction]) ).
fof(f99,definition,
! [X45] :
( ! [X46] :
( ~ r1(X45,X46)
| ( ~ p2(X46)
& sP87(X46) ) )
| ~ sP88(X45) ),
introduced(definition,[new_symbols(definition,[sP88])],[predicate_definition_introduction]) ).
fof(f100,definition,
! [X44] :
( ? [X45] :
( r1(X44,X45)
& ~ p2(X45)
& sP88(X45) )
| ~ sP89(X44) ),
introduced(definition,[new_symbols(definition,[sP89])],[predicate_definition_introduction]) ).
fof(f101,definition,
! [X42] :
( ! [X43] :
( ~ r1(X42,X43)
| ( ~ p2(X43)
& ! [X44] :
( ~ r1(X43,X44)
| sP89(X44) ) ) )
| ~ sP90(X42) ),
introduced(definition,[new_symbols(definition,[sP90])],[predicate_definition_introduction]) ).
fof(f102,definition,
! [X39] :
( ! [X40] :
( ~ r1(X39,X40)
| ( ~ p2(X40)
& ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) )
| ~ sP91(X39) ),
introduced(definition,[new_symbols(definition,[sP91])],[predicate_definition_introduction]) ).
fof(f103,definition,
! [X38] :
( ! [X39] :
( ~ r1(X38,X39)
| ( ~ p2(X39)
& sP91(X39) ) )
| ~ sP92(X38) ),
introduced(definition,[new_symbols(definition,[sP92])],[predicate_definition_introduction]) ).
fof(f104,definition,
! [X37] :
( ! [X38] :
( ~ r1(X37,X38)
| ( ~ p2(X38)
& sP92(X38) ) )
| ~ sP93(X37) ),
introduced(definition,[new_symbols(definition,[sP93])],[predicate_definition_introduction]) ).
fof(f105,definition,
! [X36] :
( ? [X37] :
( r1(X36,X37)
& ~ p2(X37)
& sP93(X37) )
| ~ sP94(X36) ),
introduced(definition,[new_symbols(definition,[sP94])],[predicate_definition_introduction]) ).
fof(f106,definition,
! [X33] :
( ! [X34] :
( ~ r1(X33,X34)
| ( ~ p2(X34)
& ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| sP94(X36) )
| p2(X35) ) ) )
| ~ sP95(X33) ),
introduced(definition,[new_symbols(definition,[sP95])],[predicate_definition_introduction]) ).
fof(f107,definition,
! [X32] :
( ! [X33] :
( ~ r1(X32,X33)
| ( ~ p2(X33)
& sP95(X33) ) )
| ~ sP96(X32) ),
introduced(definition,[new_symbols(definition,[sP96])],[predicate_definition_introduction]) ).
fof(f108,definition,
! [X31] :
( ? [X32] :
( r1(X31,X32)
& ~ p2(X32)
& sP96(X32) )
| ~ sP97(X31) ),
introduced(definition,[new_symbols(definition,[sP97])],[predicate_definition_introduction]) ).
fof(f109,definition,
! [X29] :
( ! [X30] :
( ~ r1(X29,X30)
| ( ~ p2(X30)
& ! [X31] :
( ~ r1(X30,X31)
| sP97(X31) ) ) )
| ~ sP98(X29) ),
introduced(definition,[new_symbols(definition,[sP98])],[predicate_definition_introduction]) ).
fof(f110,definition,
! [X28] :
( ! [X29] :
( ~ r1(X28,X29)
| ( ~ p2(X29)
& sP98(X29) ) )
| ~ sP99(X28) ),
introduced(definition,[new_symbols(definition,[sP99])],[predicate_definition_introduction]) ).
fof(f111,definition,
! [X27] :
( ? [X28] :
( r1(X27,X28)
& ~ p2(X28)
& sP99(X28) )
| ~ sP100(X27) ),
introduced(definition,[new_symbols(definition,[sP100])],[predicate_definition_introduction]) ).
fof(f112,definition,
! [X25] :
( ! [X26] :
( ~ r1(X25,X26)
| ( ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| sP100(X27) ) ) )
| ~ sP101(X25) ),
introduced(definition,[new_symbols(definition,[sP101])],[predicate_definition_introduction]) ).
fof(f113,definition,
! [X24] :
( ! [X25] :
( ~ r1(X24,X25)
| ( ~ p2(X25)
& sP101(X25) ) )
| ~ sP102(X24) ),
introduced(definition,[new_symbols(definition,[sP102])],[predicate_definition_introduction]) ).
fof(f114,definition,
! [X23] :
( ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& sP102(X24) )
| ~ sP103(X23) ),
introduced(definition,[new_symbols(definition,[sP103])],[predicate_definition_introduction]) ).
fof(f115,definition,
! [X21] :
( ! [X22] :
( ~ r1(X21,X22)
| ( ~ p2(X22)
& ! [X23] :
( ~ r1(X22,X23)
| sP103(X23) ) ) )
| ~ sP104(X21) ),
introduced(definition,[new_symbols(definition,[sP104])],[predicate_definition_introduction]) ).
fof(f116,definition,
! [X18] :
( ! [X19] :
( ~ r1(X18,X19)
| ( ~ p2(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) )
| ~ sP105(X18) ),
introduced(definition,[new_symbols(definition,[sP105])],[predicate_definition_introduction]) ).
fof(f117,definition,
! [X17] :
( ! [X18] :
( ~ r1(X17,X18)
| ( ~ p2(X18)
& sP105(X18) ) )
| ~ sP106(X17) ),
introduced(definition,[new_symbols(definition,[sP106])],[predicate_definition_introduction]) ).
fof(f118,definition,
! [X16] :
( ? [X17] :
( r1(X16,X17)
& ~ p2(X17)
& sP106(X17) )
| ~ sP107(X16) ),
introduced(definition,[new_symbols(definition,[sP107])],[predicate_definition_introduction]) ).
fof(f119,definition,
! [X14] :
( ! [X15] :
( ~ r1(X14,X15)
| ( ~ p2(X15)
& ! [X16] :
( ~ r1(X15,X16)
| sP107(X16) ) ) )
| ~ sP108(X14) ),
introduced(definition,[new_symbols(definition,[sP108])],[predicate_definition_introduction]) ).
fof(f120,definition,
! [X13] :
( ! [X14] :
( ~ r1(X13,X14)
| ( ~ p2(X14)
& sP108(X14) ) )
| ~ sP109(X13) ),
introduced(definition,[new_symbols(definition,[sP109])],[predicate_definition_introduction]) ).
fof(f121,definition,
! [X12] :
( ? [X13] :
( r1(X12,X13)
& ~ p2(X13)
& sP109(X13) )
| ~ sP110(X12) ),
introduced(definition,[new_symbols(definition,[sP110])],[predicate_definition_introduction]) ).
fof(f122,definition,
! [X10] :
( ! [X11] :
( ~ r1(X10,X11)
| ( ~ p2(X11)
& ! [X12] :
( ~ r1(X11,X12)
| sP110(X12) ) ) )
| ~ sP111(X10) ),
introduced(definition,[new_symbols(definition,[sP111])],[predicate_definition_introduction]) ).
fof(f123,definition,
! [X9] :
( ! [X10] :
( ~ r1(X9,X10)
| ( ~ p2(X10)
& sP111(X10) ) )
| ~ sP112(X9) ),
introduced(definition,[new_symbols(definition,[sP112])],[predicate_definition_introduction]) ).
fof(f124,definition,
! [X8] :
( ? [X9] :
( r1(X8,X9)
& ~ p2(X9)
& sP112(X9) )
| ~ sP113(X8) ),
introduced(definition,[new_symbols(definition,[sP113])],[predicate_definition_introduction]) ).
fof(f125,definition,
! [X6] :
( ! [X7] :
( ~ r1(X6,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| sP113(X8) ) ) )
| ~ sP114(X6) ),
introduced(definition,[new_symbols(definition,[sP114])],[predicate_definition_introduction]) ).
fof(f126,definition,
! [X5] :
( ! [X6] :
( ~ r1(X5,X6)
| ( ~ p2(X6)
& sP114(X6) ) )
| ~ sP115(X5) ),
introduced(definition,[new_symbols(definition,[sP115])],[predicate_definition_introduction]) ).
fof(f127,definition,
! [X4] :
( ? [X5] :
( r1(X4,X5)
& ~ p2(X5)
& sP115(X5) )
| ~ sP116(X4) ),
introduced(definition,[new_symbols(definition,[sP116])],[predicate_definition_introduction]) ).
fof(f128,definition,
! [X2] :
( ! [X3] :
( ~ r1(X2,X3)
| ( ~ p2(X3)
& ! [X4] :
( ~ r1(X3,X4)
| sP116(X4) ) ) )
| ~ sP117(X2) ),
introduced(definition,[new_symbols(definition,[sP117])],[predicate_definition_introduction]) ).
fof(f129,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| ( ~ p2(X2)
& sP117(X2) ) )
| ~ sP118(X1) ),
introduced(definition,[new_symbols(definition,[sP118])],[predicate_definition_introduction]) ).
fof(f130,plain,
? [X0] :
( ~ p2(X0)
& ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP118(X1) ) )
& ~ p2(X0)
& ! [X21] :
( ~ r1(X0,X21)
| ( ~ p2(X21)
& sP104(X21) ) )
& ~ p2(X0)
& ! [X42] :
( ~ r1(X0,X42)
| ( ~ p2(X42)
& sP90(X42) ) )
& ~ p2(X0)
& ! [X63] :
( ~ r1(X0,X63)
| ( ~ p2(X63)
& sP76(X63) ) )
& ~ p2(X0)
& ! [X84] :
( ~ r1(X0,X84)
| ( ~ p2(X84)
& ! [X85] :
( ~ r1(X84,X85)
| sP62(X85) ) ) )
& ~ p2(X0)
& ! [X100] :
( ~ r1(X0,X100)
| ( ~ p2(X100)
& ! [X101] :
( ~ r1(X100,X101)
| sP52(X101) ) ) )
& ~ p2(X0)
& ! [X116] :
( ~ r1(X0,X116)
| ( ~ p2(X116)
& ! [X117] :
( ~ r1(X116,X117)
| sP42(X117) ) ) )
& ~ p2(X0)
& ! [X132] :
( ~ r1(X0,X132)
| sP32(X132) )
& ~ p2(X0)
& ! [X143] :
( ~ r1(X0,X143)
| sP25(X143) )
& ~ p2(X0)
& ! [X154] :
( ~ r1(X0,X154)
| sP18(X154) )
& ( ! [X165] :
( ~ r1(X0,X165)
| sP11(X165) )
| p2(X0) )
& ( ! [X171] :
( ~ r1(X0,X171)
| sP7(X171) )
| p1(X0) )
& ( ! [X177] :
( ~ r1(X0,X177)
| sP3(X177) )
| p1(X0) )
& ~ p1(X0) ),
inference(definition_folding,[],[f10,f129,f128,f127,f126,f125,f124,f123,f122,f121,f120,f119,f118,f117,f116,f115,f114,f113,f112,f111,f110,f109,f108,f107,f106,f105,f104,f103,f102,f101,f100,f99,f98,f97,f96,f95,f94,f93,f92,f91,f90,f89,f88,f87,f86,f85,f84,f83,f82,f81,f80,f79,f78,f77,f76,f75,f74,f73,f72,f71,f70,f69,f68,f67,f66,f65,f64,f63,f62,f61,f60,f59,f58,f57,f56,f55,f54,f53,f52,f51,f50,f49,f48,f47,f46,f45,f44,f43,f42,f41,f40,f39,f38,f37,f36,f35,f34,f33,f32,f31,f30,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11]) ).
fof(f131,plain,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| ( ~ p2(X2)
& sP117(X2) ) )
| ~ sP118(X1) ),
inference(nnf_transformation,[],[f129]) ).
fof(f132,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP117(X1) ) )
| ~ sP118(X0) ),
inference(rectify,[],[f131]) ).
fof(f133,plain,
! [X2] :
( ! [X3] :
( ~ r1(X2,X3)
| ( ~ p2(X3)
& ! [X4] :
( ~ r1(X3,X4)
| sP116(X4) ) ) )
| ~ sP117(X2) ),
inference(nnf_transformation,[],[f128]) ).
fof(f134,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| sP116(X2) ) ) )
| ~ sP117(X0) ),
inference(rectify,[],[f133]) ).
fof(f135,plain,
! [X4] :
( ? [X5] :
( r1(X4,X5)
& ~ p2(X5)
& sP115(X5) )
| ~ sP116(X4) ),
inference(nnf_transformation,[],[f127]) ).
fof(f136,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& sP115(X1) )
| ~ sP116(X0) ),
inference(rectify,[],[f135]) ).
fof(f137,plain,
! [X0] :
( ( r1(X0,sK119(X0))
& ~ p2(sK119(X0))
& sP115(sK119(X0)) )
| ~ sP116(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK119]),skolemize(X1,sK119(X0))],[f136]) ).
fof(f138,plain,
! [X5] :
( ! [X6] :
( ~ r1(X5,X6)
| ( ~ p2(X6)
& sP114(X6) ) )
| ~ sP115(X5) ),
inference(nnf_transformation,[],[f126]) ).
fof(f139,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP114(X1) ) )
| ~ sP115(X0) ),
inference(rectify,[],[f138]) ).
fof(f140,plain,
! [X6] :
( ! [X7] :
( ~ r1(X6,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| sP113(X8) ) ) )
| ~ sP114(X6) ),
inference(nnf_transformation,[],[f125]) ).
fof(f141,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| sP113(X2) ) ) )
| ~ sP114(X0) ),
inference(rectify,[],[f140]) ).
fof(f142,plain,
! [X8] :
( ? [X9] :
( r1(X8,X9)
& ~ p2(X9)
& sP112(X9) )
| ~ sP113(X8) ),
inference(nnf_transformation,[],[f124]) ).
fof(f143,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& sP112(X1) )
| ~ sP113(X0) ),
inference(rectify,[],[f142]) ).
fof(f144,plain,
! [X0] :
( ( r1(X0,sK120(X0))
& ~ p2(sK120(X0))
& sP112(sK120(X0)) )
| ~ sP113(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK120]),skolemize(X1,sK120(X0))],[f143]) ).
fof(f145,plain,
! [X9] :
( ! [X10] :
( ~ r1(X9,X10)
| ( ~ p2(X10)
& sP111(X10) ) )
| ~ sP112(X9) ),
inference(nnf_transformation,[],[f123]) ).
fof(f146,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP111(X1) ) )
| ~ sP112(X0) ),
inference(rectify,[],[f145]) ).
fof(f147,plain,
! [X10] :
( ! [X11] :
( ~ r1(X10,X11)
| ( ~ p2(X11)
& ! [X12] :
( ~ r1(X11,X12)
| sP110(X12) ) ) )
| ~ sP111(X10) ),
inference(nnf_transformation,[],[f122]) ).
fof(f148,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| sP110(X2) ) ) )
| ~ sP111(X0) ),
inference(rectify,[],[f147]) ).
fof(f149,plain,
! [X12] :
( ? [X13] :
( r1(X12,X13)
& ~ p2(X13)
& sP109(X13) )
| ~ sP110(X12) ),
inference(nnf_transformation,[],[f121]) ).
fof(f150,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& sP109(X1) )
| ~ sP110(X0) ),
inference(rectify,[],[f149]) ).
fof(f151,plain,
! [X0] :
( ( r1(X0,sK121(X0))
& ~ p2(sK121(X0))
& sP109(sK121(X0)) )
| ~ sP110(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK121]),skolemize(X1,sK121(X0))],[f150]) ).
fof(f152,plain,
! [X13] :
( ! [X14] :
( ~ r1(X13,X14)
| ( ~ p2(X14)
& sP108(X14) ) )
| ~ sP109(X13) ),
inference(nnf_transformation,[],[f120]) ).
fof(f153,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP108(X1) ) )
| ~ sP109(X0) ),
inference(rectify,[],[f152]) ).
fof(f154,plain,
! [X14] :
( ! [X15] :
( ~ r1(X14,X15)
| ( ~ p2(X15)
& ! [X16] :
( ~ r1(X15,X16)
| sP107(X16) ) ) )
| ~ sP108(X14) ),
inference(nnf_transformation,[],[f119]) ).
fof(f155,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| sP107(X2) ) ) )
| ~ sP108(X0) ),
inference(rectify,[],[f154]) ).
fof(f156,plain,
! [X16] :
( ? [X17] :
( r1(X16,X17)
& ~ p2(X17)
& sP106(X17) )
| ~ sP107(X16) ),
inference(nnf_transformation,[],[f118]) ).
fof(f157,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& sP106(X1) )
| ~ sP107(X0) ),
inference(rectify,[],[f156]) ).
fof(f158,plain,
! [X0] :
( ( r1(X0,sK122(X0))
& ~ p2(sK122(X0))
& sP106(sK122(X0)) )
| ~ sP107(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK122]),skolemize(X1,sK122(X0))],[f157]) ).
fof(f159,plain,
! [X17] :
( ! [X18] :
( ~ r1(X17,X18)
| ( ~ p2(X18)
& sP105(X18) ) )
| ~ sP106(X17) ),
inference(nnf_transformation,[],[f117]) ).
fof(f160,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP105(X1) ) )
| ~ sP106(X0) ),
inference(rectify,[],[f159]) ).
fof(f161,plain,
! [X18] :
( ! [X19] :
( ~ r1(X18,X19)
| ( ~ p2(X19)
& ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) )
| ~ sP105(X18) ),
inference(nnf_transformation,[],[f116]) ).
fof(f162,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) )
| ~ sP105(X0) ),
inference(rectify,[],[f161]) ).
fof(f376,plain,
! [X165] :
( ? [X166] :
( r1(X165,X166)
& ~ p2(X166)
& sP10(X166) )
| ~ sP11(X165) ),
inference(nnf_transformation,[],[f22]) ).
fof(f377,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& sP10(X1) )
| ~ sP11(X0) ),
inference(rectify,[],[f376]) ).
fof(f378,plain,
! [X0] :
( ( r1(X0,sK150(X0))
& ~ p2(sK150(X0))
& sP10(sK150(X0)) )
| ~ sP11(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK150]),skolemize(X1,sK150(X0))],[f377]) ).
fof(f379,plain,
! [X166] :
( ! [X167] :
( ~ r1(X166,X167)
| ( ~ p2(X167)
& sP9(X167) ) )
| ~ sP10(X166) ),
inference(nnf_transformation,[],[f21]) ).
fof(f380,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP9(X1) ) )
| ~ sP10(X0) ),
inference(rectify,[],[f379]) ).
fof(f381,plain,
! [X167] :
( ! [X168] :
( ~ r1(X167,X168)
| ( ~ p2(X168)
& sP8(X168) ) )
| ~ sP9(X167) ),
inference(nnf_transformation,[],[f20]) ).
fof(f382,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP8(X1) ) )
| ~ sP9(X0) ),
inference(rectify,[],[f381]) ).
fof(f383,plain,
! [X168] :
( ! [X169] :
( ~ r1(X168,X169)
| ( ~ p2(X169)
& ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) )
| ~ sP8(X168) ),
inference(nnf_transformation,[],[f19]) ).
fof(f384,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
| ~ sP8(X0) ),
inference(rectify,[],[f383]) ).
fof(f403,plain,
? [X0] :
( ~ p2(X0)
& ! [X1] :
( ~ r1(X0,X1)
| ( ~ p2(X1)
& sP118(X1) ) )
& ~ p2(X0)
& ! [X2] :
( ~ r1(X0,X2)
| ( ~ p2(X2)
& sP104(X2) ) )
& ~ p2(X0)
& ! [X3] :
( ~ r1(X0,X3)
| ( ~ p2(X3)
& sP90(X3) ) )
& ~ p2(X0)
& ! [X4] :
( ~ r1(X0,X4)
| ( ~ p2(X4)
& sP76(X4) ) )
& ~ p2(X0)
& ! [X5] :
( ~ r1(X0,X5)
| ( ~ p2(X5)
& ! [X6] :
( ~ r1(X5,X6)
| sP62(X6) ) ) )
& ~ p2(X0)
& ! [X7] :
( ~ r1(X0,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| sP52(X8) ) ) )
& ~ p2(X0)
& ! [X9] :
( ~ r1(X0,X9)
| ( ~ p2(X9)
& ! [X10] :
( ~ r1(X9,X10)
| sP42(X10) ) ) )
& ~ p2(X0)
& ! [X11] :
( ~ r1(X0,X11)
| sP32(X11) )
& ~ p2(X0)
& ! [X12] :
( ~ r1(X0,X12)
| sP25(X12) )
& ~ p2(X0)
& ! [X13] :
( ~ r1(X0,X13)
| sP18(X13) )
& ( ! [X14] :
( ~ r1(X0,X14)
| sP11(X14) )
| p2(X0) )
& ( ! [X15] :
( ~ r1(X0,X15)
| sP7(X15) )
| p1(X0) )
& ( ! [X16] :
( ~ r1(X0,X16)
| sP3(X16) )
| p1(X0) )
& ~ p1(X0) ),
inference(rectify,[],[f130]) ).
fof(f404,plain,
( ~ p2(sK153)
& ! [X1] :
( ~ r1(sK153,X1)
| ( ~ p2(X1)
& sP118(X1) ) )
& ~ p2(sK153)
& ! [X2] :
( ~ r1(sK153,X2)
| ( ~ p2(X2)
& sP104(X2) ) )
& ~ p2(sK153)
& ! [X3] :
( ~ r1(sK153,X3)
| ( ~ p2(X3)
& sP90(X3) ) )
& ~ p2(sK153)
& ! [X4] :
( ~ r1(sK153,X4)
| ( ~ p2(X4)
& sP76(X4) ) )
& ~ p2(sK153)
& ! [X5] :
( ~ r1(sK153,X5)
| ( ~ p2(X5)
& ! [X6] :
( ~ r1(X5,X6)
| sP62(X6) ) ) )
& ~ p2(sK153)
& ! [X7] :
( ~ r1(sK153,X7)
| ( ~ p2(X7)
& ! [X8] :
( ~ r1(X7,X8)
| sP52(X8) ) ) )
& ~ p2(sK153)
& ! [X9] :
( ~ r1(sK153,X9)
| ( ~ p2(X9)
& ! [X10] :
( ~ r1(X9,X10)
| sP42(X10) ) ) )
& ~ p2(sK153)
& ! [X11] :
( ~ r1(sK153,X11)
| sP32(X11) )
& ~ p2(sK153)
& ! [X12] :
( ~ r1(sK153,X12)
| sP25(X12) )
& ~ p2(sK153)
& ! [X13] :
( ~ r1(sK153,X13)
| sP18(X13) )
& ( ! [X14] :
( ~ r1(sK153,X14)
| sP11(X14) )
| p2(sK153) )
& ( ! [X15] :
( ~ r1(sK153,X15)
| sP7(X15) )
| p1(sK153) )
& ( ! [X16] :
( ~ r1(sK153,X16)
| sP3(X16) )
| p1(sK153) )
& ~ p1(sK153) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK153]),skolemize(X0,sK153)],[f403]) ).
fof(f405,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f407,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP117(X1)
| ~ sP118(X0) ),
inference(cnf_transformation,[],[f132]) ).
fof(f409,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP116(X2)
| ~ sP117(X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f411,plain,
! [X0] :
( sP115(sK119(X0))
| ~ sP116(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f413,plain,
! [X0] :
( r1(X0,sK119(X0))
| ~ sP116(X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f414,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP114(X1)
| ~ sP115(X0) ),
inference(cnf_transformation,[],[f139]) ).
fof(f416,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP113(X2)
| ~ sP114(X0) ),
inference(cnf_transformation,[],[f141]) ).
fof(f418,plain,
! [X0] :
( sP112(sK120(X0))
| ~ sP113(X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f420,plain,
! [X0] :
( r1(X0,sK120(X0))
| ~ sP113(X0) ),
inference(cnf_transformation,[],[f144]) ).
fof(f421,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP111(X1)
| ~ sP112(X0) ),
inference(cnf_transformation,[],[f146]) ).
fof(f423,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP110(X2)
| ~ sP111(X0) ),
inference(cnf_transformation,[],[f148]) ).
fof(f425,plain,
! [X0] :
( sP109(sK121(X0))
| ~ sP110(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f427,plain,
! [X0] :
( r1(X0,sK121(X0))
| ~ sP110(X0) ),
inference(cnf_transformation,[],[f151]) ).
fof(f428,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP108(X1)
| ~ sP109(X0) ),
inference(cnf_transformation,[],[f153]) ).
fof(f430,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP107(X2)
| ~ sP108(X0) ),
inference(cnf_transformation,[],[f155]) ).
fof(f432,plain,
! [X0] :
( sP106(sK122(X0))
| ~ sP107(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f434,plain,
! [X0] :
( r1(X0,sK122(X0))
| ~ sP107(X0) ),
inference(cnf_transformation,[],[f158]) ).
fof(f435,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP105(X1)
| ~ sP106(X0) ),
inference(cnf_transformation,[],[f160]) ).
fof(f437,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ sP105(X0) ),
inference(cnf_transformation,[],[f162]) ).
fof(f652,plain,
! [X0] :
( sP10(sK150(X0))
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f378]) ).
fof(f654,plain,
! [X0] :
( r1(X0,sK150(X0))
| ~ sP11(X0) ),
inference(cnf_transformation,[],[f378]) ).
fof(f655,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP9(X1)
| ~ sP10(X0) ),
inference(cnf_transformation,[],[f380]) ).
fof(f657,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| sP8(X1)
| ~ sP9(X0) ),
inference(cnf_transformation,[],[f382]) ).
fof(f659,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ p1(X2)
| ~ sP8(X0) ),
inference(cnf_transformation,[],[f384]) ).
fof(f682,plain,
! [X14] :
( ~ r1(sK153,X14)
| sP11(X14)
| p2(sK153) ),
inference(cnf_transformation,[],[f404]) ).
fof(f684,plain,
~ p2(sK153),
inference(cnf_transformation,[],[f404]) ).
fof(f707,plain,
! [X1] :
( ~ r1(sK153,X1)
| sP118(X1) ),
inference(cnf_transformation,[],[f404]) ).
fof(f710,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| sP116(X2)
| sP154(X1) ),
inference(cnf_transformation,[],[f710_D]) ).
fof(f710_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| sP116(X2) )
<=> ~ sP154(X1) ),
introduced(definition,[new_symbols(definition,[sP154])],[general_splitting_component_introduction]) ).
fof(f711,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP117(X0)
| ~ sP154(X1) ),
inference(general_splitting,[],[f409,f710_D]) ).
fof(f712,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| sP113(X2)
| sP155(X1) ),
inference(cnf_transformation,[],[f712_D]) ).
fof(f712_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| sP113(X2) )
<=> ~ sP155(X1) ),
introduced(definition,[new_symbols(definition,[sP155])],[general_splitting_component_introduction]) ).
fof(f713,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP114(X0)
| ~ sP155(X1) ),
inference(general_splitting,[],[f416,f712_D]) ).
fof(f714,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| sP110(X2)
| sP156(X1) ),
inference(cnf_transformation,[],[f714_D]) ).
fof(f714_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| sP110(X2) )
<=> ~ sP156(X1) ),
introduced(definition,[new_symbols(definition,[sP156])],[general_splitting_component_introduction]) ).
fof(f715,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP111(X0)
| ~ sP156(X1) ),
inference(general_splitting,[],[f423,f714_D]) ).
fof(f716,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| sP107(X2)
| sP157(X1) ),
inference(cnf_transformation,[],[f716_D]) ).
fof(f716_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| sP107(X2) )
<=> ~ sP157(X1) ),
introduced(definition,[new_symbols(definition,[sP157])],[general_splitting_component_introduction]) ).
fof(f717,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP108(X0)
| ~ sP157(X1) ),
inference(general_splitting,[],[f430,f716_D]) ).
fof(f718,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| p1(X2)
| sP158(X1) ),
inference(cnf_transformation,[],[f718_D]) ).
fof(f718_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
<=> ~ sP158(X1) ),
introduced(definition,[new_symbols(definition,[sP158])],[general_splitting_component_introduction]) ).
fof(f719,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP105(X0)
| ~ sP158(X1) ),
inference(general_splitting,[],[f437,f718_D]) ).
fof(f798,plain,
! [X2,X1] :
( ~ r1(X1,X2)
| ~ p1(X2)
| sP198(X1) ),
inference(cnf_transformation,[],[f798_D]) ).
fof(f798_D,definition,
! [X1] :
( ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) )
<=> ~ sP198(X1) ),
introduced(definition,[new_symbols(definition,[sP198])],[general_splitting_component_introduction]) ).
fof(f799,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| ~ sP8(X0)
| ~ sP198(X1) ),
inference(general_splitting,[],[f659,f798_D]) ).
fof(f806,plain,
! [X0] :
( ~ sP118(X0)
| sP117(X0) ),
inference(resolution,[],[f407,f405]) ).
fof(f911,plain,
! [X0] :
( ~ sP115(X0)
| sP114(X0) ),
inference(resolution,[],[f414,f405]) ).
fof(f946,plain,
! [X0] :
( sP114(sK119(X0))
| ~ sP116(X0) ),
inference(resolution,[],[f911,f411]) ).
fof(f1019,plain,
! [X0] :
( ~ sP112(X0)
| sP111(X0) ),
inference(resolution,[],[f421,f405]) ).
fof(f1054,plain,
! [X0] :
( sP111(sK120(X0))
| ~ sP113(X0) ),
inference(resolution,[],[f1019,f418]) ).
fof(f1127,plain,
! [X0] :
( ~ sP109(X0)
| sP108(X0) ),
inference(resolution,[],[f428,f405]) ).
fof(f1162,plain,
! [X0] :
( sP108(sK121(X0))
| ~ sP110(X0) ),
inference(resolution,[],[f1127,f425]) ).
fof(f1234,plain,
! [X0] :
( ~ sP106(X0)
| sP105(X0) ),
inference(resolution,[],[f435,f405]) ).
fof(f1270,plain,
! [X0] :
( sP105(sK122(X0))
| ~ sP107(X0) ),
inference(resolution,[],[f1234,f432]) ).
fof(f5014,plain,
! [X0] :
( sP9(sK120(X0))
| ~ sP10(X0)
| ~ sP113(X0) ),
inference(resolution,[],[f655,f420]) ).
fof(f5087,plain,
! [X0] :
( sP8(sK121(X0))
| ~ sP9(X0)
| ~ sP110(X0) ),
inference(resolution,[],[f657,f427]) ).
fof(f5552,plain,
! [X0] :
( sP154(X0)
| sP116(X0) ),
inference(resolution,[],[f710,f405]) ).
fof(f5587,plain,
! [X0] :
( ~ sP154(X0)
| ~ sP117(X0) ),
inference(resolution,[],[f711,f405]) ).
fof(f5622,plain,
! [X0] :
( ~ sP117(X0)
| sP116(X0) ),
inference(resolution,[],[f5587,f5552]) ).
fof(f5655,plain,
! [X0] :
( sP113(sK150(X0))
| sP155(X0)
| ~ sP11(X0) ),
inference(resolution,[],[f712,f654]) ).
fof(f5658,plain,
! [X0] :
( ~ sP155(X0)
| ~ sP114(X0) ),
inference(resolution,[],[f713,f405]) ).
fof(f5695,plain,
! [X0] :
( sP156(X0)
| sP110(X0) ),
inference(resolution,[],[f714,f405]) ).
fof(f5730,plain,
! [X0] :
( ~ sP156(X0)
| ~ sP111(X0) ),
inference(resolution,[],[f715,f405]) ).
fof(f5765,plain,
! [X0] :
( ~ sP111(X0)
| sP110(X0) ),
inference(resolution,[],[f5730,f5695]) ).
fof(f5766,plain,
! [X0] :
( sP110(sK120(X0))
| ~ sP113(X0) ),
inference(resolution,[],[f5765,f1054]) ).
fof(f5767,plain,
! [X0] :
( sP157(X0)
| sP107(X0) ),
inference(resolution,[],[f716,f405]) ).
fof(f5802,plain,
! [X0] :
( ~ sP157(X0)
| ~ sP108(X0) ),
inference(resolution,[],[f717,f405]) ).
fof(f5837,plain,
! [X0] :
( ~ sP108(X0)
| sP107(X0) ),
inference(resolution,[],[f5802,f5767]) ).
fof(f5838,plain,
! [X0] :
( sP107(sK121(X0))
| ~ sP110(X0) ),
inference(resolution,[],[f5837,f1162]) ).
fof(f5839,plain,
! [X0] :
( sP158(X0)
| p1(X0) ),
inference(resolution,[],[f718,f405]) ).
fof(f5874,plain,
! [X0] :
( ~ sP158(X0)
| ~ sP105(X0) ),
inference(resolution,[],[f719,f405]) ).
fof(f5909,plain,
! [X0] :
( ~ sP105(X0)
| p1(X0) ),
inference(resolution,[],[f5874,f5839]) ).
fof(f5910,plain,
! [X0] :
( p1(sK122(X0))
| ~ sP107(X0) ),
inference(resolution,[],[f5909,f1270]) ).
fof(f8069,plain,
! [X0] :
( ~ p1(sK122(X0))
| sP198(X0)
| ~ sP107(X0) ),
inference(resolution,[],[f798,f434]) ).
fof(f8100,plain,
! [X0] :
( sP198(X0)
| ~ sP107(X0) ),
inference(forward_subsumption_resolution,[],[f8069,f5910]) ).
fof(f8101,plain,
! [X0] :
( ~ sP198(X0)
| ~ sP8(X0) ),
inference(resolution,[],[f799,f405]) ).
fof(f8136,plain,
! [X0] :
( ~ sP107(X0)
| ~ sP8(X0) ),
inference(resolution,[],[f8101,f8100]) ).
fof(f8138,plain,
! [X0] :
( ~ sP8(sK121(X0))
| ~ sP110(X0) ),
inference(resolution,[],[f8136,f5838]) ).
fof(f11313,plain,
sP118(sK153),
inference(resolution,[],[f707,f405]) ).
fof(f11356,plain,
sP117(sK153),
inference(resolution,[],[f11313,f806]) ).
fof(f11357,plain,
sP116(sK153),
inference(resolution,[],[f11356,f5622]) ).
fof(f11749,plain,
( sP11(sK119(sK153))
| p2(sK153)
| ~ sP116(sK153) ),
inference(resolution,[],[f682,f413]) ).
fof(f11816,plain,
( sP11(sK119(sK153))
| ~ sP116(sK153) ),
inference(forward_subsumption_resolution,[],[f11749,f684]) ).
fof(f11827,plain,
sP11(sK119(sK153)),
inference(forward_subsumption_resolution,[],[f11816,f11357]) ).
fof(f12645,plain,
! [X0] :
( ~ sP9(X0)
| ~ sP110(X0)
| ~ sP110(X0) ),
inference(resolution,[],[f5087,f8138]) ).
fof(f12648,plain,
! [X0] :
( ~ sP110(X0)
| ~ sP9(X0) ),
inference(duplicate_literal_removal,[],[f12645]) ).
fof(f12649,plain,
! [X0] :
( ~ sP9(sK120(X0))
| ~ sP113(X0) ),
inference(resolution,[],[f12648,f5766]) ).
fof(f12650,plain,
! [X0] :
( ~ sP113(X0)
| ~ sP10(X0)
| ~ sP113(X0) ),
inference(resolution,[],[f12649,f5014]) ).
fof(f12651,plain,
! [X0] :
( ~ sP113(X0)
| ~ sP10(X0) ),
inference(duplicate_literal_removal,[],[f12650]) ).
fof(f13486,plain,
! [X0] :
( sP155(X0)
| ~ sP11(X0)
| ~ sP10(sK150(X0)) ),
inference(resolution,[],[f5655,f12651]) ).
fof(f13488,plain,
! [X0] :
( sP155(X0)
| ~ sP11(X0) ),
inference(forward_subsumption_resolution,[],[f13486,f652]) ).
fof(f13489,plain,
! [X0] :
( ~ sP114(X0)
| ~ sP11(X0) ),
inference(resolution,[],[f13488,f5658]) ).
fof(f13491,plain,
! [X0] :
( ~ sP11(sK119(X0))
| ~ sP116(X0) ),
inference(resolution,[],[f13489,f946]) ).
fof(f13525,plain,
~ sP116(sK153),
inference(resolution,[],[f13491,f11827]) ).
fof(f13526,plain,
$false,
inference(forward_subsumption_resolution,[],[f13525,f11357]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL680+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.37 % Computer : n012.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sun Sep 27 16:36:11 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.40 Running first-order theorem proving
% 0.08/0.40 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.20/2.73 % (2573526)Detected formulas, will run a generic FOF schedule.
% 13.20/2.73 % (2573538)dis-21_1_sil=8000:lcm=predicate:random_seed=2401105608: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)
% 13.20/2.73 % (2573538)Instruction limit reached!
% 13.20/2.73 % (2573538)------------------------------
% 13.20/2.73 % (2573538)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.73 % (2573538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.73 % (2573538)CaDiCaL version: 2.1.3
% 13.20/2.73 % (2573538)Termination reason: Instruction limit
% 13.20/2.73 % (2573538)Termination phase: Saturation
% 13.20/2.73 % (2573538)Time elapsed: 0.029 s
% 13.20/2.73 % (2573538)Peak memory usage: 89 MB
% 13.20/2.73 % (2573538)Instructions burned: 131 (million)
% 13.20/2.73 % (2573537)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=940175843:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.20/2.73 % (2573533)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=3312705686:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.20/2.73 % (2573532)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=3675002773:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.20/2.73 % (2573535)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=144986526:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.20/2.73 % (2573536)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1973816092:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.20/2.73 % (2573534)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=1224836226:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.20/2.73 % (2573536)Instruction limit reached!
% 13.20/2.73 % (2573536)------------------------------
% 13.20/2.73 % (2573536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.73 % (2573536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.73 % (2573536)CaDiCaL version: 2.1.3
% 13.20/2.73 % (2573536)Termination reason: Instruction limit
% 13.20/2.73 % (2573536)Termination phase: Saturation
% 13.20/2.73 % (2573536)Time elapsed: 0.044 s
% 13.20/2.73 % (2573536)Peak memory usage: 88 MB
% 13.20/2.73 % (2573536)Instructions burned: 119 (million)
% 13.20/2.73 % (2573535)Instruction limit reached!
% 13.20/2.73 % (2573535)------------------------------
% 13.20/2.73 % (2573535)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.73 % (2573535)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.73 % (2573535)CaDiCaL version: 2.1.3
% 13.20/2.73 % (2573535)Termination reason: Instruction limit
% 13.20/2.73 % (2573535)Termination phase: Saturation
% 13.20/2.73 % (2573535)Time elapsed: 0.050 s
% 13.20/2.73 % (2573535)Peak memory usage: 90 MB
% 13.20/2.73 % (2573535)Instructions burned: 109 (million)
% 13.20/2.73 % (2573537)Instruction limit reached!
% 13.20/2.73 % (2573537)------------------------------
% 13.20/2.73 % (2573537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.20/2.73 % (2573537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.20/2.73 % (2573537)CaDiCaL version: 2.1.3
% 13.20/2.73 % (2573537)Termination reason: Instruction limit
% 13.20/2.73 % (2573537)Termination phase: Saturation
% 13.20/2.73 % (2573537)Time elapsed: 0.050 s
% 13.20/2.73 % (2573537)Peak memory usage: 89 MB
% 13.20/2.73 % (2573537)Instructions burned: 140 (million)
% 13.20/2.73 % (2573540)lrs+10_1_sil=8000:sp=occurrence:random_seed=902704410:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 13.20/2.73 % (2573549)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3492403987:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.20/2.73 % (2573548)lrs+10_1_sil=32000:urr=on:br=off:random_seed=950749216:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.20/2.73 % (2573550)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=314695407:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.20/2.73 % (2573540)Instruction limit reached!
% 18.90/3.58 % (2573540)------------------------------
% 18.90/3.58 % (2573540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573540)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573540)Termination reason: Instruction limit
% 18.90/3.58 % (2573540)Termination phase: Saturation
% 18.90/3.58 % (2573540)Time elapsed: 0.130 s
% 18.90/3.58 % (2573540)Peak memory usage: 91 MB
% 18.90/3.58 % (2573540)Instructions burned: 286 (million)
% 18.90/3.58 % (2573548)Instruction limit reached!
% 18.90/3.58 % (2573548)------------------------------
% 18.90/3.58 % (2573548)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573548)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573548)Termination reason: Instruction limit
% 18.90/3.58 % (2573548)Termination phase: Saturation
% 18.90/3.58 % (2573548)Time elapsed: 0.066 s
% 18.90/3.58 % (2573548)Peak memory usage: 89 MB
% 18.90/3.58 % (2573548)Instructions burned: 159 (million)
% 18.90/3.58 % (2573549)Instruction limit reached!
% 18.90/3.58 % (2573549)------------------------------
% 18.90/3.58 % (2573549)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573549)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573549)Termination reason: Instruction limit
% 18.90/3.58 % (2573549)Termination phase: Saturation
% 18.90/3.58 % (2573549)Time elapsed: 0.101 s
% 18.90/3.58 % (2573549)Peak memory usage: 89 MB
% 18.90/3.58 % (2573549)Instructions burned: 326 (million)
% 18.90/3.58 % (2573550)Instruction limit reached!
% 18.90/3.58 % (2573550)------------------------------
% 18.90/3.58 % (2573550)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573550)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573550)Termination reason: Instruction limit
% 18.90/3.58 % (2573550)Termination phase: Saturation
% 18.90/3.58 % (2573550)Time elapsed: 0.105 s
% 18.90/3.58 % (2573550)Peak memory usage: 89 MB
% 18.90/3.58 % (2573550)Instructions burned: 248 (million)
% 18.90/3.58 % (2573556)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4125422803:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 18.90/3.58 % (2573559)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2667510504:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 18.90/3.58 % (2573558)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3212584001:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 18.90/3.58 % (2573557)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2207268465:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 18.90/3.58 % (2573559)Instruction limit reached!
% 18.90/3.58 % (2573559)------------------------------
% 18.90/3.58 % (2573559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573559)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573559)Termination reason: Instruction limit
% 18.90/3.58 % (2573559)Termination phase: Saturation
% 18.90/3.58 % (2573559)Time elapsed: 0.035 s
% 18.90/3.58 % (2573559)Peak memory usage: 89 MB
% 18.90/3.58 % (2573559)Instructions burned: 128 (million)
% 18.90/3.58 % (2573558)Instruction limit reached!
% 18.90/3.58 % (2573558)------------------------------
% 18.90/3.58 % (2573558)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573558)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573558)Termination reason: Instruction limit
% 18.90/3.58 % (2573558)Termination phase: Saturation
% 18.90/3.58 % (2573558)Time elapsed: 0.054 s
% 18.90/3.58 % (2573558)Peak memory usage: 90 MB
% 18.90/3.58 % (2573558)Instructions burned: 113 (million)
% 18.90/3.58 % (2573556)Instruction limit reached!
% 18.90/3.58 % (2573556)------------------------------
% 18.90/3.58 % (2573556)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.90/3.58 % (2573556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.90/3.58 % (2573556)CaDiCaL version: 2.1.3
% 18.90/3.58 % (2573556)Termination reason: Instruction limit
% 18.90/3.58 % (2573556)Termination phase: Saturation
% 44.36/7.10 % (2573556)Time elapsed: 0.125 s
% 44.36/7.10 % (2573556)Peak memory usage: 89 MB
% 44.36/7.10 % (2573556)Instructions burned: 296 (million)
% 44.36/7.10 % (2573564)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3379137679:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 44.36/7.10 % (2573566)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3839684916:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 44.36/7.10 % (2573564)Instruction limit reached!
% 44.36/7.10 % (2573564)------------------------------
% 44.36/7.10 % (2573564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/7.10 % (2573564)CaDiCaL version: 2.1.3
% 44.36/7.10 % (2573564)Termination reason: Instruction limit
% 44.36/7.10 % (2573564)Termination phase: Saturation
% 44.36/7.10 % (2573564)Time elapsed: 0.052 s
% 44.36/7.10 % (2573564)Peak memory usage: 89 MB
% 44.36/7.10 % (2573564)Instructions burned: 115 (million)
% 44.36/7.10 % (2573565)lrs+10_1_sil=8000:sp=occurrence:random_seed=3891233159:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 44.36/7.10 % (2573569)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1853902402:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 44.36/7.10 % (2573566)Instruction limit reached!
% 44.36/7.10 % (2573566)------------------------------
% 44.36/7.10 % (2573566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/7.10 % (2573566)CaDiCaL version: 2.1.3
% 44.36/7.10 % (2573566)Termination reason: Instruction limit
% 44.36/7.10 % (2573566)Termination phase: Saturation
% 44.36/7.10 % (2573566)Time elapsed: 0.169 s
% 44.36/7.10 % (2573566)Peak memory usage: 91 MB
% 44.36/7.10 % (2573566)Instructions burned: 439 (million)
% 44.36/7.10 % (2573572)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2342351092:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 44.36/7.10 % (2573565)Instruction limit reached!
% 44.36/7.10 % (2573565)------------------------------
% 44.36/7.10 % (2573565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/7.10 % (2573565)CaDiCaL version: 2.1.3
% 44.36/7.10 % (2573565)Termination reason: Instruction limit
% 44.36/7.10 % (2573565)Termination phase: Saturation
% 44.36/7.10 % (2573565)Time elapsed: 0.379 s
% 44.36/7.10 % (2573565)Peak memory usage: 96 MB
% 44.36/7.10 % (2573565)Instructions burned: 907 (million)
% 44.36/7.10 % (2573572)Instruction limit reached!
% 44.36/7.10 % (2573572)------------------------------
% 44.36/7.10 % (2573572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/7.10 % (2573572)CaDiCaL version: 2.1.3
% 44.36/7.10 % (2573572)Termination reason: Instruction limit
% 44.36/7.10 % (2573572)Termination phase: Saturation
% 44.36/7.10 % (2573572)Time elapsed: 0.057 s
% 44.36/7.10 % (2573572)Peak memory usage: 89 MB
% 44.36/7.10 % (2573572)Instructions burned: 136 (million)
% 44.36/7.10 % (2573574)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2599690868:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 44.36/7.10 % (2573575)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=680200413:st=3:i=13193:sd=3:ss=axioms_2986 on theBenchmark for (2986ds/13193Mi)
% 44.36/7.10 % (2573574)Instruction limit reached!
% 44.36/7.10 % (2573574)------------------------------
% 44.36/7.10 % (2573574)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.36/7.10 % (2573574)CaDiCaL version: 2.1.3
% 44.36/7.10 % (2573574)Termination reason: Instruction limit
% 44.36/7.10 % (2573574)Termination phase: Saturation
% 44.36/7.10 % (2573574)Time elapsed: 0.238 s
% 44.36/7.10 % (2573574)Peak memory usage: 93 MB
% 44.36/7.10 % (2573574)Instructions burned: 594 (million)
% 44.36/7.10 % (2573557)Instruction limit reached!
% 44.36/7.10 % (2573557)------------------------------
% 44.36/7.10 % (2573557)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 44.36/7.10 % (2573557)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573557)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573557)Termination reason: Instruction limit
% 67.47/10.34 % (2573557)Termination phase: Saturation
% 67.47/10.34 % (2573557)Time elapsed: 1.284 s
% 67.47/10.34 % (2573557)Peak memory usage: 144 MB
% 67.47/10.34 % (2573557)Instructions burned: 2351 (million)
% 67.47/10.34 % (2573579)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=3841872991:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2982 on theBenchmark for (2982ds/125Mi)
% 67.47/10.34 % (2573579)Instruction limit reached!
% 67.47/10.34 % (2573579)------------------------------
% 67.47/10.34 % (2573579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.47/10.34 % (2573579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573579)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573579)Termination reason: Instruction limit
% 67.47/10.34 % (2573579)Termination phase: Saturation
% 67.47/10.34 % (2573579)Time elapsed: 0.063 s
% 67.47/10.34 % (2573579)Peak memory usage: 91 MB
% 67.47/10.34 % (2573579)Instructions burned: 127 (million)
% 67.47/10.34 % (2573582)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2939717580:i=134:gtgl=5:slsql=off:gtg=exists_sym_2980 on theBenchmark for (2980ds/134Mi)
% 67.47/10.34 % (2573582)Instruction limit reached!
% 67.47/10.34 % (2573582)------------------------------
% 67.47/10.34 % (2573582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.47/10.34 % (2573582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573582)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573582)Termination reason: Instruction limit
% 67.47/10.34 % (2573582)Termination phase: Saturation
% 67.47/10.34 % (2573582)Time elapsed: 0.045 s
% 67.47/10.34 % (2573582)Peak memory usage: 92 MB
% 67.47/10.34 % (2573582)Instructions burned: 134 (million)
% 67.47/10.34 % (2573584)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1629370297:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/141Mi)
% 67.47/10.34 % (2573584)Instruction limit reached!
% 67.47/10.34 % (2573584)------------------------------
% 67.47/10.34 % (2573584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.47/10.34 % (2573584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573584)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573584)Termination reason: Instruction limit
% 67.47/10.34 % (2573584)Termination phase: Saturation
% 67.47/10.34 % (2573584)Time elapsed: 0.069 s
% 67.47/10.34 % (2573584)Peak memory usage: 91 MB
% 67.47/10.34 % (2573584)Instructions burned: 143 (million)
% 67.47/10.34 % (2573586)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3732800775:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2978 on theBenchmark for (2978ds/431Mi)
% 67.47/10.34 % (2573586)Instruction limit reached!
% 67.47/10.34 % (2573586)------------------------------
% 67.47/10.34 % (2573586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.47/10.34 % (2573586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573586)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573586)Termination reason: Instruction limit
% 67.47/10.34 % (2573586)Termination phase: Saturation
% 67.47/10.34 % (2573586)Time elapsed: 0.161 s
% 67.47/10.34 % (2573586)Peak memory usage: 97 MB
% 67.47/10.34 % (2573586)Instructions burned: 434 (million)
% 67.47/10.34 % (2573590)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=1861158824:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 67.47/10.34 % (2573592)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=2629257993:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2974 on theBenchmark for (2974ds/150Mi)
% 67.47/10.34 % (2573592)Instruction limit reached!
% 67.47/10.34 % (2573592)------------------------------
% 67.47/10.34 % (2573592)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.47/10.34 % (2573592)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.47/10.34 % (2573592)CaDiCaL version: 2.1.3
% 67.47/10.34 % (2573592)Termination reason: Instruction limit
% 67.47/10.34 % (2573592)Termination phase: Saturation
% 67.47/10.34 % (2573592)Time elapsed: 0.072 s
% 67.47/10.34 % (2573592)Peak memory usage: 92 MB
% 74.88/11.46 % (2573592)Instructions burned: 151 (million)
% 74.88/11.46 % (2573598)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=703775275:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 74.88/11.46 % (2573569)Instruction limit reached!
% 74.88/11.46 % (2573569)------------------------------
% 74.88/11.46 % (2573569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573569)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573569)Termination reason: Instruction limit
% 74.88/11.46 % (2573569)Termination phase: Saturation
% 74.88/11.46 % (2573569)Time elapsed: 2.331 s
% 74.88/11.46 % (2573569)Peak memory usage: 158 MB
% 74.88/11.46 % (2573569)Instructions burned: 5203 (million)
% 74.88/11.46 % (2573602)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=147232690:i=667:av=off:fsr=off_2966 on theBenchmark for (2966ds/667Mi)
% 74.88/11.46 % (2573602)Instruction limit reached!
% 74.88/11.46 % (2573602)------------------------------
% 74.88/11.46 % (2573602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573602)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573602)Termination reason: Instruction limit
% 74.88/11.46 % (2573602)Termination phase: Saturation
% 74.88/11.46 % (2573602)Time elapsed: 0.224 s
% 74.88/11.46 % (2573602)Peak memory usage: 113 MB
% 74.88/11.46 % (2573602)Instructions burned: 668 (million)
% 74.88/11.46 % (2573604)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1636422531:s2a=on:i=185:s2at=1.8:fdi=4_2961 on theBenchmark for (2961ds/185Mi)
% 74.88/11.46 % (2573604)Instruction limit reached!
% 74.88/11.46 % (2573604)------------------------------
% 74.88/11.46 % (2573604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573604)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573604)Termination reason: Instruction limit
% 74.88/11.46 % (2573604)Termination phase: Saturation
% 74.88/11.46 % (2573604)Time elapsed: 0.050 s
% 74.88/11.46 % (2573604)Peak memory usage: 90 MB
% 74.88/11.46 % (2573604)Instructions burned: 188 (million)
% 74.88/11.46 % (2573606)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2850410642:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2959 on theBenchmark for (2959ds/193Mi)
% 74.88/11.46 % (2573606)Instruction limit reached!
% 74.88/11.46 % (2573606)------------------------------
% 74.88/11.46 % (2573606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573606)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573606)Termination reason: Instruction limit
% 74.88/11.46 % (2573606)Termination phase: Saturation
% 74.88/11.46 % (2573606)Time elapsed: 0.085 s
% 74.88/11.46 % (2573606)Peak memory usage: 92 MB
% 74.88/11.46 % (2573606)Instructions burned: 194 (million)
% 74.88/11.46 % (2573610)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2329651343:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2956 on theBenchmark for (2956ds/4850Mi)
% 74.88/11.46 % (2573590)Instruction limit reached!
% 74.88/11.46 % (2573590)------------------------------
% 74.88/11.46 % (2573590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573590)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573590)Termination reason: Instruction limit
% 74.88/11.46 % (2573590)Termination phase: Saturation
% 74.88/11.46 % (2573590)Time elapsed: 2.966 s
% 74.88/11.46 % (2573590)Peak memory usage: 177 MB
% 74.88/11.46 % (2573590)Instructions burned: 6061 (million)
% 74.88/11.46 % (2573616)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1717305410:i=12111:sd=1:ss=included_2944 on theBenchmark for (2944ds/12111Mi)
% 74.88/11.46 % (2573610)Instruction limit reached!
% 74.88/11.46 % (2573610)------------------------------
% 74.88/11.46 % (2573610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573610)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573610)Termination reason: Instruction limit
% 74.88/11.46 % (2573610)Termination phase: Saturation
% 74.88/11.46 % (2573610)Time elapsed: 1.800 s
% 74.88/11.46 % (2573610)Peak memory usage: 106 MB
% 74.88/11.46 % (2573610)Instructions burned: 4851 (million)
% 74.88/11.46 % (2573624)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=225996558:i=319:kws=precedence:fsr=off_2936 on theBenchmark for (2936ds/319Mi)
% 74.88/11.46 % (2573624)Instruction limit reached!
% 74.88/11.46 % (2573624)------------------------------
% 74.88/11.46 % (2573624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573624)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573624)Termination reason: Instruction limit
% 74.88/11.46 % (2573624)Termination phase: Saturation
% 74.88/11.46 % (2573624)Time elapsed: 0.138 s
% 74.88/11.46 % (2573624)Peak memory usage: 91 MB
% 74.88/11.46 % (2573624)Instructions burned: 320 (million)
% 74.88/11.46 % (2573628)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=818359858:i=2064:ep=RST_2932 on theBenchmark for (2932ds/2064Mi)
% 74.88/11.46 % (2573628)Instruction limit reached!
% 74.88/11.46 % (2573628)------------------------------
% 74.88/11.46 % (2573628)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573628)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573628)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573628)Termination reason: Instruction limit
% 74.88/11.46 % (2573628)Termination phase: Saturation
% 74.88/11.46 % (2573628)Time elapsed: 0.898 s
% 74.88/11.46 % (2573628)Peak memory usage: 103 MB
% 74.88/11.46 % (2573628)Instructions burned: 2064 (million)
% 74.88/11.46 % (2573637)dis-1011_128_sil=32000:random_seed=162773901:i=3706:ep=RST:av=off_2921 on theBenchmark for (2921ds/3706Mi)
% 74.88/11.46 % (2573575)Instruction limit reached!
% 74.88/11.46 % (2573575)------------------------------
% 74.88/11.46 % (2573575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573575)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573575)Termination reason: Instruction limit
% 74.88/11.46 % (2573575)Termination phase: Saturation
% 74.88/11.46 % (2573575)Time elapsed: 6.950 s
% 74.88/11.46 % (2573575)Peak memory usage: 236 MB
% 74.88/11.46 % (2573575)Instructions burned: 13193 (million)
% 74.88/11.46 % (2573640)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1468138061:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2914 on theBenchmark for (2914ds/757Mi)
% 74.88/11.46 % (2573598)Instruction limit reached!
% 74.88/11.46 % (2573598)------------------------------
% 74.88/11.46 % (2573598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573598)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573598)Termination reason: Instruction limit
% 74.88/11.46 % (2573598)Termination phase: Saturation
% 74.88/11.46 % (2573598)Time elapsed: 6.148 s
% 74.88/11.46 % (2573598)Peak memory usage: 195 MB
% 74.88/11.46 % (2573598)Instructions burned: 14157 (million)
% 74.88/11.46 % (2573640)Instruction limit reached!
% 74.88/11.46 % (2573640)------------------------------
% 74.88/11.46 % (2573640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573640)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573640)Termination reason: Instruction limit
% 74.88/11.46 % (2573640)Termination phase: Saturation
% 74.88/11.46 % (2573640)Time elapsed: 0.406 s
% 74.88/11.46 % (2573640)Peak memory usage: 103 MB
% 74.88/11.46 % (2573640)Instructions burned: 757 (million)
% 74.88/11.46 % (2573642)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=334007079:i=13913:ss=axioms:sgt=8_2908 on theBenchmark for (2908ds/13913Mi)
% 74.88/11.46 % (2573643)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=881680383:i=9925:aac=none_2907 on theBenchmark for (2907ds/9925Mi)
% 74.88/11.46 % (2573637)Instruction limit reached!
% 74.88/11.46 % (2573637)------------------------------
% 74.88/11.46 % (2573637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573637)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573637)Termination reason: Instruction limit
% 74.88/11.46 % (2573637)Termination phase: Saturation
% 74.88/11.46 % (2573637)Time elapsed: 1.503 s
% 74.88/11.46 % (2573637)Peak memory usage: 92 MB
% 74.88/11.46 % (2573637)Instructions burned: 3707 (million)
% 74.88/11.46 % (2573646)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=442047077:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2904 on theBenchmark for (2904ds/2479Mi)
% 74.88/11.46 % (2573616)Instruction limit reached!
% 74.88/11.46 % (2573616)------------------------------
% 74.88/11.46 % (2573616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 74.88/11.46 % (2573616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 74.88/11.46 % (2573616)CaDiCaL version: 2.1.3
% 74.88/11.46 % (2573616)Termination reason: Instruction limit
% 74.88/11.46 % (2573616)Termination phase: Saturation
% 74.88/11.46 % (2573616)Time elapsed: 4.464 s
% 74.88/11.46 % (2573616)Peak memory usage: 159 MB
% 74.88/11.46 % (2573616)Instructions burned: 12114 (million)
% 74.88/11.46 % (2573651)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=1353836308:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2897 on theBenchmark for (2897ds/440Mi)
% 74.88/11.46 % (2573651)First to succeed.
% 74.88/11.46 % (2573651)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2573526"
% 74.88/11.46 % (2573651)Refutation found. Thanks to Tanya!
% 74.88/11.46 % SZS status Theorem for theBenchmark
% 74.88/11.46 % SZS output start Proof for theBenchmark
% See solution above
% 75.61/11.59 % (2573651)------------------------------
% 75.61/11.59 % (2573651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.61/11.59 % (2573651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.61/11.59 % (2573651)CaDiCaL version: 2.1.3
% 75.61/11.59 % (2573651)Termination reason: Refutation
% 75.61/11.59 % (2573651)Time elapsed: 0.083 s
% 75.61/11.59 % (2573651)Peak memory usage: 95 MB
% 75.61/11.59 % (2573651)Instructions burned: 300 (million)
% 75.61/11.59 % (2573651)------------------------------
% 75.61/11.59 % (2573651)------------------------------
% 75.61/11.59 % (2573526)Success in time 10.697 s
% 75.61/11.59 % Vampire exiting
%------------------------------------------------------------------------------