%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL658+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:54:23 AM UTC 2026
% Result : Theorem 9.88s 2.28s
% Output : Refutation 10.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 32
% Syntax : Number of formulae : 354 ( 35 unt; 31 def)
% Number of atoms : 3608 ( 0 equ)
% Maximal formula atoms : 238 ( 10 avg)
% Number of connectives : 5998 (2744 ~;2857 |; 370 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 61 ( 8 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 34 ( 33 usr; 28 prp; 0-2 aty)
% Number of functors : 37 ( 37 usr; 11 con; 0-1 aty)
% Number of variables : 2191 ( 0 sgn2030 !; 161 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f3,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ~ ! [X17] :
( ~ r1(X14,X17)
| p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ~ ! [X33] :
( ~ r1(X30,X33)
| p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ~ ! [X48] :
( ~ r1(X45,X48)
| p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ~ ! [X62] :
( ~ r1(X59,X62)
| p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ~ ! [X75] :
( ~ r1(X72,X75)
| p1(X75) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ~ ! [X87] :
( ~ r1(X84,X87)
| p1(X87) ) ) ) ) ) ) ) ) ) )
| ~ ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( ( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) )
| ~ ! [X100] :
( ~ r1(X95,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100)
| ~ ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ~ ( ! [X105] :
( ~ r1(X102,X105)
| p1(X105) )
| ~ p1(X102) ) ) ) )
& ( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ~ ! [X107] :
( ~ r1(X106,X107)
| p1(X107) ) )
| ~ ! [X108] :
( ~ r1(X95,X108)
| p1(X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) ) )
& ! [X111] :
( ~ r1(X95,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
| ~ ! [X114] :
( ~ r1(X111,X114)
| p1(X114) ) )
& ( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
| ~ ! [X119] :
( ~ r1(X95,X119)
| p1(X119)
| ~ ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) )
| ~ p1(X120) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X122] :
( ~ r1(X0,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ! [X131] :
( ~ r1(X129,X131)
| ~ ! [X132] :
( ~ r1(X131,X132)
| p1(X132) ) )
| ~ ! [X133] :
( ~ r1(X129,X133)
| p1(X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) )
| ~ p1(X134) ) ) ) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| p1(X153) ) )
| ~ ! [X154] :
( ~ r1(X151,X154)
| p1(X154) ) ) ) ) ) ) )
& ! [X155] :
( ~ r1(X0,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| p1(X161) ) )
| ~ ! [X162] :
( ~ r1(X159,X162)
| p1(X162) ) ) ) ) ) )
& ! [X163] :
( ~ r1(X0,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ~ ! [X169] :
( ~ r1(X166,X169)
| p1(X169) ) ) ) ) )
& ! [X170] :
( ~ r1(X0,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| p1(X174) ) )
| ~ ! [X175] :
( ~ r1(X172,X175)
| p1(X175) ) ) ) )
& ! [X176] :
( ~ r1(X0,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) ) )
| ~ ! [X180] :
( ~ r1(X177,X180)
| p1(X180) ) ) )
& ! [X181] :
( ~ r1(X0,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) ) )
| ~ ! [X184] :
( ~ r1(X181,X184)
| p1(X184) ) ) ) ),
inference(rectify,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ~ ! [X17] :
( ~ r1(X14,X17)
| p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ~ ! [X33] :
( ~ r1(X30,X33)
| p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ~ ! [X48] :
( ~ r1(X45,X48)
| p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ~ ! [X62] :
( ~ r1(X59,X62)
| p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ~ ! [X75] :
( ~ r1(X72,X75)
| p1(X75) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ~ ! [X87] :
( ~ r1(X84,X87)
| p1(X87) ) ) ) ) ) ) ) ) ) )
| ~ ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( ( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ~ ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) )
| ~ ! [X100] :
( ~ r1(X95,X100)
| ! [X101] :
( ~ r1(X100,X101)
| p1(X101) )
| ~ p1(X100)
| ~ ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ~ ( ! [X105] :
( ~ r1(X102,X105)
| p1(X105) )
| ~ p1(X102) ) ) ) )
& ( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ~ ! [X107] :
( ~ r1(X106,X107)
| p1(X107) ) )
| ~ ! [X108] :
( ~ r1(X95,X108)
| p1(X108)
| ~ ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) ) )
& ! [X111] :
( ~ r1(X95,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
| ~ ! [X114] :
( ~ r1(X111,X114)
| p1(X114) ) )
& ( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
| ~ ! [X119] :
( ~ r1(X95,X119)
| p1(X119)
| ~ ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) )
| ~ p1(X120) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X122] :
( ~ r1(X0,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ! [X127] :
( ~ r1(X126,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ! [X131] :
( ~ r1(X129,X131)
| ~ ! [X132] :
( ~ r1(X131,X132)
| p1(X132) ) )
| ~ ! [X133] :
( ~ r1(X129,X133)
| p1(X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) )
| ~ p1(X134) ) ) ) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| p1(X153) ) )
| ~ ! [X154] :
( ~ r1(X151,X154)
| p1(X154) ) ) ) ) ) ) )
& ! [X155] :
( ~ r1(X0,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| p1(X161) ) )
| ~ ! [X162] :
( ~ r1(X159,X162)
| p1(X162) ) ) ) ) ) )
& ! [X163] :
( ~ r1(X0,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ~ ! [X169] :
( ~ r1(X166,X169)
| p1(X169) ) ) ) ) )
& ! [X170] :
( ~ r1(X0,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| p1(X174) ) )
| ~ ! [X175] :
( ~ r1(X172,X175)
| p1(X175) ) ) ) )
& ! [X176] :
( ~ r1(X0,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) ) )
| ~ ! [X180] :
( ~ r1(X177,X180)
| p1(X180) ) ) )
& ! [X181] :
( ~ r1(X0,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) ) )
| ~ ! [X184] :
( ~ r1(X181,X184)
| p1(X184) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ? [X33] :
( r1(X30,X33)
& ~ p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ? [X48] :
( r1(X45,X48)
& ~ p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ? [X75] :
( r1(X72,X75)
& ~ p1(X75) ) ) ) ) ) ) ) ) ) ) )
& ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ? [X87] :
( r1(X84,X87)
& ~ p1(X87) ) ) ) ) ) ) ) ) ) )
& ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( ( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ~ p1(X99) )
& p1(X98) ) )
| ? [X100] :
( r1(X95,X100)
& ? [X101] :
( r1(X100,X101)
& ~ p1(X101) )
& p1(X100)
& ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ( ? [X105] :
( r1(X102,X105)
& ~ p1(X105) )
& p1(X102) ) ) ) )
& ( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ? [X107] :
( r1(X106,X107)
& ~ p1(X107) ) )
| ? [X108] :
( r1(X95,X108)
& ~ p1(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) ) )
& ! [X111] :
( ~ r1(X95,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
| ? [X114] :
( r1(X111,X114)
& ~ p1(X114) ) )
& ( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ? [X117] :
( r1(X116,X117)
& ? [X118] :
( r1(X117,X118)
& ~ p1(X118) )
& p1(X117) ) ) )
| ? [X119] :
( r1(X95,X119)
& ~ p1(X119)
& ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) )
| ~ p1(X120) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X122] :
( r1(X0,X122)
& ? [X123] :
( r1(X122,X123)
& ? [X124] :
( r1(X123,X124)
& ? [X125] :
( r1(X124,X125)
& ? [X126] :
( r1(X125,X126)
& ? [X127] :
( r1(X126,X127)
& ? [X128] :
( r1(X127,X128)
& ? [X129] :
( r1(X128,X129)
& ? [X130] :
( r1(X129,X130)
& ~ p1(X130) )
& ? [X131] :
( r1(X129,X131)
& ! [X132] :
( ~ r1(X131,X132)
| p1(X132) ) )
& ! [X133] :
( ~ r1(X129,X133)
| p1(X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) ) ) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| p1(X153) ) )
| ? [X154] :
( r1(X151,X154)
& ~ p1(X154) ) ) ) ) ) ) )
& ! [X155] :
( ~ r1(X0,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| p1(X161) ) )
| ? [X162] :
( r1(X159,X162)
& ~ p1(X162) ) ) ) ) ) )
& ! [X163] :
( ~ r1(X0,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ? [X169] :
( r1(X166,X169)
& ~ p1(X169) ) ) ) ) )
& ! [X170] :
( ~ r1(X0,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| p1(X174) ) )
| ? [X175] :
( r1(X172,X175)
& ~ p1(X175) ) ) ) )
& ! [X176] :
( ~ r1(X0,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) ) )
| ? [X180] :
( r1(X177,X180)
& ~ p1(X180) ) ) )
& ! [X181] :
( ~ r1(X0,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) ) )
| ? [X184] :
( r1(X181,X184)
& ~ p1(X184) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ? [X33] :
( r1(X30,X33)
& ~ p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ? [X48] :
( r1(X45,X48)
& ~ p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ? [X75] :
( r1(X72,X75)
& ~ p1(X75) ) ) ) ) ) ) ) ) ) ) )
& ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ? [X87] :
( r1(X84,X87)
& ~ p1(X87) ) ) ) ) ) ) ) ) ) )
& ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( ( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ~ p1(X99) )
& p1(X98) ) )
| ? [X100] :
( r1(X95,X100)
& ? [X101] :
( r1(X100,X101)
& ~ p1(X101) )
& p1(X100)
& ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ( ? [X105] :
( r1(X102,X105)
& ~ p1(X105) )
& p1(X102) ) ) ) )
& ( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ? [X107] :
( r1(X106,X107)
& ~ p1(X107) ) )
| ? [X108] :
( r1(X95,X108)
& ~ p1(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) ) )
& ! [X111] :
( ~ r1(X95,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
| ? [X114] :
( r1(X111,X114)
& ~ p1(X114) ) )
& ( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ? [X117] :
( r1(X116,X117)
& ? [X118] :
( r1(X117,X118)
& ~ p1(X118) )
& p1(X117) ) ) )
| ? [X119] :
( r1(X95,X119)
& ~ p1(X119)
& ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) )
| ~ p1(X120) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X122] :
( r1(X0,X122)
& ? [X123] :
( r1(X122,X123)
& ? [X124] :
( r1(X123,X124)
& ? [X125] :
( r1(X124,X125)
& ? [X126] :
( r1(X125,X126)
& ? [X127] :
( r1(X126,X127)
& ? [X128] :
( r1(X127,X128)
& ? [X129] :
( r1(X128,X129)
& ? [X130] :
( r1(X129,X130)
& ~ p1(X130) )
& ? [X131] :
( r1(X129,X131)
& ! [X132] :
( ~ r1(X131,X132)
| p1(X132) ) )
& ! [X133] :
( ~ r1(X129,X133)
| p1(X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) ) ) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| p1(X153) ) )
| ? [X154] :
( r1(X151,X154)
& ~ p1(X154) ) ) ) ) ) ) )
& ! [X155] :
( ~ r1(X0,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| p1(X161) ) )
| ? [X162] :
( r1(X159,X162)
& ~ p1(X162) ) ) ) ) ) )
& ! [X163] :
( ~ r1(X0,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ? [X169] :
( r1(X166,X169)
& ~ p1(X169) ) ) ) ) )
& ! [X170] :
( ~ r1(X0,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| p1(X174) ) )
| ? [X175] :
( r1(X172,X175)
& ~ p1(X175) ) ) ) )
& ! [X176] :
( ~ r1(X0,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) ) )
| ? [X180] :
( r1(X177,X180)
& ~ p1(X180) ) ) )
& ! [X181] :
( ~ r1(X0,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) ) )
| ? [X184] :
( r1(X181,X184)
& ~ p1(X184) ) ) ),
inference(flattening,[],[f6]) ).
fof(f8,definition,
! [X95] :
( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ? [X117] :
( r1(X116,X117)
& ? [X118] :
( r1(X117,X118)
& ~ p1(X118) )
& p1(X117) ) ) )
| ~ sP0(X95) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X95] :
( ? [X100] :
( r1(X95,X100)
& ? [X101] :
( r1(X100,X101)
& ~ p1(X101) )
& p1(X100)
& ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ( ? [X105] :
( r1(X102,X105)
& ~ p1(X105) )
& p1(X102) ) ) )
| ~ sP1(X95) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X95] :
( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ? [X107] :
( r1(X106,X107)
& ~ p1(X107) ) )
| ? [X108] :
( r1(X95,X108)
& ~ p1(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) )
| ~ sP2(X95) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X95] :
( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ~ p1(X99) )
& p1(X98) ) )
| sP1(X95)
| ~ sP3(X95) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f12,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ? [X33] :
( r1(X30,X33)
& ~ p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ? [X48] :
( r1(X45,X48)
& ~ p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ? [X75] :
( r1(X72,X75)
& ~ p1(X75) ) ) ) ) ) ) ) ) ) ) )
& ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ? [X87] :
( r1(X84,X87)
& ~ p1(X87) ) ) ) ) ) ) ) ) ) )
& ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( sP3(X95)
& sP2(X95)
& ! [X111] :
( ~ r1(X95,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
| ? [X114] :
( r1(X111,X114)
& ~ p1(X114) ) )
& ( sP0(X95)
| ? [X119] :
( r1(X95,X119)
& ~ p1(X119)
& ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) )
| ~ p1(X120) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X122] :
( r1(X0,X122)
& ? [X123] :
( r1(X122,X123)
& ? [X124] :
( r1(X123,X124)
& ? [X125] :
( r1(X124,X125)
& ? [X126] :
( r1(X125,X126)
& ? [X127] :
( r1(X126,X127)
& ? [X128] :
( r1(X127,X128)
& ? [X129] :
( r1(X128,X129)
& ? [X130] :
( r1(X129,X130)
& ~ p1(X130) )
& ? [X131] :
( r1(X129,X131)
& ! [X132] :
( ~ r1(X131,X132)
| p1(X132) ) )
& ! [X133] :
( ~ r1(X129,X133)
| p1(X133)
| ? [X134] :
( r1(X133,X134)
& ? [X135] :
( r1(X134,X135)
& ~ p1(X135) )
& p1(X134) ) ) ) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| p1(X153) ) )
| ? [X154] :
( r1(X151,X154)
& ~ p1(X154) ) ) ) ) ) ) )
& ! [X155] :
( ~ r1(X0,X155)
| ! [X156] :
( ~ r1(X155,X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| ! [X161] :
( ~ r1(X160,X161)
| p1(X161) ) )
| ? [X162] :
( r1(X159,X162)
& ~ p1(X162) ) ) ) ) ) )
& ! [X163] :
( ~ r1(X0,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ! [X165] :
( ~ r1(X164,X165)
| ! [X166] :
( ~ r1(X165,X166)
| ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| p1(X168) ) )
| ? [X169] :
( r1(X166,X169)
& ~ p1(X169) ) ) ) ) )
& ! [X170] :
( ~ r1(X0,X170)
| ! [X171] :
( ~ r1(X170,X171)
| ! [X172] :
( ~ r1(X171,X172)
| ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| p1(X174) ) )
| ? [X175] :
( r1(X172,X175)
& ~ p1(X175) ) ) ) )
& ! [X176] :
( ~ r1(X0,X176)
| ! [X177] :
( ~ r1(X176,X177)
| ! [X178] :
( ~ r1(X177,X178)
| ! [X179] :
( ~ r1(X178,X179)
| p1(X179) ) )
| ? [X180] :
( r1(X177,X180)
& ~ p1(X180) ) ) )
& ! [X181] :
( ~ r1(X0,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ! [X183] :
( ~ r1(X182,X183)
| p1(X183) ) )
| ? [X184] :
( r1(X181,X184)
& ~ p1(X184) ) ) ),
inference(definition_folding,[],[f7,f11,f10,f9,f8]) ).
fof(f13,plain,
! [X95] :
( ! [X96] :
( ~ r1(X95,X96)
| p1(X96) )
| ~ p1(X95)
| ! [X97] :
( ~ r1(X95,X97)
| ? [X98] :
( r1(X97,X98)
& ? [X99] :
( r1(X98,X99)
& ~ p1(X99) )
& p1(X98) ) )
| sP1(X95)
| ~ sP3(X95) ),
inference(nnf_transformation,[],[f11]) ).
fof(f14,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(rectify,[],[f13]) ).
fof(f15,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ( r1(X2,sK4(X2))
& r1(sK4(X2),sK5(X2))
& ~ p1(sK5(X2))
& p1(sK4(X2)) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f14]) ).
fof(f16,plain,
! [X95] :
( p1(X95)
| ! [X106] :
( ~ r1(X95,X106)
| ? [X107] :
( r1(X106,X107)
& ~ p1(X107) ) )
| ? [X108] :
( r1(X95,X108)
& ~ p1(X108)
& ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| p1(X110) )
| ~ p1(X109) ) )
| ~ sP2(X95) ),
inference(nnf_transformation,[],[f10]) ).
fof(f17,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ~ p1(X2) ) )
| ? [X3] :
( r1(X0,X3)
& ~ p1(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f16]) ).
fof(f18,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK6(X1))
& ~ p1(sK6(X1)) ) )
| ( r1(X0,sK7(X0))
& ~ p1(sK7(X0))
& ! [X4] :
( ~ r1(sK7(X0),X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f17]) ).
fof(f19,plain,
! [X95] :
( ? [X100] :
( r1(X95,X100)
& ? [X101] :
( r1(X100,X101)
& ~ p1(X101) )
& p1(X100)
& ! [X102] :
( ~ r1(X100,X102)
| ! [X103] :
( ~ r1(X102,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p1(X104) )
| ~ p1(X103) )
| ( ? [X105] :
( r1(X102,X105)
& ~ p1(X105) )
& p1(X102) ) ) )
| ~ sP1(X95) ),
inference(nnf_transformation,[],[f9]) ).
fof(f20,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p1(X2) )
& p1(X1)
& ! [X3] :
( ~ r1(X1,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( ? [X6] :
( r1(X3,X6)
& ~ p1(X6) )
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f19]) ).
fof(f21,plain,
! [X0] :
( ( r1(X0,sK8(X0))
& r1(sK8(X0),sK9(X0))
& ~ p1(sK9(X0))
& p1(sK8(X0))
& ! [X3] :
( ~ r1(sK8(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( r1(X3,sK10(X3))
& ~ p1(sK10(X3))
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f20]) ).
fof(f22,plain,
! [X95] :
( ! [X115] :
( ~ r1(X95,X115)
| ! [X116] :
( ~ r1(X115,X116)
| p1(X116)
| ? [X117] :
( r1(X116,X117)
& ? [X118] :
( r1(X117,X118)
& ~ p1(X118) )
& p1(X117) ) ) )
| ~ sP0(X95) ),
inference(nnf_transformation,[],[f8]) ).
fof(f23,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f22]) ).
fof(f24,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ( r1(X2,sK11(X2))
& r1(sK11(X2),sK12(X2))
& ~ p1(sK12(X2))
& p1(sK11(X2)) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f23]) ).
fof(f25,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ? [X17] :
( r1(X14,X17)
& ~ p1(X17) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X18] :
( ~ r1(X0,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ? [X33] :
( r1(X30,X33)
& ~ p1(X33) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X34] :
( ~ r1(X0,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ? [X48] :
( r1(X45,X48)
& ~ p1(X48) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X49] :
( ~ r1(X0,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ? [X62] :
( r1(X59,X62)
& ~ p1(X62) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(X0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ? [X75] :
( r1(X72,X75)
& ~ p1(X75) ) ) ) ) ) ) ) ) ) ) )
& ! [X76] :
( ~ r1(X0,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ? [X87] :
( r1(X84,X87)
& ~ p1(X87) ) ) ) ) ) ) ) ) ) )
& ! [X88] :
( ~ r1(X0,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( sP3(X95)
& sP2(X95)
& ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| p1(X98) ) )
| ? [X99] :
( r1(X96,X99)
& ~ p1(X99) ) )
& ( sP0(X95)
| ? [X100] :
( r1(X95,X100)
& ~ p1(X100)
& ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) )
| ~ p1(X101) ) ) ) ) ) ) ) ) ) ) ) )
& ? [X103] :
( r1(X0,X103)
& ? [X104] :
( r1(X103,X104)
& ? [X105] :
( r1(X104,X105)
& ? [X106] :
( r1(X105,X106)
& ? [X107] :
( r1(X106,X107)
& ? [X108] :
( r1(X107,X108)
& ? [X109] :
( r1(X108,X109)
& ? [X110] :
( r1(X109,X110)
& ? [X111] :
( r1(X110,X111)
& ~ p1(X111) )
& ? [X112] :
( r1(X110,X112)
& ! [X113] :
( ~ r1(X112,X113)
| p1(X113) ) )
& ! [X114] :
( ~ r1(X110,X114)
| p1(X114)
| ? [X115] :
( r1(X114,X115)
& ? [X116] :
( r1(X115,X116)
& ~ p1(X116) )
& p1(X115) ) ) ) ) ) ) ) ) ) )
& ! [X117] :
( ~ r1(X0,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ? [X126] :
( r1(X123,X126)
& ~ p1(X126) ) ) ) ) ) ) ) )
& ! [X127] :
( ~ r1(X0,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ! [X134] :
( ~ r1(X133,X134)
| p1(X134) ) )
| ? [X135] :
( r1(X132,X135)
& ~ p1(X135) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(X0,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p1(X142) ) )
| ? [X143] :
( r1(X140,X143)
& ~ p1(X143) ) ) ) ) ) )
& ! [X144] :
( ~ r1(X0,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ? [X150] :
( r1(X147,X150)
& ~ p1(X150) ) ) ) ) )
& ! [X151] :
( ~ r1(X0,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ! [X155] :
( ~ r1(X154,X155)
| p1(X155) ) )
| ? [X156] :
( r1(X153,X156)
& ~ p1(X156) ) ) ) )
& ! [X157] :
( ~ r1(X0,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| p1(X160) ) )
| ? [X161] :
( r1(X158,X161)
& ~ p1(X161) ) ) )
& ! [X162] :
( ~ r1(X0,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| p1(X164) ) )
| ? [X165] :
( r1(X162,X165)
& ~ p1(X165) ) ) ),
inference(rectify,[],[f12]) ).
fof(f26,plain,
( ! [X1] :
( ~ r1(sK13,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p1(X16) ) )
| ( r1(X14,sK14(X14))
& ~ p1(sK14(X14)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X18] :
( ~ r1(sK13,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ! [X32] :
( ~ r1(X31,X32)
| p1(X32) ) )
| ( r1(X30,sK15(X30))
& ~ p1(sK15(X30)) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X34] :
( ~ r1(sK13,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) ) )
| ( r1(X45,sK16(X45))
& ~ p1(sK16(X45)) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X49] :
( ~ r1(sK13,X49)
| ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) ) )
| ( r1(X59,sK17(X59))
& ~ p1(sK17(X59)) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(sK13,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| ! [X67] :
( ~ r1(X66,X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ! [X70] :
( ~ r1(X69,X70)
| ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ! [X74] :
( ~ r1(X73,X74)
| p1(X74) ) )
| ( r1(X72,sK18(X72))
& ~ p1(sK18(X72)) ) ) ) ) ) ) ) ) ) ) )
& ! [X76] :
( ~ r1(sK13,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ! [X84] :
( ~ r1(X83,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) ) )
| ( r1(X84,sK19(X84))
& ~ p1(sK19(X84)) ) ) ) ) ) ) ) ) ) )
& ! [X88] :
( ~ r1(sK13,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( sP3(X95)
& sP2(X95)
& ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| p1(X98) ) )
| ( r1(X96,sK20(X96))
& ~ p1(sK20(X96)) ) )
& ( sP0(X95)
| ( r1(X95,sK21(X95))
& ~ p1(sK21(X95))
& ! [X101] :
( ~ r1(sK21(X95),X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) )
| ~ p1(X101) ) ) ) ) ) ) ) ) ) ) ) )
& r1(sK13,sK22)
& r1(sK22,sK23)
& r1(sK23,sK24)
& r1(sK24,sK25)
& r1(sK25,sK26)
& r1(sK26,sK27)
& r1(sK27,sK28)
& r1(sK28,sK29)
& r1(sK29,sK30)
& ~ p1(sK30)
& r1(sK29,sK31)
& ! [X113] :
( ~ r1(sK31,X113)
| p1(X113) )
& ! [X114] :
( ~ r1(sK29,X114)
| p1(X114)
| ( r1(X114,sK32(X114))
& r1(sK32(X114),sK33(X114))
& ~ p1(sK33(X114))
& p1(sK32(X114)) ) )
& ! [X117] :
( ~ r1(sK13,X117)
| ! [X118] :
( ~ r1(X117,X118)
| ! [X119] :
( ~ r1(X118,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| ! [X123] :
( ~ r1(X122,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ( r1(X123,sK34(X123))
& ~ p1(sK34(X123)) ) ) ) ) ) ) ) )
& ! [X127] :
( ~ r1(sK13,X127)
| ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| ! [X134] :
( ~ r1(X133,X134)
| p1(X134) ) )
| ( r1(X132,sK35(X132))
& ~ p1(sK35(X132)) ) ) ) ) ) ) )
& ! [X136] :
( ~ r1(sK13,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ! [X138] :
( ~ r1(X137,X138)
| ! [X139] :
( ~ r1(X138,X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p1(X142) ) )
| ( r1(X140,sK36(X140))
& ~ p1(sK36(X140)) ) ) ) ) ) )
& ! [X144] :
( ~ r1(sK13,X144)
| ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ! [X149] :
( ~ r1(X148,X149)
| p1(X149) ) )
| ( r1(X147,sK37(X147))
& ~ p1(sK37(X147)) ) ) ) ) )
& ! [X151] :
( ~ r1(sK13,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| ! [X155] :
( ~ r1(X154,X155)
| p1(X155) ) )
| ( r1(X153,sK38(X153))
& ~ p1(sK38(X153)) ) ) ) )
& ! [X157] :
( ~ r1(sK13,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ! [X160] :
( ~ r1(X159,X160)
| p1(X160) ) )
| ( r1(X158,sK39(X158))
& ~ p1(sK39(X158)) ) ) )
& ! [X162] :
( ~ r1(sK13,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| p1(X164) ) )
| ( r1(X162,sK40(X162))
& ~ p1(sK40(X162)) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40]),skolemize(X0,sK13),skolemize(X17,sK14(X14)),skolemize(X33,sK15(X30)),skolemize(X48,sK16(X45)),skolemize(X62,sK17(X59)),skolemize(X75,sK18(X72)),skolemize(X87,sK19(X84)),skolemize(X99,sK20(X96)),skolemize(X100,sK21(X95)),skolemize(X103,sK22),skolemize(X104,sK23),skolemize(X105,sK24),skolemize(X106,sK25),skolemize(X107,sK26),skolemize(X108,sK27),skolemize(X109,sK28),skolemize(X110,sK29),skolemize(X111,sK30),skolemize(X112,sK31),skolemize(X115,sK32(X114)),skolemize(X116,sK33(X114)),skolemize(X126,sK34(X123)),skolemize(X135,sK35(X132)),skolemize(X143,sK36(X140)),skolemize(X150,sK37(X147)),skolemize(X156,sK38(X153)),skolemize(X161,sK39(X158)),skolemize(X165,sK40(X162))],[f25]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ p1(sK5(X2))
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1)
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f30,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(sK4(X2),sK5(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f31,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(X2,sK4(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f32,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f33,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f34,plain,
! [X0,X1] :
( ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f35,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f36,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f37,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f18]) ).
fof(f38,plain,
! [X3,X0,X4,X5] :
( ~ r1(sK8(X0),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f42,plain,
! [X0] :
( ~ p1(sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f43,plain,
! [X0] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f44,plain,
! [X0] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f21]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| p1(sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ p1(sK12(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f47,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f24]) ).
fof(f63,plain,
! [X114] :
( ~ r1(sK29,X114)
| p1(X114)
| p1(sK32(X114)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f64,plain,
! [X114] :
( ~ p1(sK33(X114))
| p1(X114)
| ~ r1(sK29,X114) ),
inference(cnf_transformation,[],[f26]) ).
fof(f65,plain,
! [X114] :
( r1(sK32(X114),sK33(X114))
| p1(X114)
| ~ r1(sK29,X114) ),
inference(cnf_transformation,[],[f26]) ).
fof(f66,plain,
! [X114] :
( r1(X114,sK32(X114))
| p1(X114)
| ~ r1(sK29,X114) ),
inference(cnf_transformation,[],[f26]) ).
fof(f67,plain,
! [X113] :
( ~ r1(sK31,X113)
| p1(X113) ),
inference(cnf_transformation,[],[f26]) ).
fof(f68,plain,
r1(sK29,sK31),
inference(cnf_transformation,[],[f26]) ).
fof(f69,plain,
~ p1(sK30),
inference(cnf_transformation,[],[f26]) ).
fof(f70,plain,
r1(sK29,sK30),
inference(cnf_transformation,[],[f26]) ).
fof(f71,plain,
r1(sK28,sK29),
inference(cnf_transformation,[],[f26]) ).
fof(f72,plain,
r1(sK27,sK28),
inference(cnf_transformation,[],[f26]) ).
fof(f73,plain,
r1(sK26,sK27),
inference(cnf_transformation,[],[f26]) ).
fof(f74,plain,
r1(sK25,sK26),
inference(cnf_transformation,[],[f26]) ).
fof(f75,plain,
r1(sK24,sK25),
inference(cnf_transformation,[],[f26]) ).
fof(f76,plain,
r1(sK23,sK24),
inference(cnf_transformation,[],[f26]) ).
fof(f77,plain,
r1(sK22,sK23),
inference(cnf_transformation,[],[f26]) ).
fof(f78,plain,
r1(sK13,sK22),
inference(cnf_transformation,[],[f26]) ).
fof(f79,plain,
! [X101,X90,X91,X88,X89,X94,X95,X102,X92,X93] :
( ~ r1(sK21(X95),X101)
| ~ r1(X88,X89)
| ~ r1(X89,X90)
| ~ r1(X90,X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(X93,X94)
| ~ r1(X94,X95)
| sP0(X95)
| ~ r1(sK13,X88)
| ~ r1(X101,X102)
| p1(X102)
| ~ p1(X101) ),
inference(cnf_transformation,[],[f26]) ).
fof(f80,plain,
! [X90,X91,X88,X89,X94,X95,X92,X93] :
( ~ p1(sK21(X95))
| ~ r1(X88,X89)
| ~ r1(X89,X90)
| ~ r1(X90,X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(X93,X94)
| ~ r1(X94,X95)
| sP0(X95)
| ~ r1(sK13,X88) ),
inference(cnf_transformation,[],[f26]) ).
fof(f81,plain,
! [X90,X91,X88,X89,X94,X95,X92,X93] :
( ~ r1(sK13,X88)
| ~ r1(X88,X89)
| ~ r1(X89,X90)
| ~ r1(X90,X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(X93,X94)
| ~ r1(X94,X95)
| sP0(X95)
| r1(X95,sK21(X95)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f84,plain,
! [X90,X91,X88,X89,X94,X95,X92,X93] :
( ~ r1(sK13,X88)
| ~ r1(X88,X89)
| ~ r1(X89,X90)
| ~ r1(X90,X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(X93,X94)
| ~ r1(X94,X95)
| sP2(X95) ),
inference(cnf_transformation,[],[f26]) ).
fof(f85,plain,
! [X90,X91,X88,X89,X94,X95,X92,X93] :
( ~ r1(sK13,X88)
| ~ r1(X88,X89)
| ~ r1(X89,X90)
| ~ r1(X90,X91)
| ~ r1(X91,X92)
| ~ r1(X92,X93)
| ~ r1(X93,X94)
| ~ r1(X94,X95)
| sP3(X95) ),
inference(cnf_transformation,[],[f26]) ).
fof(f86,plain,
! [X82,X83,X80,X78,X81,X79,X86,X76,X77,X84,X85] :
( ~ p1(sK19(X84))
| ~ r1(X76,X77)
| ~ r1(X77,X78)
| ~ r1(X78,X79)
| ~ r1(X79,X80)
| ~ r1(X80,X81)
| ~ r1(X81,X82)
| ~ r1(X82,X83)
| ~ r1(X83,X84)
| ~ r1(X84,X85)
| ~ r1(X85,X86)
| p1(X86)
| ~ r1(sK13,X76) ),
inference(cnf_transformation,[],[f26]) ).
fof(f87,plain,
! [X82,X83,X80,X78,X81,X79,X86,X76,X77,X84,X85] :
( ~ r1(sK13,X76)
| ~ r1(X76,X77)
| ~ r1(X77,X78)
| ~ r1(X78,X79)
| ~ r1(X79,X80)
| ~ r1(X80,X81)
| ~ r1(X81,X82)
| ~ r1(X82,X83)
| ~ r1(X83,X84)
| ~ r1(X84,X85)
| ~ r1(X85,X86)
| p1(X86)
| r1(X84,sK19(X84)) ),
inference(cnf_transformation,[],[f26]) ).
fof(f106,plain,
( p1(sK29)
| r1(sK31,sK6(sK31))
| r1(sK29,sK7(sK29))
| ~ sP2(sK29) ),
inference(resolution,[],[f37,f68]) ).
fof(f109,definition,
( spl41_1
<=> sP2(sK29) ),
introduced(definition,[new_symbols(definition,[spl41_1])],[avatar_definition]) ).
fof(f110,plain,
( sP2(sK29)
| ~ spl41_1 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f111,plain,
( ~ sP2(sK29)
| spl41_1 ),
inference(avatar_component_clause,[],[f109]) ).
fof(f113,definition,
( spl41_2
<=> r1(sK29,sK7(sK29)) ),
introduced(definition,[new_symbols(definition,[spl41_2])],[avatar_definition]) ).
fof(f114,plain,
( ~ r1(sK29,sK7(sK29))
| spl41_2 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f115,plain,
( r1(sK29,sK7(sK29))
| ~ spl41_2 ),
inference(avatar_component_clause,[],[f113]) ).
fof(f121,definition,
( spl41_4
<=> p1(sK29) ),
introduced(definition,[new_symbols(definition,[spl41_4])],[avatar_definition]) ).
fof(f122,plain,
( ~ p1(sK29)
| spl41_4 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f123,plain,
( p1(sK29)
| ~ spl41_4 ),
inference(avatar_component_clause,[],[f121]) ).
fof(f126,definition,
( spl41_5
<=> r1(sK31,sK6(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_5])],[avatar_definition]) ).
fof(f128,plain,
( r1(sK31,sK6(sK31))
| ~ spl41_5 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f129,plain,
( ~ spl41_1
| spl41_2
| spl41_5
| spl41_4 ),
inference(avatar_split_clause,[],[f106,f121,f126,f113,f109]) ).
fof(f384,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f43,f45]) ).
fof(f385,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f43,f47]) ).
fof(f386,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f43,f48]) ).
fof(f388,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f386,f42]) ).
fof(f389,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f385,f42]) ).
fof(f390,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f384,f42]) ).
fof(f401,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f38,f43]) ).
fof(f404,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| p1(sK9(X0))
| ~ sP1(X0) ),
inference(duplicate_literal_removal,[],[f401]) ).
fof(f405,plain,
! [X2,X0,X1] :
( ~ r1(sK9(X0),X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ p1(X1)
| ~ sP1(X0) ),
inference(forward_subsumption_resolution,[],[f404,f42]) ).
fof(f421,plain,
! [X0] :
( p1(X0)
| ~ p1(sK29)
| ~ r1(sK29,X0)
| r1(sK31,sK4(sK31))
| sP1(sK29)
| ~ sP3(sK29) ),
inference(resolution,[],[f31,f68]) ).
fof(f424,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| r1(sK31,sK4(sK31))
| sP1(sK29)
| ~ sP3(sK29) )
| ~ spl41_4 ),
inference(forward_subsumption_resolution,[],[f421,f123]) ).
fof(f450,definition,
( spl41_62
<=> sP3(sK29) ),
introduced(definition,[new_symbols(definition,[spl41_62])],[avatar_definition]) ).
fof(f451,plain,
( sP3(sK29)
| ~ spl41_62 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f452,plain,
( ~ sP3(sK29)
| spl41_62 ),
inference(avatar_component_clause,[],[f450]) ).
fof(f454,definition,
( spl41_63
<=> sP1(sK29) ),
introduced(definition,[new_symbols(definition,[spl41_63])],[avatar_definition]) ).
fof(f455,plain,
( ~ sP1(sK29)
| spl41_63 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f456,plain,
( sP1(sK29)
| ~ spl41_63 ),
inference(avatar_component_clause,[],[f454]) ).
fof(f462,definition,
( spl41_65
<=> ! [X0] :
( p1(X0)
| ~ r1(sK29,X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_65])],[avatar_definition]) ).
fof(f463,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| p1(X0) )
| ~ spl41_65 ),
inference(avatar_component_clause,[],[f462]) ).
fof(f466,definition,
( spl41_66
<=> r1(sK31,sK4(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_66])],[avatar_definition]) ).
fof(f468,plain,
( r1(sK31,sK4(sK31))
| ~ spl41_66 ),
inference(avatar_component_clause,[],[f466]) ).
fof(f469,plain,
( ~ spl41_62
| spl41_63
| spl41_66
| spl41_65
| ~ spl41_4 ),
inference(avatar_split_clause,[],[f424,f121,f462,f466,f454,f450]) ).
fof(f597,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP3(X6) ),
inference(resolution,[],[f85,f78]) ).
fof(f621,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK32(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK32(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK29,sK7(X0)) ),
inference(resolution,[],[f35,f66]) ).
fof(f624,plain,
! [X2,X0,X1] :
( ~ r1(sK32(sK7(X0)),X2)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK32(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK29,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f621,f36]) ).
fof(f625,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP2(X6) ),
inference(resolution,[],[f84,f78]) ).
fof(f641,plain,
! [X0] :
( p1(X0)
| ~ p1(sK29)
| ~ r1(sK29,X0)
| r1(sK4(sK31),sK5(sK31))
| sP1(sK29)
| ~ sP3(sK29) ),
inference(resolution,[],[f30,f68]) ).
fof(f655,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f389,f44]) ).
fof(f657,plain,
! [X0] :
( r1(sK11(sK9(X0)),sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f655]) ).
fof(f665,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(sK32(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK32(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK29,sK7(X0)) ),
inference(resolution,[],[f32,f66]) ).
fof(f668,plain,
! [X2,X0,X1] :
( ~ r1(sK32(sK7(X0)),X2)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK32(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK29,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f665,f33]) ).
fof(f669,plain,
! [X0] :
( ~ sP1(X0)
| p1(sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f390,f44]) ).
fof(f671,plain,
! [X0] :
( p1(sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f669]) ).
fof(f672,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f388,f44]) ).
fof(f674,plain,
! [X0] :
( r1(sK9(X0),sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f672]) ).
fof(f675,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0)))
| ~ sP1(X0) ),
inference(resolution,[],[f674,f405]) ).
fof(f682,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(sK11(sK9(X0)),X1)
| p1(X1)
| ~ p1(sK11(sK9(X0))) ),
inference(duplicate_literal_removal,[],[f675]) ).
fof(f684,plain,
! [X0,X1] :
( ~ r1(sK11(sK9(X0)),X1)
| ~ sP0(X0)
| ~ sP1(X0)
| p1(X1) ),
inference(forward_subsumption_resolution,[],[f682,f671]) ).
fof(f685,plain,
! [X0] :
( ~ sP0(X0)
| ~ sP1(X0)
| p1(sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(resolution,[],[f684,f657]) ).
fof(f689,plain,
! [X0] :
( p1(sK12(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f685]) ).
fof(f690,plain,
! [X2,X0,X1] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ r1(X1,sK9(X0))
| p1(sK9(X0))
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(resolution,[],[f689,f46]) ).
fof(f691,plain,
! [X2,X0,X1] :
( ~ r1(X1,sK9(X0))
| ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X2,X1)
| ~ sP0(X2) ),
inference(forward_subsumption_resolution,[],[f690,f42]) ).
fof(f693,plain,
! [X0,X1] :
( ~ sP0(X0)
| ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| ~ sP0(X1)
| ~ sP1(X0) ),
inference(resolution,[],[f691,f43]) ).
fof(f694,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X1) ),
inference(duplicate_literal_removal,[],[f693]) ).
fof(f695,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0)
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f694,f44]) ).
fof(f697,plain,
! [X0] :
( ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f695]) ).
fof(f698,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| ~ p1(sK32(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK29,sK7(X1)) ),
inference(resolution,[],[f668,f65]) ).
fof(f702,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| ~ p1(sK32(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f698]) ).
fof(f703,plain,
! [X0,X1] :
( ~ p1(sK32(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| ~ p1(sK6(X0))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f702,f33]) ).
fof(f730,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP3(X5) ),
inference(resolution,[],[f597,f77]) ).
fof(f738,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP3(X4) ),
inference(resolution,[],[f730,f76]) ).
fof(f746,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP3(X3) ),
inference(resolution,[],[f738,f75]) ).
fof(f754,plain,
! [X2,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP3(X2) ),
inference(resolution,[],[f746,f74]) ).
fof(f762,plain,
! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| sP3(X1) ),
inference(resolution,[],[f754,f73]) ).
fof(f770,plain,
! [X0] :
( ~ r1(sK28,X0)
| sP3(X0) ),
inference(resolution,[],[f762,f72]) ).
fof(f778,plain,
sP3(sK29),
inference(resolution,[],[f770,f71]) ).
fof(f789,plain,
( $false
| spl41_62 ),
inference(forward_subsumption_resolution,[],[f778,f452]) ).
fof(f790,plain,
spl41_62,
inference(avatar_contradiction_clause,[],[f789]) ).
fof(f845,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP2(X5) ),
inference(resolution,[],[f625,f77]) ).
fof(f849,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP2(X4) ),
inference(resolution,[],[f845,f76]) ).
fof(f853,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP2(X3) ),
inference(resolution,[],[f849,f75]) ).
fof(f857,plain,
! [X2,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP2(X2) ),
inference(resolution,[],[f853,f74]) ).
fof(f861,plain,
! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| sP2(X1) ),
inference(resolution,[],[f857,f73]) ).
fof(f865,plain,
! [X0] :
( ~ r1(sK28,X0)
| sP2(X0) ),
inference(resolution,[],[f861,f72]) ).
fof(f869,plain,
sP2(sK29),
inference(resolution,[],[f865,f71]) ).
fof(f875,plain,
( $false
| spl41_1 ),
inference(forward_subsumption_resolution,[],[f869,f111]) ).
fof(f876,plain,
spl41_1,
inference(avatar_contradiction_clause,[],[f875]) ).
fof(f929,plain,
( p1(sK6(sK31))
| ~ spl41_5 ),
inference(resolution,[],[f128,f67]) ).
fof(f942,definition,
( spl41_121
<=> p1(sK6(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_121])],[avatar_definition]) ).
fof(f944,plain,
( p1(sK6(sK31))
| ~ spl41_121 ),
inference(avatar_component_clause,[],[f942]) ).
fof(f959,plain,
( spl41_121
| ~ spl41_5 ),
inference(avatar_split_clause,[],[f929,f126,f942]) ).
fof(f960,plain,
( ~ sP0(sK29)
| ~ spl41_63 ),
inference(resolution,[],[f456,f697]) ).
fof(f961,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| ~ p1(sK32(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK29,sK7(X1)) ),
inference(resolution,[],[f624,f65]) ).
fof(f965,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| ~ p1(sK32(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f961]) ).
fof(f966,plain,
! [X0,X1] :
( ~ p1(sK32(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK33(sK7(X1)))
| r1(X0,sK6(X0))
| ~ sP2(X1)
| ~ r1(sK29,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f965,f36]) ).
fof(f967,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| r1(X6,sK21(X6)) ),
inference(resolution,[],[f81,f78]) ).
fof(f991,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK22,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| p1(X9)
| r1(X7,sK19(X7)) ),
inference(resolution,[],[f87,f78]) ).
fof(f1126,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP0(X7)
| ~ r1(sK13,X0)
| ~ r1(sK32(sK21(X7)),X8)
| p1(X8)
| ~ p1(sK32(sK21(X7)))
| p1(sK21(X7))
| ~ r1(sK29,sK21(X7)) ),
inference(resolution,[],[f79,f66]) ).
fof(f1129,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK32(sK21(X7)),X8)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| sP0(X7)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(X8)
| ~ p1(sK32(sK21(X7)))
| ~ r1(sK29,sK21(X7)) ),
inference(forward_subsumption_resolution,[],[f1126,f80]) ).
fof(f1130,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK33(sK21(X6)))
| ~ p1(sK32(sK21(X6)))
| ~ r1(sK29,sK21(X6))
| p1(sK21(X6))
| ~ r1(sK29,sK21(X6)) ),
inference(resolution,[],[f1129,f65]) ).
fof(f1134,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK33(sK21(X6)))
| ~ p1(sK32(sK21(X6)))
| ~ r1(sK29,sK21(X6))
| p1(sK21(X6)) ),
inference(duplicate_literal_removal,[],[f1130]) ).
fof(f1135,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ p1(sK32(sK21(X6)))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| sP0(X6)
| ~ r1(sK13,X7)
| ~ r1(X7,X0)
| p1(sK33(sK21(X6)))
| ~ r1(X0,X1)
| ~ r1(sK29,sK21(X6)) ),
inference(forward_subsumption_resolution,[],[f1134,f80]) ).
fof(f1190,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| r1(X5,sK21(X5)) ),
inference(resolution,[],[f967,f77]) ).
fof(f1194,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| r1(X4,sK21(X4)) ),
inference(resolution,[],[f1190,f76]) ).
fof(f1198,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP0(X3)
| r1(X3,sK21(X3)) ),
inference(resolution,[],[f1194,f75]) ).
fof(f1202,plain,
! [X2,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP0(X2)
| r1(X2,sK21(X2)) ),
inference(resolution,[],[f1198,f74]) ).
fof(f1206,plain,
! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| sP0(X1)
| r1(X1,sK21(X1)) ),
inference(resolution,[],[f1202,f73]) ).
fof(f1210,plain,
! [X0] :
( r1(X0,sK21(X0))
| sP0(X0)
| ~ r1(sK28,X0) ),
inference(resolution,[],[f1206,f72]) ).
fof(f1279,plain,
( sP0(sK29)
| ~ r1(sK28,sK29)
| p1(sK21(sK29))
| p1(sK32(sK21(sK29))) ),
inference(resolution,[],[f1210,f63]) ).
fof(f1610,definition,
( spl41_213
<=> p1(sK32(sK21(sK29))) ),
introduced(definition,[new_symbols(definition,[spl41_213])],[avatar_definition]) ).
fof(f1612,plain,
( p1(sK32(sK21(sK29)))
| ~ spl41_213 ),
inference(avatar_component_clause,[],[f1610]) ).
fof(f1614,definition,
( spl41_214
<=> p1(sK21(sK29)) ),
introduced(definition,[new_symbols(definition,[spl41_214])],[avatar_definition]) ).
fof(f1616,plain,
( p1(sK21(sK29))
| ~ spl41_214 ),
inference(avatar_component_clause,[],[f1614]) ).
fof(f1618,plain,
( sP0(sK29)
| p1(sK21(sK29))
| p1(sK32(sK21(sK29))) ),
inference(forward_subsumption_resolution,[],[f1279,f71]) ).
fof(f1622,definition,
( spl41_215
<=> sP0(sK29) ),
introduced(definition,[new_symbols(definition,[spl41_215])],[avatar_definition]) ).
fof(f1623,plain,
( ~ sP0(sK29)
| spl41_215 ),
inference(avatar_component_clause,[],[f1622]) ).
fof(f1624,plain,
( sP0(sK29)
| ~ spl41_215 ),
inference(avatar_component_clause,[],[f1622]) ).
fof(f1625,plain,
( spl41_213
| spl41_214
| spl41_215 ),
inference(avatar_split_clause,[],[f1618,f1622,f1614,f1610]) ).
fof(f1635,plain,
( p1(sK30)
| ~ spl41_65 ),
inference(resolution,[],[f463,f70]) ).
fof(f1640,plain,
( $false
| ~ spl41_65 ),
inference(forward_subsumption_resolution,[],[f1635,f69]) ).
fof(f1641,plain,
~ spl41_65,
inference(avatar_contradiction_clause,[],[f1640]) ).
fof(f1643,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| r1(sK4(sK31),sK5(sK31))
| sP1(sK29)
| ~ sP3(sK29) )
| ~ spl41_4 ),
inference(forward_subsumption_resolution,[],[f641,f123]) ).
fof(f1647,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| r1(sK4(sK31),sK5(sK31))
| ~ sP3(sK29) )
| ~ spl41_4
| spl41_63 ),
inference(forward_subsumption_resolution,[],[f1643,f455]) ).
fof(f1651,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| r1(sK4(sK31),sK5(sK31)) )
| ~ spl41_4
| ~ spl41_62
| spl41_63 ),
inference(forward_subsumption_resolution,[],[f1647,f451]) ).
fof(f1660,definition,
( spl41_219
<=> r1(sK4(sK31),sK5(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_219])],[avatar_definition]) ).
fof(f1662,plain,
( r1(sK4(sK31),sK5(sK31))
| ~ spl41_219 ),
inference(avatar_component_clause,[],[f1660]) ).
fof(f1663,plain,
( spl41_219
| spl41_65
| ~ spl41_4
| ~ spl41_62
| spl41_63 ),
inference(avatar_split_clause,[],[f1651,f454,f450,f121,f462,f1660]) ).
fof(f1861,definition,
( spl41_232
<=> p1(sK32(sK7(sK29))) ),
introduced(definition,[new_symbols(definition,[spl41_232])],[avatar_definition]) ).
fof(f1862,plain,
( ~ p1(sK32(sK7(sK29)))
| spl41_232 ),
inference(avatar_component_clause,[],[f1861]) ).
fof(f1863,plain,
( p1(sK32(sK7(sK29)))
| ~ spl41_232 ),
inference(avatar_component_clause,[],[f1861]) ).
fof(f1865,definition,
( spl41_233
<=> p1(sK7(sK29)) ),
introduced(definition,[new_symbols(definition,[spl41_233])],[avatar_definition]) ).
fof(f1866,plain,
( ~ p1(sK7(sK29))
| spl41_233 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1867,plain,
( p1(sK7(sK29))
| ~ spl41_233 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1970,plain,
( $false
| ~ spl41_63
| ~ spl41_215 ),
inference(forward_subsumption_resolution,[],[f960,f1624]) ).
fof(f1971,plain,
( ~ spl41_63
| ~ spl41_215 ),
inference(avatar_contradiction_clause,[],[f1970]) ).
fof(f1975,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK29)
| sP0(sK29)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK33(sK21(sK29)))
| ~ r1(X6,X0)
| ~ r1(sK29,sK21(sK29)) )
| ~ spl41_213 ),
inference(resolution,[],[f1612,f1135]) ).
fof(f1976,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK29)
| sP0(sK29)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK33(sK21(sK29)))
| ~ r1(X6,X0) )
| ~ spl41_213 ),
inference(forward_subsumption_resolution,[],[f1975,f81]) ).
fof(f1977,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK29)
| ~ r1(sK13,X5)
| ~ r1(X5,X6)
| p1(sK33(sK21(sK29)))
| ~ r1(X6,X0) )
| ~ spl41_213
| spl41_215 ),
inference(forward_subsumption_resolution,[],[f1976,f1623]) ).
fof(f1979,definition,
( spl41_235
<=> p1(sK33(sK21(sK29))) ),
introduced(definition,[new_symbols(definition,[spl41_235])],[avatar_definition]) ).
fof(f1981,plain,
( p1(sK33(sK21(sK29)))
| ~ spl41_235 ),
inference(avatar_component_clause,[],[f1979]) ).
fof(f1983,definition,
( spl41_236
<=> ! [X2,X6,X4,X3,X0,X5,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X5)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,sK29)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl41_236])],[avatar_definition]) ).
fof(f1984,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK13,X5)
| ~ r1(X0,X1)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,sK29)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl41_236 ),
inference(avatar_component_clause,[],[f1983]) ).
fof(f1985,plain,
( spl41_235
| spl41_236
| ~ spl41_213
| spl41_215 ),
inference(avatar_split_clause,[],[f1977,f1622,f1610,f1983,f1979]) ).
fof(f1986,plain,
( p1(sK21(sK29))
| ~ r1(sK29,sK21(sK29))
| ~ spl41_235 ),
inference(resolution,[],[f1981,f64]) ).
fof(f1988,definition,
( spl41_237
<=> r1(sK29,sK21(sK29)) ),
introduced(definition,[new_symbols(definition,[spl41_237])],[avatar_definition]) ).
fof(f1990,plain,
( ~ r1(sK29,sK21(sK29))
| spl41_237 ),
inference(avatar_component_clause,[],[f1988]) ).
fof(f1991,plain,
( ~ spl41_237
| spl41_214
| ~ spl41_235 ),
inference(avatar_split_clause,[],[f1986,f1979,f1614,f1988]) ).
fof(f1992,plain,
( sP0(sK29)
| ~ r1(sK28,sK29)
| spl41_237 ),
inference(resolution,[],[f1990,f1210]) ).
fof(f1993,plain,
( ~ r1(sK28,sK29)
| spl41_215
| spl41_237 ),
inference(forward_subsumption_resolution,[],[f1992,f1623]) ).
fof(f1994,plain,
( $false
| spl41_215
| spl41_237 ),
inference(forward_subsumption_resolution,[],[f1993,f71]) ).
fof(f1995,plain,
( spl41_215
| spl41_237 ),
inference(avatar_contradiction_clause,[],[f1994]) ).
fof(f1996,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK22,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X3,sK29)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X1,X5) )
| ~ spl41_236 ),
inference(resolution,[],[f1984,f78]) ).
fof(f2001,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK29)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X1,X4) )
| ~ spl41_236 ),
inference(resolution,[],[f1996,f77]) ).
fof(f2006,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK24,X0)
| ~ r1(X1,sK29)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X0,X3) )
| ~ spl41_236 ),
inference(resolution,[],[f2001,f76]) ).
fof(f2011,plain,
( ! [X2,X0,X1] :
( ~ r1(sK25,X2)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X0,sK29) )
| ~ spl41_236 ),
inference(resolution,[],[f2006,f75]) ).
fof(f2016,plain,
( ! [X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK29) )
| ~ spl41_236 ),
inference(resolution,[],[f2011,f74]) ).
fof(f2021,plain,
( ! [X0] :
( ~ r1(sK27,X0)
| ~ r1(X0,sK29) )
| ~ spl41_236 ),
inference(resolution,[],[f2016,f73]) ).
fof(f2026,plain,
( ~ r1(sK28,sK29)
| ~ spl41_236 ),
inference(resolution,[],[f2021,f72]) ).
fof(f2031,plain,
( $false
| ~ spl41_236 ),
inference(forward_subsumption_resolution,[],[f2026,f71]) ).
fof(f2032,plain,
~ spl41_236,
inference(avatar_contradiction_clause,[],[f2031]) ).
fof(f2043,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,sK29)
| sP0(sK29)
| ~ r1(sK13,X0) )
| ~ spl41_214 ),
inference(resolution,[],[f1616,f80]) ).
fof(f2044,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,sK29)
| ~ r1(sK13,X0) )
| ~ spl41_214
| spl41_215 ),
inference(forward_subsumption_resolution,[],[f2043,f1623]) ).
fof(f2045,plain,
( spl41_236
| ~ spl41_214
| spl41_215 ),
inference(avatar_split_clause,[],[f2044,f1622,f1614,f1983]) ).
fof(f2092,definition,
( spl41_242
<=> p1(sK5(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_242])],[avatar_definition]) ).
fof(f2093,plain,
( ~ p1(sK5(sK31))
| spl41_242 ),
inference(avatar_component_clause,[],[f2092]) ).
fof(f2094,plain,
( p1(sK5(sK31))
| ~ spl41_242 ),
inference(avatar_component_clause,[],[f2092]) ).
fof(f2125,definition,
( spl41_249
<=> ! [X0] :
( p1(X0)
| ~ r1(sK4(sK31),X0) ) ),
introduced(definition,[new_symbols(definition,[spl41_249])],[avatar_definition]) ).
fof(f2126,plain,
( ! [X0] :
( ~ r1(sK4(sK31),X0)
| p1(X0) )
| ~ spl41_249 ),
inference(avatar_component_clause,[],[f2125]) ).
fof(f2197,plain,
( ! [X0,X1] :
( ~ r1(X1,sK31)
| ~ p1(X1)
| p1(X0)
| ~ r1(X1,X0)
| sP1(X1)
| ~ sP3(X1) )
| ~ spl41_242 ),
inference(resolution,[],[f2094,f29]) ).
fof(f2757,definition,
( spl41_317
<=> ! [X0,X1] :
( ~ r1(sK31,X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl41_317])],[avatar_definition]) ).
fof(f2758,plain,
( ! [X0,X1] :
( ~ r1(sK31,X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl41_317 ),
inference(avatar_component_clause,[],[f2757]) ).
fof(f2854,plain,
( ! [X0] :
( ~ p1(sK29)
| p1(X0)
| ~ r1(sK29,X0)
| sP1(sK29)
| ~ sP3(sK29) )
| ~ spl41_242 ),
inference(resolution,[],[f2197,f68]) ).
fof(f2855,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| sP1(sK29)
| ~ sP3(sK29) )
| ~ spl41_4
| ~ spl41_242 ),
inference(forward_subsumption_resolution,[],[f2854,f123]) ).
fof(f2856,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0)
| ~ sP3(sK29) )
| ~ spl41_4
| spl41_63
| ~ spl41_242 ),
inference(forward_subsumption_resolution,[],[f2855,f455]) ).
fof(f2857,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK29,X0) )
| ~ spl41_4
| ~ spl41_62
| spl41_63
| ~ spl41_242 ),
inference(forward_subsumption_resolution,[],[f2856,f451]) ).
fof(f2858,plain,
( spl41_65
| ~ spl41_4
| ~ spl41_62
| spl41_63
| ~ spl41_242 ),
inference(avatar_split_clause,[],[f2857,f2092,f454,f450,f121,f462]) ).
fof(f2863,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK23,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK19(X6)) ),
inference(resolution,[],[f991,f77]) ).
fof(f2868,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK24,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK19(X5)) ),
inference(resolution,[],[f2863,f76]) ).
fof(f2873,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK19(X4)) ),
inference(resolution,[],[f2868,f75]) ).
fof(f2878,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK19(X3)) ),
inference(resolution,[],[f2873,f74]) ).
fof(f2883,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK19(X2)) ),
inference(resolution,[],[f2878,f73]) ).
fof(f2888,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK19(X1)) ),
inference(resolution,[],[f2883,f72]) ).
fof(f2893,plain,
! [X2,X0,X1] :
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK19(X0)) ),
inference(resolution,[],[f2888,f71]) ).
fof(f2902,plain,
! [X0,X1] :
( ~ r1(sK31,X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK31,sK19(sK31)) ),
inference(resolution,[],[f2893,f68]) ).
fof(f2931,definition,
( spl41_331
<=> r1(sK31,sK19(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_331])],[avatar_definition]) ).
fof(f2933,plain,
( r1(sK31,sK19(sK31))
| ~ spl41_331 ),
inference(avatar_component_clause,[],[f2931]) ).
fof(f2934,plain,
( spl41_331
| spl41_317 ),
inference(avatar_split_clause,[],[f2902,f2757,f2931]) ).
fof(f2940,plain,
( p1(sK19(sK31))
| ~ spl41_331 ),
inference(resolution,[],[f2933,f67]) ).
fof(f2953,definition,
( spl41_333
<=> p1(sK19(sK31)) ),
introduced(definition,[new_symbols(definition,[spl41_333])],[avatar_definition]) ).
fof(f2955,plain,
( p1(sK19(sK31))
| ~ spl41_333 ),
inference(avatar_component_clause,[],[f2953]) ).
fof(f2967,plain,
( spl41_333
| ~ spl41_331 ),
inference(avatar_split_clause,[],[f2940,f2931,f2953]) ).
fof(f2976,plain,
( ! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,sK31)
| ~ r1(sK31,X8)
| ~ r1(X8,X9)
| p1(X9)
| ~ r1(sK13,X0) )
| ~ spl41_333 ),
inference(resolution,[],[f2955,f86]) ).
fof(f2978,definition,
( spl41_338
<=> ! [X5,X3,X4,X2,X0,X6,X1,X7] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X7,sK31)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl41_338])],[avatar_definition]) ).
fof(f2979,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X7,sK31)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl41_338 ),
inference(avatar_component_clause,[],[f2978]) ).
fof(f2980,plain,
( spl41_317
| spl41_338
| ~ spl41_333 ),
inference(avatar_split_clause,[],[f2976,f2953,f2978,f2757]) ).
fof(f2981,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK22,X0)
| ~ r1(X1,sK31)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X6,X5)
| ~ r1(X0,X6) )
| ~ spl41_338 ),
inference(resolution,[],[f2979,f78]) ).
fof(f2986,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK23,X5)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X0,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f2981,f77]) ).
fof(f2991,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK24,X4)
| ~ r1(X2,X0)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X0,X1)
| ~ r1(X1,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f2986,f76]) ).
fof(f2996,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK25,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X3)
| ~ r1(X3,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f2991,f75]) ).
fof(f3001,plain,
( ! [X2,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f2996,f74]) ).
fof(f3006,plain,
( ! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f3001,f73]) ).
fof(f3011,plain,
( ! [X0] :
( ~ r1(sK28,X0)
| ~ r1(X0,sK31) )
| ~ spl41_338 ),
inference(resolution,[],[f3006,f72]) ).
fof(f3016,plain,
( ~ r1(sK29,sK31)
| ~ spl41_338 ),
inference(resolution,[],[f3011,f71]) ).
fof(f3024,plain,
( $false
| ~ spl41_338 ),
inference(forward_subsumption_resolution,[],[f3016,f68]) ).
fof(f3025,plain,
~ spl41_338,
inference(avatar_contradiction_clause,[],[f3024]) ).
fof(f3224,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK4(sK31),X0) )
| ~ spl41_66
| ~ spl41_317 ),
inference(resolution,[],[f2758,f468]) ).
fof(f3229,plain,
( spl41_249
| ~ spl41_66
| ~ spl41_317 ),
inference(avatar_split_clause,[],[f3224,f2757,f466,f2125]) ).
fof(f3230,plain,
( p1(sK5(sK31))
| ~ spl41_219
| ~ spl41_249 ),
inference(resolution,[],[f2126,f1662]) ).
fof(f3237,plain,
( $false
| ~ spl41_219
| spl41_242
| ~ spl41_249 ),
inference(forward_subsumption_resolution,[],[f3230,f2093]) ).
fof(f3238,plain,
( ~ spl41_219
| spl41_242
| ~ spl41_249 ),
inference(avatar_contradiction_clause,[],[f3237]) ).
fof(f3325,plain,
( ! [X0] :
( p1(sK29)
| ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| ~ p1(sK6(X0))
| ~ sP2(sK29)
| ~ r1(sK29,sK7(sK29)) )
| ~ spl41_232 ),
inference(resolution,[],[f1863,f703]) ).
fof(f3326,plain,
( ! [X0] :
( p1(sK29)
| ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| r1(X0,sK6(X0))
| ~ sP2(sK29)
| ~ r1(sK29,sK7(sK29)) )
| ~ spl41_232 ),
inference(resolution,[],[f1863,f966]) ).
fof(f3327,plain,
( ! [X0] :
( p1(sK29)
| ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| r1(X0,sK6(X0))
| ~ sP2(sK29) )
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3326,f37]) ).
fof(f3328,plain,
( ! [X0] :
( p1(sK29)
| ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| ~ p1(sK6(X0))
| ~ sP2(sK29) )
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3325,f34]) ).
fof(f3329,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| r1(X0,sK6(X0))
| ~ sP2(sK29) )
| spl41_4
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3327,f122]) ).
fof(f3330,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| ~ p1(sK6(X0))
| ~ sP2(sK29) )
| spl41_4
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3328,f122]) ).
fof(f3331,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| r1(X0,sK6(X0)) )
| ~ spl41_1
| spl41_4
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3329,f110]) ).
fof(f3332,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| p1(sK33(sK7(sK29)))
| ~ p1(sK6(X0)) )
| ~ spl41_1
| spl41_4
| ~ spl41_232 ),
inference(forward_subsumption_resolution,[],[f3330,f110]) ).
fof(f3334,definition,
( spl41_362
<=> p1(sK33(sK7(sK29))) ),
introduced(definition,[new_symbols(definition,[spl41_362])],[avatar_definition]) ).
fof(f3336,plain,
( p1(sK33(sK7(sK29)))
| ~ spl41_362 ),
inference(avatar_component_clause,[],[f3334]) ).
fof(f3338,definition,
( spl41_363
<=> ! [X0] :
( ~ r1(sK29,X0)
| r1(X0,sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl41_363])],[avatar_definition]) ).
fof(f3339,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK29,X0) )
| ~ spl41_363 ),
inference(avatar_component_clause,[],[f3338]) ).
fof(f3340,plain,
( spl41_362
| spl41_363
| ~ spl41_1
| spl41_4
| ~ spl41_232 ),
inference(avatar_split_clause,[],[f3331,f1861,f121,f109,f3338,f3334]) ).
fof(f3342,definition,
( spl41_364
<=> ! [X0] :
( ~ r1(sK29,X0)
| ~ p1(sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl41_364])],[avatar_definition]) ).
fof(f3343,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ p1(sK6(X0)) )
| ~ spl41_364 ),
inference(avatar_component_clause,[],[f3342]) ).
fof(f3344,plain,
( spl41_362
| spl41_364
| ~ spl41_1
| spl41_4
| ~ spl41_232 ),
inference(avatar_split_clause,[],[f3332,f1861,f121,f109,f3342,f3334]) ).
fof(f3345,plain,
( p1(sK7(sK29))
| ~ r1(sK29,sK7(sK29))
| ~ spl41_362 ),
inference(resolution,[],[f3336,f64]) ).
fof(f3346,plain,
( ~ spl41_2
| spl41_233
| ~ spl41_362 ),
inference(avatar_split_clause,[],[f3345,f3334,f1865,f113]) ).
fof(f3348,plain,
( ! [X0] :
( r1(X0,sK7(X0))
| p1(X0)
| ~ r1(X0,sK31)
| ~ sP2(X0) )
| ~ spl41_121 ),
inference(resolution,[],[f944,f34]) ).
fof(f3725,plain,
( p1(sK29)
| ~ r1(sK29,sK31)
| ~ sP2(sK29)
| spl41_2
| ~ spl41_121 ),
inference(resolution,[],[f3348,f114]) ).
fof(f3767,plain,
( ~ r1(sK29,sK31)
| ~ sP2(sK29)
| spl41_2
| spl41_4
| ~ spl41_121 ),
inference(forward_subsumption_resolution,[],[f3725,f122]) ).
fof(f3781,plain,
( ~ sP2(sK29)
| spl41_2
| spl41_4
| ~ spl41_121 ),
inference(forward_subsumption_resolution,[],[f3767,f68]) ).
fof(f3801,plain,
( $false
| ~ spl41_1
| spl41_2
| spl41_4
| ~ spl41_121 ),
inference(forward_subsumption_resolution,[],[f3781,f110]) ).
fof(f3802,plain,
( ~ spl41_1
| spl41_2
| spl41_4
| ~ spl41_121 ),
inference(avatar_contradiction_clause,[],[f3801]) ).
fof(f3805,plain,
( p1(sK7(sK29))
| p1(sK32(sK7(sK29)))
| ~ spl41_2 ),
inference(resolution,[],[f115,f63]) ).
fof(f3968,plain,
( ~ r1(sK29,sK31)
| p1(sK6(sK31))
| ~ spl41_363 ),
inference(resolution,[],[f3339,f67]) ).
fof(f4020,plain,
( ~ r1(sK29,sK31)
| ~ spl41_363
| ~ spl41_364 ),
inference(forward_subsumption_resolution,[],[f3968,f3343]) ).
fof(f4363,plain,
( $false
| ~ spl41_363
| ~ spl41_364 ),
inference(forward_subsumption_resolution,[],[f4020,f68]) ).
fof(f4364,plain,
( ~ spl41_363
| ~ spl41_364 ),
inference(avatar_contradiction_clause,[],[f4363]) ).
fof(f4382,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| r1(X0,sK6(X0))
| p1(sK29)
| ~ sP2(sK29) )
| ~ spl41_233 ),
inference(resolution,[],[f1867,f36]) ).
fof(f4383,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ p1(sK6(X0))
| p1(sK29)
| ~ sP2(sK29) )
| ~ spl41_233 ),
inference(resolution,[],[f1867,f33]) ).
fof(f4384,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK29) )
| spl41_4
| ~ spl41_233 ),
inference(forward_subsumption_resolution,[],[f4382,f122]) ).
fof(f4385,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| r1(X0,sK6(X0)) )
| ~ spl41_1
| spl41_4
| ~ spl41_233 ),
inference(forward_subsumption_resolution,[],[f4384,f110]) ).
fof(f4386,plain,
( spl41_363
| ~ spl41_1
| spl41_4
| ~ spl41_233 ),
inference(avatar_split_clause,[],[f4385,f1865,f121,f109,f3338]) ).
fof(f4388,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ p1(sK6(X0))
| ~ sP2(sK29) )
| spl41_4
| ~ spl41_233 ),
inference(forward_subsumption_resolution,[],[f4383,f122]) ).
fof(f4390,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ p1(sK6(X0)) )
| ~ spl41_1
| spl41_4
| ~ spl41_233 ),
inference(forward_subsumption_resolution,[],[f4388,f110]) ).
fof(f4391,plain,
( spl41_364
| ~ spl41_1
| spl41_4
| ~ spl41_233 ),
inference(avatar_split_clause,[],[f4390,f1865,f121,f109,f3342]) ).
fof(f4392,plain,
( p1(sK32(sK7(sK29)))
| ~ spl41_2
| spl41_233 ),
inference(forward_subsumption_resolution,[],[f3805,f1866]) ).
fof(f4393,plain,
( $false
| ~ spl41_2
| spl41_232
| spl41_233 ),
inference(forward_subsumption_resolution,[],[f4392,f1862]) ).
fof(f4394,plain,
( ~ spl41_2
| spl41_232
| spl41_233 ),
inference(avatar_contradiction_clause,[],[f4393]) ).
cnf(s2,plain,
( ~ spl41_1
| spl41_2
| spl41_4
| spl41_5 ),
inference(sat_conversion,[],[f129]) ).
cnf(s24,plain,
( ~ spl41_4
| ~ spl41_62
| spl41_63
| spl41_65
| spl41_66 ),
inference(sat_conversion,[],[f469]) ).
cnf(s42,plain,
spl41_62,
inference(sat_conversion,[],[f790]) ).
cnf(s50,plain,
spl41_1,
inference(sat_conversion,[],[f876]) ).
cnf(s58,plain,
( ~ spl41_5
| spl41_121 ),
inference(sat_conversion,[],[f959]) ).
cnf(s118,plain,
( spl41_213
| spl41_214
| spl41_215 ),
inference(sat_conversion,[],[f1625]) ).
cnf(s121,plain,
~ spl41_65,
inference(sat_conversion,[],[f1641]) ).
cnf(s123,plain,
( ~ spl41_4
| ~ spl41_62
| spl41_63
| spl41_65
| spl41_219 ),
inference(sat_conversion,[],[f1663]) ).
cnf(s140,plain,
( ~ spl41_63
| ~ spl41_215 ),
inference(sat_conversion,[],[f1971]) ).
cnf(s141,plain,
( ~ spl41_213
| spl41_215
| spl41_235
| spl41_236 ),
inference(sat_conversion,[],[f1985]) ).
cnf(s142,plain,
( spl41_214
| ~ spl41_235
| ~ spl41_237 ),
inference(sat_conversion,[],[f1991]) ).
cnf(s143,plain,
( spl41_215
| spl41_237 ),
inference(sat_conversion,[],[f1995]) ).
cnf(s144,plain,
~ spl41_236,
inference(sat_conversion,[],[f2032]) ).
cnf(s145,plain,
( ~ spl41_214
| spl41_215
| spl41_236 ),
inference(sat_conversion,[],[f2045]) ).
cnf(s210,plain,
( ~ spl41_4
| ~ spl41_62
| spl41_63
| spl41_65
| ~ spl41_242 ),
inference(sat_conversion,[],[f2858]) ).
cnf(s216,plain,
( spl41_317
| spl41_331 ),
inference(sat_conversion,[],[f2934]) ).
cnf(s220,plain,
( ~ spl41_331
| spl41_333 ),
inference(sat_conversion,[],[f2967]) ).
cnf(s222,plain,
( spl41_317
| ~ spl41_333
| spl41_338 ),
inference(sat_conversion,[],[f2980]) ).
cnf(s223,plain,
~ spl41_338,
inference(sat_conversion,[],[f3025]) ).
cnf(s235,plain,
( ~ spl41_66
| spl41_249
| ~ spl41_317 ),
inference(sat_conversion,[],[f3229]) ).
cnf(s236,plain,
( ~ spl41_219
| spl41_242
| ~ spl41_249 ),
inference(sat_conversion,[],[f3238]) ).
cnf(s245,plain,
( ~ spl41_1
| spl41_4
| ~ spl41_232
| spl41_362
| spl41_363 ),
inference(sat_conversion,[],[f3340]) ).
cnf(s246,plain,
( ~ spl41_1
| spl41_4
| ~ spl41_232
| spl41_362
| spl41_364 ),
inference(sat_conversion,[],[f3344]) ).
cnf(s247,plain,
( ~ spl41_2
| spl41_233
| ~ spl41_362 ),
inference(sat_conversion,[],[f3346]) ).
cnf(s257,plain,
( ~ spl41_1
| spl41_2
| spl41_4
| ~ spl41_121 ),
inference(sat_conversion,[],[f3802]) ).
cnf(s340,plain,
( ~ spl41_363
| ~ spl41_364 ),
inference(sat_conversion,[],[f4364]) ).
cnf(s344,plain,
( ~ spl41_1
| spl41_4
| ~ spl41_233
| spl41_363 ),
inference(sat_conversion,[],[f4386]) ).
cnf(s346,plain,
( ~ spl41_1
| spl41_4
| ~ spl41_233
| spl41_364 ),
inference(sat_conversion,[],[f4391]) ).
cnf(s347,plain,
( ~ spl41_2
| spl41_232
| spl41_233 ),
inference(sat_conversion,[],[f4394]) ).
cnf(s348,plain,
( spl41_317
| ~ spl41_333 ),
inference(rat,[],[s222,s223]) ).
cnf(s349,plain,
( ~ spl41_213
| spl41_215
| spl41_235 ),
inference(rat,[],[s141,s144]) ).
cnf(s354,plain,
( ~ spl41_4
| spl41_63
| spl41_66 ),
inference(rat,[],[s24,s121,s42]) ).
cnf(s357,plain,
( spl41_2
| spl41_4
| spl41_5 ),
inference(rat,[],[s2,s50]) ).
cnf(s359,plain,
spl41_317,
inference(rat,[],[s220,s216,s348]) ).
cnf(s360,plain,
( spl41_63
| ~ spl41_4 ),
inference(rat,[],[s235,s236,s354,s123,s210,s121,s42,s359]) ).
cnf(s361,plain,
spl41_215,
inference(rat,[],[s349,s118,s142,s143,s145,s144]) ).
cnf(s365,plain,
~ spl41_63,
inference(rat,[],[s140,s361]) ).
cnf(s369,plain,
~ spl41_4,
inference(rat,[],[s360,s365]) ).
cnf(s370,plain,
spl41_2,
inference(rat,[],[s58,s357,s257,s369,s50]) ).
cnf(s371,plain,
spl41_363,
inference(rat,[],[s245,s347,s247,s344,s50,s369,s370]) ).
cnf(s373,plain,
~ spl41_364,
inference(rat,[],[s340,s371]) ).
cnf(s374,plain,
~ spl41_233,
inference(rat,[],[s346,s369,s50,s373]) ).
cnf(s375,plain,
~ spl41_362,
inference(rat,[],[s247,s370,s374]) ).
cnf(s376,plain,
spl41_232,
inference(rat,[],[s347,s370,s374]) ).
cnf(s380,plain,
$false,
inference(rat,[],[s246,s373,s369,s50,s375,s376]) ).
fof(f4395,plain,
$false,
inference(avatar_sat_refutation,[],[s380]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL658+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n011.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 27 16:21:45 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.88/2.28 % (2598504)Detected formulas, will run a generic FOF schedule.
% 9.88/2.28 % (2598510)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=3472576845:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.88/2.28 % (2598512)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2065335958:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.88/2.28 % (2598511)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=3264402533:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.88/2.28 % (2598514)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2728120946:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.88/2.28 % (2598515)dis-21_1_sil=8000:lcm=predicate:random_seed=2999674874: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)
% 9.88/2.28 % (2598509)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=3355540629:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.88/2.28 % (2598513)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2538339356:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.88/2.28 % (2598513)Instruction limit reached!
% 9.88/2.28 % (2598513)------------------------------
% 9.88/2.28 % (2598513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598513)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598513)Termination reason: Instruction limit
% 9.88/2.28 % (2598513)Termination phase: Saturation
% 9.88/2.28 % (2598513)Time elapsed: 0.049 s
% 9.88/2.28 % (2598513)Peak memory usage: 87 MB
% 9.88/2.28 % (2598513)Instructions burned: 119 (million)
% 9.88/2.28 % (2598514)Instruction limit reached!
% 9.88/2.28 % (2598514)------------------------------
% 9.88/2.28 % (2598514)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598514)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598514)Termination reason: Instruction limit
% 9.88/2.28 % (2598514)Termination phase: Saturation
% 9.88/2.28 % (2598514)Time elapsed: 0.057 s
% 9.88/2.28 % (2598514)Peak memory usage: 88 MB
% 9.88/2.28 % (2598514)Instructions burned: 141 (million)
% 9.88/2.28 % (2598515)Instruction limit reached!
% 9.88/2.28 % (2598515)------------------------------
% 9.88/2.28 % (2598515)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598515)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598515)Termination reason: Instruction limit
% 9.88/2.28 % (2598515)Termination phase: Saturation
% 9.88/2.28 % (2598515)Time elapsed: 0.058 s
% 9.88/2.28 % (2598515)Peak memory usage: 88 MB
% 9.88/2.28 % (2598515)Instructions burned: 130 (million)
% 9.88/2.28 % (2598512)Instruction limit reached!
% 9.88/2.28 % (2598512)------------------------------
% 9.88/2.28 % (2598512)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598512)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598512)Termination reason: Instruction limit
% 9.88/2.28 % (2598512)Termination phase: Saturation
% 9.88/2.28 % (2598512)Time elapsed: 0.061 s
% 9.88/2.28 % (2598512)Peak memory usage: 91 MB
% 9.88/2.28 % (2598512)Instructions burned: 110 (million)
% 9.88/2.28 % (2598523)lrs+10_1_sil=8000:sp=occurrence:random_seed=2674189821:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 9.88/2.28 % (2598525)lrs+1011_1_sil=32000:sp=occurrence:random_seed=580226240:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 9.88/2.28 % (2598526)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=695999235:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 9.88/2.28 % (2598524)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1336127105:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 9.88/2.28 % (2598524)Instruction limit reached!
% 9.88/2.28 % (2598524)------------------------------
% 9.88/2.28 % (2598524)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598524)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598524)Termination reason: Instruction limit
% 9.88/2.28 % (2598524)Termination phase: Saturation
% 9.88/2.28 % (2598524)Time elapsed: 0.067 s
% 9.88/2.28 % (2598524)Peak memory usage: 89 MB
% 9.88/2.28 % (2598524)Instructions burned: 159 (million)
% 9.88/2.28 % (2598526)Instruction limit reached!
% 9.88/2.28 % (2598526)------------------------------
% 9.88/2.28 % (2598526)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598526)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598526)Termination reason: Instruction limit
% 9.88/2.28 % (2598526)Termination phase: Saturation
% 9.88/2.28 % (2598526)Time elapsed: 0.107 s
% 9.88/2.28 % (2598526)Peak memory usage: 89 MB
% 9.88/2.28 % (2598526)Instructions burned: 249 (million)
% 9.88/2.28 % (2598523)Instruction limit reached!
% 9.88/2.28 % (2598523)------------------------------
% 9.88/2.28 % (2598523)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598523)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598523)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598523)Termination reason: Instruction limit
% 9.88/2.28 % (2598523)Termination phase: Saturation
% 9.88/2.28 % (2598523)Time elapsed: 0.143 s
% 9.88/2.28 % (2598523)Peak memory usage: 90 MB
% 9.88/2.28 % (2598523)Instructions burned: 287 (million)
% 9.88/2.28 % (2598525)Instruction limit reached!
% 9.88/2.28 % (2598525)------------------------------
% 9.88/2.28 % (2598525)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598525)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598525)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598525)Termination reason: Instruction limit
% 9.88/2.28 % (2598525)Termination phase: Saturation
% 9.88/2.28 % (2598525)Time elapsed: 0.137 s
% 9.88/2.28 % (2598525)Peak memory usage: 89 MB
% 9.88/2.28 % (2598525)Instructions burned: 326 (million)
% 9.88/2.28 % (2598531)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=4201285636:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.88/2.28 % (2598532)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=560699031:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 9.88/2.28 % (2598533)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2905094251:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.88/2.28 % (2598534)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=4204821537:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.88/2.28 % (2598533)Instruction limit reached!
% 9.88/2.28 % (2598533)------------------------------
% 9.88/2.28 % (2598533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598533)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598533)Termination reason: Instruction limit
% 9.88/2.28 % (2598533)Termination phase: Saturation
% 9.88/2.28 % (2598533)Time elapsed: 0.070 s
% 9.88/2.28 % (2598533)Peak memory usage: 90 MB
% 9.88/2.28 % (2598533)Instructions burned: 133 (million)
% 9.88/2.28 % (2598531)Instruction limit reached!
% 9.88/2.28 % (2598531)------------------------------
% 9.88/2.28 % (2598531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598531)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598531)Termination reason: Instruction limit
% 9.88/2.28 % (2598531)Termination phase: Saturation
% 9.88/2.28 % (2598531)Time elapsed: 0.138 s
% 9.88/2.28 % (2598531)Peak memory usage: 89 MB
% 9.88/2.28 % (2598531)Instructions burned: 295 (million)
% 9.88/2.28 % (2598534)Instruction limit reached!
% 9.88/2.28 % (2598534)------------------------------
% 9.88/2.28 % (2598534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598534)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598534)Termination reason: Instruction limit
% 9.88/2.28 % (2598534)Termination phase: Saturation
% 9.88/2.28 % (2598534)Time elapsed: 0.071 s
% 9.88/2.28 % (2598534)Peak memory usage: 89 MB
% 9.88/2.28 % (2598534)Instructions burned: 127 (million)
% 9.88/2.28 % (2598539)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2925809056:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 9.88/2.28 % (2598540)lrs+10_1_sil=8000:sp=occurrence:random_seed=1244523087:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.88/2.28 % (2598541)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2184196965:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.88/2.28 % (2598539)Instruction limit reached!
% 9.88/2.28 % (2598539)------------------------------
% 9.88/2.28 % (2598539)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598539)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598539)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598539)Termination reason: Instruction limit
% 9.88/2.28 % (2598539)Termination phase: Saturation
% 9.88/2.28 % (2598539)Time elapsed: 0.055 s
% 9.88/2.28 % (2598539)Peak memory usage: 89 MB
% 9.88/2.28 % (2598539)Instructions burned: 115 (million)
% 9.88/2.28 % (2598541)Instruction limit reached!
% 9.88/2.28 % (2598541)------------------------------
% 9.88/2.28 % (2598541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598541)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598541)Termination reason: Instruction limit
% 9.88/2.28 % (2598541)Termination phase: Saturation
% 9.88/2.28 % (2598541)Time elapsed: 0.166 s
% 9.88/2.28 % (2598541)Peak memory usage: 89 MB
% 9.88/2.28 % (2598541)Instructions burned: 440 (million)
% 9.88/2.28 % (2598545)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=964544458:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 9.88/2.28 % (2598509)First to succeed.
% 9.88/2.28 % (2598509)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2598504"
% 9.88/2.28 % (2598546)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3309366893:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2989 on theBenchmark for (2989ds/134Mi)
% 9.88/2.28 % (2598546)Instruction limit reached!
% 9.88/2.28 % (2598546)------------------------------
% 9.88/2.28 % (2598546)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598546)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598546)Termination reason: Instruction limit
% 9.88/2.28 % (2598546)Termination phase: Saturation
% 9.88/2.28 % (2598546)Time elapsed: 0.057 s
% 9.88/2.28 % (2598546)Peak memory usage: 89 MB
% 9.88/2.28 % (2598546)Instructions burned: 135 (million)
% 9.88/2.28 % (2598540)Instruction limit reached!
% 9.88/2.28 % (2598540)------------------------------
% 9.88/2.28 % (2598540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.88/2.28 % (2598540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.88/2.28 % (2598540)CaDiCaL version: 2.1.3
% 9.88/2.28 % (2598540)Termination reason: Instruction limit
% 9.88/2.28 % (2598540)Termination phase: Saturation
% 9.88/2.28 % (2598540)Time elapsed: 0.446 s
% 9.88/2.28 % (2598540)Peak memory usage: 94 MB
% 9.88/2.28 % (2598540)Instructions burned: 908 (million)
% 9.88/2.28 % (2598509)Refutation found. Thanks to Tanya!
% 9.88/2.28 % SZS status Theorem for theBenchmark
% 9.88/2.28 % SZS output start Proof for theBenchmark
% See solution above
% 10.59/2.48 % (2598509)------------------------------
% 10.59/2.48 % (2598509)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.59/2.48 % (2598509)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.59/2.48 % (2598509)CaDiCaL version: 2.1.3
% 10.59/2.48 % (2598509)Termination reason: Refutation
% 10.59/2.48 % (2598509)Time elapsed: 0.983 s
% 10.59/2.48 % (2598509)Peak memory usage: 134 MB
% 10.59/2.48 % (2598509)Instructions burned: 1492 (million)
% 10.59/2.48 % (2598509)------------------------------
% 10.59/2.48 % (2598509)------------------------------
% 10.59/2.48 % (2598504)Success in time 1.418 s
% 10.59/2.48 % Vampire exiting
%------------------------------------------------------------------------------