%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LCL662+1.005 : 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 : n026.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:26 AM UTC 2026
% Result : Theorem 43.62s 10.20s
% Output : Refutation 65.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 12
% Syntax : Number of formulae : 126 ( 17 unt; 10 def)
% Number of atoms : 2011 ( 0 equ)
% Maximal formula atoms : 208 ( 15 avg)
% Number of connectives : 4038 (2153 ~;1686 |; 189 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 73 ( 12 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 11 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 1 con; 0-1 aty)
% Number of variables : 1599 ( 0 sgn1525 !; 74 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : r1(X0,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity) ).
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)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) )
& ~ p2(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)
| ~ ( ~ ! [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(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)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p2(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)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ~ p2(X1) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ~ p2(X0) ) ) ) ) ) )
& ~ p1(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)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [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)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) )
& ~ p2(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)
| ~ ( ~ ! [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(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)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p2(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)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p2(X0) ) ) ) ) ) )
& ~ p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ( ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ p1(X1) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ~ p2(X1) ) ) ) ) ) )
& ~ p1(X1) ) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ p1(X0) ) ) ) ) ) )
& ~ p2(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) ) ) ) ) ) )
& ~ 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)
| ~ p2(X0) ) ) ) ) ) )
& ~ p1(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)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X21] :
( ~ r1(X0,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)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,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)
| ~ p1(X41) ) ) ) ) ) )
& ~ p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X48,X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ~ ( ~ ! [X57] :
( ~ r1(X56,X57)
| ~ ! [X58] :
( ~ r1(X57,X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) )
& ~ p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [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)
| ~ ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,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)
| ~ p2(X83) ) ) ) ) ) )
& ~ p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ~ ! [X86] :
( ~ r1(X85,X86)
| ~ ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| ~ ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| ~ ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) )
& ~ p2(X93) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X100] :
( ~ r1(X0,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| ~ ! [X103] :
( ~ r1(X102,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)
| ~ ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) )
& ~ p1(X109) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,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)
| ~ ( ~ ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| ~ ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) )
& ~ p1(X125) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X132] :
( ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X132,X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| ! [X136] :
( ~ r1(X135,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) ) ) ) ) ) )
& ~ p2(X136) ) ) ) ) ) )
| ~ ! [X143] :
( ~ r1(X0,X143)
| ~ ! [X144] :
( ~ r1(X143,X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,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) ) ) ) ) ) )
& ~ p1(X147) ) ) ) ) ) )
| ~ ! [X154] :
( ~ r1(X0,X154)
| ~ ! [X155] :
( ~ r1(X154,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)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) )
& ~ p1(X158) ) ) ) ) ) )
| ( ~ ! [X165] :
( ~ r1(X0,X165)
| ~ ! [X166] :
( ~ r1(X165,X166)
| ~ ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X171] :
( ~ r1(X0,X171)
| ~ ! [X172] :
( ~ r1(X171,X172)
| ~ ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X177] :
( ~ r1(X0,X177)
| ~ ! [X178] :
( ~ r1(X177,X178)
| ~ ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
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)
| ~ ! [X17] :
( ~ r1(X16,X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X21] :
( ~ r1(X0,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)
| ~ ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,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)
| ~ p1(X41) ) ) ) ) ) )
& ~ p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ~ ! [X49] :
( ~ r1(X48,X49)
| ~ ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ~ ! [X53] :
( ~ r1(X52,X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ~ ( ~ ! [X57] :
( ~ r1(X56,X57)
| ~ ! [X58] :
( ~ r1(X57,X58)
| ~ ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) )
& ~ p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [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)
| ~ ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,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)
| ~ p2(X83) ) ) ) ) ) )
& ~ p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ~ ! [X86] :
( ~ r1(X85,X86)
| ~ ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ~ ! [X90] :
( ~ r1(X89,X90)
| ~ ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ~ ( ~ ! [X94] :
( ~ r1(X93,X94)
| ~ ! [X95] :
( ~ r1(X94,X95)
| ~ ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) )
& ~ p2(X93) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X100] :
( ~ r1(X0,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| ~ ! [X103] :
( ~ r1(X102,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)
| ~ ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) )
& ~ p1(X109) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,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)
| ~ ( ~ ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| ~ ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) )
& ~ p1(X125) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X132] :
( ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X132,X133)
| ~ ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| ! [X136] :
( ~ r1(X135,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) ) ) ) ) ) )
& ~ p2(X136) ) ) ) ) ) )
| ~ ! [X143] :
( ~ r1(X0,X143)
| ~ ! [X144] :
( ~ r1(X143,X144)
| ~ ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,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) ) ) ) ) ) )
& ~ p1(X147) ) ) ) ) ) )
| ~ ! [X154] :
( ~ r1(X0,X154)
| ~ ! [X155] :
( ~ r1(X154,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)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) )
& ~ p1(X158) ) ) ) ) ) )
| ( ~ ! [X165] :
( ~ r1(X0,X165)
| ~ ! [X166] :
( ~ r1(X165,X166)
| ~ ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) )
& ~ p2(X0) )
| ( ~ ! [X171] :
( ~ r1(X0,X171)
| ~ ! [X172] :
( ~ r1(X171,X172)
| ~ ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) )
& ~ p1(X0) )
| ( ~ ! [X177] :
( ~ r1(X0,X177)
| ~ ! [X178] :
( ~ r1(X177,X178)
| ~ ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) )
& ~ p1(X0) )
| p1(X0) ),
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)
| ? [X17] :
( r1(X16,X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X21] :
( ~ r1(X0,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)
& ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,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)
| ~ p1(X41) ) ) ) ) ) )
| p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ? [X45] :
( r1(X44,X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ? [X49] :
( r1(X48,X49)
& ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ? [X58] :
( r1(X57,X58)
& ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) )
| p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [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)
& ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,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)
| ~ p2(X83) ) ) ) ) ) )
| p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ? [X86] :
( r1(X85,X86)
& ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ? [X90] :
( r1(X89,X90)
& ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ? [X95] :
( r1(X94,X95)
& ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) )
| p2(X93) ) ) ) ) ) ) ) ) ) )
& ! [X100] :
( ~ r1(X0,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ! [X103] :
( ~ r1(X102,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)
& ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) )
| p1(X109) ) ) ) ) ) ) ) ) ) )
& ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,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)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) )
| p1(X125) ) ) ) ) ) ) ) ) ) )
& ! [X132] :
( ~ r1(X0,X132)
| ? [X133] :
( r1(X132,X133)
& ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| ! [X136] :
( ~ r1(X135,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) ) ) ) ) ) )
| p2(X136) ) ) ) ) )
& ! [X143] :
( ~ r1(X0,X143)
| ? [X144] :
( r1(X143,X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,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) ) ) ) ) ) )
| p1(X147) ) ) ) ) )
& ! [X154] :
( ~ r1(X0,X154)
| ? [X155] :
( r1(X154,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)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) )
| p1(X158) ) ) ) ) )
& ( ! [X165] :
( ~ r1(X0,X165)
| ? [X166] :
( r1(X165,X166)
& ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) )
| p2(X0) )
& ( ! [X171] :
( ~ r1(X0,X171)
| ? [X172] :
( r1(X171,X172)
& ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) )
| p1(X0) )
& ( ! [X177] :
( ~ r1(X0,X177)
| ? [X178] :
( r1(X177,X178)
& ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) )
| p1(X0) )
& ~ p1(X0) ),
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)
| ? [X17] :
( r1(X16,X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X21] :
( ~ r1(X0,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)
& ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,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)
| ~ p1(X41) ) ) ) ) ) )
| p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X42] :
( ~ r1(X0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ? [X45] :
( r1(X44,X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ? [X49] :
( r1(X48,X49)
& ! [X50] :
( ~ r1(X49,X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ? [X53] :
( r1(X52,X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ? [X58] :
( r1(X57,X58)
& ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) )
| p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [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)
& ! [X75] :
( ~ r1(X74,X75)
| ! [X76] :
( ~ r1(X75,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)
| ~ p2(X83) ) ) ) ) ) )
| p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ? [X86] :
( r1(X85,X86)
& ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ? [X90] :
( r1(X89,X90)
& ! [X91] :
( ~ r1(X90,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ? [X95] :
( r1(X94,X95)
& ! [X96] :
( ~ r1(X95,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) )
| p2(X93) ) ) ) ) ) ) ) ) ) )
& ! [X100] :
( ~ r1(X0,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ! [X103] :
( ~ r1(X102,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)
& ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) )
| p1(X109) ) ) ) ) ) ) ) ) ) )
& ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,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)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ! [X128] :
( ~ r1(X127,X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) )
| p1(X125) ) ) ) ) ) ) ) ) ) )
& ! [X132] :
( ~ r1(X0,X132)
| ? [X133] :
( r1(X132,X133)
& ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| ! [X136] :
( ~ r1(X135,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) ) ) ) ) ) )
| p2(X136) ) ) ) ) )
& ! [X143] :
( ~ r1(X0,X143)
| ? [X144] :
( r1(X143,X144)
& ! [X145] :
( ~ r1(X144,X145)
| ! [X146] :
( ~ r1(X145,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) ) ) ) ) ) )
| p1(X147) ) ) ) ) )
& ! [X154] :
( ~ r1(X0,X154)
| ? [X155] :
( r1(X154,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)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) )
| p1(X158) ) ) ) ) )
& ( ! [X165] :
( ~ r1(X0,X165)
| ? [X166] :
( r1(X165,X166)
& ! [X167] :
( ~ r1(X166,X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) )
| p2(X0) )
& ( ! [X171] :
( ~ r1(X0,X171)
| ? [X172] :
( r1(X171,X172)
& ! [X173] :
( ~ r1(X172,X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) )
| p1(X0) )
& ( ! [X177] :
( ~ r1(X0,X177)
| ? [X178] :
( r1(X177,X178)
& ! [X179] :
( ~ r1(X178,X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) )
| p1(X0) )
& ~ p1(X0) ),
inference(flattening,[],[f6]) ).
fof(f8,plain,
( ! [X1] :
( ~ r1(sK0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ( r1(X4,sK1(X4))
& ! [X6] :
( ~ r1(sK1(X4),X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ( r1(X8,sK2(X8))
& ! [X10] :
( ~ r1(sK2(X8),X10)
| ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| ( r1(X12,sK3(X12))
& ! [X14] :
( ~ r1(sK3(X12),X14)
| ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ( r1(X16,sK4(X16))
& ! [X18] :
( ~ r1(sK4(X16),X18)
| ! [X19] :
( ~ r1(X18,X19)
| ! [X20] :
( ~ r1(X19,X20)
| p1(X20) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X21] :
( ~ r1(sK0,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ( r1(X23,sK5(X23))
& ! [X25] :
( ~ r1(sK5(X23),X25)
| ! [X26] :
( ~ r1(X25,X26)
| ! [X27] :
( ~ r1(X26,X27)
| ( r1(X27,sK6(X27))
& ! [X29] :
( ~ r1(sK6(X27),X29)
| ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| ( r1(X31,sK7(X31))
& ! [X33] :
( ~ r1(sK7(X31),X33)
| ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| ! [X36] :
( ~ r1(X35,X36)
| ( r1(X36,sK8(X36))
& ! [X38] :
( ~ r1(sK8(X36),X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ~ p1(X41) ) ) ) ) ) )
| p2(X35) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X42] :
( ~ r1(sK0,X42)
| ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| ( r1(X44,sK9(X44))
& ! [X46] :
( ~ r1(sK9(X44),X46)
| ! [X47] :
( ~ r1(X46,X47)
| ! [X48] :
( ~ r1(X47,X48)
| ( r1(X48,sK10(X48))
& ! [X50] :
( ~ r1(sK10(X48),X50)
| ! [X51] :
( ~ r1(X50,X51)
| ! [X52] :
( ~ r1(X51,X52)
| ( r1(X52,sK11(X52))
& ! [X54] :
( ~ r1(sK11(X52),X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( r1(X57,sK12(X57))
& ! [X59] :
( ~ r1(sK12(X57),X59)
| ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| ! [X62] :
( ~ r1(X61,X62)
| ~ p1(X62) ) ) ) ) ) )
| p1(X56) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X63] :
( ~ r1(sK0,X63)
| ! [X64] :
( ~ r1(X63,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ( r1(X65,sK13(X65))
& ! [X67] :
( ~ r1(sK13(X65),X67)
| ! [X68] :
( ~ r1(X67,X68)
| ! [X69] :
( ~ r1(X68,X69)
| ( r1(X69,sK14(X69))
& ! [X71] :
( ~ r1(sK14(X69),X71)
| ! [X72] :
( ~ r1(X71,X72)
| ! [X73] :
( ~ r1(X72,X73)
| ( r1(X73,sK15(X73))
& ! [X75] :
( ~ r1(sK15(X73),X75)
| ! [X76] :
( ~ r1(X75,X76)
| ! [X77] :
( ~ r1(X76,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ( r1(X78,sK16(X78))
& ! [X80] :
( ~ r1(sK16(X78),X80)
| ! [X81] :
( ~ r1(X80,X81)
| ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| ~ p2(X83) ) ) ) ) ) )
| p1(X77) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X84] :
( ~ r1(sK0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ( r1(X85,sK17(X85))
& ! [X87] :
( ~ r1(sK17(X85),X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ( r1(X89,sK18(X89))
& ! [X91] :
( ~ r1(sK18(X89),X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ( r1(X94,sK19(X94))
& ! [X96] :
( ~ r1(sK19(X94),X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ~ p1(X99) ) ) ) ) ) )
| p2(X93) ) ) ) ) ) ) ) ) ) )
& ! [X100] :
( ~ r1(sK0,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ( r1(X101,sK20(X101))
& ! [X103] :
( ~ r1(sK20(X101),X103)
| ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| ( r1(X105,sK21(X105))
& ! [X107] :
( ~ r1(sK21(X105),X107)
| ! [X108] :
( ~ r1(X107,X108)
| ! [X109] :
( ~ r1(X108,X109)
| ! [X110] :
( ~ r1(X109,X110)
| ( r1(X110,sK22(X110))
& ! [X112] :
( ~ r1(sK22(X110),X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| ! [X115] :
( ~ r1(X114,X115)
| ~ p1(X115) ) ) ) ) ) )
| p1(X109) ) ) ) ) ) ) ) ) ) )
& ! [X116] :
( ~ r1(sK0,X116)
| ! [X117] :
( ~ r1(X116,X117)
| ( r1(X117,sK23(X117))
& ! [X119] :
( ~ r1(sK23(X117),X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| ( r1(X121,sK24(X121))
& ! [X123] :
( ~ r1(sK24(X121),X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ! [X126] :
( ~ r1(X125,X126)
| ( r1(X126,sK25(X126))
& ! [X128] :
( ~ r1(sK25(X126),X128)
| ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| ! [X131] :
( ~ r1(X130,X131)
| ~ p2(X131) ) ) ) ) ) )
| p1(X125) ) ) ) ) ) ) ) ) ) )
& ! [X132] :
( ~ r1(sK0,X132)
| ( r1(X132,sK26(X132))
& ! [X134] :
( ~ r1(sK26(X132),X134)
| ! [X135] :
( ~ r1(X134,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ! [X137] :
( ~ r1(X136,X137)
| ( r1(X137,sK27(X137))
& ! [X139] :
( ~ r1(sK27(X137),X139)
| ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| ~ p1(X142) ) ) ) ) ) )
| p2(X136) ) ) ) ) )
& ! [X143] :
( ~ r1(sK0,X143)
| ( r1(X143,sK28(X143))
& ! [X145] :
( ~ r1(sK28(X143),X145)
| ! [X146] :
( ~ r1(X145,X146)
| ! [X147] :
( ~ r1(X146,X147)
| ! [X148] :
( ~ r1(X147,X148)
| ( r1(X148,sK29(X148))
& ! [X150] :
( ~ r1(sK29(X148),X150)
| ! [X151] :
( ~ r1(X150,X151)
| ! [X152] :
( ~ r1(X151,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ~ p1(X153) ) ) ) ) ) )
| p1(X147) ) ) ) ) )
& ! [X154] :
( ~ r1(sK0,X154)
| ( r1(X154,sK30(X154))
& ! [X156] :
( ~ r1(sK30(X154),X156)
| ! [X157] :
( ~ r1(X156,X157)
| ! [X158] :
( ~ r1(X157,X158)
| ! [X159] :
( ~ r1(X158,X159)
| ( r1(X159,sK31(X159))
& ! [X161] :
( ~ r1(sK31(X159),X161)
| ! [X162] :
( ~ r1(X161,X162)
| ! [X163] :
( ~ r1(X162,X163)
| ! [X164] :
( ~ r1(X163,X164)
| ~ p2(X164) ) ) ) ) ) )
| p1(X158) ) ) ) ) )
& ( ! [X165] :
( ~ r1(sK0,X165)
| ( r1(X165,sK32(X165))
& ! [X167] :
( ~ r1(sK32(X165),X167)
| ! [X168] :
( ~ r1(X167,X168)
| ! [X169] :
( ~ r1(X168,X169)
| ! [X170] :
( ~ r1(X169,X170)
| ~ p1(X170) ) ) ) ) ) )
| p2(sK0) )
& ( ! [X171] :
( ~ r1(sK0,X171)
| ( r1(X171,sK33(X171))
& ! [X173] :
( ~ r1(sK33(X171),X173)
| ! [X174] :
( ~ r1(X173,X174)
| ! [X175] :
( ~ r1(X174,X175)
| ! [X176] :
( ~ r1(X175,X176)
| ~ p1(X176) ) ) ) ) ) )
| p1(sK0) )
& ( ! [X177] :
( ~ r1(sK0,X177)
| ( r1(X177,sK34(X177))
& ! [X179] :
( ~ r1(sK34(X177),X179)
| ! [X180] :
( ~ r1(X179,X180)
| ! [X181] :
( ~ r1(X180,X181)
| ! [X182] :
( ~ r1(X181,X182)
| ~ p2(X182) ) ) ) ) ) )
| p1(sK0) )
& ~ p1(sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34]),skolemize(X0,sK0),skolemize(X5,sK1(X4)),skolemize(X9,sK2(X8)),skolemize(X13,sK3(X12)),skolemize(X17,sK4(X16)),skolemize(X24,sK5(X23)),skolemize(X28,sK6(X27)),skolemize(X32,sK7(X31)),skolemize(X37,sK8(X36)),skolemize(X45,sK9(X44)),skolemize(X49,sK10(X48)),skolemize(X53,sK11(X52)),skolemize(X58,sK12(X57)),skolemize(X66,sK13(X65)),skolemize(X70,sK14(X69)),skolemize(X74,sK15(X73)),skolemize(X79,sK16(X78)),skolemize(X86,sK17(X85)),skolemize(X90,sK18(X89)),skolemize(X95,sK19(X94)),skolemize(X102,sK20(X101)),skolemize(X106,sK21(X105)),skolemize(X111,sK22(X110)),skolemize(X118,sK23(X117)),skolemize(X122,sK24(X121)),skolemize(X127,sK25(X126)),skolemize(X133,sK26(X132)),skolemize(X138,sK27(X137)),skolemize(X144,sK28(X143)),skolemize(X149,sK29(X148)),skolemize(X155,sK30(X154)),skolemize(X160,sK31(X159)),skolemize(X166,sK32(X165)),skolemize(X172,sK33(X171)),skolemize(X178,sK34(X177))],[f7]) ).
fof(f9,plain,
! [X0] : r1(X0,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f10,plain,
~ p1(sK0),
inference(cnf_transformation,[],[f8]) ).
fof(f13,plain,
! [X171,X176,X174,X175,X173] :
( ~ r1(sK0,X171)
| ~ r1(sK33(X171),X173)
| ~ r1(X173,X174)
| ~ r1(X174,X175)
| ~ r1(X175,X176)
| ~ p1(X176)
| p1(sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f14,plain,
! [X171] :
( ~ r1(sK0,X171)
| r1(X171,sK33(X171))
| p1(sK0) ),
inference(cnf_transformation,[],[f8]) ).
fof(f53,plain,
! [X2,X3,X10,X11,X18,X1,X6,X8,X16,X7,X4,X14,X19,X15,X12,X20] :
( ~ r1(sK4(X16),X18)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK1(X4),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK2(X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(sK3(X12),X14)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| ~ r1(sK0,X1)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| p1(X20) ),
inference(cnf_transformation,[],[f8]) ).
fof(f54,plain,
! [X2,X3,X10,X11,X1,X8,X6,X7,X14,X4,X16,X15,X12] :
( ~ r1(sK3(X12),X14)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK1(X4),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK2(X8),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(sK0,X1)
| ~ r1(X14,X15)
| ~ r1(X15,X16)
| r1(X16,sK4(X16)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f55,plain,
! [X2,X3,X10,X11,X1,X8,X6,X7,X4,X12] :
( ~ r1(sK2(X8),X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK1(X4),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK0,X1)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| r1(X12,sK3(X12)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f56,plain,
! [X2,X3,X1,X8,X6,X7,X4] :
( ~ r1(sK1(X4),X6)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK0,X1)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| r1(X8,sK2(X8)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f57,plain,
! [X2,X3,X1,X4] :
( ~ r1(sK0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| r1(X4,sK1(X4)) ),
inference(cnf_transformation,[],[f8]) ).
fof(f60,plain,
! [X171,X176,X174,X175,X173] :
( ~ r1(sK33(X171),X173)
| ~ r1(sK0,X171)
| ~ r1(X173,X174)
| ~ r1(X174,X175)
| ~ r1(X175,X176)
| ~ p1(X176) ),
inference(forward_subsumption_resolution,[],[f13,f10]) ).
fof(f61,plain,
! [X171] :
( r1(X171,sK33(X171))
| ~ r1(sK0,X171) ),
inference(forward_subsumption_resolution,[],[f14,f10]) ).
fof(f127,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X2,sK1(X2)) ),
inference(resolution,[],[f57,f9]) ).
fof(f186,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK2(X6),X7)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK1(X3),X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X7,X8)
| r1(X8,sK3(X8)) ),
inference(resolution,[],[f55,f9]) ).
fof(f393,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK3(X9),X10)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK1(X3),X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(sK2(X6),X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X10,X11)
| r1(X11,sK4(X11)) ),
inference(resolution,[],[f54,f9]) ).
fof(f421,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X14,X4,X5,X12,X13] :
( ~ r1(sK4(X12),X13)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK1(X3),X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(sK2(X6),X7)
| ~ r1(X7,X8)
| ~ r1(X8,X9)
| ~ r1(sK3(X9),X10)
| ~ r1(X10,X11)
| ~ r1(X11,X12)
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X13,X14)
| p1(X14) ),
inference(resolution,[],[f53,f9]) ).
fof(f449,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK1(X3),X4)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X4,X5)
| r1(X5,sK2(X5)) ),
inference(resolution,[],[f56,f9]) ).
fof(f2045,plain,
! [X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| r1(X1,sK1(X1)) ),
inference(resolution,[],[f127,f9]) ).
fof(f2053,plain,
! [X0] :
( r1(X0,sK1(X0))
| ~ r1(sK0,X0) ),
inference(resolution,[],[f2045,f9]) ).
fof(f2301,definition,
( spl35_106
<=> r1(sK0,sK1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl35_106])],[avatar_definition]) ).
fof(f2302,plain,
( r1(sK0,sK1(sK0))
| ~ spl35_106 ),
inference(avatar_component_clause,[],[f2301]) ).
fof(f2303,plain,
( ~ r1(sK0,sK1(sK0))
| spl35_106 ),
inference(avatar_component_clause,[],[f2301]) ).
fof(f2328,plain,
( ~ r1(sK0,sK0)
| spl35_106 ),
inference(resolution,[],[f2303,f2053]) ).
fof(f2329,plain,
( $false
| spl35_106 ),
inference(forward_subsumption_resolution,[],[f2328,f9]) ).
fof(f2330,plain,
spl35_106,
inference(avatar_contradiction_clause,[],[f2329]) ).
fof(f2591,definition,
( spl35_149
<=> ! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(sK0,X0)
| ~ r1(X2,sK0)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl35_149])],[avatar_definition]) ).
fof(f2592,plain,
( ! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK0)
| ~ r1(X1,X2) )
| ~ spl35_149 ),
inference(avatar_component_clause,[],[f2591]) ).
fof(f2673,plain,
( ! [X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X1,sK0)
| ~ r1(X0,X1) )
| ~ spl35_149 ),
inference(resolution,[],[f2592,f9]) ).
fof(f4937,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK1(X2),X4)
| ~ r1(X1,X2)
| ~ r1(sK0,X3)
| ~ r1(X3,X0)
| ~ r1(X0,X1)
| r1(X4,sK2(X4)) ),
inference(resolution,[],[f449,f9]) ).
fof(f10181,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK2(X5),X7)
| ~ r1(X1,X2)
| ~ r1(sK1(X2),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(sK0,X6)
| ~ r1(X6,X0)
| ~ r1(X0,X1)
| r1(X7,sK3(X7)) ),
inference(resolution,[],[f186,f9]) ).
fof(f10199,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK1(X1),X2)
| ~ r1(X0,X1)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X0)
| r1(sK2(X4),sK3(sK2(X4))) ),
inference(resolution,[],[f10181,f9]) ).
fof(f10292,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK1(X1),X2)
| ~ r1(X0,X1)
| ~ r1(X2,X3)
| ~ r1(sK0,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X0)
| r1(sK2(X3),sK3(sK2(X3))) ),
inference(resolution,[],[f10199,f9]) ).
fof(f10347,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK1(X1),X2)
| ~ r1(X0,X1)
| ~ r1(sK0,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X0)
| r1(sK2(X2),sK3(sK2(X2))) ),
inference(resolution,[],[f10292,f9]) ).
fof(f10396,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK0,sK1(X1))
| ~ r1(sK0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X0)
| r1(sK2(sK33(sK1(X1))),sK3(sK2(sK33(sK1(X1)))))
| ~ r1(X0,X1) ),
inference(resolution,[],[f10347,f61]) ).
fof(f14289,definition,
( spl35_925
<=> ! [X0] :
( ~ r1(X0,sK0)
| ~ r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl35_925])],[avatar_definition]) ).
fof(f14290,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| ~ r1(X0,sK0) )
| ~ spl35_925 ),
inference(avatar_component_clause,[],[f14289]) ).
fof(f14310,plain,
( ~ r1(sK0,sK0)
| ~ spl35_925 ),
inference(resolution,[],[f14290,f9]) ).
fof(f14329,plain,
( $false
| ~ spl35_925 ),
inference(forward_subsumption_resolution,[],[f14310,f9]) ).
fof(f14330,plain,
~ spl35_925,
inference(avatar_contradiction_clause,[],[f14329]) ).
fof(f16458,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK3(X8),X10)
| ~ r1(X1,X2)
| ~ r1(sK1(X2),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(sK2(X5),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK0,X9)
| ~ r1(X9,X0)
| ~ r1(X0,X1)
| r1(X10,sK4(X10)) ),
inference(resolution,[],[f393,f9]) ).
fof(f16475,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK2(X4),X5)
| ~ r1(sK1(X1),X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X0,X1)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(sK0,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X0)
| r1(sK3(X7),sK4(sK3(X7))) ),
inference(resolution,[],[f16458,f9]) ).
fof(f16498,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK2(X3),X5)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X4,X0)
| ~ r1(sK1(X0),X1)
| ~ r1(X5,X6)
| ~ r1(sK0,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X4)
| r1(sK3(X6),sK4(sK3(X6))) ),
inference(resolution,[],[f16475,f9]) ).
fof(f16528,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK2(X2),X5)
| ~ r1(X1,X2)
| ~ r1(X3,X4)
| ~ r1(sK1(X4),X0)
| ~ r1(X0,X1)
| ~ r1(sK0,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X3)
| r1(sK3(X5),sK4(sK3(X5))) ),
inference(resolution,[],[f16498,f9]) ).
fof(f16551,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK1(X3),X4)
| ~ r1(X2,X3)
| ~ r1(X0,X1)
| ~ r1(X4,X0)
| ~ r1(sK0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X2)
| r1(sK3(sK2(X1)),sK4(sK3(sK2(X1)))) ),
inference(resolution,[],[f16528,f9]) ).
fof(f16588,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK1(X1),X2)
| ~ r1(X2,X3)
| ~ r1(X0,X1)
| ~ r1(sK0,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X0)
| r1(sK3(sK2(X3)),sK4(sK3(sK2(X3)))) ),
inference(resolution,[],[f16551,f9]) ).
fof(f16641,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK1(X0),X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X2)
| r1(sK3(sK2(X1)),sK4(sK3(sK2(X1)))) ),
inference(resolution,[],[f16588,f9]) ).
fof(f16705,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK0,sK1(X1))
| ~ r1(sK0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X0)
| r1(sK3(sK2(sK33(sK1(X1)))),sK4(sK3(sK2(sK33(sK1(X1))))))
| ~ r1(X0,X1) ),
inference(resolution,[],[f16641,f61]) ).
fof(f17049,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(sK3(sK2(sK33(sK1(sK0)))),sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ r1(X2,sK0)
| ~ r1(sK0,sK0) ),
inference(resolution,[],[f16705,f2053]) ).
fof(f17499,definition,
( spl35_1061
<=> r1(sK1(sK0),sK33(sK1(sK0))) ),
introduced(definition,[new_symbols(definition,[spl35_1061])],[avatar_definition]) ).
fof(f17500,plain,
( r1(sK1(sK0),sK33(sK1(sK0)))
| ~ spl35_1061 ),
inference(avatar_component_clause,[],[f17499]) ).
fof(f17501,plain,
( ~ r1(sK1(sK0),sK33(sK1(sK0)))
| spl35_1061 ),
inference(avatar_component_clause,[],[f17499]) ).
fof(f17503,plain,
( ~ r1(sK0,sK1(sK0))
| spl35_1061 ),
inference(resolution,[],[f17501,f61]) ).
fof(f17504,plain,
( $false
| ~ spl35_106
| spl35_1061 ),
inference(forward_subsumption_resolution,[],[f17503,f2302]) ).
fof(f17505,plain,
( ~ spl35_106
| spl35_1061 ),
inference(avatar_contradiction_clause,[],[f17504]) ).
fof(f17520,plain,
( ! [X2,X0,X1] :
( ~ r1(X0,sK0)
| ~ r1(sK0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X0)
| r1(sK33(sK1(sK0)),sK2(sK33(sK1(sK0)))) )
| ~ spl35_1061 ),
inference(resolution,[],[f17500,f4937]) ).
fof(f23578,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12,X13] :
( ~ r1(sK4(X11),X13)
| ~ r1(X1,X2)
| ~ r1(sK1(X2),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(sK2(X5),X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| ~ r1(sK3(X8),X9)
| ~ r1(X9,X10)
| ~ r1(X10,X11)
| ~ r1(sK0,X12)
| ~ r1(X12,X0)
| ~ r1(X0,X1)
| p1(X13) ),
inference(resolution,[],[f421,f9]) ).
fof(f23592,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5,X12] :
( ~ r1(sK3(X7),X8)
| ~ r1(sK1(X1),X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(sK2(X4),X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X0,X1)
| ~ r1(X8,X9)
| ~ r1(X9,X10)
| ~ r1(sK0,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X0)
| p1(sK4(X10)) ),
inference(resolution,[],[f23578,f9]) ).
fof(f23621,plain,
! [X2,X3,X10,X0,X11,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK3(X6),X8)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(sK2(X3),X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X7,X0)
| ~ r1(sK1(X0),X1)
| ~ r1(X8,X9)
| ~ r1(sK0,X10)
| ~ r1(X10,X11)
| ~ r1(X11,X7)
| p1(sK4(X9)) ),
inference(resolution,[],[f23592,f9]) ).
fof(f23661,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK3(X5),X8)
| ~ r1(X1,X2)
| ~ r1(sK2(X2),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X6,X7)
| ~ r1(sK1(X7),X0)
| ~ r1(X0,X1)
| ~ r1(sK0,X9)
| ~ r1(X9,X10)
| ~ r1(X10,X6)
| p1(sK4(X8)) ),
inference(resolution,[],[f23621,f9]) ).
fof(f23682,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( ~ r1(sK2(X1),X2)
| ~ r1(X0,X1)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X5,X6)
| ~ r1(sK1(X6),X7)
| ~ r1(X7,X0)
| ~ r1(sK0,X8)
| ~ r1(X8,X9)
| ~ r1(X9,X5)
| p1(sK4(sK3(X4))) ),
inference(resolution,[],[f23661,f9]) ).
fof(f23706,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK2(X1),X2)
| ~ r1(X0,X1)
| ~ r1(X2,X3)
| ~ r1(X4,X5)
| ~ r1(sK1(X5),X6)
| ~ r1(X6,X0)
| ~ r1(sK0,X7)
| ~ r1(X7,X8)
| ~ r1(X8,X4)
| p1(sK4(sK3(X3))) ),
inference(resolution,[],[f23682,f9]) ).
fof(f23730,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK2(X1),X2)
| ~ r1(X0,X1)
| ~ r1(X3,X4)
| ~ r1(sK1(X4),X5)
| ~ r1(X5,X0)
| ~ r1(sK0,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X3)
| p1(sK4(sK3(X2))) ),
inference(resolution,[],[f23706,f9]) ).
fof(f23754,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK1(X3),X4)
| ~ r1(X2,X3)
| ~ r1(X0,X1)
| ~ r1(X4,X0)
| ~ r1(sK0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X2)
| p1(sK4(sK3(sK2(X1)))) ),
inference(resolution,[],[f23730,f9]) ).
fof(f23798,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK1(X1),X2)
| ~ r1(X2,X3)
| ~ r1(X0,X1)
| ~ r1(sK0,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X0)
| p1(sK4(sK3(sK2(X3)))) ),
inference(resolution,[],[f23754,f9]) ).
fof(f23862,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK1(X0),X1)
| ~ r1(X2,X0)
| ~ r1(sK0,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X2)
| p1(sK4(sK3(sK2(X1)))) ),
inference(resolution,[],[f23798,f9]) ).
fof(f23937,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK0,sK1(X1))
| ~ r1(sK0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X0)
| p1(sK4(sK3(sK2(sK33(sK1(X1))))))
| ~ r1(X0,X1) ),
inference(resolution,[],[f23862,f61]) ).
fof(f24067,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ r1(X2,sK0)
| ~ r1(sK0,sK0) ),
inference(resolution,[],[f23937,f2053]) ).
fof(f32585,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(sK2(sK33(sK1(sK0))),sK3(sK2(sK33(sK1(sK0)))))
| ~ r1(X2,sK0)
| ~ r1(sK0,sK0) ),
inference(resolution,[],[f10396,f2053]) ).
fof(f33727,plain,
( ! [X0] :
( ~ r1(X0,sK0)
| ~ r1(sK0,X0) )
| ~ spl35_149 ),
inference(resolution,[],[f2673,f9]) ).
fof(f33740,plain,
( spl35_925
| ~ spl35_149 ),
inference(avatar_split_clause,[],[f33727,f2591,f14289]) ).
fof(f34021,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(sK3(sK2(sK33(sK1(sK0)))),sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ r1(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f17049,f9]) ).
fof(f34023,definition,
( spl35_2610
<=> r1(sK3(sK2(sK33(sK1(sK0)))),sK4(sK3(sK2(sK33(sK1(sK0)))))) ),
introduced(definition,[new_symbols(definition,[spl35_2610])],[avatar_definition]) ).
fof(f34025,plain,
( r1(sK3(sK2(sK33(sK1(sK0)))),sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ spl35_2610 ),
inference(avatar_component_clause,[],[f34023]) ).
fof(f34060,definition,
( spl35_2613
<=> r1(sK2(sK33(sK1(sK0))),sK3(sK2(sK33(sK1(sK0))))) ),
introduced(definition,[new_symbols(definition,[spl35_2613])],[avatar_definition]) ).
fof(f34062,plain,
( r1(sK2(sK33(sK1(sK0))),sK3(sK2(sK33(sK1(sK0)))))
| ~ spl35_2613 ),
inference(avatar_component_clause,[],[f34060]) ).
fof(f34073,definition,
( spl35_2616
<=> r1(sK33(sK1(sK0)),sK2(sK33(sK1(sK0)))) ),
introduced(definition,[new_symbols(definition,[spl35_2616])],[avatar_definition]) ).
fof(f34075,plain,
( r1(sK33(sK1(sK0)),sK2(sK33(sK1(sK0))))
| ~ spl35_2616 ),
inference(avatar_component_clause,[],[f34073]) ).
fof(f34076,plain,
( spl35_2616
| spl35_149
| ~ spl35_1061 ),
inference(avatar_split_clause,[],[f17520,f17499,f2591,f34073]) ).
fof(f34261,definition,
( spl35_2660
<=> p1(sK4(sK3(sK2(sK33(sK1(sK0)))))) ),
introduced(definition,[new_symbols(definition,[spl35_2660])],[avatar_definition]) ).
fof(f34263,plain,
( p1(sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ spl35_2660 ),
inference(avatar_component_clause,[],[f34261]) ).
fof(f34305,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ r1(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f24067,f9]) ).
fof(f34919,plain,
! [X2,X0,X1] :
( ~ r1(sK0,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(sK2(sK33(sK1(sK0))),sK3(sK2(sK33(sK1(sK0)))))
| ~ r1(X2,sK0) ),
inference(forward_subsumption_resolution,[],[f32585,f9]) ).
fof(f35059,plain,
( spl35_2610
| spl35_149 ),
inference(avatar_split_clause,[],[f34021,f2591,f34023]) ).
fof(f35207,plain,
( spl35_2660
| spl35_149 ),
inference(avatar_split_clause,[],[f34305,f2591,f34261]) ).
fof(f35720,plain,
( spl35_2613
| spl35_149 ),
inference(avatar_split_clause,[],[f34919,f2591,f34060]) ).
fof(f43699,plain,
( ! [X2,X0,X1] :
( ~ r1(sK0,sK1(sK0))
| ~ r1(sK2(sK33(sK1(sK0))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ p1(X2) )
| ~ spl35_2616 ),
inference(resolution,[],[f34075,f60]) ).
fof(f43700,plain,
( ! [X2,X0,X1] :
( ~ r1(sK2(sK33(sK1(sK0))),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ p1(X2) )
| ~ spl35_106
| ~ spl35_2616 ),
inference(forward_subsumption_resolution,[],[f43699,f2302]) ).
fof(f47036,plain,
( ! [X0,X1] :
( ~ r1(sK3(sK2(sK33(sK1(sK0)))),X0)
| ~ r1(X0,X1)
| ~ p1(X1) )
| ~ spl35_106
| ~ spl35_2613
| ~ spl35_2616 ),
inference(resolution,[],[f43700,f34062]) ).
fof(f47065,definition,
( spl35_4159
<=> ! [X0,X1] :
( ~ r1(sK3(sK2(sK33(sK1(sK0)))),X0)
| ~ p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl35_4159])],[avatar_definition]) ).
fof(f47066,plain,
( ! [X0,X1] :
( ~ r1(sK3(sK2(sK33(sK1(sK0)))),X0)
| ~ p1(X1)
| ~ r1(X0,X1) )
| ~ spl35_4159 ),
inference(avatar_component_clause,[],[f47065]) ).
fof(f47103,plain,
( spl35_4159
| ~ spl35_106
| ~ spl35_2613
| ~ spl35_2616 ),
inference(avatar_split_clause,[],[f47036,f34073,f34060,f2301,f47065]) ).
fof(f47332,plain,
( ! [X0] :
( ~ p1(X0)
| ~ r1(sK4(sK3(sK2(sK33(sK1(sK0))))),X0) )
| ~ spl35_2610
| ~ spl35_4159 ),
inference(resolution,[],[f47066,f34025]) ).
fof(f47413,definition,
( spl35_4204
<=> ! [X0] :
( ~ p1(X0)
| ~ r1(sK4(sK3(sK2(sK33(sK1(sK0))))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl35_4204])],[avatar_definition]) ).
fof(f47414,plain,
( ! [X0] :
( ~ r1(sK4(sK3(sK2(sK33(sK1(sK0))))),X0)
| ~ p1(X0) )
| ~ spl35_4204 ),
inference(avatar_component_clause,[],[f47413]) ).
fof(f47457,plain,
( spl35_4204
| ~ spl35_2610
| ~ spl35_4159 ),
inference(avatar_split_clause,[],[f47332,f47065,f34023,f47413]) ).
fof(f47459,plain,
( ~ p1(sK4(sK3(sK2(sK33(sK1(sK0))))))
| ~ spl35_4204 ),
inference(resolution,[],[f47414,f9]) ).
fof(f47536,plain,
( $false
| ~ spl35_2660
| ~ spl35_4204 ),
inference(forward_subsumption_resolution,[],[f47459,f34263]) ).
fof(f47537,plain,
( ~ spl35_2660
| ~ spl35_4204 ),
inference(avatar_contradiction_clause,[],[f47536]) ).
cnf(s98,plain,
spl35_106,
inference(sat_conversion,[],[f2330]) ).
cnf(s897,plain,
~ spl35_925,
inference(sat_conversion,[],[f14330]) ).
cnf(s1042,plain,
( ~ spl35_106
| spl35_1061 ),
inference(sat_conversion,[],[f17505]) ).
cnf(s2689,plain,
( ~ spl35_149
| spl35_925 ),
inference(sat_conversion,[],[f33740]) ).
cnf(s2757,plain,
( spl35_149
| ~ spl35_1061
| spl35_2616 ),
inference(sat_conversion,[],[f34076]) ).
cnf(s3010,plain,
( spl35_149
| spl35_2610 ),
inference(sat_conversion,[],[f35059]) ).
cnf(s3044,plain,
( spl35_149
| spl35_2660 ),
inference(sat_conversion,[],[f35207]) ).
cnf(s3209,plain,
( spl35_149
| spl35_2613 ),
inference(sat_conversion,[],[f35720]) ).
cnf(s5034,plain,
( ~ spl35_106
| ~ spl35_2613
| ~ spl35_2616
| spl35_4159 ),
inference(sat_conversion,[],[f47103]) ).
cnf(s5089,plain,
( ~ spl35_2610
| ~ spl35_4159
| spl35_4204 ),
inference(sat_conversion,[],[f47457]) ).
cnf(s5103,plain,
( ~ spl35_2660
| ~ spl35_4204 ),
inference(sat_conversion,[],[f47537]) ).
cnf(s5121,plain,
~ spl35_149,
inference(rat,[],[s2689,s897]) ).
cnf(s5137,plain,
spl35_2613,
inference(rat,[],[s3209,s5121]) ).
cnf(s5143,plain,
spl35_2660,
inference(rat,[],[s3044,s5121]) ).
cnf(s5144,plain,
spl35_2610,
inference(rat,[],[s3010,s5121]) ).
cnf(s5285,plain,
~ spl35_4204,
inference(rat,[],[s5103,s5143]) ).
cnf(s5286,plain,
~ spl35_4159,
inference(rat,[],[s5089,s5285,s5144]) ).
cnf(s5532,plain,
~ spl35_2616,
inference(rat,[],[s5034,s5286,s5137,s98]) ).
cnf(s5712,plain,
spl35_1061,
inference(rat,[],[s1042,s98]) ).
cnf(s5719,plain,
$false,
inference(rat,[],[s2757,s5121,s5532,s5712]) ).
fof(f47538,plain,
$false,
inference(avatar_sat_refutation,[],[s5719]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL662+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.37 % Computer : n026.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 16:26:41 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.43 Running first-order theorem proving
% 0.10/0.43 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
% 19.87/3.95 % (3046990)Detected formulas, will run a generic FOF schedule.
% 19.87/3.95 % (3047010)dis-21_1_sil=8000:lcm=predicate:random_seed=465400451: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)
% 19.87/3.95 % (3047004)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=387509727:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 19.87/3.95 % (3047007)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2465486768:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 19.87/3.95 % (3047005)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=1491462510:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 19.87/3.95 % (3047006)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=595008446:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 19.87/3.95 % (3047008)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=88568342:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 19.87/3.95 % (3047009)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2889302523:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 19.87/3.95 % (3047010)Instruction limit reached!
% 19.87/3.95 % (3047010)------------------------------
% 19.87/3.95 % (3047010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.95 % (3047010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.95 % (3047010)CaDiCaL version: 2.1.3
% 19.87/3.95 % (3047010)Termination reason: Instruction limit
% 19.87/3.95 % (3047010)Termination phase: Saturation
% 19.87/3.95 % (3047010)Time elapsed: 0.090 s
% 19.87/3.95 % (3047010)Peak memory usage: 89 MB
% 19.87/3.95 % (3047010)Instructions burned: 129 (million)
% 19.87/3.95 % (3047007)Instruction limit reached!
% 19.87/3.95 % (3047007)------------------------------
% 19.87/3.95 % (3047007)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.95 % (3047007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.95 % (3047007)CaDiCaL version: 2.1.3
% 19.87/3.95 % (3047007)Termination reason: Instruction limit
% 19.87/3.95 % (3047007)Termination phase: Saturation
% 19.87/3.95 % (3047007)Time elapsed: 0.101 s
% 19.87/3.95 % (3047007)Peak memory usage: 90 MB
% 19.87/3.95 % (3047007)Instructions burned: 109 (million)
% 19.87/3.95 % (3047008)Instruction limit reached!
% 19.87/3.95 % (3047008)------------------------------
% 19.87/3.95 % (3047008)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.95 % (3047008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.95 % (3047008)CaDiCaL version: 2.1.3
% 19.87/3.95 % (3047008)Termination reason: Instruction limit
% 19.87/3.95 % (3047008)Termination phase: Saturation
% 19.87/3.95 % (3047008)Time elapsed: 0.097 s
% 19.87/3.95 % (3047008)Peak memory usage: 88 MB
% 19.87/3.95 % (3047008)Instructions burned: 120 (million)
% 19.87/3.95 % (3047009)Instruction limit reached!
% 19.87/3.95 % (3047009)------------------------------
% 19.87/3.95 % (3047009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.87/3.95 % (3047009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.87/3.95 % (3047009)CaDiCaL version: 2.1.3
% 19.87/3.95 % (3047009)Termination reason: Instruction limit
% 19.87/3.95 % (3047009)Termination phase: Saturation
% 19.87/3.95 % (3047009)Time elapsed: 0.100 s
% 19.87/3.95 % (3047009)Peak memory usage: 89 MB
% 19.87/3.95 % (3047009)Instructions burned: 141 (million)
% 19.87/3.95 % (3047021)lrs+10_1_sil=8000:sp=occurrence:random_seed=3291707194:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 19.87/3.95 % (3047022)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3305262674:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 19.87/3.95 % (3047023)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3769204572:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 19.87/3.95 % (3047025)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=3955008920:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 19.87/3.95 % (3047021)Instruction limit reached!
% 31.08/5.48 % (3047021)------------------------------
% 31.08/5.48 % (3047021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047021)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047021)Termination reason: Instruction limit
% 31.08/5.48 % (3047021)Termination phase: Saturation
% 31.08/5.48 % (3047021)Time elapsed: 0.230 s
% 31.08/5.48 % (3047021)Peak memory usage: 93 MB
% 31.08/5.48 % (3047021)Instructions burned: 285 (million)
% 31.08/5.48 % (3047022)Instruction limit reached!
% 31.08/5.48 % (3047022)------------------------------
% 31.08/5.48 % (3047022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047022)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047022)Termination reason: Instruction limit
% 31.08/5.48 % (3047022)Termination phase: Saturation
% 31.08/5.48 % (3047022)Time elapsed: 0.124 s
% 31.08/5.48 % (3047022)Peak memory usage: 88 MB
% 31.08/5.48 % (3047022)Instructions burned: 157 (million)
% 31.08/5.48 % (3047025)Instruction limit reached!
% 31.08/5.48 % (3047025)------------------------------
% 31.08/5.48 % (3047025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047025)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047025)Termination reason: Instruction limit
% 31.08/5.48 % (3047025)Termination phase: Saturation
% 31.08/5.48 % (3047025)Time elapsed: 0.201 s
% 31.08/5.48 % (3047025)Peak memory usage: 88 MB
% 31.08/5.48 % (3047025)Instructions burned: 248 (million)
% 31.08/5.48 % (3047023)Instruction limit reached!
% 31.08/5.48 % (3047023)------------------------------
% 31.08/5.48 % (3047023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047023)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047023)Termination reason: Instruction limit
% 31.08/5.48 % (3047023)Termination phase: Saturation
% 31.08/5.48 % (3047023)Time elapsed: 0.209 s
% 31.08/5.48 % (3047023)Peak memory usage: 91 MB
% 31.08/5.48 % (3047023)Instructions burned: 326 (million)
% 31.08/5.48 % (3047033)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3765262258:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2993 on theBenchmark for (2993ds/294Mi)
% 31.08/5.48 % (3047034)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3579204333:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 31.08/5.48 % (3047036)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2406843703:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 31.08/5.48 % (3047035)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=4088955009:cts=off:i=113:fsr=off:ss=included:sgt=4_2992 on theBenchmark for (2992ds/113Mi)
% 31.08/5.48 % (3047033)Instruction limit reached!
% 31.08/5.48 % (3047033)------------------------------
% 31.08/5.48 % (3047033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047033)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047033)Termination reason: Instruction limit
% 31.08/5.48 % (3047033)Termination phase: Saturation
% 31.08/5.48 % (3047033)Time elapsed: 0.236 s
% 31.08/5.48 % (3047033)Peak memory usage: 89 MB
% 31.08/5.48 % (3047033)Instructions burned: 294 (million)
% 31.08/5.48 % (3047035)Instruction limit reached!
% 31.08/5.48 % (3047035)------------------------------
% 31.08/5.48 % (3047035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047035)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047035)Termination reason: Instruction limit
% 31.08/5.48 % (3047035)Termination phase: Saturation
% 31.08/5.48 % (3047035)Time elapsed: 0.091 s
% 31.08/5.48 % (3047035)Peak memory usage: 89 MB
% 31.08/5.48 % (3047035)Instructions burned: 113 (million)
% 31.08/5.48 % (3047036)Instruction limit reached!
% 31.08/5.48 % (3047036)------------------------------
% 31.08/5.48 % (3047036)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.08/5.48 % (3047036)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.08/5.48 % (3047036)CaDiCaL version: 2.1.3
% 31.08/5.48 % (3047036)Termination reason: Instruction limit
% 31.08/5.48 % (3047036)Termination phase: Saturation
% 43.62/10.20 % (3047036)Time elapsed: 0.111 s
% 43.62/10.20 % (3047036)Peak memory usage: 89 MB
% 43.62/10.20 % (3047036)Instructions burned: 128 (million)
% 43.62/10.20 % (3047041)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=1313003254:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2989 on theBenchmark for (2989ds/114Mi)
% 43.62/10.20 % (3047044)lrs+10_1_sil=8000:sp=occurrence:random_seed=1937251300:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2988 on theBenchmark for (2988ds/907Mi)
% 43.62/10.20 % (3047045)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2810430165:i=437:sd=1:aac=none:ss=included_2988 on theBenchmark for (2988ds/437Mi)
% 43.62/10.20 % (3047041)Instruction limit reached!
% 43.62/10.20 % (3047041)------------------------------
% 43.62/10.20 % (3047041)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047041)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047041)Termination reason: Instruction limit
% 43.62/10.20 % (3047041)Termination phase: Saturation
% 43.62/10.20 % (3047041)Time elapsed: 0.096 s
% 43.62/10.20 % (3047041)Peak memory usage: 89 MB
% 43.62/10.20 % (3047041)Instructions burned: 114 (million)
% 43.62/10.20 % (3047045)Instruction limit reached!
% 43.62/10.20 % (3047045)------------------------------
% 43.62/10.20 % (3047045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047045)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047045)Termination reason: Instruction limit
% 43.62/10.20 % (3047045)Termination phase: Saturation
% 43.62/10.20 % (3047045)Time elapsed: 0.264 s
% 43.62/10.20 % (3047045)Peak memory usage: 89 MB
% 43.62/10.20 % (3047045)Instructions burned: 437 (million)
% 43.62/10.20 % (3047049)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1823539727:i=5202:ss=axioms:sgt=16_2985 on theBenchmark for (2985ds/5202Mi)
% 43.62/10.20 % (3047050)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4106577186:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2983 on theBenchmark for (2983ds/134Mi)
% 43.62/10.20 % (3047050)Instruction limit reached!
% 43.62/10.20 % (3047050)------------------------------
% 43.62/10.20 % (3047050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047050)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047050)Termination reason: Instruction limit
% 43.62/10.20 % (3047050)Termination phase: Saturation
% 43.62/10.20 % (3047050)Time elapsed: 0.095 s
% 43.62/10.20 % (3047050)Peak memory usage: 89 MB
% 43.62/10.20 % (3047050)Instructions burned: 137 (million)
% 43.62/10.20 % (3047053)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=176703010:st=8:i=592:sd=3:ep=RST:ss=axioms_2980 on theBenchmark for (2980ds/592Mi)
% 43.62/10.20 % (3047044)Instruction limit reached!
% 43.62/10.20 % (3047044)------------------------------
% 43.62/10.20 % (3047044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047044)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047044)Termination reason: Instruction limit
% 43.62/10.20 % (3047044)Termination phase: Saturation
% 43.62/10.20 % (3047044)Time elapsed: 0.785 s
% 43.62/10.20 % (3047044)Peak memory usage: 103 MB
% 43.62/10.20 % (3047044)Instructions burned: 907 (million)
% 43.62/10.20 % (3047055)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=609073501:st=3:i=13193:sd=3:ss=axioms_2978 on theBenchmark for (2978ds/13193Mi)
% 43.62/10.20 % (3047053)Instruction limit reached!
% 43.62/10.20 % (3047053)------------------------------
% 43.62/10.20 % (3047053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047053)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047053)Termination reason: Instruction limit
% 43.62/10.20 % (3047053)Termination phase: Saturation
% 43.62/10.20 % (3047053)Time elapsed: 0.479 s
% 43.62/10.20 % (3047053)Peak memory usage: 94 MB
% 43.62/10.20 % (3047053)Instructions burned: 593 (million)
% 43.62/10.20 % (3047060)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=3181110389:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/125Mi)
% 43.62/10.20 % (3047060)Instruction limit reached!
% 43.62/10.20 % (3047060)------------------------------
% 43.62/10.20 % (3047060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047060)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047060)Termination reason: Instruction limit
% 43.62/10.20 % (3047060)Termination phase: Saturation
% 43.62/10.20 % (3047060)Time elapsed: 0.140 s
% 43.62/10.20 % (3047060)Peak memory usage: 91 MB
% 43.62/10.20 % (3047060)Instructions burned: 125 (million)
% 43.62/10.20 % (3047062)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3732682953:i=134:gtgl=5:slsql=off:gtg=exists_sym_2969 on theBenchmark for (2969ds/134Mi)
% 43.62/10.20 % (3047034)Instruction limit reached!
% 43.62/10.20 % (3047034)------------------------------
% 43.62/10.20 % (3047034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047034)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047034)Termination reason: Instruction limit
% 43.62/10.20 % (3047034)Termination phase: Saturation
% 43.62/10.20 % (3047034)Time elapsed: 2.456 s
% 43.62/10.20 % (3047034)Peak memory usage: 141 MB
% 43.62/10.20 % (3047034)Instructions burned: 2350 (million)
% 43.62/10.20 % (3047062)Instruction limit reached!
% 43.62/10.20 % (3047062)------------------------------
% 43.62/10.20 % (3047062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047062)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047062)Termination reason: Instruction limit
% 43.62/10.20 % (3047062)Termination phase: Saturation
% 43.62/10.20 % (3047062)Time elapsed: 0.132 s
% 43.62/10.20 % (3047062)Peak memory usage: 91 MB
% 43.62/10.20 % (3047062)Instructions burned: 135 (million)
% 43.62/10.20 % (3047064)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2335421668:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2965 on theBenchmark for (2965ds/141Mi)
% 43.62/10.20 % (3047064)Instruction limit reached!
% 43.62/10.20 % (3047064)------------------------------
% 43.62/10.20 % (3047064)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047064)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047064)Termination reason: Instruction limit
% 43.62/10.20 % (3047064)Termination phase: Saturation
% 43.62/10.20 % (3047064)Time elapsed: 0.133 s
% 43.62/10.20 % (3047064)Peak memory usage: 91 MB
% 43.62/10.20 % (3047064)Instructions burned: 142 (million)
% 43.62/10.20 % (3047065)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3890920517:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2965 on theBenchmark for (2965ds/431Mi)
% 43.62/10.20 % (3047068)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=427336404:i=6060:aac=none:ins=25_2962 on theBenchmark for (2962ds/6060Mi)
% 43.62/10.20 % (3047065)Instruction limit reached!
% 43.62/10.20 % (3047065)------------------------------
% 43.62/10.20 % (3047065)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047065)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047065)Termination reason: Instruction limit
% 43.62/10.20 % (3047065)Termination phase: Saturation
% 43.62/10.20 % (3047065)Time elapsed: 0.354 s
% 43.62/10.20 % (3047065)Peak memory usage: 91 MB
% 43.62/10.20 % (3047065)Instructions burned: 432 (million)
% 43.62/10.20 % (3047072)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1451421088:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2959 on theBenchmark for (2959ds/150Mi)
% 43.62/10.20 % (3047072)Instruction limit reached!
% 43.62/10.20 % (3047072)------------------------------
% 43.62/10.20 % (3047072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047072)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047072)Termination reason: Instruction limit
% 43.62/10.20 % (3047072)Termination phase: Saturation
% 43.62/10.20 % (3047072)Time elapsed: 0.129 s
% 43.62/10.20 % (3047072)Peak memory usage: 92 MB
% 43.62/10.20 % (3047072)Instructions burned: 151 (million)
% 43.62/10.20 % (3047074)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=825631693:i=14155:bd=all_2955 on theBenchmark for (2955ds/14155Mi)
% 43.62/10.20 % (3047049)Instruction limit reached!
% 43.62/10.20 % (3047049)------------------------------
% 43.62/10.20 % (3047049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047049)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047049)Termination reason: Instruction limit
% 43.62/10.20 % (3047049)Termination phase: Saturation
% 43.62/10.20 % (3047049)Time elapsed: 4.736 s
% 43.62/10.20 % (3047049)Peak memory usage: 167 MB
% 43.62/10.20 % (3047049)Instructions burned: 5202 (million)
% 43.62/10.20 % (3047080)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3935019946:i=667:av=off:fsr=off_2935 on theBenchmark for (2935ds/667Mi)
% 43.62/10.20 % (3047080)Instruction limit reached!
% 43.62/10.20 % (3047080)------------------------------
% 43.62/10.20 % (3047080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047080)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047080)Termination reason: Instruction limit
% 43.62/10.20 % (3047080)Termination phase: Saturation
% 43.62/10.20 % (3047080)Time elapsed: 0.468 s
% 43.62/10.20 % (3047080)Peak memory usage: 105 MB
% 43.62/10.20 % (3047080)Instructions burned: 668 (million)
% 43.62/10.20 % (3047082)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3878331476:s2a=on:i=185:s2at=1.8:fdi=4_2928 on theBenchmark for (2928ds/185Mi)
% 43.62/10.20 % (3047082)Instruction limit reached!
% 43.62/10.20 % (3047082)------------------------------
% 43.62/10.20 % (3047082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047082)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047082)Termination reason: Instruction limit
% 43.62/10.20 % (3047082)Termination phase: Saturation
% 43.62/10.20 % (3047082)Time elapsed: 0.158 s
% 43.62/10.20 % (3047082)Peak memory usage: 90 MB
% 43.62/10.20 % (3047082)Instructions burned: 185 (million)
% 43.62/10.20 % (3047086)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3825878653:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2924 on theBenchmark for (2924ds/193Mi)
% 43.62/10.20 % (3047086)Instruction limit reached!
% 43.62/10.20 % (3047086)------------------------------
% 43.62/10.20 % (3047086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.62/10.20 % (3047086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.62/10.20 % (3047086)CaDiCaL version: 2.1.3
% 43.62/10.20 % (3047086)Termination reason: Instruction limit
% 43.62/10.20 % (3047086)Termination phase: Saturation
% 43.62/10.20 % (3047086)Time elapsed: 0.179 s
% 43.62/10.20 % (3047086)Peak memory usage: 93 MB
% 43.62/10.20 % (3047086)Instructions burned: 193 (million)
% 43.62/10.20 % (3047090)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3608081513:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2920 on theBenchmark for (2920ds/4850Mi)
% 43.62/10.20 % (3047004)First to succeed.
% 43.62/10.20 % (3047004)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3046990"
% 43.62/10.20 % (3047004)Refutation found. Thanks to Tanya!
% 43.62/10.20 % SZS status Theorem for theBenchmark
% 43.62/10.20 % SZS output start Proof for theBenchmark
% See solution above
% 65.67/10.48 % (3047004)------------------------------
% 65.67/10.48 % (3047004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 65.67/10.48 % (3047004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 65.67/10.48 % (3047004)CaDiCaL version: 2.1.3
% 65.67/10.48 % (3047004)Termination reason: Refutation
% 65.67/10.48 % (3047004)Time elapsed: 8.469 s
% 65.67/10.48 % (3047004)Peak memory usage: 187 MB
% 65.67/10.48 % (3047004)Instructions burned: 8681 (million)
% 65.67/10.48 % (3047004)------------------------------
% 65.67/10.48 % (3047004)------------------------------
% 65.67/10.48 % (3046990)Success in time 9.156 s
% 65.67/10.48 % Vampire exiting
%------------------------------------------------------------------------------