%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:59:07 AM UTC 2026
% Result : Theorem 40.57s 6.17s
% Output : Refutation 40.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 43
% Syntax : Number of formulae : 455 ( 27 unt; 42 def)
% Number of atoms : 4198 ( 0 equ)
% Maximal formula atoms : 239 ( 9 avg)
% Number of connectives : 6757 (3014 ~;3211 |; 494 &)
% ( 38 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 47 ( 8 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 45 ( 44 usr; 39 prp; 0-2 aty)
% Number of functors : 46 ( 46 usr; 9 con; 0-1 aty)
% Number of variables : 2078 ( 0 sgn1881 !; 197 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) )
| ~ ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ( ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| ( ( p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p1(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) )
| ~ p1(X1) ) ) )
& ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p1(X0) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| p1(X11) ) )
| ~ ! [X12] :
( ~ r1(X9,X12)
| p1(X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ~ ! [X18] :
( ~ r1(X15,X18)
| p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X26,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ~ ! [X51] :
( ~ r1(X48,X51)
| p1(X51) ) ) ) ) ) ) ) ) ) )
| ~ ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) )
| ~ p1(X60) ) )
| ~ ! [X62] :
( ~ r1(X57,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p1(X63) )
| ~ p1(X62)
| ~ ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ~ ( ! [X67] :
( ~ r1(X64,X67)
| p1(X67) )
| ~ p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ~ ! [X70] :
( ~ r1(X57,X70)
| p1(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ~ ! [X76] :
( ~ r1(X73,X76)
| p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| p1(X80) )
| ~ p1(X79) ) ) )
| ~ ! [X81] :
( ~ r1(X57,X81)
| p1(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90) )
| ! [X91] :
( ~ r1(X89,X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
| ~ ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p1(X95) )
| ~ p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| p1(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ~ ! [X109] :
( ~ r1(X106,X109)
| p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| p1(X115) ) )
| ~ ! [X116] :
( ~ r1(X113,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ~ ! [X122] :
( ~ r1(X119,X122)
| p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p1(X127) ) )
| ~ ! [X128] :
( ~ r1(X125,X128)
| p1(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ~ ! [X134] :
( ~ r1(X131,X134)
| p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p1(X138) ) )
| ~ ! [X139] :
( ~ r1(X136,X139)
| p1(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ~ ! [X148] :
( ~ r1(X147,X148)
| p1(X148) ) )
| ~ ! [X149] :
( ~ r1(X146,X149)
| p1(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ~ ! [X155] :
( ~ r1(X152,X155)
| p1(X155) ) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| p1(X11) ) )
| ~ ! [X12] :
( ~ r1(X9,X12)
| p1(X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ~ ! [X18] :
( ~ r1(X15,X18)
| p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| p1(X28) ) )
| ~ ! [X29] :
( ~ r1(X26,X29)
| p1(X29)
| ~ ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ~ ! [X35] :
( ~ r1(X32,X35)
| p1(X35) ) ) ) ) ) ) ) ) ) ) )
| ~ ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ~ ! [X44] :
( ~ r1(X43,X44)
| p1(X44) ) )
| ~ ! [X45] :
( ~ r1(X42,X45)
| p1(X45)
| ~ ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ~ ! [X51] :
( ~ r1(X48,X51)
| p1(X51) ) ) ) ) ) ) ) ) ) )
| ~ ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ~ ! [X60] :
( ~ r1(X59,X60)
| ! [X61] :
( ~ r1(X60,X61)
| p1(X61) )
| ~ p1(X60) ) )
| ~ ! [X62] :
( ~ r1(X57,X62)
| ! [X63] :
( ~ r1(X62,X63)
| p1(X63) )
| ~ p1(X62)
| ~ ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ~ ( ! [X67] :
( ~ r1(X64,X67)
| p1(X67) )
| ~ p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ~ ! [X69] :
( ~ r1(X68,X69)
| p1(X69) ) )
| ~ ! [X70] :
( ~ r1(X57,X70)
| p1(X70)
| ~ ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ~ ! [X76] :
( ~ r1(X73,X76)
| p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ~ ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| p1(X80) )
| ~ p1(X79) ) ) )
| ~ ! [X81] :
( ~ r1(X57,X81)
| p1(X81)
| ~ ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
| ~ ( ~ ! [X84] :
( ~ r1(X0,X84)
| ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| ! [X87] :
( ~ r1(X86,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90) )
| ! [X91] :
( ~ r1(X89,X91)
| ~ ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
| ~ ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ~ ! [X94] :
( ~ r1(X93,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p1(X95) )
| ~ p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ~ ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| p1(X103)
| ~ ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ~ ! [X109] :
( ~ r1(X106,X109)
| p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ~ ! [X115] :
( ~ r1(X114,X115)
| p1(X115) ) )
| ~ ! [X116] :
( ~ r1(X113,X116)
| p1(X116)
| ~ ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ~ ! [X122] :
( ~ r1(X119,X122)
| p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ~ ! [X127] :
( ~ r1(X126,X127)
| p1(X127) ) )
| ~ ! [X128] :
( ~ r1(X125,X128)
| p1(X128)
| ~ ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ~ ! [X134] :
( ~ r1(X131,X134)
| p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ~ ! [X138] :
( ~ r1(X137,X138)
| p1(X138) ) )
| ~ ! [X139] :
( ~ r1(X136,X139)
| p1(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ~ ! [X145] :
( ~ r1(X142,X145)
| p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ~ ! [X148] :
( ~ r1(X147,X148)
| p1(X148) ) )
| ~ ! [X149] :
( ~ r1(X146,X149)
| p1(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ~ ! [X155] :
( ~ r1(X152,X155)
| p1(X155) ) ) ) ) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( ( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) ) )
& ( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) ) )
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,definition,
! [X57] :
( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ~ sP0(X57) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X57] :
( ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) )
| ~ sP1(X57) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X57] :
( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) )
| ~ sP2(X57) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X57] :
( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| sP1(X57)
| ~ sP3(X57) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X73] :
( ~ r1(X57,X73)
| ! [X74] :
( ~ r1(X73,X74)
| ! [X75] :
( ~ r1(X74,X75)
| p1(X75) ) )
| ? [X76] :
( r1(X73,X76)
& ~ p1(X76) ) )
& ( sP0(X57)
| ? [X81] :
( r1(X57,X81)
& ~ p1(X81)
& ! [X82] :
( ~ r1(X81,X82)
| ! [X83] :
( ~ r1(X82,X83)
| p1(X83) )
| ~ p1(X82) ) ) ) ) ) ) ) ) ) )
& ? [X84] :
( r1(X0,X84)
& ? [X85] :
( r1(X84,X85)
& ? [X86] :
( r1(X85,X86)
& ? [X87] :
( r1(X86,X87)
& ? [X88] :
( r1(X87,X88)
& ? [X89] :
( r1(X88,X89)
& ? [X90] :
( r1(X89,X90)
& ~ p1(X90) )
& ? [X91] :
( r1(X89,X91)
& ! [X92] :
( ~ r1(X91,X92)
| p1(X92) ) )
& ! [X93] :
( ~ r1(X89,X93)
| p1(X93)
| ? [X94] :
( r1(X93,X94)
& ? [X95] :
( r1(X94,X95)
& ~ p1(X95) )
& p1(X94) ) ) ) ) ) ) ) )
& ! [X96] :
( ~ r1(X0,X96)
| ! [X97] :
( ~ r1(X96,X97)
| ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| ! [X100] :
( ~ r1(X99,X100)
| ( ( p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| ? [X102] :
( r1(X101,X102)
& ~ p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103)
& ! [X104] :
( ~ r1(X103,X104)
| ! [X105] :
( ~ r1(X104,X105)
| p1(X105) )
| ~ p1(X104) ) ) )
& ! [X106] :
( ~ r1(X100,X106)
| ! [X107] :
( ~ r1(X106,X107)
| ! [X108] :
( ~ r1(X107,X108)
| p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109) ) ) ) ) ) ) ) )
& ! [X110] :
( ~ r1(X0,X110)
| ! [X111] :
( ~ r1(X110,X111)
| ! [X112] :
( ~ r1(X111,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ( ( p1(X113)
| ! [X114] :
( ~ r1(X113,X114)
| ? [X115] :
( r1(X114,X115)
& ~ p1(X115) ) )
| ? [X116] :
( r1(X113,X116)
& ~ p1(X116)
& ! [X117] :
( ~ r1(X116,X117)
| ! [X118] :
( ~ r1(X117,X118)
| p1(X118) )
| ~ p1(X117) ) ) )
& ! [X119] :
( ~ r1(X113,X119)
| ! [X120] :
( ~ r1(X119,X120)
| ! [X121] :
( ~ r1(X120,X121)
| p1(X121) ) )
| ? [X122] :
( r1(X119,X122)
& ~ p1(X122) ) ) ) ) ) ) )
& ! [X123] :
( ~ r1(X0,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| ( ( p1(X125)
| ! [X126] :
( ~ r1(X125,X126)
| ? [X127] :
( r1(X126,X127)
& ~ p1(X127) ) )
| ? [X128] :
( r1(X125,X128)
& ~ p1(X128)
& ! [X129] :
( ~ r1(X128,X129)
| ! [X130] :
( ~ r1(X129,X130)
| p1(X130) )
| ~ p1(X129) ) ) )
& ! [X131] :
( ~ r1(X125,X131)
| ! [X132] :
( ~ r1(X131,X132)
| ! [X133] :
( ~ r1(X132,X133)
| p1(X133) ) )
| ? [X134] :
( r1(X131,X134)
& ~ p1(X134) ) ) ) ) ) )
& ! [X135] :
( ~ r1(X0,X135)
| ! [X136] :
( ~ r1(X135,X136)
| ( ( p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| ? [X138] :
( r1(X137,X138)
& ~ p1(X138) ) )
| ? [X139] :
( r1(X136,X139)
& ~ p1(X139)
& ! [X140] :
( ~ r1(X139,X140)
| ! [X141] :
( ~ r1(X140,X141)
| p1(X141) )
| ~ p1(X140) ) ) )
& ! [X142] :
( ~ r1(X136,X142)
| ! [X143] :
( ~ r1(X142,X143)
| ! [X144] :
( ~ r1(X143,X144)
| p1(X144) ) )
| ? [X145] :
( r1(X142,X145)
& ~ p1(X145) ) ) ) ) )
& ! [X146] :
( ~ r1(X0,X146)
| ( ( p1(X146)
| ! [X147] :
( ~ r1(X146,X147)
| ? [X148] :
( r1(X147,X148)
& ~ p1(X148) ) )
| ? [X149] :
( r1(X146,X149)
& ~ p1(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p1(X151) )
| ~ p1(X150) ) ) )
& ! [X152] :
( ~ r1(X146,X152)
| ! [X153] :
( ~ r1(X152,X153)
| ! [X154] :
( ~ r1(X153,X154)
| p1(X154) ) )
| ? [X155] :
( r1(X152,X155)
& ~ p1(X155) ) ) ) ) ),
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f12,plain,
! [X57] :
( ! [X58] :
( ~ r1(X57,X58)
| p1(X58) )
| ~ p1(X57)
| ! [X59] :
( ~ r1(X57,X59)
| ? [X60] :
( r1(X59,X60)
& ? [X61] :
( r1(X60,X61)
& ~ p1(X61) )
& p1(X60) ) )
| sP1(X57)
| ~ sP3(X57) ),
inference(nnf_transformation,[],[f10]) ).
fof(f13,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(rectify,[],[f12]) ).
fof(f14,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| p1(X1) )
| ~ p1(X0)
| ! [X2] :
( ~ r1(X0,X2)
| ( r1(X2,sK4(X2))
& r1(sK4(X2),sK5(X2))
& ~ p1(sK5(X2))
& p1(sK4(X2)) ) )
| sP1(X0)
| ~ sP3(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f13]) ).
fof(f15,plain,
! [X57] :
( p1(X57)
| ! [X68] :
( ~ r1(X57,X68)
| ? [X69] :
( r1(X68,X69)
& ~ p1(X69) ) )
| ? [X70] :
( r1(X57,X70)
& ~ p1(X70)
& ! [X71] :
( ~ r1(X70,X71)
| ! [X72] :
( ~ r1(X71,X72)
| p1(X72) )
| ~ p1(X71) ) )
| ~ sP2(X57) ),
inference(nnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ? [X2] :
( r1(X1,X2)
& ~ p1(X2) ) )
| ? [X3] :
( r1(X0,X3)
& ~ p1(X3)
& ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(rectify,[],[f15]) ).
fof(f17,plain,
! [X0] :
( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( r1(X1,sK6(X1))
& ~ p1(sK6(X1)) ) )
| ( r1(X0,sK7(X0))
& ~ p1(sK7(X0))
& ! [X4] :
( ~ r1(sK7(X0),X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) ) )
| ~ sP2(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f16]) ).
fof(f18,plain,
! [X57] :
( ? [X62] :
( r1(X57,X62)
& ? [X63] :
( r1(X62,X63)
& ~ p1(X63) )
& p1(X62)
& ! [X64] :
( ~ r1(X62,X64)
| ! [X65] :
( ~ r1(X64,X65)
| ! [X66] :
( ~ r1(X65,X66)
| p1(X66) )
| ~ p1(X65) )
| ( ? [X67] :
( r1(X64,X67)
& ~ p1(X67) )
& p1(X64) ) ) )
| ~ sP1(X57) ),
inference(nnf_transformation,[],[f8]) ).
fof(f19,plain,
! [X0] :
( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p1(X2) )
& p1(X1)
& ! [X3] :
( ~ r1(X1,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( ? [X6] :
( r1(X3,X6)
& ~ p1(X6) )
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ( r1(X0,sK8(X0))
& r1(sK8(X0),sK9(X0))
& ~ p1(sK9(X0))
& p1(sK8(X0))
& ! [X3] :
( ~ r1(sK8(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| p1(X5) )
| ~ p1(X4) )
| ( r1(X3,sK10(X3))
& ~ p1(sK10(X3))
& p1(X3) ) ) )
| ~ sP1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f19]) ).
fof(f21,plain,
! [X57] :
( ! [X77] :
( ~ r1(X57,X77)
| ! [X78] :
( ~ r1(X77,X78)
| p1(X78)
| ? [X79] :
( r1(X78,X79)
& ? [X80] :
( r1(X79,X80)
& ~ p1(X80) )
& p1(X79) ) ) )
| ~ sP0(X57) ),
inference(nnf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p1(X4) )
& p1(X3) ) ) )
| ~ sP0(X0) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2)
| ( r1(X2,sK11(X2))
& r1(sK11(X2),sK12(X2))
& ~ p1(sK12(X2))
& p1(sK11(X2)) ) ) )
| ~ sP0(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f22]) ).
fof(f24,plain,
? [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ? [X11] :
( r1(X10,X11)
& ~ p1(X11) ) )
| ? [X12] :
( r1(X9,X12)
& ~ p1(X12)
& ! [X13] :
( ~ r1(X12,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ? [X18] :
( r1(X15,X18)
& ~ p1(X18) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(X0,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ? [X28] :
( r1(X27,X28)
& ~ p1(X28) ) )
| ? [X29] :
( r1(X26,X29)
& ~ p1(X29)
& ! [X30] :
( ~ r1(X29,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ? [X35] :
( r1(X32,X35)
& ~ p1(X35) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(X0,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ? [X44] :
( r1(X43,X44)
& ~ p1(X44) ) )
| ? [X45] :
( r1(X42,X45)
& ~ p1(X45)
& ! [X46] :
( ~ r1(X45,X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ? [X51] :
( r1(X48,X51)
& ~ p1(X51) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(X0,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60) ) )
| ? [X61] :
( r1(X58,X61)
& ~ p1(X61) ) )
& ( sP0(X57)
| ? [X62] :
( r1(X57,X62)
& ~ p1(X62)
& ! [X63] :
( ~ r1(X62,X63)
| ! [X64] :
( ~ r1(X63,X64)
| p1(X64) )
| ~ p1(X63) ) ) ) ) ) ) ) ) ) )
& ? [X65] :
( r1(X0,X65)
& ? [X66] :
( r1(X65,X66)
& ? [X67] :
( r1(X66,X67)
& ? [X68] :
( r1(X67,X68)
& ? [X69] :
( r1(X68,X69)
& ? [X70] :
( r1(X69,X70)
& ? [X71] :
( r1(X70,X71)
& ~ p1(X71) )
& ? [X72] :
( r1(X70,X72)
& ! [X73] :
( ~ r1(X72,X73)
| p1(X73) ) )
& ! [X74] :
( ~ r1(X70,X74)
| p1(X74)
| ? [X75] :
( r1(X74,X75)
& ? [X76] :
( r1(X75,X76)
& ~ p1(X76) )
& p1(X75) ) ) ) ) ) ) ) )
& ! [X77] :
( ~ r1(X0,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ( ( p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| ? [X83] :
( r1(X82,X83)
& ~ p1(X83) ) )
| ? [X84] :
( r1(X81,X84)
& ~ p1(X84)
& ! [X85] :
( ~ r1(X84,X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) )
| ~ p1(X85) ) ) )
& ! [X87] :
( ~ r1(X81,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| p1(X89) ) )
| ? [X90] :
( r1(X87,X90)
& ~ p1(X90) ) ) ) ) ) ) ) )
& ! [X91] :
( ~ r1(X0,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ( ( p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| ? [X96] :
( r1(X95,X96)
& ~ p1(X96) ) )
| ? [X97] :
( r1(X94,X97)
& ~ p1(X97)
& ! [X98] :
( ~ r1(X97,X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) ) )
& ! [X100] :
( ~ r1(X94,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ? [X103] :
( r1(X100,X103)
& ~ p1(X103) ) ) ) ) ) ) )
& ! [X104] :
( ~ r1(X0,X104)
| ! [X105] :
( ~ r1(X104,X105)
| ! [X106] :
( ~ r1(X105,X106)
| ( ( p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| ? [X108] :
( r1(X107,X108)
& ~ p1(X108) ) )
| ? [X109] :
( r1(X106,X109)
& ~ p1(X109)
& ! [X110] :
( ~ r1(X109,X110)
| ! [X111] :
( ~ r1(X110,X111)
| p1(X111) )
| ~ p1(X110) ) ) )
& ! [X112] :
( ~ r1(X106,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| p1(X114) ) )
| ? [X115] :
( r1(X112,X115)
& ~ p1(X115) ) ) ) ) ) )
& ! [X116] :
( ~ r1(X0,X116)
| ! [X117] :
( ~ r1(X116,X117)
| ( ( p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| ? [X119] :
( r1(X118,X119)
& ~ p1(X119) ) )
| ? [X120] :
( r1(X117,X120)
& ~ p1(X120)
& ! [X121] :
( ~ r1(X120,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) )
| ~ p1(X121) ) ) )
& ! [X123] :
( ~ r1(X117,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ? [X126] :
( r1(X123,X126)
& ~ p1(X126) ) ) ) ) )
& ! [X127] :
( ~ r1(X0,X127)
| ( ( p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| ? [X129] :
( r1(X128,X129)
& ~ p1(X129) ) )
| ? [X130] :
( r1(X127,X130)
& ~ p1(X130)
& ! [X131] :
( ~ r1(X130,X131)
| ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131) ) ) )
& ! [X133] :
( ~ r1(X127,X133)
| ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) ) )
| ? [X136] :
( r1(X133,X136)
& ~ p1(X136) ) ) ) ) ),
inference(rectify,[],[f11]) ).
fof(f25,plain,
( ! [X1] :
( ~ r1(sK13,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| ! [X5] :
( ~ r1(X4,X5)
| ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| ! [X9] :
( ~ r1(X8,X9)
| ( ( p1(X9)
| ! [X10] :
( ~ r1(X9,X10)
| ( r1(X10,sK14(X10))
& ~ p1(sK14(X10)) ) )
| ( r1(X9,sK15(X9))
& ~ p1(sK15(X9))
& ! [X13] :
( ~ r1(sK15(X9),X13)
| ! [X14] :
( ~ r1(X13,X14)
| p1(X14) )
| ~ p1(X13) ) ) )
& ! [X15] :
( ~ r1(X9,X15)
| ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p1(X17) ) )
| ( r1(X15,sK16(X15))
& ~ p1(sK16(X15)) ) ) ) ) ) ) ) ) ) ) ) )
& ! [X19] :
( ~ r1(sK13,X19)
| ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| ! [X22] :
( ~ r1(X21,X22)
| ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| ( ( p1(X26)
| ! [X27] :
( ~ r1(X26,X27)
| ( r1(X27,sK17(X27))
& ~ p1(sK17(X27)) ) )
| ( r1(X26,sK18(X26))
& ~ p1(sK18(X26))
& ! [X30] :
( ~ r1(sK18(X26),X30)
| ! [X31] :
( ~ r1(X30,X31)
| p1(X31) )
| ~ p1(X30) ) ) )
& ! [X32] :
( ~ r1(X26,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ! [X34] :
( ~ r1(X33,X34)
| p1(X34) ) )
| ( r1(X32,sK19(X32))
& ~ p1(sK19(X32)) ) ) ) ) ) ) ) ) ) ) )
& ! [X36] :
( ~ r1(sK13,X36)
| ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| ! [X41] :
( ~ r1(X40,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( p1(X42)
| ! [X43] :
( ~ r1(X42,X43)
| ( r1(X43,sK20(X43))
& ~ p1(sK20(X43)) ) )
| ( r1(X42,sK21(X42))
& ~ p1(sK21(X42))
& ! [X46] :
( ~ r1(sK21(X42),X46)
| ! [X47] :
( ~ r1(X46,X47)
| p1(X47) )
| ~ p1(X46) ) ) )
& ! [X48] :
( ~ r1(X42,X48)
| ! [X49] :
( ~ r1(X48,X49)
| ! [X50] :
( ~ r1(X49,X50)
| p1(X50) ) )
| ( r1(X48,sK22(X48))
& ~ p1(sK22(X48)) ) ) ) ) ) ) ) ) ) )
& ! [X52] :
( ~ r1(sK13,X52)
| ! [X53] :
( ~ r1(X52,X53)
| ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| ! [X56] :
( ~ r1(X55,X56)
| ! [X57] :
( ~ r1(X56,X57)
| ( sP3(X57)
& sP2(X57)
& ! [X58] :
( ~ r1(X57,X58)
| ! [X59] :
( ~ r1(X58,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60) ) )
| ( r1(X58,sK23(X58))
& ~ p1(sK23(X58)) ) )
& ( sP0(X57)
| ( r1(X57,sK24(X57))
& ~ p1(sK24(X57))
& ! [X63] :
( ~ r1(sK24(X57),X63)
| ! [X64] :
( ~ r1(X63,X64)
| p1(X64) )
| ~ p1(X63) ) ) ) ) ) ) ) ) ) )
& r1(sK13,sK25)
& r1(sK25,sK26)
& r1(sK26,sK27)
& r1(sK27,sK28)
& r1(sK28,sK29)
& r1(sK29,sK30)
& r1(sK30,sK31)
& ~ p1(sK31)
& r1(sK30,sK32)
& ! [X73] :
( ~ r1(sK32,X73)
| p1(X73) )
& ! [X74] :
( ~ r1(sK30,X74)
| p1(X74)
| ( r1(X74,sK33(X74))
& r1(sK33(X74),sK34(X74))
& ~ p1(sK34(X74))
& p1(sK33(X74)) ) )
& ! [X77] :
( ~ r1(sK13,X77)
| ! [X78] :
( ~ r1(X77,X78)
| ! [X79] :
( ~ r1(X78,X79)
| ! [X80] :
( ~ r1(X79,X80)
| ! [X81] :
( ~ r1(X80,X81)
| ( ( p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| ( r1(X82,sK35(X82))
& ~ p1(sK35(X82)) ) )
| ( r1(X81,sK36(X81))
& ~ p1(sK36(X81))
& ! [X85] :
( ~ r1(sK36(X81),X85)
| ! [X86] :
( ~ r1(X85,X86)
| p1(X86) )
| ~ p1(X85) ) ) )
& ! [X87] :
( ~ r1(X81,X87)
| ! [X88] :
( ~ r1(X87,X88)
| ! [X89] :
( ~ r1(X88,X89)
| p1(X89) ) )
| ( r1(X87,sK37(X87))
& ~ p1(sK37(X87)) ) ) ) ) ) ) ) )
& ! [X91] :
( ~ r1(sK13,X91)
| ! [X92] :
( ~ r1(X91,X92)
| ! [X93] :
( ~ r1(X92,X93)
| ! [X94] :
( ~ r1(X93,X94)
| ( ( p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| ( r1(X95,sK38(X95))
& ~ p1(sK38(X95)) ) )
| ( r1(X94,sK39(X94))
& ~ p1(sK39(X94))
& ! [X98] :
( ~ r1(sK39(X94),X98)
| ! [X99] :
( ~ r1(X98,X99)
| p1(X99) )
| ~ p1(X98) ) ) )
& ! [X100] :
( ~ r1(X94,X100)
| ! [X101] :
( ~ r1(X100,X101)
| ! [X102] :
( ~ r1(X101,X102)
| p1(X102) ) )
| ( r1(X100,sK40(X100))
& ~ p1(sK40(X100)) ) ) ) ) ) ) )
& ! [X104] :
( ~ r1(sK13,X104)
| ! [X105] :
( ~ r1(X104,X105)
| ! [X106] :
( ~ r1(X105,X106)
| ( ( p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| ( r1(X107,sK41(X107))
& ~ p1(sK41(X107)) ) )
| ( r1(X106,sK42(X106))
& ~ p1(sK42(X106))
& ! [X110] :
( ~ r1(sK42(X106),X110)
| ! [X111] :
( ~ r1(X110,X111)
| p1(X111) )
| ~ p1(X110) ) ) )
& ! [X112] :
( ~ r1(X106,X112)
| ! [X113] :
( ~ r1(X112,X113)
| ! [X114] :
( ~ r1(X113,X114)
| p1(X114) ) )
| ( r1(X112,sK43(X112))
& ~ p1(sK43(X112)) ) ) ) ) ) )
& ! [X116] :
( ~ r1(sK13,X116)
| ! [X117] :
( ~ r1(X116,X117)
| ( ( p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| ( r1(X118,sK44(X118))
& ~ p1(sK44(X118)) ) )
| ( r1(X117,sK45(X117))
& ~ p1(sK45(X117))
& ! [X121] :
( ~ r1(sK45(X117),X121)
| ! [X122] :
( ~ r1(X121,X122)
| p1(X122) )
| ~ p1(X121) ) ) )
& ! [X123] :
( ~ r1(X117,X123)
| ! [X124] :
( ~ r1(X123,X124)
| ! [X125] :
( ~ r1(X124,X125)
| p1(X125) ) )
| ( r1(X123,sK46(X123))
& ~ p1(sK46(X123)) ) ) ) ) )
& ! [X127] :
( ~ r1(sK13,X127)
| ( ( p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| ( r1(X128,sK47(X128))
& ~ p1(sK47(X128)) ) )
| ( r1(X127,sK48(X127))
& ~ p1(sK48(X127))
& ! [X131] :
( ~ r1(sK48(X127),X131)
| ! [X132] :
( ~ r1(X131,X132)
| p1(X132) )
| ~ p1(X131) ) ) )
& ! [X133] :
( ~ r1(X127,X133)
| ! [X134] :
( ~ r1(X133,X134)
| ! [X135] :
( ~ r1(X134,X135)
| p1(X135) ) )
| ( r1(X133,sK49(X133))
& ~ p1(sK49(X133)) ) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49]),skolemize(X0,sK13),skolemize(X11,sK14(X10)),skolemize(X12,sK15(X9)),skolemize(X18,sK16(X15)),skolemize(X28,sK17(X27)),skolemize(X29,sK18(X26)),skolemize(X35,sK19(X32)),skolemize(X44,sK20(X43)),skolemize(X45,sK21(X42)),skolemize(X51,sK22(X48)),skolemize(X61,sK23(X58)),skolemize(X62,sK24(X57)),skolemize(X65,sK25),skolemize(X66,sK26),skolemize(X67,sK27),skolemize(X68,sK28),skolemize(X69,sK29),skolemize(X70,sK30),skolemize(X71,sK31),skolemize(X72,sK32),skolemize(X75,sK33(X74)),skolemize(X76,sK34(X74)),skolemize(X83,sK35(X82)),skolemize(X84,sK36(X81)),skolemize(X90,sK37(X87)),skolemize(X96,sK38(X95)),skolemize(X97,sK39(X94)),skolemize(X103,sK40(X100)),skolemize(X108,sK41(X107)),skolemize(X109,sK42(X106)),skolemize(X115,sK43(X112)),skolemize(X119,sK44(X118)),skolemize(X120,sK45(X117)),skolemize(X126,sK46(X123)),skolemize(X129,sK47(X128)),skolemize(X130,sK48(X127)),skolemize(X136,sK49(X133))],[f24]) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ p1(sK5(X2))
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1)
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(sK4(X2),sK5(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| p1(X1)
| ~ p1(X0)
| ~ r1(X0,X1)
| r1(X2,sK4(X2))
| sP1(X0)
| ~ sP3(X0) ),
inference(cnf_transformation,[],[f14]) ).
fof(f30,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f31,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0,X1] :
( ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0,X1,X4,X5] :
( ~ r1(sK7(X0),X4)
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f34,plain,
! [X0,X1] :
( ~ p1(sK7(X0))
| ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f35,plain,
! [X0,X1] :
( ~ r1(X0,X1)
| p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
! [X3,X0,X4,X5] :
( ~ r1(sK8(X0),X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ p1(X4)
| p1(X3)
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f40,plain,
! [X0] :
( ~ p1(sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f41,plain,
! [X0] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X0] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f20]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| p1(sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ p1(sK12(X2))
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X0,X1)
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f87,plain,
! [X74] :
( ~ r1(sK30,X74)
| p1(X74)
| p1(sK33(X74)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f88,plain,
! [X74] :
( ~ p1(sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f89,plain,
! [X74] :
( r1(sK33(X74),sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f90,plain,
! [X74] :
( r1(X74,sK33(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f91,plain,
! [X73] :
( ~ r1(sK32,X73)
| p1(X73) ),
inference(cnf_transformation,[],[f25]) ).
fof(f92,plain,
r1(sK30,sK32),
inference(cnf_transformation,[],[f25]) ).
fof(f93,plain,
~ p1(sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f94,plain,
r1(sK30,sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f95,plain,
r1(sK29,sK30),
inference(cnf_transformation,[],[f25]) ).
fof(f96,plain,
r1(sK28,sK29),
inference(cnf_transformation,[],[f25]) ).
fof(f97,plain,
r1(sK27,sK28),
inference(cnf_transformation,[],[f25]) ).
fof(f98,plain,
r1(sK26,sK27),
inference(cnf_transformation,[],[f25]) ).
fof(f99,plain,
r1(sK25,sK26),
inference(cnf_transformation,[],[f25]) ).
fof(f100,plain,
r1(sK13,sK25),
inference(cnf_transformation,[],[f25]) ).
fof(f101,plain,
! [X56,X54,X57,X55,X52,X63,X53,X64] :
( ~ r1(sK24(X57),X63)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| ~ r1(sK13,X52)
| ~ r1(X63,X64)
| p1(X64)
| ~ p1(X63) ),
inference(cnf_transformation,[],[f25]) ).
fof(f102,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ p1(sK24(X57))
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f103,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP0(X57)
| r1(X57,sK24(X57)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f104,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( ~ p1(sK23(X58))
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f105,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| ~ r1(X57,X58)
| ~ r1(X58,X59)
| ~ r1(X59,X60)
| p1(X60)
| r1(X58,sK23(X58)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f106,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP2(X57) ),
inference(cnf_transformation,[],[f25]) ).
fof(f107,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ r1(sK13,X52)
| ~ r1(X52,X53)
| ~ r1(X53,X54)
| ~ r1(X54,X55)
| ~ r1(X55,X56)
| ~ r1(X56,X57)
| sP3(X57) ),
inference(cnf_transformation,[],[f25]) ).
fof(f108,plain,
! [X50,X40,X38,X41,X48,X39,X36,X49,X37,X42] :
( ~ p1(sK22(X48))
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X48)
| ~ r1(X48,X49)
| ~ r1(X49,X50)
| p1(X50)
| ~ r1(sK13,X36) ),
inference(cnf_transformation,[],[f25]) ).
fof(f109,plain,
! [X50,X40,X38,X41,X39,X48,X36,X49,X37,X42] :
( ~ r1(sK13,X36)
| ~ r1(X36,X37)
| ~ r1(X37,X38)
| ~ r1(X38,X39)
| ~ r1(X39,X40)
| ~ r1(X40,X41)
| ~ r1(X41,X42)
| ~ r1(X42,X48)
| ~ r1(X48,X49)
| ~ r1(X49,X50)
| p1(X50)
| r1(X48,sK22(X48)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f119,plain,
! [X21,X19,X26,X27,X24,X22,X25,X23,X20] :
( ~ p1(sK18(X26))
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| p1(X26)
| ~ r1(X26,X27)
| ~ p1(sK17(X27))
| ~ r1(sK13,X19) ),
inference(cnf_transformation,[],[f25]) ).
fof(f120,plain,
! [X21,X19,X26,X27,X24,X22,X25,X23,X20] :
( ~ p1(sK17(X27))
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| p1(X26)
| ~ r1(X26,X27)
| ~ r1(sK13,X19)
| r1(X26,sK18(X26)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f122,plain,
! [X21,X19,X26,X27,X24,X22,X25,X23,X20] :
( ~ p1(sK18(X26))
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| p1(X26)
| ~ r1(X26,X27)
| r1(X27,sK17(X27))
| ~ r1(sK13,X19) ),
inference(cnf_transformation,[],[f25]) ).
fof(f123,plain,
! [X21,X19,X26,X27,X24,X22,X25,X23,X20] :
( ~ r1(sK13,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| ~ r1(X21,X22)
| ~ r1(X22,X23)
| ~ r1(X23,X24)
| ~ r1(X24,X25)
| ~ r1(X25,X26)
| p1(X26)
| ~ r1(X26,X27)
| r1(X27,sK17(X27))
| r1(X26,sK18(X26)) ),
inference(cnf_transformation,[],[f25]) ).
fof(f279,definition,
( spl50_24
<=> ! [X2,X1] :
( ~ r1(sK32,X1)
| p1(X2)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_24])],[avatar_definition]) ).
fof(f280,plain,
( ! [X2,X1] :
( ~ r1(sK32,X1)
| p1(X2)
| ~ r1(X1,X2) )
| ~ spl50_24 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f482,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP2(X4) ),
inference(resolution,[],[f106,f100]) ).
fof(f487,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP3(X4) ),
inference(resolution,[],[f107,f100]) ).
fof(f2961,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| r1(X5,sK23(X5)) ),
inference(resolution,[],[f105,f100]) ).
fof(f3107,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK23(X4)) ),
inference(resolution,[],[f2961,f99]) ).
fof(f3110,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK23(X3)) ),
inference(resolution,[],[f3107,f98]) ).
fof(f3115,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK23(X2)) ),
inference(resolution,[],[f3110,f97]) ).
fof(f3120,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK23(X1)) ),
inference(resolution,[],[f3115,f96]) ).
fof(f3125,plain,
! [X2,X0,X1] :
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK23(X0)) ),
inference(resolution,[],[f3120,f95]) ).
fof(f3130,plain,
! [X0,X1] :
( ~ r1(sK32,X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK32,sK23(sK32)) ),
inference(resolution,[],[f3125,f92]) ).
fof(f3195,definition,
( spl50_319
<=> p1(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_319])],[avatar_definition]) ).
fof(f3196,plain,
( ~ p1(sK30)
| spl50_319 ),
inference(avatar_component_clause,[],[f3195]) ).
fof(f3197,plain,
( p1(sK30)
| ~ spl50_319 ),
inference(avatar_component_clause,[],[f3195]) ).
fof(f3615,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X7,X8)
| p1(X8)
| r1(X6,sK22(X6)) ),
inference(resolution,[],[f109,f100]) ).
fof(f3785,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK26,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,sK22(X5)) ),
inference(resolution,[],[f3615,f99]) ).
fof(f3788,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| r1(X4,sK22(X4)) ),
inference(resolution,[],[f3785,f98]) ).
fof(f3793,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| r1(X3,sK22(X3)) ),
inference(resolution,[],[f3788,f97]) ).
fof(f3798,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| r1(X2,sK22(X2)) ),
inference(resolution,[],[f3793,f96]) ).
fof(f3803,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| r1(X1,sK22(X1)) ),
inference(resolution,[],[f3798,f95]) ).
fof(f8461,definition,
( spl50_734
<=> ! [X2,X4,X0,X3,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X4,sK30)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_734])],[avatar_definition]) ).
fof(f8462,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X4,sK30)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl50_734 ),
inference(avatar_component_clause,[],[f8461]) ).
fof(f8466,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK25,X0)
| ~ r1(X1,sK30)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X0,X3) )
| ~ spl50_734 ),
inference(resolution,[],[f8462,f100]) ).
fof(f8469,plain,
( ! [X2,X0,X1] :
( ~ r1(sK26,X2)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X0,sK30) )
| ~ spl50_734 ),
inference(resolution,[],[f8466,f99]) ).
fof(f8472,plain,
( ! [X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK30) )
| ~ spl50_734 ),
inference(resolution,[],[f8469,f98]) ).
fof(f8477,plain,
( ! [X0] :
( ~ r1(sK28,X0)
| ~ r1(X0,sK30) )
| ~ spl50_734 ),
inference(resolution,[],[f8472,f97]) ).
fof(f8482,plain,
( ~ r1(sK29,sK30)
| ~ spl50_734 ),
inference(resolution,[],[f8477,f96]) ).
fof(f8487,plain,
( $false
| ~ spl50_734 ),
inference(forward_subsumption_resolution,[],[f8482,f95]) ).
fof(f8488,plain,
~ spl50_734,
inference(avatar_contradiction_clause,[],[f8487]) ).
fof(f10001,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| p1(X6)
| ~ r1(X6,X7)
| r1(X7,sK17(X7))
| r1(X6,sK18(X6)) ),
inference(resolution,[],[f123,f100]) ).
fof(f10616,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| p1(X5)
| ~ r1(X5,X6)
| r1(X6,sK17(X6))
| r1(X5,sK18(X5)) ),
inference(resolution,[],[f10001,f99]) ).
fof(f10619,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| p1(X4)
| ~ r1(X4,X5)
| r1(X5,sK17(X5))
| r1(X4,sK18(X4)) ),
inference(resolution,[],[f10616,f98]) ).
fof(f10624,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p1(X3)
| ~ r1(X3,X4)
| r1(X4,sK17(X4))
| r1(X3,sK18(X3)) ),
inference(resolution,[],[f10619,f97]) ).
fof(f10628,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK29,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| ~ r1(X2,X3)
| r1(X3,sK17(X3))
| r1(X2,sK18(X2)) ),
inference(resolution,[],[f10624,f96]) ).
fof(f10633,plain,
! [X2,X0,X1] :
( ~ r1(sK30,X0)
| ~ r1(X0,X1)
| p1(X1)
| ~ r1(X1,X2)
| r1(X2,sK17(X2))
| r1(X1,sK18(X1)) ),
inference(resolution,[],[f10628,f95]) ).
fof(f13053,plain,
! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| r1(X4,sK24(X4)) ),
inference(resolution,[],[f103,f100]) ).
fof(f13462,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP0(X3)
| r1(X3,sK24(X3)) ),
inference(resolution,[],[f13053,f99]) ).
fof(f13465,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP0(X2)
| r1(X2,sK24(X2)) ),
inference(resolution,[],[f13462,f98]) ).
fof(f13470,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP0(X1)
| r1(X1,sK24(X1)) ),
inference(resolution,[],[f13465,f97]) ).
fof(f13474,plain,
! [X0] :
( r1(X0,sK24(X0))
| sP0(X0)
| ~ r1(sK29,X0) ),
inference(resolution,[],[f13470,f96]) ).
fof(f13611,plain,
( sP0(sK30)
| ~ r1(sK29,sK30)
| p1(sK24(sK30))
| p1(sK33(sK24(sK30))) ),
inference(resolution,[],[f13474,f87]) ).
fof(f13831,plain,
( sP0(sK30)
| p1(sK24(sK30))
| p1(sK33(sK24(sK30))) ),
inference(forward_subsumption_resolution,[],[f13611,f95]) ).
fof(f13863,definition,
( spl50_829
<=> p1(sK33(sK24(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_829])],[avatar_definition]) ).
fof(f13864,plain,
( ~ p1(sK33(sK24(sK30)))
| spl50_829 ),
inference(avatar_component_clause,[],[f13863]) ).
fof(f13865,plain,
( p1(sK33(sK24(sK30)))
| ~ spl50_829 ),
inference(avatar_component_clause,[],[f13863]) ).
fof(f13867,definition,
( spl50_830
<=> sP0(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_830])],[avatar_definition]) ).
fof(f13868,plain,
( ~ sP0(sK30)
| spl50_830 ),
inference(avatar_component_clause,[],[f13867]) ).
fof(f13869,plain,
( sP0(sK30)
| ~ spl50_830 ),
inference(avatar_component_clause,[],[f13867]) ).
fof(f16598,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| ~ r1(sK13,X0)
| ~ r1(sK33(sK24(X5)),X6)
| p1(X6)
| ~ p1(sK33(sK24(X5)))
| p1(sK24(X5))
| ~ r1(sK30,sK24(X5)) ),
inference(resolution,[],[f101,f90]) ).
fof(f16600,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(sK33(sK24(X5)),X6)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| sP0(X5)
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| p1(X6)
| ~ p1(sK33(sK24(X5)))
| ~ r1(sK30,sK24(X5)) ),
inference(forward_subsumption_resolution,[],[f16598,f102]) ).
fof(f19662,definition,
( spl50_1308
<=> r1(sK30,sK24(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_1308])],[avatar_definition]) ).
fof(f19663,plain,
( r1(sK30,sK24(sK30))
| ~ spl50_1308 ),
inference(avatar_component_clause,[],[f19662]) ).
fof(f19664,plain,
( ~ r1(sK30,sK24(sK30))
| spl50_1308 ),
inference(avatar_component_clause,[],[f19662]) ).
fof(f19666,definition,
( spl50_1309
<=> p1(sK24(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_1309])],[avatar_definition]) ).
fof(f19667,plain,
( ~ p1(sK24(sK30))
| spl50_1309 ),
inference(avatar_component_clause,[],[f19666]) ).
fof(f19668,plain,
( p1(sK24(sK30))
| ~ spl50_1309 ),
inference(avatar_component_clause,[],[f19666]) ).
fof(f19670,plain,
( sP0(sK30)
| ~ r1(sK29,sK30)
| spl50_1308 ),
inference(resolution,[],[f19664,f13474]) ).
fof(f19671,plain,
( ~ r1(sK29,sK30)
| spl50_830
| spl50_1308 ),
inference(forward_subsumption_resolution,[],[f19670,f13868]) ).
fof(f19672,plain,
( $false
| spl50_830
| spl50_1308 ),
inference(forward_subsumption_resolution,[],[f19671,f95]) ).
fof(f19673,plain,
( spl50_830
| spl50_1308 ),
inference(avatar_contradiction_clause,[],[f19672]) ).
fof(f19674,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK30)
| sP0(sK30)
| ~ r1(sK13,X0) )
| ~ spl50_1309 ),
inference(resolution,[],[f19668,f102]) ).
fof(f19675,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,sK30)
| ~ r1(sK13,X0) )
| spl50_830
| ~ spl50_1309 ),
inference(forward_subsumption_resolution,[],[f19674,f13868]) ).
fof(f19676,plain,
( spl50_734
| spl50_830
| ~ spl50_1309 ),
inference(avatar_split_clause,[],[f19675,f19666,f13867,f8461]) ).
fof(f26043,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ p1(sK33(sK24(X4)))
| ~ r1(sK30,sK24(X4))
| p1(sK24(X4))
| ~ r1(sK30,sK24(X4)) ),
inference(resolution,[],[f16600,f89]) ).
fof(f26049,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ p1(sK33(sK24(X4)))
| ~ r1(sK30,sK24(X4))
| p1(sK24(X4)) ),
inference(duplicate_literal_removal,[],[f26043]) ).
fof(f26052,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ p1(sK33(sK24(X4)))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| sP0(X4)
| ~ r1(sK13,X5)
| ~ r1(X5,X0)
| p1(sK34(sK24(X4)))
| ~ r1(X0,X1)
| ~ r1(sK30,sK24(X4)) ),
inference(forward_subsumption_resolution,[],[f26049,f102]) ).
fof(f32200,plain,
( p1(sK24(sK30))
| p1(sK33(sK24(sK30)))
| spl50_830 ),
inference(forward_subsumption_resolution,[],[f13831,f13868]) ).
fof(f32202,plain,
( p1(sK33(sK24(sK30)))
| spl50_830
| spl50_1309 ),
inference(forward_subsumption_resolution,[],[f32200,f19667]) ).
fof(f32205,plain,
( $false
| spl50_829
| spl50_830
| spl50_1309 ),
inference(forward_subsumption_resolution,[],[f32202,f13864]) ).
fof(f32206,plain,
( spl50_829
| spl50_830
| spl50_1309 ),
inference(avatar_contradiction_clause,[],[f32205]) ).
fof(f33101,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP2(X3) ),
inference(resolution,[],[f482,f99]) ).
fof(f33105,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP2(X2) ),
inference(resolution,[],[f33101,f98]) ).
fof(f33111,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP2(X1) ),
inference(resolution,[],[f33105,f97]) ).
fof(f33116,plain,
! [X0] :
( ~ r1(sK29,X0)
| sP2(X0) ),
inference(resolution,[],[f33111,f96]) ).
fof(f33121,plain,
sP2(sK30),
inference(resolution,[],[f33116,f95]) ).
fof(f36535,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30))
| ~ sP2(sK30) ),
inference(resolution,[],[f35,f92]) ).
fof(f52308,plain,
! [X2,X3,X0,X1] :
( ~ r1(sK26,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| sP3(X3) ),
inference(resolution,[],[f487,f99]) ).
fof(f52316,plain,
! [X2,X0,X1] :
( ~ r1(sK27,X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| sP3(X2) ),
inference(resolution,[],[f52308,f98]) ).
fof(f52325,plain,
! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| sP3(X1) ),
inference(resolution,[],[f52316,f97]) ).
fof(f52334,plain,
! [X0] :
( ~ r1(sK29,X0)
| sP3(X0) ),
inference(resolution,[],[f52325,f96]) ).
fof(f52343,plain,
sP3(sK30),
inference(resolution,[],[f52334,f95]) ).
fof(f52900,definition,
( spl50_3963
<=> r1(sK32,sK4(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_3963])],[avatar_definition]) ).
fof(f52901,plain,
( ~ r1(sK32,sK4(sK32))
| spl50_3963 ),
inference(avatar_component_clause,[],[f52900]) ).
fof(f52902,plain,
( r1(sK32,sK4(sK32))
| ~ spl50_3963 ),
inference(avatar_component_clause,[],[f52900]) ).
fof(f52904,definition,
( spl50_3964
<=> ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_3964])],[avatar_definition]) ).
fof(f52905,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| p1(X0) )
| ~ spl50_3964 ),
inference(avatar_component_clause,[],[f52904]) ).
fof(f52950,plain,
( p1(sK31)
| ~ spl50_3964 ),
inference(resolution,[],[f52905,f94]) ).
fof(f52962,plain,
( $false
| ~ spl50_3964 ),
inference(forward_subsumption_resolution,[],[f52950,f93]) ).
fof(f52963,plain,
~ spl50_3964,
inference(avatar_contradiction_clause,[],[f52962]) ).
fof(f56427,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30)) ),
inference(forward_subsumption_resolution,[],[f36535,f33121]) ).
fof(f56483,plain,
( r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30))
| spl50_319 ),
inference(forward_subsumption_resolution,[],[f56427,f3196]) ).
fof(f56485,definition,
( spl50_4358
<=> r1(sK30,sK7(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_4358])],[avatar_definition]) ).
fof(f56486,plain,
( ~ r1(sK30,sK7(sK30))
| spl50_4358 ),
inference(avatar_component_clause,[],[f56485]) ).
fof(f56487,plain,
( r1(sK30,sK7(sK30))
| ~ spl50_4358 ),
inference(avatar_component_clause,[],[f56485]) ).
fof(f56489,definition,
( spl50_4359
<=> r1(sK32,sK6(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_4359])],[avatar_definition]) ).
fof(f56491,plain,
( r1(sK32,sK6(sK32))
| ~ spl50_4359 ),
inference(avatar_component_clause,[],[f56489]) ).
fof(f56492,plain,
( spl50_4358
| spl50_4359
| spl50_319 ),
inference(avatar_split_clause,[],[f56483,f3195,f56489,f56485]) ).
fof(f56493,plain,
( p1(sK7(sK30))
| p1(sK33(sK7(sK30)))
| ~ spl50_4358 ),
inference(resolution,[],[f56487,f87]) ).
fof(f56524,definition,
( spl50_4361
<=> p1(sK7(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_4361])],[avatar_definition]) ).
fof(f56525,plain,
( ~ p1(sK7(sK30))
| spl50_4361 ),
inference(avatar_component_clause,[],[f56524]) ).
fof(f56526,plain,
( p1(sK7(sK30))
| ~ spl50_4361 ),
inference(avatar_component_clause,[],[f56524]) ).
fof(f56529,definition,
( spl50_4362
<=> p1(sK33(sK7(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_4362])],[avatar_definition]) ).
fof(f56531,plain,
( p1(sK33(sK7(sK30)))
| ~ spl50_4362 ),
inference(avatar_component_clause,[],[f56529]) ).
fof(f56532,plain,
( spl50_4362
| spl50_4361
| ~ spl50_4358 ),
inference(avatar_split_clause,[],[f56493,f56485,f56524,f56529]) ).
fof(f56533,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0))
| p1(sK30)
| ~ sP2(sK30) )
| ~ spl50_4361 ),
inference(resolution,[],[f56526,f34]) ).
fof(f56534,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| ~ p1(sK6(X0))
| p1(sK30)
| ~ sP2(sK30) )
| ~ spl50_4361 ),
inference(resolution,[],[f56526,f31]) ).
fof(f56535,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| ~ p1(sK6(X0))
| ~ sP2(sK30) )
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f56534,f3196]) ).
fof(f56536,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK30) )
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f56533,f3196]) ).
fof(f56537,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f56535,f33121]) ).
fof(f56538,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0) )
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f56536,f33121]) ).
fof(f57109,plain,
( ~ r1(sK30,sK32)
| p1(sK6(sK32))
| spl50_319
| ~ spl50_4361 ),
inference(resolution,[],[f56538,f91]) ).
fof(f57411,plain,
( ~ r1(sK30,sK32)
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f57109,f56537]) ).
fof(f57499,plain,
( $false
| spl50_319
| ~ spl50_4361 ),
inference(forward_subsumption_resolution,[],[f57411,f92]) ).
fof(f57500,plain,
( spl50_319
| ~ spl50_4361 ),
inference(avatar_contradiction_clause,[],[f57499]) ).
fof(f57738,plain,
( p1(sK6(sK32))
| ~ spl50_4359 ),
inference(resolution,[],[f56491,f91]) ).
fof(f60961,plain,
( ! [X0] :
( r1(X0,sK7(X0))
| p1(X0)
| ~ r1(X0,sK32)
| ~ sP2(X0) )
| ~ spl50_4359 ),
inference(resolution,[],[f32,f57738]) ).
fof(f61866,plain,
( p1(sK30)
| ~ r1(sK30,sK32)
| ~ sP2(sK30)
| spl50_4358
| ~ spl50_4359 ),
inference(resolution,[],[f60961,f56486]) ).
fof(f62735,plain,
( p1(sK30)
| ~ sP2(sK30)
| spl50_4358
| ~ spl50_4359 ),
inference(forward_subsumption_resolution,[],[f61866,f92]) ).
fof(f62752,plain,
( p1(sK30)
| spl50_4358
| ~ spl50_4359 ),
inference(forward_subsumption_resolution,[],[f62735,f33121]) ).
fof(f62786,plain,
( spl50_319
| spl50_4358
| ~ spl50_4359 ),
inference(avatar_split_clause,[],[f62752,f56489,f56485,f3195]) ).
fof(f96646,definition,
( spl50_7794
<=> r1(sK4(sK32),sK5(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_7794])],[avatar_definition]) ).
fof(f96647,plain,
( ~ r1(sK4(sK32),sK5(sK32))
| spl50_7794 ),
inference(avatar_component_clause,[],[f96646]) ).
fof(f96648,plain,
( r1(sK4(sK32),sK5(sK32))
| ~ spl50_7794 ),
inference(avatar_component_clause,[],[f96646]) ).
fof(f96687,definition,
( spl50_7799
<=> r1(sK32,sK23(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_7799])],[avatar_definition]) ).
fof(f96689,plain,
( r1(sK32,sK23(sK32))
| ~ spl50_7799 ),
inference(avatar_component_clause,[],[f96687]) ).
fof(f96690,plain,
( spl50_7799
| spl50_24 ),
inference(avatar_split_clause,[],[f3130,f279,f96687]) ).
fof(f96707,plain,
( p1(sK23(sK32))
| ~ spl50_7799 ),
inference(resolution,[],[f96689,f91]) ).
fof(f96715,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,sK32)
| ~ r1(sK32,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(sK13,X0) )
| ~ spl50_7799 ),
inference(resolution,[],[f96707,f104]) ).
fof(f96938,definition,
( spl50_7814
<=> ! [X0] :
( p1(X0)
| ~ r1(sK4(sK32),X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_7814])],[avatar_definition]) ).
fof(f96939,plain,
( ! [X0] :
( ~ r1(sK4(sK32),X0)
| p1(X0) )
| ~ spl50_7814 ),
inference(avatar_component_clause,[],[f96938]) ).
fof(f98446,definition,
( spl50_7888
<=> ! [X2,X3,X4,X0,X5,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X5,sK32)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_7888])],[avatar_definition]) ).
fof(f98447,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X5,sK32)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl50_7888 ),
inference(avatar_component_clause,[],[f98446]) ).
fof(f98448,plain,
( spl50_24
| spl50_7888
| ~ spl50_7799 ),
inference(avatar_split_clause,[],[f96715,f96687,f98446,f279]) ).
fof(f98449,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK25,X0)
| ~ r1(X1,sK32)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X0,X4) )
| ~ spl50_7888 ),
inference(resolution,[],[f98447,f100]) ).
fof(f98459,plain,
( ! [X2,X3,X0,X1] :
( ~ r1(sK26,X3)
| ~ r1(X1,X0)
| ~ r1(X2,X1)
| ~ r1(X3,X2)
| ~ r1(X0,sK32) )
| ~ spl50_7888 ),
inference(resolution,[],[f98449,f99]) ).
fof(f98469,plain,
( ! [X2,X0,X1] :
( ~ r1(sK27,X2)
| ~ r1(X2,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK32) )
| ~ spl50_7888 ),
inference(resolution,[],[f98459,f98]) ).
fof(f98480,plain,
( ! [X0,X1] :
( ~ r1(sK28,X0)
| ~ r1(X0,X1)
| ~ r1(X1,sK32) )
| ~ spl50_7888 ),
inference(resolution,[],[f98469,f97]) ).
fof(f98491,plain,
( ! [X0] :
( ~ r1(sK29,X0)
| ~ r1(X0,sK32) )
| ~ spl50_7888 ),
inference(resolution,[],[f98480,f96]) ).
fof(f98502,plain,
( ~ r1(sK30,sK32)
| ~ spl50_7888 ),
inference(resolution,[],[f98491,f95]) ).
fof(f98513,plain,
( $false
| ~ spl50_7888 ),
inference(forward_subsumption_resolution,[],[f98502,f92]) ).
fof(f98514,plain,
~ spl50_7888,
inference(avatar_contradiction_clause,[],[f98513]) ).
fof(f98523,definition,
( spl50_7890
<=> p1(sK5(sK32)) ),
introduced(definition,[new_symbols(definition,[spl50_7890])],[avatar_definition]) ).
fof(f98525,plain,
( p1(sK5(sK32))
| ~ spl50_7890 ),
inference(avatar_component_clause,[],[f98523]) ).
fof(f98536,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK4(sK32),X0) )
| ~ spl50_24
| ~ spl50_3963 ),
inference(resolution,[],[f280,f52902]) ).
fof(f98548,plain,
( spl50_7814
| ~ spl50_24
| ~ spl50_3963 ),
inference(avatar_split_clause,[],[f98536,f52900,f279,f96938]) ).
fof(f98562,plain,
( p1(sK5(sK32))
| ~ spl50_7794
| ~ spl50_7814 ),
inference(resolution,[],[f96939,f96648]) ).
fof(f98573,plain,
( spl50_7890
| ~ spl50_7794
| ~ spl50_7814 ),
inference(avatar_split_clause,[],[f98562,f96938,f96646,f98523]) ).
fof(f99076,plain,
! [X0,X1] :
( ~ sP1(sK30)
| ~ r1(sK8(sK30),X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK8(sK30),sK23(sK8(sK30))) ),
inference(resolution,[],[f42,f3125]) ).
fof(f99078,plain,
! [X2,X0,X1] :
( ~ sP1(sK30)
| ~ r1(sK8(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK22(X0)) ),
inference(resolution,[],[f42,f3803]) ).
fof(f99081,plain,
! [X0,X1] :
( ~ sP1(sK30)
| ~ r1(sK8(sK30),X0)
| p1(X0)
| ~ r1(X0,X1)
| r1(X1,sK17(X1))
| r1(X0,sK18(X0)) ),
inference(resolution,[],[f42,f10633]) ).
fof(f99680,definition,
( spl50_7911
<=> sP1(sK30) ),
introduced(definition,[new_symbols(definition,[spl50_7911])],[avatar_definition]) ).
fof(f99681,plain,
( sP1(sK30)
| ~ spl50_7911 ),
inference(avatar_component_clause,[],[f99680]) ).
fof(f99682,plain,
( ~ sP1(sK30)
| spl50_7911 ),
inference(avatar_component_clause,[],[f99680]) ).
fof(f101542,plain,
! [X0,X1] :
( ~ sP1(X0)
| ~ r1(X1,sK8(X0))
| p1(sK9(X0))
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(resolution,[],[f41,f46]) ).
fof(f101545,plain,
! [X0,X1] :
( ~ r1(X1,sK8(X0))
| ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X1) ),
inference(forward_subsumption_resolution,[],[f101542,f40]) ).
fof(f103678,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK9(X0),sK11(sK9(X0)))
| ~ sP0(X0)
| ~ sP1(X0) ),
inference(resolution,[],[f101545,f42]) ).
fof(f103679,plain,
! [X0] :
( r1(sK9(X0),sK11(sK9(X0)))
| ~ sP1(X0)
| ~ sP0(X0) ),
inference(duplicate_literal_removal,[],[f103678]) ).
fof(f103959,plain,
( ! [X0,X1] :
( ~ r1(X1,sK32)
| ~ p1(X1)
| p1(X0)
| ~ r1(X1,X0)
| sP1(X1)
| ~ sP3(X1) )
| ~ spl50_7890 ),
inference(resolution,[],[f27,f98525]) ).
fof(f103960,plain,
( ! [X0] :
( ~ p1(sK30)
| p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_7890 ),
inference(resolution,[],[f103959,f92]) ).
fof(f103961,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_319
| ~ spl50_7890 ),
inference(forward_subsumption_resolution,[],[f103960,f3197]) ).
fof(f103962,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| ~ sP3(sK30) )
| ~ spl50_319
| ~ spl50_7890
| spl50_7911 ),
inference(forward_subsumption_resolution,[],[f103961,f99682]) ).
fof(f103963,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) )
| ~ spl50_319
| ~ spl50_7890
| spl50_7911 ),
inference(forward_subsumption_resolution,[],[f103962,f52343]) ).
fof(f103966,plain,
( spl50_3964
| ~ spl50_319
| ~ spl50_7890
| spl50_7911 ),
inference(avatar_split_clause,[],[f103963,f99680,f98523,f3195,f52904]) ).
fof(f105800,plain,
! [X0] :
( p1(X0)
| ~ p1(sK30)
| ~ r1(sK30,X0)
| r1(sK32,sK4(sK32))
| sP1(sK30)
| ~ sP3(sK30) ),
inference(resolution,[],[f29,f92]) ).
fof(f105844,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK32,sK4(sK32))
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_319 ),
inference(forward_subsumption_resolution,[],[f105800,f3197]) ).
fof(f105906,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_319
| spl50_3963 ),
inference(forward_subsumption_resolution,[],[f105844,f52901]) ).
fof(f105910,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| ~ sP3(sK30) )
| ~ spl50_319
| spl50_3963
| spl50_7911 ),
inference(forward_subsumption_resolution,[],[f105906,f99682]) ).
fof(f105911,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) )
| ~ spl50_319
| spl50_3963
| spl50_7911 ),
inference(forward_subsumption_resolution,[],[f105910,f52343]) ).
fof(f105912,plain,
( spl50_3964
| ~ spl50_319
| spl50_3963
| spl50_7911 ),
inference(avatar_split_clause,[],[f105911,f99680,f52900,f3195,f52904]) ).
fof(f107456,plain,
( ! [X0,X1] :
( ~ r1(sK8(sK30),X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK8(sK30),sK23(sK8(sK30))) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f99076,f99681]) ).
fof(f107458,definition,
( spl50_8415
<=> r1(sK8(sK30),sK23(sK8(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8415])],[avatar_definition]) ).
fof(f107460,plain,
( r1(sK8(sK30),sK23(sK8(sK30)))
| ~ spl50_8415 ),
inference(avatar_component_clause,[],[f107458]) ).
fof(f107465,definition,
( spl50_8417
<=> ! [X0,X1] :
( ~ r1(sK8(sK30),X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl50_8417])],[avatar_definition]) ).
fof(f107466,plain,
( ! [X0,X1] :
( ~ r1(sK8(sK30),X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl50_8417 ),
inference(avatar_component_clause,[],[f107465]) ).
fof(f107467,plain,
( spl50_8415
| spl50_8417
| ~ spl50_7911 ),
inference(avatar_split_clause,[],[f107456,f99680,f107465,f107458]) ).
fof(f107483,plain,
( ! [X0,X1] :
( ~ r1(sK23(sK8(sK30)),X0)
| ~ r1(X0,X1)
| p1(X1)
| ~ p1(X0)
| p1(sK23(sK8(sK30)))
| ~ sP1(sK30) )
| ~ spl50_8415 ),
inference(resolution,[],[f107460,f36]) ).
fof(f107486,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| p1(sK23(sK8(sK30)))
| p1(sK11(sK23(sK8(sK30))))
| ~ sP0(X0) )
| ~ spl50_8415 ),
inference(resolution,[],[f107460,f43]) ).
fof(f107487,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| p1(sK23(sK8(sK30)))
| r1(sK11(sK23(sK8(sK30))),sK12(sK23(sK8(sK30))))
| ~ sP0(X0) )
| ~ spl50_8415 ),
inference(resolution,[],[f107460,f45]) ).
fof(f107488,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| p1(sK23(sK8(sK30)))
| r1(sK23(sK8(sK30)),sK11(sK23(sK8(sK30))))
| ~ sP0(X0) )
| ~ spl50_8415 ),
inference(resolution,[],[f107460,f46]) ).
fof(f107491,plain,
( ! [X0,X1] :
( ~ r1(sK23(sK8(sK30)),X0)
| ~ r1(X0,X1)
| p1(X1)
| ~ p1(X0)
| p1(sK23(sK8(sK30))) )
| ~ spl50_7911
| ~ spl50_8415 ),
inference(forward_subsumption_resolution,[],[f107483,f99681]) ).
fof(f107493,definition,
( spl50_8418
<=> p1(sK11(sK23(sK8(sK30)))) ),
introduced(definition,[new_symbols(definition,[spl50_8418])],[avatar_definition]) ).
fof(f107495,plain,
( p1(sK11(sK23(sK8(sK30))))
| ~ spl50_8418 ),
inference(avatar_component_clause,[],[f107493]) ).
fof(f107497,definition,
( spl50_8419
<=> p1(sK23(sK8(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8419])],[avatar_definition]) ).
fof(f107498,plain,
( ~ p1(sK23(sK8(sK30)))
| spl50_8419 ),
inference(avatar_component_clause,[],[f107497]) ).
fof(f107499,plain,
( p1(sK23(sK8(sK30)))
| ~ spl50_8419 ),
inference(avatar_component_clause,[],[f107497]) ).
fof(f107504,definition,
( spl50_8421
<=> ! [X0] :
( ~ r1(X0,sK8(sK30))
| ~ sP0(X0) ) ),
introduced(definition,[new_symbols(definition,[spl50_8421])],[avatar_definition]) ).
fof(f107505,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| ~ sP0(X0) )
| ~ spl50_8421 ),
inference(avatar_component_clause,[],[f107504]) ).
fof(f107506,plain,
( spl50_8418
| spl50_8419
| spl50_8421
| ~ spl50_8415 ),
inference(avatar_split_clause,[],[f107486,f107458,f107504,f107497,f107493]) ).
fof(f107514,definition,
( spl50_8423
<=> ! [X0,X1] :
( ~ r1(sK23(sK8(sK30)),X0)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl50_8423])],[avatar_definition]) ).
fof(f107515,plain,
( ! [X0,X1] :
( ~ r1(sK23(sK8(sK30)),X0)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl50_8423 ),
inference(avatar_component_clause,[],[f107514]) ).
fof(f107516,plain,
( spl50_8419
| spl50_8423
| ~ spl50_7911
| ~ spl50_8415 ),
inference(avatar_split_clause,[],[f107491,f107458,f99680,f107514,f107497]) ).
fof(f107530,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,sK8(sK30))
| ~ r1(sK8(sK30),X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(sK13,X0) )
| ~ spl50_8419 ),
inference(resolution,[],[f107499,f104]) ).
fof(f107540,plain,
( ! [X2,X0,X1] :
( ~ r1(sK8(sK30),X0)
| ~ r1(X0,X1)
| ~ r1(X1,X2)
| p1(X2)
| r1(X0,sK22(X0)) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f99078,f99681]) ).
fof(f107542,plain,
( ! [X0,X1] :
( ~ r1(sK9(sK30),X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK9(sK30),sK22(sK9(sK30)))
| ~ sP1(sK30) )
| ~ spl50_7911 ),
inference(resolution,[],[f107540,f41]) ).
fof(f107555,plain,
( ! [X0,X1] :
( ~ r1(sK9(sK30),X0)
| ~ r1(X0,X1)
| p1(X1)
| r1(sK9(sK30),sK22(sK9(sK30))) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f107542,f99681]) ).
fof(f107557,definition,
( spl50_8426
<=> r1(sK9(sK30),sK22(sK9(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8426])],[avatar_definition]) ).
fof(f107559,plain,
( r1(sK9(sK30),sK22(sK9(sK30)))
| ~ spl50_8426 ),
inference(avatar_component_clause,[],[f107557]) ).
fof(f107564,definition,
( spl50_8428
<=> ! [X0,X1] :
( ~ r1(sK9(sK30),X0)
| p1(X1)
| ~ r1(X0,X1) ) ),
introduced(definition,[new_symbols(definition,[spl50_8428])],[avatar_definition]) ).
fof(f107565,plain,
( ! [X0,X1] :
( ~ r1(sK9(sK30),X0)
| p1(X1)
| ~ r1(X0,X1) )
| ~ spl50_8428 ),
inference(avatar_component_clause,[],[f107564]) ).
fof(f107566,plain,
( spl50_8426
| spl50_8428
| ~ spl50_7911 ),
inference(avatar_split_clause,[],[f107555,f99680,f107564,f107557]) ).
fof(f107596,definition,
( spl50_8432
<=> p1(sK9(sK30)) ),
introduced(definition,[new_symbols(definition,[spl50_8432])],[avatar_definition]) ).
fof(f107597,plain,
( ~ p1(sK9(sK30))
| spl50_8432 ),
inference(avatar_component_clause,[],[f107596]) ).
fof(f107598,plain,
( p1(sK9(sK30))
| ~ spl50_8432 ),
inference(avatar_component_clause,[],[f107596]) ).
fof(f107660,plain,
( ! [X0,X1] :
( ~ r1(sK8(sK30),X0)
| p1(X0)
| ~ r1(X0,X1)
| r1(X1,sK17(X1))
| r1(X0,sK18(X0)) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f99081,f99681]) ).
fof(f107662,plain,
( ! [X0] :
( p1(sK9(sK30))
| ~ r1(sK9(sK30),X0)
| r1(X0,sK17(X0))
| r1(sK9(sK30),sK18(sK9(sK30)))
| ~ sP1(sK30) )
| ~ spl50_7911 ),
inference(resolution,[],[f107660,f41]) ).
fof(f107989,definition,
( spl50_8461
<=> ! [X2,X3,X4,X0,X5,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X5,sK8(sK30))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_8461])],[avatar_definition]) ).
fof(f107990,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(X5,sK8(sK30))
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl50_8461 ),
inference(avatar_component_clause,[],[f107989]) ).
fof(f107991,plain,
( spl50_8417
| spl50_8461
| ~ spl50_8419 ),
inference(avatar_split_clause,[],[f107530,f107497,f107989,f107465]) ).
fof(f107993,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK9(sK30),X0)
| ~ sP1(sK30) )
| ~ spl50_8417 ),
inference(resolution,[],[f107466,f41]) ).
fof(f108293,plain,
( ! [X0] :
( ~ r1(sK9(sK30),X0)
| r1(X0,sK17(X0))
| r1(sK9(sK30),sK18(sK9(sK30)))
| ~ sP1(sK30) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f107662,f40]) ).
fof(f108297,plain,
( ! [X0] :
( ~ r1(sK9(sK30),X0)
| p1(X0) )
| ~ spl50_7911
| ~ spl50_8417 ),
inference(forward_subsumption_resolution,[],[f107993,f99681]) ).
fof(f108298,plain,
( ! [X0] :
( ~ r1(sK9(sK30),X0)
| r1(X0,sK17(X0))
| r1(sK9(sK30),sK18(sK9(sK30))) )
| ~ spl50_7911 ),
inference(forward_subsumption_resolution,[],[f108293,f99681]) ).
fof(f108320,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK11(sK9(sK30)),X0)
| ~ sP1(sK30)
| ~ sP0(sK30) )
| ~ spl50_8428 ),
inference(resolution,[],[f107565,f103679]) ).
fof(f108331,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK11(sK9(sK30)),X0)
| ~ sP0(sK30) )
| ~ spl50_7911
| ~ spl50_8428 ),
inference(forward_subsumption_resolution,[],[f108320,f99681]) ).
fof(f108332,plain,
( ! [X0] :
( ~ r1(sK11(sK9(sK30)),X0)
| p1(X0) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428 ),
inference(forward_subsumption_resolution,[],[f108331,f13869]) ).
fof(f108386,definition,
( spl50_8500
<=> r1(sK9(sK30),sK18(sK9(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8500])],[avatar_definition]) ).
fof(f108387,plain,
( ~ r1(sK9(sK30),sK18(sK9(sK30)))
| spl50_8500 ),
inference(avatar_component_clause,[],[f108386]) ).
fof(f108388,plain,
( r1(sK9(sK30),sK18(sK9(sK30)))
| ~ spl50_8500 ),
inference(avatar_component_clause,[],[f108386]) ).
fof(f108390,definition,
( spl50_8501
<=> ! [X0] :
( ~ r1(sK9(sK30),X0)
| r1(X0,sK17(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl50_8501])],[avatar_definition]) ).
fof(f108391,plain,
( ! [X0] :
( ~ r1(sK9(sK30),X0)
| r1(X0,sK17(X0)) )
| ~ spl50_8501 ),
inference(avatar_component_clause,[],[f108390]) ).
fof(f108392,plain,
( spl50_8500
| spl50_8501
| ~ spl50_7911 ),
inference(avatar_split_clause,[],[f108298,f99680,f108390,f108386]) ).
fof(f108394,plain,
( p1(sK18(sK9(sK30)))
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8500 ),
inference(resolution,[],[f108388,f108297]) ).
fof(f108402,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)
| ~ r1(X6,sK9(sK30))
| p1(sK9(sK30))
| ~ r1(sK9(sK30),X7)
| r1(X7,sK17(X7))
| ~ r1(sK13,X0) )
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8500 ),
inference(resolution,[],[f108394,f122]) ).
fof(f108432,definition,
( spl50_8503
<=> ! [X5,X3,X4,X2,X0,X6,X1] :
( ~ r1(X0,X1)
| ~ r1(sK13,X0)
| ~ r1(X6,sK9(sK30))
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl50_8503])],[avatar_definition]) ).
fof(f108433,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] :
( ~ r1(X6,sK9(sK30))
| ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2) )
| ~ spl50_8503 ),
inference(avatar_component_clause,[],[f108432]) ).
fof(f108434,plain,
( spl50_8501
| spl50_8432
| spl50_8503
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8500 ),
inference(avatar_split_clause,[],[f108402,f108386,f107465,f99680,f108432,f107596,f108390]) ).
fof(f108438,plain,
( ~ sP1(sK30)
| ~ spl50_8432 ),
inference(resolution,[],[f107598,f40]) ).
fof(f108439,plain,
( $false
| ~ spl50_7911
| ~ spl50_8432 ),
inference(forward_subsumption_resolution,[],[f108438,f99681]) ).
fof(f108440,plain,
( ~ spl50_7911
| ~ spl50_8432 ),
inference(avatar_contradiction_clause,[],[f108439]) ).
fof(f108441,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK8(sK30))
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X1,X5)
| ~ sP1(sK30) )
| ~ spl50_8503 ),
inference(resolution,[],[f108433,f41]) ).
fof(f108442,plain,
( ! [X2,X3,X0,X1,X4,X5] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK8(sK30))
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ r1(X1,X5) )
| ~ spl50_7911
| ~ spl50_8503 ),
inference(forward_subsumption_resolution,[],[f108441,f99681]) ).
fof(f108443,plain,
( spl50_8461
| ~ spl50_7911
| ~ spl50_8503 ),
inference(avatar_split_clause,[],[f108442,f108432,f99680,f107989]) ).
fof(f108444,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK30)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X1,X4)
| ~ sP1(sK30) )
| ~ spl50_8461 ),
inference(resolution,[],[f107990,f42]) ).
fof(f108445,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(sK13,X0)
| ~ r1(X0,X1)
| ~ r1(X2,sK30)
| ~ r1(X3,X2)
| ~ r1(X4,X3)
| ~ r1(X1,X4) )
| ~ spl50_7911
| ~ spl50_8461 ),
inference(forward_subsumption_resolution,[],[f108444,f99681]) ).
fof(f108446,plain,
( spl50_734
| ~ spl50_7911
| ~ spl50_8461 ),
inference(avatar_split_clause,[],[f108445,f107989,f99680,f8461]) ).
fof(f108447,plain,
( r1(sK11(sK9(sK30)),sK17(sK11(sK9(sK30))))
| ~ sP1(sK30)
| ~ sP0(sK30)
| ~ spl50_8501 ),
inference(resolution,[],[f108391,f103679]) ).
fof(f108467,plain,
( r1(sK11(sK9(sK30)),sK17(sK11(sK9(sK30))))
| ~ sP0(sK30)
| ~ spl50_7911
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108447,f99681]) ).
fof(f108470,plain,
( r1(sK11(sK9(sK30)),sK17(sK11(sK9(sK30))))
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108467,f13869]) ).
fof(f108471,plain,
( p1(sK17(sK11(sK9(sK30))))
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| ~ spl50_8501 ),
inference(resolution,[],[f108470,f108332]) ).
fof(f108483,plain,
( ! [X2,X3,X0,X1,X6,X7,X4,X5] :
( ~ r1(X7,sK11(sK9(sK30)))
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(X7)
| ~ r1(X0,X1)
| ~ r1(sK13,X0)
| r1(X7,sK18(X7)) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| ~ spl50_8501 ),
inference(resolution,[],[f108471,f120]) ).
fof(f108732,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,sK9(sK30))
| p1(sK9(sK30))
| ~ r1(X6,X0)
| ~ r1(sK13,X6)
| r1(sK9(sK30),sK18(sK9(sK30)))
| ~ sP1(sK30)
| ~ sP0(sK30) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| ~ spl50_8501 ),
inference(resolution,[],[f108483,f103679]) ).
fof(f108733,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,sK9(sK30))
| ~ r1(X6,X0)
| ~ r1(sK13,X6)
| r1(sK9(sK30),sK18(sK9(sK30)))
| ~ sP1(sK30)
| ~ sP0(sK30) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108732,f40]) ).
fof(f108734,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,sK9(sK30))
| ~ r1(X6,X0)
| ~ r1(sK13,X6)
| ~ sP1(sK30)
| ~ sP0(sK30) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| spl50_8500
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108733,f108387]) ).
fof(f108735,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,sK9(sK30))
| ~ r1(X6,X0)
| ~ r1(sK13,X6)
| ~ sP0(sK30) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| spl50_8500
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108734,f99681]) ).
fof(f108736,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,sK9(sK30))
| ~ r1(X6,X0)
| ~ r1(sK13,X6) )
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| spl50_8500
| ~ spl50_8501 ),
inference(forward_subsumption_resolution,[],[f108735,f13869]) ).
fof(f108741,plain,
( spl50_8503
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| spl50_8500
| ~ spl50_8501 ),
inference(avatar_split_clause,[],[f108736,f108390,f108386,f107564,f99680,f13867,f108432]) ).
fof(f108747,plain,
( p1(sK22(sK9(sK30)))
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8426 ),
inference(resolution,[],[f107559,f108297]) ).
fof(f108754,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,sK9(sK30))
| ~ r1(sK9(sK30),X7)
| ~ r1(X7,X8)
| p1(X8)
| ~ r1(sK13,X0) )
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8426 ),
inference(resolution,[],[f108747,f108]) ).
fof(f109166,plain,
( spl50_8428
| spl50_8503
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8426 ),
inference(avatar_split_clause,[],[f108754,f107557,f107465,f99680,f108432,f107564]) ).
fof(f110945,plain,
! [X0] :
( p1(X0)
| ~ p1(sK30)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| sP1(sK30)
| ~ sP3(sK30) ),
inference(resolution,[],[f28,f92]) ).
fof(f112806,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| sP0(sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0)
| ~ r1(sK30,sK24(sK30)) )
| ~ spl50_829 ),
inference(resolution,[],[f26052,f13865]) ).
fof(f112807,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| sP0(sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0) )
| ~ spl50_829 ),
inference(forward_subsumption_resolution,[],[f112806,f103]) ).
fof(f112808,plain,
( ! [X2,X3,X0,X1,X4] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,sK30)
| ~ r1(sK13,X3)
| ~ r1(X3,X4)
| p1(sK34(sK24(sK30)))
| ~ r1(X4,X0) )
| ~ spl50_829
| spl50_830 ),
inference(forward_subsumption_resolution,[],[f112807,f13868]) ).
fof(f112819,definition,
( spl50_8670
<=> p1(sK34(sK24(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8670])],[avatar_definition]) ).
fof(f112821,plain,
( p1(sK34(sK24(sK30)))
| ~ spl50_8670 ),
inference(avatar_component_clause,[],[f112819]) ).
fof(f112822,plain,
( spl50_8670
| spl50_734
| ~ spl50_829
| spl50_830 ),
inference(avatar_split_clause,[],[f112808,f13867,f13863,f8461,f112819]) ).
fof(f112823,plain,
( p1(sK24(sK30))
| ~ r1(sK30,sK24(sK30))
| ~ spl50_8670 ),
inference(resolution,[],[f112821,f88]) ).
fof(f112824,plain,
( ~ r1(sK30,sK24(sK30))
| spl50_1309
| ~ spl50_8670 ),
inference(forward_subsumption_resolution,[],[f112823,f19667]) ).
fof(f112825,plain,
( $false
| ~ spl50_1308
| spl50_1309
| ~ spl50_8670 ),
inference(forward_subsumption_resolution,[],[f112824,f19663]) ).
fof(f112826,plain,
( ~ spl50_1308
| spl50_1309
| ~ spl50_8670 ),
inference(avatar_contradiction_clause,[],[f112825]) ).
fof(f112858,plain,
( ! [X0] :
( ~ r1(sK18(sK9(sK30)),X0)
| p1(X0) )
| ~ spl50_8428
| ~ spl50_8500 ),
inference(resolution,[],[f108388,f107565]) ).
fof(f112859,plain,
( r1(sK18(sK9(sK30)),sK17(sK18(sK9(sK30))))
| ~ spl50_8500
| ~ spl50_8501 ),
inference(resolution,[],[f108388,f108391]) ).
fof(f112862,plain,
( p1(sK18(sK9(sK30)))
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8500 ),
inference(resolution,[],[f108388,f108297]) ).
fof(f112871,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)
| ~ r1(X6,sK9(sK30))
| p1(sK9(sK30))
| ~ r1(sK9(sK30),X7)
| ~ p1(sK17(X7))
| ~ r1(sK13,X0) )
| ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8500 ),
inference(resolution,[],[f112862,f119]) ).
fof(f112872,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)
| ~ r1(X6,sK9(sK30))
| ~ r1(sK9(sK30),X7)
| ~ p1(sK17(X7))
| ~ r1(sK13,X0) )
| ~ spl50_7911
| ~ spl50_8417
| spl50_8432
| ~ spl50_8500 ),
inference(forward_subsumption_resolution,[],[f112871,f107597]) ).
fof(f112898,definition,
( spl50_8672
<=> ! [X7] :
( ~ r1(sK9(sK30),X7)
| ~ p1(sK17(X7)) ) ),
introduced(definition,[new_symbols(definition,[spl50_8672])],[avatar_definition]) ).
fof(f112899,plain,
( ! [X7] :
( ~ r1(sK9(sK30),X7)
| ~ p1(sK17(X7)) )
| ~ spl50_8672 ),
inference(avatar_component_clause,[],[f112898]) ).
fof(f112900,plain,
( spl50_8672
| spl50_8503
| ~ spl50_7911
| ~ spl50_8417
| spl50_8432
| ~ spl50_8500 ),
inference(avatar_split_clause,[],[f112872,f108386,f107596,f107465,f99680,f108432,f112898]) ).
fof(f112903,plain,
( ~ p1(sK17(sK18(sK9(sK30))))
| ~ spl50_8500
| ~ spl50_8672 ),
inference(resolution,[],[f112899,f108388]) ).
fof(f112943,plain,
( p1(sK17(sK18(sK9(sK30))))
| ~ spl50_8428
| ~ spl50_8500
| ~ spl50_8501 ),
inference(resolution,[],[f112859,f112858]) ).
fof(f112957,plain,
( $false
| ~ spl50_8428
| ~ spl50_8500
| ~ spl50_8501
| ~ spl50_8672 ),
inference(forward_subsumption_resolution,[],[f112943,f112903]) ).
fof(f112958,plain,
( ~ spl50_8428
| ~ spl50_8500
| ~ spl50_8501
| ~ spl50_8672 ),
inference(avatar_contradiction_clause,[],[f112957]) ).
fof(f112991,plain,
( ~ sP0(sK30)
| ~ sP1(sK30)
| ~ spl50_8421 ),
inference(resolution,[],[f107505,f42]) ).
fof(f112992,plain,
( ~ sP1(sK30)
| ~ spl50_830
| ~ spl50_8421 ),
inference(forward_subsumption_resolution,[],[f112991,f13869]) ).
fof(f112993,plain,
( $false
| ~ spl50_830
| ~ spl50_7911
| ~ spl50_8421 ),
inference(forward_subsumption_resolution,[],[f112992,f99681]) ).
fof(f112994,plain,
( ~ spl50_830
| ~ spl50_7911
| ~ spl50_8421 ),
inference(avatar_contradiction_clause,[],[f112993]) ).
fof(f112995,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| r1(sK23(sK8(sK30)),sK11(sK23(sK8(sK30))))
| ~ sP0(X0) )
| ~ spl50_8415
| spl50_8419 ),
inference(forward_subsumption_resolution,[],[f107488,f107498]) ).
fof(f113202,definition,
( spl50_8693
<=> r1(sK23(sK8(sK30)),sK11(sK23(sK8(sK30)))) ),
introduced(definition,[new_symbols(definition,[spl50_8693])],[avatar_definition]) ).
fof(f113204,plain,
( r1(sK23(sK8(sK30)),sK11(sK23(sK8(sK30))))
| ~ spl50_8693 ),
inference(avatar_component_clause,[],[f113202]) ).
fof(f113205,plain,
( spl50_8693
| spl50_8421
| ~ spl50_8415
| spl50_8419 ),
inference(avatar_split_clause,[],[f112995,f107497,f107458,f107504,f113202]) ).
fof(f113206,plain,
( ! [X0] :
( ~ p1(sK11(sK23(sK8(sK30))))
| p1(X0)
| ~ r1(sK11(sK23(sK8(sK30))),X0) )
| ~ spl50_8423
| ~ spl50_8693 ),
inference(resolution,[],[f113204,f107515]) ).
fof(f113215,plain,
( ! [X0] :
( ~ r1(sK11(sK23(sK8(sK30))),X0)
| p1(X0) )
| ~ spl50_8418
| ~ spl50_8423
| ~ spl50_8693 ),
inference(forward_subsumption_resolution,[],[f113206,f107495]) ).
fof(f113838,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| r1(sK11(sK23(sK8(sK30))),sK12(sK23(sK8(sK30))))
| ~ sP0(X0) )
| ~ spl50_8415
| spl50_8419 ),
inference(forward_subsumption_resolution,[],[f107487,f107498]) ).
fof(f113852,definition,
( spl50_8762
<=> r1(sK11(sK23(sK8(sK30))),sK12(sK23(sK8(sK30)))) ),
introduced(definition,[new_symbols(definition,[spl50_8762])],[avatar_definition]) ).
fof(f113854,plain,
( r1(sK11(sK23(sK8(sK30))),sK12(sK23(sK8(sK30))))
| ~ spl50_8762 ),
inference(avatar_component_clause,[],[f113852]) ).
fof(f113855,plain,
( spl50_8762
| spl50_8421
| ~ spl50_8415
| spl50_8419 ),
inference(avatar_split_clause,[],[f113838,f107497,f107458,f107504,f113852]) ).
fof(f113856,plain,
( p1(sK12(sK23(sK8(sK30))))
| ~ spl50_8418
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(resolution,[],[f113854,f113215]) ).
fof(f113864,plain,
( ! [X0,X1] :
( ~ r1(X0,sK23(sK8(sK30)))
| p1(sK23(sK8(sK30)))
| ~ r1(X1,X0)
| ~ sP0(X1) )
| ~ spl50_8418
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(resolution,[],[f113856,f44]) ).
fof(f113865,plain,
( ! [X0,X1] :
( ~ r1(X0,sK23(sK8(sK30)))
| ~ r1(X1,X0)
| ~ sP0(X1) )
| ~ spl50_8418
| spl50_8419
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(forward_subsumption_resolution,[],[f113864,f107498]) ).
fof(f113866,plain,
( ! [X0] :
( ~ r1(X0,sK8(sK30))
| ~ sP0(X0) )
| ~ spl50_8415
| ~ spl50_8418
| spl50_8419
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(resolution,[],[f113865,f107460]) ).
fof(f113867,plain,
( spl50_8421
| ~ spl50_8415
| ~ spl50_8418
| spl50_8419
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(avatar_split_clause,[],[f113866,f113852,f113202,f107514,f107497,f107493,f107458,f107504]) ).
fof(f113872,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| sP1(sK30)
| ~ sP3(sK30) )
| ~ spl50_319 ),
inference(forward_subsumption_resolution,[],[f110945,f3197]) ).
fof(f113873,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| r1(sK4(sK32),sK5(sK32))
| sP1(sK30) )
| ~ spl50_319 ),
inference(forward_subsumption_resolution,[],[f113872,f52343]) ).
fof(f113874,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0)
| sP1(sK30) )
| ~ spl50_319
| spl50_7794 ),
inference(forward_subsumption_resolution,[],[f113873,f96647]) ).
fof(f113875,plain,
( ! [X0] :
( p1(X0)
| ~ r1(sK30,X0) )
| ~ spl50_319
| spl50_7794
| spl50_7911 ),
inference(forward_subsumption_resolution,[],[f113874,f99682]) ).
fof(f113876,plain,
( spl50_3964
| ~ spl50_319
| spl50_7794
| spl50_7911 ),
inference(avatar_split_clause,[],[f113875,f99680,f96646,f3195,f52904]) ).
fof(f114311,definition,
( spl50_8802
<=> p1(sK34(sK7(sK30))) ),
introduced(definition,[new_symbols(definition,[spl50_8802])],[avatar_definition]) ).
fof(f114312,plain,
( ~ p1(sK34(sK7(sK30)))
| spl50_8802 ),
inference(avatar_component_clause,[],[f114311]) ).
fof(f114313,plain,
( p1(sK34(sK7(sK30)))
| ~ spl50_8802 ),
inference(avatar_component_clause,[],[f114311]) ).
fof(f121191,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(sK33(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK30,sK7(X0)) ),
inference(resolution,[],[f30,f90]) ).
fof(f121193,plain,
! [X2,X0,X1] :
( ~ r1(sK33(sK7(X0)),X2)
| ~ p1(sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK30,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f121191,f31]) ).
fof(f121553,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| ~ p1(sK33(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK30,sK7(X1)) ),
inference(resolution,[],[f121193,f89]) ).
fof(f121563,plain,
! [X0,X1] :
( ~ p1(sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| ~ p1(sK33(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f121553]) ).
fof(f121567,plain,
! [X0,X1] :
( ~ p1(sK33(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| ~ p1(sK6(X0))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f121563,f31]) ).
fof(f121596,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ p1(sK6(X0))
| ~ sP2(sK30)
| ~ r1(sK30,sK7(sK30)) )
| ~ spl50_4362 ),
inference(resolution,[],[f121567,f56531]) ).
fof(f121597,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ p1(sK6(X0))
| ~ sP2(sK30) )
| ~ spl50_4362 ),
inference(forward_subsumption_resolution,[],[f121596,f32]) ).
fof(f121598,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ p1(sK6(X0))
| ~ sP2(sK30) )
| spl50_319
| ~ spl50_4362 ),
inference(forward_subsumption_resolution,[],[f121597,f3196]) ).
fof(f121599,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| ~ p1(sK6(X0)) )
| spl50_319
| ~ spl50_4362 ),
inference(forward_subsumption_resolution,[],[f121598,f33121]) ).
fof(f121608,definition,
( spl50_9138
<=> ! [X0] :
( ~ r1(sK30,X0)
| ~ p1(sK6(X0)) ) ),
introduced(definition,[new_symbols(definition,[spl50_9138])],[avatar_definition]) ).
fof(f121609,plain,
( ! [X0] :
( ~ p1(sK6(X0))
| ~ r1(sK30,X0) )
| ~ spl50_9138 ),
inference(avatar_component_clause,[],[f121608]) ).
fof(f121610,plain,
( spl50_8802
| spl50_9138
| spl50_319
| ~ spl50_4362 ),
inference(avatar_split_clause,[],[f121599,f56529,f3195,f121608,f114311]) ).
fof(f121611,plain,
( p1(sK7(sK30))
| ~ r1(sK30,sK7(sK30))
| ~ spl50_8802 ),
inference(resolution,[],[f114313,f88]) ).
fof(f121612,plain,
( ~ r1(sK30,sK7(sK30))
| spl50_4361
| ~ spl50_8802 ),
inference(forward_subsumption_resolution,[],[f121611,f56525]) ).
fof(f121613,plain,
( $false
| ~ spl50_4358
| spl50_4361
| ~ spl50_8802 ),
inference(forward_subsumption_resolution,[],[f121612,f56487]) ).
fof(f121614,plain,
( ~ spl50_4358
| spl50_4361
| ~ spl50_8802 ),
inference(avatar_contradiction_clause,[],[f121613]) ).
fof(f122535,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(sK33(sK7(X0)),X2)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| p1(sK7(X0))
| ~ r1(sK30,sK7(X0)) ),
inference(resolution,[],[f33,f90]) ).
fof(f122537,plain,
! [X2,X0,X1] :
( ~ r1(sK33(sK7(X0)),X2)
| r1(X1,sK6(X1))
| p1(X0)
| ~ r1(X0,X1)
| p1(X2)
| ~ p1(sK33(sK7(X0)))
| ~ sP2(X0)
| ~ r1(sK30,sK7(X0)) ),
inference(forward_subsumption_resolution,[],[f122535,f34]) ).
fof(f122558,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| ~ p1(sK33(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1))
| p1(sK7(X1))
| ~ r1(sK30,sK7(X1)) ),
inference(resolution,[],[f122537,f89]) ).
fof(f122568,plain,
! [X0,X1] :
( r1(X0,sK6(X0))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| ~ p1(sK33(sK7(X1)))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1))
| p1(sK7(X1)) ),
inference(duplicate_literal_removal,[],[f122558]) ).
fof(f122570,plain,
! [X0,X1] :
( ~ p1(sK33(sK7(X1)))
| p1(X1)
| ~ r1(X1,X0)
| p1(sK34(sK7(X1)))
| r1(X0,sK6(X0))
| ~ sP2(X1)
| ~ r1(sK30,sK7(X1)) ),
inference(forward_subsumption_resolution,[],[f122568,f34]) ).
fof(f126207,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| r1(X0,sK6(X0))
| ~ sP2(sK30)
| ~ r1(sK30,sK7(sK30)) )
| ~ spl50_4362 ),
inference(resolution,[],[f122570,f56531]) ).
fof(f126208,plain,
( ! [X0] :
( p1(sK30)
| ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| r1(X0,sK6(X0))
| ~ sP2(sK30) )
| ~ spl50_4362 ),
inference(forward_subsumption_resolution,[],[f126207,f35]) ).
fof(f126209,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| p1(sK34(sK7(sK30)))
| r1(X0,sK6(X0))
| ~ sP2(sK30) )
| spl50_319
| ~ spl50_4362 ),
inference(forward_subsumption_resolution,[],[f126208,f3196]) ).
fof(f126210,plain,
( ! [X0] :
( ~ r1(sK30,X0)
| r1(X0,sK6(X0))
| ~ sP2(sK30) )
| spl50_319
| ~ spl50_4362
| spl50_8802 ),
inference(forward_subsumption_resolution,[],[f126209,f114312]) ).
fof(f126211,plain,
( ! [X0] :
( r1(X0,sK6(X0))
| ~ r1(sK30,X0) )
| spl50_319
| ~ spl50_4362
| spl50_8802 ),
inference(forward_subsumption_resolution,[],[f126210,f33121]) ).
fof(f126938,plain,
( ~ r1(sK30,sK32)
| p1(sK6(sK32))
| spl50_319
| ~ spl50_4362
| spl50_8802 ),
inference(resolution,[],[f126211,f91]) ).
fof(f127641,plain,
( ~ r1(sK30,sK32)
| spl50_319
| ~ spl50_4362
| spl50_8802
| ~ spl50_9138 ),
inference(forward_subsumption_resolution,[],[f126938,f121609]) ).
fof(f127753,plain,
( $false
| spl50_319
| ~ spl50_4362
| spl50_8802
| ~ spl50_9138 ),
inference(forward_subsumption_resolution,[],[f127641,f92]) ).
fof(f127754,plain,
( spl50_319
| ~ spl50_4362
| spl50_8802
| ~ spl50_9138 ),
inference(avatar_contradiction_clause,[],[f127753]) ).
cnf(s6208,plain,
~ spl50_734,
inference(sat_conversion,[],[f8488]) ).
cnf(s14235,plain,
( spl50_830
| spl50_1308 ),
inference(sat_conversion,[],[f19673]) ).
cnf(s14241,plain,
( spl50_734
| spl50_830
| ~ spl50_1309 ),
inference(sat_conversion,[],[f19676]) ).
cnf(s22354,plain,
( spl50_829
| spl50_830
| spl50_1309 ),
inference(sat_conversion,[],[f32206]) ).
cnf(s33941,plain,
~ spl50_3964,
inference(sat_conversion,[],[f52963]) ).
cnf(s35578,plain,
( spl50_319
| spl50_4358
| spl50_4359 ),
inference(sat_conversion,[],[f56492]) ).
cnf(s35611,plain,
( ~ spl50_4358
| spl50_4361
| spl50_4362 ),
inference(sat_conversion,[],[f56532]) ).
cnf(s35790,plain,
( spl50_319
| ~ spl50_4361 ),
inference(sat_conversion,[],[f57500]) ).
cnf(s37605,plain,
( spl50_319
| spl50_4358
| ~ spl50_4359 ),
inference(sat_conversion,[],[f62786]) ).
cnf(s51905,plain,
( spl50_24
| spl50_7799 ),
inference(sat_conversion,[],[f96690]) ).
cnf(s52572,plain,
( spl50_24
| ~ spl50_7799
| spl50_7888 ),
inference(sat_conversion,[],[f98448]) ).
cnf(s52585,plain,
~ spl50_7888,
inference(sat_conversion,[],[f98514]) ).
cnf(s52614,plain,
( ~ spl50_24
| ~ spl50_3963
| spl50_7814 ),
inference(sat_conversion,[],[f98548]) ).
cnf(s52630,plain,
( ~ spl50_7794
| ~ spl50_7814
| spl50_7890 ),
inference(sat_conversion,[],[f98573]) ).
cnf(s56426,plain,
( ~ spl50_319
| spl50_3964
| ~ spl50_7890
| spl50_7911 ),
inference(sat_conversion,[],[f103966]) ).
cnf(s57073,plain,
( ~ spl50_319
| spl50_3963
| spl50_3964
| spl50_7911 ),
inference(sat_conversion,[],[f105912]) ).
cnf(s57835,plain,
( ~ spl50_7911
| spl50_8415
| spl50_8417 ),
inference(sat_conversion,[],[f107467]) ).
cnf(s57851,plain,
( ~ spl50_8415
| spl50_8418
| spl50_8419
| spl50_8421 ),
inference(sat_conversion,[],[f107506]) ).
cnf(s57858,plain,
( ~ spl50_7911
| ~ spl50_8415
| spl50_8419
| spl50_8423 ),
inference(sat_conversion,[],[f107516]) ).
cnf(s57890,plain,
( ~ spl50_7911
| spl50_8426
| spl50_8428 ),
inference(sat_conversion,[],[f107566]) ).
cnf(s58067,plain,
( spl50_8417
| ~ spl50_8419
| spl50_8461 ),
inference(sat_conversion,[],[f107991]) ).
cnf(s58256,plain,
( ~ spl50_7911
| spl50_8500
| spl50_8501 ),
inference(sat_conversion,[],[f108392]) ).
cnf(s58268,plain,
( ~ spl50_7911
| ~ spl50_8417
| spl50_8432
| ~ spl50_8500
| spl50_8501
| spl50_8503 ),
inference(sat_conversion,[],[f108434]) ).
cnf(s58274,plain,
( ~ spl50_7911
| ~ spl50_8432 ),
inference(sat_conversion,[],[f108440]) ).
cnf(s58281,plain,
( ~ spl50_7911
| spl50_8461
| ~ spl50_8503 ),
inference(sat_conversion,[],[f108443]) ).
cnf(s58286,plain,
( spl50_734
| ~ spl50_7911
| ~ spl50_8461 ),
inference(sat_conversion,[],[f108446]) ).
cnf(s58432,plain,
( ~ spl50_830
| ~ spl50_7911
| ~ spl50_8428
| spl50_8500
| ~ spl50_8501
| spl50_8503 ),
inference(sat_conversion,[],[f108741]) ).
cnf(s58670,plain,
( ~ spl50_7911
| ~ spl50_8417
| ~ spl50_8426
| spl50_8428
| spl50_8503 ),
inference(sat_conversion,[],[f109166]) ).
cnf(s59615,plain,
( spl50_734
| ~ spl50_829
| spl50_830
| spl50_8670 ),
inference(sat_conversion,[],[f112822]) ).
cnf(s59618,plain,
( ~ spl50_1308
| spl50_1309
| ~ spl50_8670 ),
inference(sat_conversion,[],[f112826]) ).
cnf(s59713,plain,
( ~ spl50_7911
| ~ spl50_8417
| spl50_8432
| ~ spl50_8500
| spl50_8503
| spl50_8672 ),
inference(sat_conversion,[],[f112900]) ).
cnf(s59759,plain,
( ~ spl50_8428
| ~ spl50_8500
| ~ spl50_8501
| ~ spl50_8672 ),
inference(sat_conversion,[],[f112958]) ).
cnf(s59803,plain,
( ~ spl50_830
| ~ spl50_7911
| ~ spl50_8421 ),
inference(sat_conversion,[],[f112994]) ).
cnf(s59918,plain,
( ~ spl50_8415
| spl50_8419
| spl50_8421
| spl50_8693 ),
inference(sat_conversion,[],[f113205]) ).
cnf(s60283,plain,
( ~ spl50_8415
| spl50_8419
| spl50_8421
| spl50_8762 ),
inference(sat_conversion,[],[f113855]) ).
cnf(s60296,plain,
( ~ spl50_8415
| ~ spl50_8418
| spl50_8419
| spl50_8421
| ~ spl50_8423
| ~ spl50_8693
| ~ spl50_8762 ),
inference(sat_conversion,[],[f113867]) ).
cnf(s60315,plain,
( ~ spl50_319
| spl50_3964
| spl50_7794
| spl50_7911 ),
inference(sat_conversion,[],[f113876]) ).
cnf(s64576,plain,
( spl50_319
| ~ spl50_4362
| spl50_8802
| spl50_9138 ),
inference(sat_conversion,[],[f121610]) ).
cnf(s64579,plain,
( ~ spl50_4358
| spl50_4361
| ~ spl50_8802 ),
inference(sat_conversion,[],[f121614]) ).
cnf(s67372,plain,
( spl50_319
| ~ spl50_4362
| spl50_8802
| ~ spl50_9138 ),
inference(sat_conversion,[],[f127754]) ).
cnf(s67407,plain,
( spl50_24
| ~ spl50_7799 ),
inference(rat,[],[s52572,s52585]) ).
cnf(s67459,plain,
spl50_24,
inference(rat,[],[s51905,s67407]) ).
cnf(s67461,plain,
( spl50_830
| spl50_829 ),
inference(rat,[],[s14241,s22354,s6208]) ).
cnf(s67463,plain,
spl50_830,
inference(rat,[],[s59618,s59615,s14235,s14241,s67461,s6208]) ).
cnf(s67484,plain,
( spl50_4358
| spl50_319 ),
inference(rat,[],[s35578,s37605]) ).
cnf(s67485,plain,
( ~ spl50_4362
| spl50_8802
| spl50_319 ),
inference(rat,[],[s64576,s67372]) ).
cnf(s67486,plain,
spl50_319,
inference(rat,[],[s67485,s35611,s64579,s67484,s35790]) ).
cnf(s67488,plain,
( spl50_8500
| ~ spl50_8428
| ~ spl50_7911
| spl50_8503 ),
inference(rat,[],[s58256,s58432,s67463]) ).
cnf(s67489,plain,
( ~ spl50_8428
| ~ spl50_8417
| ~ spl50_7911 ),
inference(rat,[],[s59759,s59713,s58268,s67488,s58274,s58281,s58286,s6208]) ).
cnf(s67490,plain,
( ~ spl50_8417
| ~ spl50_7911 ),
inference(rat,[],[s58670,s57890,s67489,s58281,s58286,s6208]) ).
cnf(s67491,plain,
~ spl50_7911,
inference(rat,[],[s60296,s57851,s57858,s59918,s60283,s57835,s58067,s67490,s58286,s59803,s6208,s67463]) ).
cnf(s67493,plain,
spl50_7794,
inference(rat,[],[s60315,s67486,s33941,s67491]) ).
cnf(s67494,plain,
spl50_3963,
inference(rat,[],[s57073,s67486,s33941,s67491]) ).
cnf(s67495,plain,
~ spl50_7890,
inference(rat,[],[s56426,s67486,s33941,s67491]) ).
cnf(s67496,plain,
~ spl50_7814,
inference(rat,[],[s52630,s67495,s67493]) ).
cnf(s67499,plain,
$false,
inference(rat,[],[s52614,s67459,s67496,s67494]) ).
fof(f127757,plain,
$false,
inference(avatar_sat_refutation,[],[s67499]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.37 % Computer : n020.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 16:10:34 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 Running first-order model finding
% 0.11/0.40 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.17/3.43 % (3575426)Will run a generic schedule for satisfiability detection.
% 21.17/3.43 % (3575433)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=47850025:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 21.17/3.43 % (3575432)% WARNING: option uhcvi not known.
% 21.17/3.43 % (3575432)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1275319868:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 21.17/3.43 % (3575431)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3652830466_2999 on theBenchmark for (2999ds/0Mi)
% 21.17/3.43 % (3575434)dis+10_1_sil=32000:sp=arity:random_seed=936405618:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 21.17/3.43 % (3575435)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1094991240:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 21.17/3.43 % (3575437)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=237109967:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 21.17/3.43 % (3575436)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1277973040:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 21.17/3.43 % TRYING [1]
% 21.17/3.43 % TRYING [2]
% 21.17/3.43 % TRYING [3]
% 21.17/3.43 % (3575434)Instruction limit reached!
% 21.17/3.43 % (3575434)------------------------------
% 21.17/3.43 % (3575434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.17/3.43 % (3575434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.43 % (3575434)CaDiCaL version: 2.1.3
% 21.17/3.43 % (3575434)Termination reason: Instruction limit
% 21.17/3.43 % (3575434)Termination phase: Saturation
% 21.17/3.43 % (3575434)Time elapsed: 0.049 s
% 21.17/3.43 % (3575434)Peak memory usage: 12 MB
% 21.17/3.43 % (3575434)Instructions burned: 104 (million)
% 21.17/3.43 % (3575435)Instruction limit reached!
% 21.17/3.43 % (3575435)------------------------------
% 21.17/3.43 % (3575435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.17/3.43 % (3575435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.43 % (3575435)CaDiCaL version: 2.1.3
% 21.17/3.43 % (3575435)Termination reason: Instruction limit
% 21.17/3.43 % (3575435)Termination phase: Saturation
% 21.17/3.43 % (3575435)Time elapsed: 0.052 s
% 21.17/3.43 % (3575435)Peak memory usage: 12 MB
% 21.17/3.43 % (3575435)Instructions burned: 116 (million)
% 21.17/3.43 % (3575436)Instruction limit reached!
% 21.17/3.43 % (3575436)------------------------------
% 21.17/3.43 % (3575436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.17/3.43 % (3575436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.43 % (3575436)CaDiCaL version: 2.1.3
% 21.17/3.43 % (3575436)Termination reason: Instruction limit
% 21.17/3.43 % (3575436)Termination phase: Saturation
% 21.17/3.43 % (3575436)Time elapsed: 0.062 s
% 21.17/3.43 % (3575436)Peak memory usage: 12 MB
% 21.17/3.43 % (3575436)Instructions burned: 132 (million)
% 21.17/3.43 % (3575445)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2391855901:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 21.17/3.43 % (3575446)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=827167181:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 21.17/3.43 % TRYING [1]
% 21.17/3.43 % TRYING [2]
% 21.17/3.43 % TRYING [3]
% 21.17/3.43 % (3575447)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1673539678:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 21.17/3.43 % (3575437)Instruction limit reached!
% 21.17/3.43 % (3575437)------------------------------
% 21.17/3.43 % (3575437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.17/3.43 % (3575437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.17/3.43 % (3575437)CaDiCaL version: 2.1.3
% 21.17/3.43 % (3575437)Termination reason: Instruction limit
% 21.17/3.43 % (3575437)Termination phase: Saturation
% 21.17/3.43 % (3575437)Time elapsed: 0.084 s
% 21.17/3.43 % (3575437)Peak memory usage: 14 MB
% 21.17/3.43 % (3575437)Instructions burned: 160 (million)
% 21.17/3.43 % (3575451)ott-21_1_sil=16000:fs=off:random_seed=1249973449:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 21.17/3.43 % TRYING [4]
% 21.17/3.43 % TRYING [4]
% 21.17/3.43 % (3575446)Instruction limit reached!
% 21.17/3.43 % (3575446)------------------------------
% 21.17/3.43 % (3575446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.17/3.43 % (3575446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575446)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575446)Termination reason: Instruction limit
% 40.57/6.16 % (3575446)Termination phase: Saturation
% 40.57/6.16 % (3575446)Time elapsed: 0.068 s
% 40.57/6.16 % (3575446)Peak memory usage: 12 MB
% 40.57/6.16 % (3575446)Instructions burned: 132 (million)
% 40.57/6.16 % (3575453)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=806182718:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 40.57/6.16 % (3575451)Instruction limit reached!
% 40.57/6.16 % (3575451)------------------------------
% 40.57/6.16 % (3575451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575451)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575451)Termination reason: Instruction limit
% 40.57/6.16 % (3575451)Termination phase: Saturation
% 40.57/6.16 % (3575451)Time elapsed: 0.094 s
% 40.57/6.16 % (3575451)Peak memory usage: 13 MB
% 40.57/6.16 % (3575451)Instructions burned: 181 (million)
% 40.57/6.16 % (3575455)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1496590430:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 40.57/6.16 % TRYING [1]
% 40.57/6.16 % TRYING [2]
% 40.57/6.16 % TRYING [3]
% 40.57/6.16 % TRYING [4]
% 40.57/6.16 % (3575453)Instruction limit reached!
% 40.57/6.16 % (3575453)------------------------------
% 40.57/6.16 % (3575453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575453)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575453)Termination reason: Instruction limit
% 40.57/6.16 % (3575453)Termination phase: Saturation
% 40.57/6.16 % (3575453)Time elapsed: 0.227 s
% 40.57/6.16 % (3575453)Peak memory usage: 14 MB
% 40.57/6.16 % (3575453)Instructions burned: 478 (million)
% 40.57/6.16 % (3575457)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3794499348:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 40.57/6.16 % TRYING [5]
% 40.57/6.16 % (3575445)Instruction limit reached!
% 40.57/6.16 % (3575445)------------------------------
% 40.57/6.16 % (3575445)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575445)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575445)Termination reason: Instruction limit
% 40.57/6.16 % (3575445)Termination phase: Finite model building SAT solving
% 40.57/6.16 % (3575445)Time elapsed: 0.382 s
% 40.57/6.16 % (3575445)Peak memory usage: 14 MB
% 40.57/6.16 % (3575445)Instructions burned: 715 (million)
% 40.57/6.16 % (3575447)Instruction limit reached!
% 40.57/6.16 % (3575447)------------------------------
% 40.57/6.16 % (3575447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575447)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575447)Termination reason: Instruction limit
% 40.57/6.16 % (3575447)Termination phase: Saturation
% 40.57/6.16 % (3575447)Time elapsed: 0.375 s
% 40.57/6.16 % (3575447)Peak memory usage: 17 MB
% 40.57/6.16 % (3575447)Instructions burned: 685 (million)
% 40.57/6.16 % (3575459)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4112592919:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 40.57/6.16 % (3575460)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=276107159:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 40.57/6.16 % TRYING [14]
% 40.57/6.16 % (3575455)Instruction limit reached!
% 40.57/6.16 % (3575455)------------------------------
% 40.57/6.16 % (3575455)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575455)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575455)Termination reason: Instruction limit
% 40.57/6.16 % (3575455)Termination phase: Finite model building SAT solving
% 40.57/6.16 % (3575455)Time elapsed: 0.375 s
% 40.57/6.16 % (3575455)Peak memory usage: 15 MB
% 40.57/6.16 % (3575455)Instructions burned: 867 (million)
% 40.57/6.16 % (3575463)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=425340153:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 40.57/6.16 % TRYING [5]
% 40.57/6.16 % (3575460)Instruction limit reached!
% 40.57/6.16 % (3575460)------------------------------
% 40.57/6.16 % (3575460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575460)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575460)Termination reason: Instruction limit
% 40.57/6.16 % (3575460)Termination phase: Saturation
% 40.57/6.16 % (3575460)Time elapsed: 0.301 s
% 40.57/6.16 % (3575460)Peak memory usage: 16 MB
% 40.57/6.16 % (3575460)Instructions burned: 693 (million)
% 40.57/6.16 % (3575459)Instruction limit reached!
% 40.57/6.16 % (3575459)------------------------------
% 40.57/6.16 % (3575459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575459)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575459)Termination reason: Instruction limit
% 40.57/6.16 % (3575459)Termination phase: Finite model building SAT solving
% 40.57/6.16 % (3575459)Time elapsed: 0.315 s
% 40.57/6.16 % (3575459)Peak memory usage: 34 MB
% 40.57/6.16 % (3575459)Instructions burned: 890 (million)
% 40.57/6.16 % (3575465)fmb+10_1_sil=64000:random_seed=1018028638:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 40.57/6.16 % TRYING [1]
% 40.57/6.16 % TRYING [2]
% 40.57/6.16 % (3575466)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2899809624:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 40.57/6.16 % TRYING [3]
% 40.57/6.16 % TRYING [20]
% 40.57/6.16 % TRYING [4]
% 40.57/6.16 % TRYING [5]
% 40.57/6.16 % (3575463)Instruction limit reached!
% 40.57/6.16 % (3575463)------------------------------
% 40.57/6.16 % (3575463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575463)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575463)Termination reason: Instruction limit
% 40.57/6.16 % (3575463)Termination phase: Saturation
% 40.57/6.16 % (3575463)Time elapsed: 0.374 s
% 40.57/6.16 % (3575463)Peak memory usage: 15 MB
% 40.57/6.16 % (3575463)Instructions burned: 881 (million)
% 40.57/6.16 % (3575469)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=55762503:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 40.57/6.16 % TRYING [8]
% 40.57/6.16 % (3575457)Instruction limit reached!
% 40.57/6.16 % (3575457)------------------------------
% 40.57/6.16 % (3575457)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575457)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575457)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575457)Termination reason: Instruction limit
% 40.57/6.16 % (3575457)Termination phase: Saturation
% 40.57/6.16 % (3575457)Time elapsed: 0.630 s
% 40.57/6.16 % (3575457)Peak memory usage: 23 MB
% 40.57/6.16 % (3575457)Instructions burned: 1181 (million)
% 40.57/6.16 % (3575471)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2003891710:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 40.57/6.16 % (3575469)Instruction limit reached!
% 40.57/6.16 % (3575469)------------------------------
% 40.57/6.16 % (3575469)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575469)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575469)Termination reason: Instruction limit
% 40.57/6.16 % (3575469)Termination phase: Finite model building SAT solving
% 40.57/6.16 % (3575469)Time elapsed: 0.480 s
% 40.57/6.16 % (3575469)Peak memory usage: 28 MB
% 40.57/6.16 % (3575469)Instructions burned: 920 (million)
% 40.57/6.16 % (3575473)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2766097608:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi)
% 40.57/6.16 % TRYING [6]
% 40.57/6.16 % (3575473)Instruction limit reached!
% 40.57/6.16 % (3575473)------------------------------
% 40.57/6.16 % (3575473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.16 % (3575473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.16 % (3575473)CaDiCaL version: 2.1.3
% 40.57/6.16 % (3575473)Termination reason: Instruction limit
% 40.57/6.16 % (3575473)Termination phase: Saturation
% 40.57/6.16 % (3575473)Time elapsed: 0.667 s
% 40.57/6.16 % (3575473)Peak memory usage: 39 MB
% 40.57/6.16 % (3575473)Instructions burned: 1475 (million)
% 40.57/6.16 % (3575475)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2664835116:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 40.57/6.16 % TRYING [77]
% 40.57/6.16 % (3575471)Instruction limit reached!
% 40.57/6.16 % (3575471)------------------------------
% 40.57/6.17 % (3575471)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575471)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575471)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575471)Termination reason: Instruction limit
% 40.57/6.17 % (3575471)Termination phase: Saturation
% 40.57/6.17 % (3575471)Time elapsed: 1.927 s
% 40.57/6.17 % (3575471)Peak memory usage: 17 MB
% 40.57/6.17 % (3575471)Instructions burned: 5133 (million)
% 40.57/6.17 % (3575477)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2371584052:fmbsr=2.30978:i=2174_2969 on theBenchmark for (2969ds/2174Mi)
% 40.57/6.17 % TRYING [16]
% 40.57/6.17 % (3575477)Instruction limit reached!
% 40.57/6.17 % (3575477)------------------------------
% 40.57/6.17 % (3575477)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575477)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575477)Termination reason: Instruction limit
% 40.57/6.17 % (3575477)Termination phase: Finite model building SAT solving
% 40.57/6.17 % (3575477)Time elapsed: 1.167 s
% 40.57/6.17 % (3575477)Peak memory usage: 76 MB
% 40.57/6.17 % (3575477)Instructions burned: 2175 (million)
% 40.57/6.17 % (3575479)ott-2_1_sil=16000:newcnf=on:random_seed=2400331942:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2957 on theBenchmark for (2957ds/869Mi)
% 40.57/6.17 % (3575479)Instruction limit reached!
% 40.57/6.17 % (3575479)------------------------------
% 40.57/6.17 % (3575479)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575479)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575479)Termination reason: Instruction limit
% 40.57/6.17 % (3575479)Termination phase: Saturation
% 40.57/6.17 % (3575479)Time elapsed: 0.421 s
% 40.57/6.17 % (3575479)Peak memory usage: 14 MB
% 40.57/6.17 % (3575479)Instructions burned: 869 (million)
% 40.57/6.17 % (3575475)Instruction limit reached!
% 40.57/6.17 % (3575475)------------------------------
% 40.57/6.17 % (3575475)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575475)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575475)Termination reason: Instruction limit
% 40.57/6.17 % (3575475)Termination phase: Finite model building constraint generation
% 40.57/6.17 % (3575475)Time elapsed: 2.435 s
% 40.57/6.17 % (3575475)Peak memory usage: 521 MB
% 40.57/6.17 % (3575475)Instructions burned: 6325 (million)
% 40.57/6.17 % (3575481)ott+10_1_sil=32000:tgt=ground:random_seed=3375833655:i=5114:av=off_2953 on theBenchmark for (2953ds/5114Mi)
% 40.57/6.17 % (3575483)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1303307706:i=54282_2952 on theBenchmark for (2952ds/54282Mi)
% 40.57/6.17 % TRYING [1]
% 40.57/6.17 % TRYING [2]
% 40.57/6.17 % (3575466)Instruction limit reached!
% 40.57/6.17 % (3575466)------------------------------
% 40.57/6.17 % (3575466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575466)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575466)Termination reason: Instruction limit
% 40.57/6.17 % (3575466)Termination phase: Finite model building SAT solving
% 40.57/6.17 % (3575466)Time elapsed: 3.941 s
% 40.57/6.17 % (3575466)Peak memory usage: 94 MB
% 40.57/6.17 % (3575466)Instructions burned: 9516 (million)
% 40.57/6.17 % TRYING [3]
% 40.57/6.17 % (3575485)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3166634911:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 40.57/6.17 % TRYING [4]
% 40.57/6.17 % TRYING [5]
% 40.57/6.17 % TRYING [6]
% 40.57/6.17 % (3575433) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3575426-3575433"...
% 40.57/6.17 % (3575433)...printing done.
% 40.57/6.17 % (3575433)Refutation found. Thanks to Tanya!
% 40.57/6.17 % SZS status Theorem for theBenchmark
% 40.57/6.17 % SZS output start Proof for theBenchmark
% See solution above
% 40.57/6.17 % (3575433)------------------------------
% 40.57/6.17 % (3575433)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.57/6.17 % (3575433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.57/6.17 % (3575433)CaDiCaL version: 2.1.3
% 40.57/6.17 % (3575433)Termination reason: Refutation
% 40.57/6.17 % (3575433)Time elapsed: 5.719 s
% 40.57/6.17 % (3575433)Peak memory usage: 82 MB
% 40.57/6.17 % (3575433)Instructions burned: 20161 (million)
% 40.57/6.17 % (3575426)Success in time 5.761 s
% 40.57/6.17 % Vampire exiting
%------------------------------------------------------------------------------