%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL676+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n008.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 12:00:02 PM UTC 2026
% Result : Theorem 5.79s 1.37s
% Output : Refutation 5.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 29
% Syntax : Number of formulae : 264 ( 10 unt; 27 def)
% Number of atoms : 5489 ( 0 equ)
% Maximal formula atoms : 769 ( 20 avg)
% Number of connectives : 7767 (2542 ~;4346 |; 851 &)
% ( 27 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 35 ( 33 usr; 29 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-1 aty)
% Number of variables : 1560 ( 0 sgn1328 !; 232 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X0,X1)
& r1(X1,X2) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitivity) ).
fof(f3,conjecture,
~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) ) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p3(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| 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)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f4,negated_conjecture,
~ ~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ~ p5(X1) ) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ p3(X0) ) )
| ( ~ ! [X1] :
( ~ r1(X0,X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ~ p5(X0) ) )
& ( ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ! [X1] :
( ~ r1(X0,X1)
| 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)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| ( ( ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
& ( p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) ) )
| ~ ( ( ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1) )
| ~ p2(X0) ) ) )
& ( p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p4(X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p3(X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p2(X0)
| p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false )
| ~ ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false )
| ~ ! [X0] :
( ~ r1(X1,X0)
| ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X0] :
( ~ r1(X1,X0)
| $false ) )
| ~ ( p1(X0)
| ! [X1] :
( ~ r1(X0,X1)
| $false ) ) ) ) )
& ! [X1] :
( ~ r1(X0,X1)
| p2(X1)
| ~ ! [X0] :
( ~ r1(X1,X0)
| p2(X0)
| ~ ! [X1] :
( ~ r1(X0,X1)
| ! [X0] :
( ~ r1(X1,X0)
| p2(X0) )
| ~ p2(X1) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
fof(f5,plain,
~ ~ ? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ p5(X3) ) ) )
& ( ! [X4] :
( ~ r1(X0,X4)
| p2(X4) )
| ~ ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p2(X7) )
| ~ p2(X6) ) ) ) )
| ! [X8] :
( ~ r1(X0,X8)
| p3(X8) )
| ~ ! [X9] :
( ~ r1(X0,X9)
| p3(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| p3(X11) )
| ~ p3(X10) ) )
| ( ~ ! [X12] :
( ~ r1(X0,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ~ p5(X13) ) )
& ( ! [X14] :
( ~ r1(X0,X14)
| p2(X14) )
| ~ ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p2(X17) )
| ~ p2(X16) ) ) ) )
| ! [X18] :
( ~ r1(X0,X18)
| p1(X18) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p1(X21) )
| ~ p1(X20) ) )
| ~ ( ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p2(X25) )
| ~ p2(X24) ) ) )
| ~ ! [X26] :
( ~ r1(X0,X26)
| p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| p2(X30) )
| ~ p2(X29) ) ) )
| ~ ! [X31] :
( ~ r1(X0,X31)
| ( ( ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
| ~ ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ( p2(X31)
| ~ ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
| ~ ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X42,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ~ ! [X50] :
( ~ r1(X42,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) )
| ~ ( ( ! [X52] :
( ~ r1(X41,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
| ~ ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) )
& ( p2(X41)
| ~ ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X61] :
( ~ r1(X0,X61)
| p4(X61)
| p3(X61)
| p2(X61)
| p1(X61)
| ! [X62] :
( ~ r1(X61,X62)
| p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) ) ) )
| ~ ! [X65] :
( ~ r1(X0,X65)
| p2(X65)
| p1(X65)
| ! [X66] :
( ~ r1(X65,X66)
| p4(X66)
| p3(X66)
| p2(X66)
| p1(X66)
| ! [X67] :
( ~ r1(X66,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] :
( ~ r1(X67,X68)
| p4(X68)
| p3(X68)
| p2(X68)
| p1(X68)
| ! [X69] :
( ~ r1(X68,X69)
| $false ) ) ) )
| ~ ! [X70] :
( ~ r1(X65,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X73] :
( ~ r1(X72,X73)
| p4(X73)
| p3(X73)
| p2(X73)
| p1(X73)
| ! [X74] :
( ~ r1(X73,X74)
| p4(X74)
| p3(X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false ) ) ) ) )
| ~ ( p2(X70)
| p1(X70)
| ! [X76] :
( ~ r1(X70,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| p4(X77)
| p3(X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] :
( ~ r1(X78,X79)
| $false ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| p4(X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| $false ) ) ) )
| ~ ! [X84] :
( ~ r1(X0,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] :
( ~ r1(X85,X86)
| p4(X86)
| p3(X86)
| p2(X86)
| p1(X86)
| ! [X87] :
( ~ r1(X86,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) ) ) )
| ~ ! [X89] :
( ~ r1(X84,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| p4(X91)
| p3(X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] :
( ~ r1(X92,X93)
| p4(X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| $false ) ) ) ) )
| ~ ( p1(X89)
| ! [X95] :
( ~ r1(X89,X95)
| p4(X95)
| p3(X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| p4(X97)
| p3(X97)
| p2(X97)
| p1(X97)
| ! [X98] :
( ~ r1(X97,X98)
| $false ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X99] :
( ~ r1(X0,X99)
| p4(X99)
| p3(X99)
| p2(X99)
| p1(X99)
| ! [X100] :
( ~ r1(X99,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| $false ) ) )
| ~ ! [X102] :
( ~ r1(X0,X102)
| p4(X102)
| p3(X102)
| p2(X102)
| p1(X102)
| ! [X103] :
( ~ r1(X102,X103)
| p4(X103)
| p3(X103)
| p2(X103)
| p1(X103)
| ! [X104] :
( ~ r1(X103,X104)
| p4(X104)
| p3(X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| $false ) ) )
| ~ ! [X106] :
( ~ r1(X102,X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| p4(X108)
| p3(X108)
| p2(X108)
| p1(X108)
| ! [X109] :
( ~ r1(X108,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) ) ) )
| ~ ( p4(X106)
| p3(X106)
| p2(X106)
| p1(X106)
| ! [X111] :
( ~ r1(X106,X111)
| p4(X111)
| p3(X111)
| p2(X111)
| p1(X111)
| ! [X112] :
( ~ r1(X111,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] :
( ~ r1(X112,X113)
| $false ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X114] :
( ~ r1(X0,X114)
| p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| $false ) ) )
| ~ ! [X117] :
( ~ r1(X0,X117)
| p3(X117)
| p2(X117)
| p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| p4(X118)
| p3(X118)
| p2(X118)
| p1(X118)
| ! [X119] :
( ~ r1(X118,X119)
| p4(X119)
| p3(X119)
| p2(X119)
| p1(X119)
| ! [X120] :
( ~ r1(X119,X120)
| $false ) ) )
| ~ ! [X121] :
( ~ r1(X117,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] :
( ~ r1(X122,X123)
| p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) ) ) )
| ~ ( p3(X121)
| p2(X121)
| p1(X121)
| ! [X126] :
( ~ r1(X121,X126)
| p4(X126)
| p3(X126)
| p2(X126)
| p1(X126)
| ! [X127] :
( ~ r1(X126,X127)
| p4(X127)
| p3(X127)
| p2(X127)
| p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| $false ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X129] :
( ~ r1(X0,X129)
| p4(X129)
| p3(X129)
| p2(X129)
| p1(X129)
| ! [X130] :
( ~ r1(X129,X130)
| p4(X130)
| p3(X130)
| p2(X130)
| p1(X130)
| ! [X131] :
( ~ r1(X130,X131)
| $false ) ) )
| ~ ! [X132] :
( ~ r1(X0,X132)
| p2(X132)
| p1(X132)
| ! [X133] :
( ~ r1(X132,X133)
| p4(X133)
| p3(X133)
| p2(X133)
| p1(X133)
| ! [X134] :
( ~ r1(X133,X134)
| p4(X134)
| p3(X134)
| p2(X134)
| p1(X134)
| ! [X135] :
( ~ r1(X134,X135)
| $false ) ) )
| ~ ! [X136] :
( ~ r1(X132,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p2(X137)
| p1(X137)
| ! [X138] :
( ~ r1(X137,X138)
| p4(X138)
| p3(X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| p4(X139)
| p3(X139)
| p2(X139)
| p1(X139)
| ! [X140] :
( ~ r1(X139,X140)
| $false ) ) ) )
| ~ ( p2(X136)
| p1(X136)
| ! [X141] :
( ~ r1(X136,X141)
| p4(X141)
| p3(X141)
| p2(X141)
| p1(X141)
| ! [X142] :
( ~ r1(X141,X142)
| p4(X142)
| p3(X142)
| p2(X142)
| p1(X142)
| ! [X143] :
( ~ r1(X142,X143)
| $false ) ) ) ) ) ) )
& ( p1(X0)
| ! [X144] :
( ~ r1(X0,X144)
| p4(X144)
| p3(X144)
| p2(X144)
| p1(X144)
| ! [X145] :
( ~ r1(X144,X145)
| p4(X145)
| p3(X145)
| p2(X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) ) )
| ~ ! [X147] :
( ~ r1(X0,X147)
| p1(X147)
| ! [X148] :
( ~ r1(X147,X148)
| p4(X148)
| p3(X148)
| p2(X148)
| p1(X148)
| ! [X149] :
( ~ r1(X148,X149)
| p4(X149)
| p3(X149)
| p2(X149)
| p1(X149)
| ! [X150] :
( ~ r1(X149,X150)
| $false ) ) )
| ~ ! [X151] :
( ~ r1(X147,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ! [X153] :
( ~ r1(X152,X153)
| p4(X153)
| p3(X153)
| p2(X153)
| p1(X153)
| ! [X154] :
( ~ r1(X153,X154)
| p4(X154)
| p3(X154)
| p2(X154)
| p1(X154)
| ! [X155] :
( ~ r1(X154,X155)
| $false ) ) ) )
| ~ ( p1(X151)
| ! [X156] :
( ~ r1(X151,X156)
| p4(X156)
| p3(X156)
| p2(X156)
| p1(X156)
| ! [X157] :
( ~ r1(X156,X157)
| p4(X157)
| p3(X157)
| p2(X157)
| p1(X157)
| ! [X158] :
( ~ r1(X157,X158)
| $false ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X159] :
( ~ r1(X0,X159)
| p4(X159)
| p3(X159)
| p2(X159)
| p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| $false ) )
| ~ ! [X161] :
( ~ r1(X0,X161)
| p4(X161)
| p3(X161)
| p2(X161)
| p1(X161)
| ! [X162] :
( ~ r1(X161,X162)
| p4(X162)
| p3(X162)
| p2(X162)
| p1(X162)
| ! [X163] :
( ~ r1(X162,X163)
| $false ) )
| ~ ! [X164] :
( ~ r1(X161,X164)
| ! [X165] :
( ~ r1(X164,X165)
| p4(X165)
| p3(X165)
| p2(X165)
| p1(X165)
| ! [X166] :
( ~ r1(X165,X166)
| p4(X166)
| p3(X166)
| p2(X166)
| p1(X166)
| ! [X167] :
( ~ r1(X166,X167)
| $false ) ) )
| ~ ( p4(X164)
| p3(X164)
| p2(X164)
| p1(X164)
| ! [X168] :
( ~ r1(X164,X168)
| p4(X168)
| p3(X168)
| p2(X168)
| p1(X168)
| ! [X169] :
( ~ r1(X168,X169)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X170] :
( ~ r1(X0,X170)
| p4(X170)
| p3(X170)
| p2(X170)
| p1(X170)
| ! [X171] :
( ~ r1(X170,X171)
| $false ) )
| ~ ! [X172] :
( ~ r1(X0,X172)
| p3(X172)
| p2(X172)
| p1(X172)
| ! [X173] :
( ~ r1(X172,X173)
| p4(X173)
| p3(X173)
| p2(X173)
| p1(X173)
| ! [X174] :
( ~ r1(X173,X174)
| $false ) )
| ~ ! [X175] :
( ~ r1(X172,X175)
| ! [X176] :
( ~ r1(X175,X176)
| p3(X176)
| p2(X176)
| p1(X176)
| ! [X177] :
( ~ r1(X176,X177)
| p4(X177)
| p3(X177)
| p2(X177)
| p1(X177)
| ! [X178] :
( ~ r1(X177,X178)
| $false ) ) )
| ~ ( p3(X175)
| p2(X175)
| p1(X175)
| ! [X179] :
( ~ r1(X175,X179)
| p4(X179)
| p3(X179)
| p2(X179)
| p1(X179)
| ! [X180] :
( ~ r1(X179,X180)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X181] :
( ~ r1(X0,X181)
| p4(X181)
| p3(X181)
| p2(X181)
| p1(X181)
| ! [X182] :
( ~ r1(X181,X182)
| $false ) )
| ~ ! [X183] :
( ~ r1(X0,X183)
| p2(X183)
| p1(X183)
| ! [X184] :
( ~ r1(X183,X184)
| p4(X184)
| p3(X184)
| p2(X184)
| p1(X184)
| ! [X185] :
( ~ r1(X184,X185)
| $false ) )
| ~ ! [X186] :
( ~ r1(X183,X186)
| ! [X187] :
( ~ r1(X186,X187)
| p2(X187)
| p1(X187)
| ! [X188] :
( ~ r1(X187,X188)
| p4(X188)
| p3(X188)
| p2(X188)
| p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| $false ) ) )
| ~ ( p2(X186)
| p1(X186)
| ! [X190] :
( ~ r1(X186,X190)
| p4(X190)
| p3(X190)
| p2(X190)
| p1(X190)
| ! [X191] :
( ~ r1(X190,X191)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X192] :
( ~ r1(X0,X192)
| p4(X192)
| p3(X192)
| p2(X192)
| p1(X192)
| ! [X193] :
( ~ r1(X192,X193)
| $false ) )
| ~ ! [X194] :
( ~ r1(X0,X194)
| p1(X194)
| ! [X195] :
( ~ r1(X194,X195)
| p4(X195)
| p3(X195)
| p2(X195)
| p1(X195)
| ! [X196] :
( ~ r1(X195,X196)
| $false ) )
| ~ ! [X197] :
( ~ r1(X194,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198)
| ! [X199] :
( ~ r1(X198,X199)
| p4(X199)
| p3(X199)
| p2(X199)
| p1(X199)
| ! [X200] :
( ~ r1(X199,X200)
| $false ) ) )
| ~ ( p1(X197)
| ! [X201] :
( ~ r1(X197,X201)
| p4(X201)
| p3(X201)
| p2(X201)
| p1(X201)
| ! [X202] :
( ~ r1(X201,X202)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X203] :
( ~ r1(X0,X203)
| $false )
| ~ ! [X204] :
( ~ r1(X0,X204)
| p4(X204)
| p3(X204)
| p2(X204)
| p1(X204)
| ! [X205] :
( ~ r1(X204,X205)
| $false )
| ~ ! [X206] :
( ~ r1(X204,X206)
| ! [X207] :
( ~ r1(X206,X207)
| p4(X207)
| p3(X207)
| p2(X207)
| p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| $false ) )
| ~ ( p4(X206)
| p3(X206)
| p2(X206)
| p1(X206)
| ! [X209] :
( ~ r1(X206,X209)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X210] :
( ~ r1(X0,X210)
| $false )
| ~ ! [X211] :
( ~ r1(X0,X211)
| p3(X211)
| p2(X211)
| p1(X211)
| ! [X212] :
( ~ r1(X211,X212)
| $false )
| ~ ! [X213] :
( ~ r1(X211,X213)
| ! [X214] :
( ~ r1(X213,X214)
| p3(X214)
| p2(X214)
| p1(X214)
| ! [X215] :
( ~ r1(X214,X215)
| $false ) )
| ~ ( p3(X213)
| p2(X213)
| p1(X213)
| ! [X216] :
( ~ r1(X213,X216)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X217] :
( ~ r1(X0,X217)
| $false )
| ~ ! [X218] :
( ~ r1(X0,X218)
| p2(X218)
| p1(X218)
| ! [X219] :
( ~ r1(X218,X219)
| $false )
| ~ ! [X220] :
( ~ r1(X218,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p2(X221)
| p1(X221)
| ! [X222] :
( ~ r1(X221,X222)
| $false ) )
| ~ ( p2(X220)
| p1(X220)
| ! [X223] :
( ~ r1(X220,X223)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X224] :
( ~ r1(X0,X224)
| $false )
| ~ ! [X225] :
( ~ r1(X0,X225)
| p1(X225)
| ! [X226] :
( ~ r1(X225,X226)
| $false )
| ~ ! [X227] :
( ~ r1(X225,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228)
| ! [X229] :
( ~ r1(X228,X229)
| $false ) )
| ~ ( p1(X227)
| ! [X230] :
( ~ r1(X227,X230)
| $false ) ) ) ) )
& ! [X231] :
( ~ r1(X0,X231)
| p2(X231)
| ~ ! [X232] :
( ~ r1(X231,X232)
| p2(X232)
| ~ ! [X233] :
( ~ r1(X232,X233)
| ! [X234] :
( ~ r1(X233,X234)
| p2(X234) )
| ~ p2(X233) ) ) ) ) ),
inference(rectify,[],[f4]) ).
fof(f6,plain,
? [X0] :
~ ( ( ! [X1] :
( ~ r1(X0,X1)
| p1(X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ~ p5(X3) ) ) )
& ( ! [X4] :
( ~ r1(X0,X4)
| p2(X4) )
| ~ ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ~ ! [X6] :
( ~ r1(X5,X6)
| ! [X7] :
( ~ r1(X6,X7)
| p2(X7) )
| ~ p2(X6) ) ) ) )
| ! [X8] :
( ~ r1(X0,X8)
| p3(X8) )
| ~ ! [X9] :
( ~ r1(X0,X9)
| p3(X9)
| ~ ! [X10] :
( ~ r1(X9,X10)
| ! [X11] :
( ~ r1(X10,X11)
| p3(X11) )
| ~ p3(X10) ) )
| ( ~ ! [X12] :
( ~ r1(X0,X12)
| ~ ! [X13] :
( ~ r1(X12,X13)
| ~ p5(X13) ) )
& ( ! [X14] :
( ~ r1(X0,X14)
| p2(X14) )
| ~ ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ~ ! [X16] :
( ~ r1(X15,X16)
| ! [X17] :
( ~ r1(X16,X17)
| p2(X17) )
| ~ p2(X16) ) ) ) )
| ! [X18] :
( ~ r1(X0,X18)
| p1(X18) )
| ~ ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ~ ! [X20] :
( ~ r1(X19,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p1(X21) )
| ~ p1(X20) ) )
| ~ ( ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ~ ! [X24] :
( ~ r1(X23,X24)
| ! [X25] :
( ~ r1(X24,X25)
| p2(X25) )
| ~ p2(X24) ) ) )
| ~ ! [X26] :
( ~ r1(X0,X26)
| p2(X26)
| ~ ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ~ ! [X29] :
( ~ r1(X0,X29)
| ! [X30] :
( ~ r1(X29,X30)
| p2(X30) )
| ~ p2(X29) ) ) )
| ~ ! [X31] :
( ~ r1(X0,X31)
| ( ( ! [X32] :
( ~ r1(X31,X32)
| ! [X33] :
( ~ r1(X32,X33)
| p2(X33)
| ~ ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
| ~ ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ~ ! [X37] :
( ~ r1(X36,X37)
| ! [X38] :
( ~ r1(X37,X38)
| p2(X38) )
| ~ p2(X37) ) ) )
& ( p2(X31)
| ~ ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
| ~ ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X42,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ~ ! [X50] :
( ~ r1(X42,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) )
| ~ ( ( ! [X52] :
( ~ r1(X41,X52)
| ! [X53] :
( ~ r1(X52,X53)
| p2(X53)
| ~ ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
| ~ ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ~ ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) )
& ( p2(X41)
| ~ ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X61] :
( ~ r1(X0,X61)
| p4(X61)
| p3(X61)
| p2(X61)
| p1(X61)
| ! [X62] :
( ~ r1(X61,X62)
| p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) ) ) )
| ~ ! [X65] :
( ~ r1(X0,X65)
| p2(X65)
| p1(X65)
| ! [X66] :
( ~ r1(X65,X66)
| p4(X66)
| p3(X66)
| p2(X66)
| p1(X66)
| ! [X67] :
( ~ r1(X66,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] :
( ~ r1(X67,X68)
| p4(X68)
| p3(X68)
| p2(X68)
| p1(X68)
| ! [X69] :
( ~ r1(X68,X69)
| $false ) ) ) )
| ~ ! [X70] :
( ~ r1(X65,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X73] :
( ~ r1(X72,X73)
| p4(X73)
| p3(X73)
| p2(X73)
| p1(X73)
| ! [X74] :
( ~ r1(X73,X74)
| p4(X74)
| p3(X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false ) ) ) ) )
| ~ ( p2(X70)
| p1(X70)
| ! [X76] :
( ~ r1(X70,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| p4(X77)
| p3(X77)
| p2(X77)
| p1(X77)
| ! [X78] :
( ~ r1(X77,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] :
( ~ r1(X78,X79)
| $false ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| p4(X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| $false ) ) ) )
| ~ ! [X84] :
( ~ r1(X0,X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] :
( ~ r1(X85,X86)
| p4(X86)
| p3(X86)
| p2(X86)
| p1(X86)
| ! [X87] :
( ~ r1(X86,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) ) ) )
| ~ ! [X89] :
( ~ r1(X84,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| p4(X91)
| p3(X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] :
( ~ r1(X92,X93)
| p4(X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| $false ) ) ) ) )
| ~ ( p1(X89)
| ! [X95] :
( ~ r1(X89,X95)
| p4(X95)
| p3(X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| p4(X97)
| p3(X97)
| p2(X97)
| p1(X97)
| ! [X98] :
( ~ r1(X97,X98)
| $false ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X99] :
( ~ r1(X0,X99)
| p4(X99)
| p3(X99)
| p2(X99)
| p1(X99)
| ! [X100] :
( ~ r1(X99,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| $false ) ) )
| ~ ! [X102] :
( ~ r1(X0,X102)
| p4(X102)
| p3(X102)
| p2(X102)
| p1(X102)
| ! [X103] :
( ~ r1(X102,X103)
| p4(X103)
| p3(X103)
| p2(X103)
| p1(X103)
| ! [X104] :
( ~ r1(X103,X104)
| p4(X104)
| p3(X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| $false ) ) )
| ~ ! [X106] :
( ~ r1(X102,X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| p4(X108)
| p3(X108)
| p2(X108)
| p1(X108)
| ! [X109] :
( ~ r1(X108,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) ) ) )
| ~ ( p4(X106)
| p3(X106)
| p2(X106)
| p1(X106)
| ! [X111] :
( ~ r1(X106,X111)
| p4(X111)
| p3(X111)
| p2(X111)
| p1(X111)
| ! [X112] :
( ~ r1(X111,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] :
( ~ r1(X112,X113)
| $false ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X114] :
( ~ r1(X0,X114)
| p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| $false ) ) )
| ~ ! [X117] :
( ~ r1(X0,X117)
| p3(X117)
| p2(X117)
| p1(X117)
| ! [X118] :
( ~ r1(X117,X118)
| p4(X118)
| p3(X118)
| p2(X118)
| p1(X118)
| ! [X119] :
( ~ r1(X118,X119)
| p4(X119)
| p3(X119)
| p2(X119)
| p1(X119)
| ! [X120] :
( ~ r1(X119,X120)
| $false ) ) )
| ~ ! [X121] :
( ~ r1(X117,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] :
( ~ r1(X122,X123)
| p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) ) ) )
| ~ ( p3(X121)
| p2(X121)
| p1(X121)
| ! [X126] :
( ~ r1(X121,X126)
| p4(X126)
| p3(X126)
| p2(X126)
| p1(X126)
| ! [X127] :
( ~ r1(X126,X127)
| p4(X127)
| p3(X127)
| p2(X127)
| p1(X127)
| ! [X128] :
( ~ r1(X127,X128)
| $false ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X129] :
( ~ r1(X0,X129)
| p4(X129)
| p3(X129)
| p2(X129)
| p1(X129)
| ! [X130] :
( ~ r1(X129,X130)
| p4(X130)
| p3(X130)
| p2(X130)
| p1(X130)
| ! [X131] :
( ~ r1(X130,X131)
| $false ) ) )
| ~ ! [X132] :
( ~ r1(X0,X132)
| p2(X132)
| p1(X132)
| ! [X133] :
( ~ r1(X132,X133)
| p4(X133)
| p3(X133)
| p2(X133)
| p1(X133)
| ! [X134] :
( ~ r1(X133,X134)
| p4(X134)
| p3(X134)
| p2(X134)
| p1(X134)
| ! [X135] :
( ~ r1(X134,X135)
| $false ) ) )
| ~ ! [X136] :
( ~ r1(X132,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p2(X137)
| p1(X137)
| ! [X138] :
( ~ r1(X137,X138)
| p4(X138)
| p3(X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| p4(X139)
| p3(X139)
| p2(X139)
| p1(X139)
| ! [X140] :
( ~ r1(X139,X140)
| $false ) ) ) )
| ~ ( p2(X136)
| p1(X136)
| ! [X141] :
( ~ r1(X136,X141)
| p4(X141)
| p3(X141)
| p2(X141)
| p1(X141)
| ! [X142] :
( ~ r1(X141,X142)
| p4(X142)
| p3(X142)
| p2(X142)
| p1(X142)
| ! [X143] :
( ~ r1(X142,X143)
| $false ) ) ) ) ) ) )
& ( p1(X0)
| ! [X144] :
( ~ r1(X0,X144)
| p4(X144)
| p3(X144)
| p2(X144)
| p1(X144)
| ! [X145] :
( ~ r1(X144,X145)
| p4(X145)
| p3(X145)
| p2(X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) ) )
| ~ ! [X147] :
( ~ r1(X0,X147)
| p1(X147)
| ! [X148] :
( ~ r1(X147,X148)
| p4(X148)
| p3(X148)
| p2(X148)
| p1(X148)
| ! [X149] :
( ~ r1(X148,X149)
| p4(X149)
| p3(X149)
| p2(X149)
| p1(X149)
| ! [X150] :
( ~ r1(X149,X150)
| $false ) ) )
| ~ ! [X151] :
( ~ r1(X147,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ! [X153] :
( ~ r1(X152,X153)
| p4(X153)
| p3(X153)
| p2(X153)
| p1(X153)
| ! [X154] :
( ~ r1(X153,X154)
| p4(X154)
| p3(X154)
| p2(X154)
| p1(X154)
| ! [X155] :
( ~ r1(X154,X155)
| $false ) ) ) )
| ~ ( p1(X151)
| ! [X156] :
( ~ r1(X151,X156)
| p4(X156)
| p3(X156)
| p2(X156)
| p1(X156)
| ! [X157] :
( ~ r1(X156,X157)
| p4(X157)
| p3(X157)
| p2(X157)
| p1(X157)
| ! [X158] :
( ~ r1(X157,X158)
| $false ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X159] :
( ~ r1(X0,X159)
| p4(X159)
| p3(X159)
| p2(X159)
| p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| $false ) )
| ~ ! [X161] :
( ~ r1(X0,X161)
| p4(X161)
| p3(X161)
| p2(X161)
| p1(X161)
| ! [X162] :
( ~ r1(X161,X162)
| p4(X162)
| p3(X162)
| p2(X162)
| p1(X162)
| ! [X163] :
( ~ r1(X162,X163)
| $false ) )
| ~ ! [X164] :
( ~ r1(X161,X164)
| ! [X165] :
( ~ r1(X164,X165)
| p4(X165)
| p3(X165)
| p2(X165)
| p1(X165)
| ! [X166] :
( ~ r1(X165,X166)
| p4(X166)
| p3(X166)
| p2(X166)
| p1(X166)
| ! [X167] :
( ~ r1(X166,X167)
| $false ) ) )
| ~ ( p4(X164)
| p3(X164)
| p2(X164)
| p1(X164)
| ! [X168] :
( ~ r1(X164,X168)
| p4(X168)
| p3(X168)
| p2(X168)
| p1(X168)
| ! [X169] :
( ~ r1(X168,X169)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X170] :
( ~ r1(X0,X170)
| p4(X170)
| p3(X170)
| p2(X170)
| p1(X170)
| ! [X171] :
( ~ r1(X170,X171)
| $false ) )
| ~ ! [X172] :
( ~ r1(X0,X172)
| p3(X172)
| p2(X172)
| p1(X172)
| ! [X173] :
( ~ r1(X172,X173)
| p4(X173)
| p3(X173)
| p2(X173)
| p1(X173)
| ! [X174] :
( ~ r1(X173,X174)
| $false ) )
| ~ ! [X175] :
( ~ r1(X172,X175)
| ! [X176] :
( ~ r1(X175,X176)
| p3(X176)
| p2(X176)
| p1(X176)
| ! [X177] :
( ~ r1(X176,X177)
| p4(X177)
| p3(X177)
| p2(X177)
| p1(X177)
| ! [X178] :
( ~ r1(X177,X178)
| $false ) ) )
| ~ ( p3(X175)
| p2(X175)
| p1(X175)
| ! [X179] :
( ~ r1(X175,X179)
| p4(X179)
| p3(X179)
| p2(X179)
| p1(X179)
| ! [X180] :
( ~ r1(X179,X180)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X181] :
( ~ r1(X0,X181)
| p4(X181)
| p3(X181)
| p2(X181)
| p1(X181)
| ! [X182] :
( ~ r1(X181,X182)
| $false ) )
| ~ ! [X183] :
( ~ r1(X0,X183)
| p2(X183)
| p1(X183)
| ! [X184] :
( ~ r1(X183,X184)
| p4(X184)
| p3(X184)
| p2(X184)
| p1(X184)
| ! [X185] :
( ~ r1(X184,X185)
| $false ) )
| ~ ! [X186] :
( ~ r1(X183,X186)
| ! [X187] :
( ~ r1(X186,X187)
| p2(X187)
| p1(X187)
| ! [X188] :
( ~ r1(X187,X188)
| p4(X188)
| p3(X188)
| p2(X188)
| p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| $false ) ) )
| ~ ( p2(X186)
| p1(X186)
| ! [X190] :
( ~ r1(X186,X190)
| p4(X190)
| p3(X190)
| p2(X190)
| p1(X190)
| ! [X191] :
( ~ r1(X190,X191)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X192] :
( ~ r1(X0,X192)
| p4(X192)
| p3(X192)
| p2(X192)
| p1(X192)
| ! [X193] :
( ~ r1(X192,X193)
| $false ) )
| ~ ! [X194] :
( ~ r1(X0,X194)
| p1(X194)
| ! [X195] :
( ~ r1(X194,X195)
| p4(X195)
| p3(X195)
| p2(X195)
| p1(X195)
| ! [X196] :
( ~ r1(X195,X196)
| $false ) )
| ~ ! [X197] :
( ~ r1(X194,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198)
| ! [X199] :
( ~ r1(X198,X199)
| p4(X199)
| p3(X199)
| p2(X199)
| p1(X199)
| ! [X200] :
( ~ r1(X199,X200)
| $false ) ) )
| ~ ( p1(X197)
| ! [X201] :
( ~ r1(X197,X201)
| p4(X201)
| p3(X201)
| p2(X201)
| p1(X201)
| ! [X202] :
( ~ r1(X201,X202)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X203] :
( ~ r1(X0,X203)
| $false )
| ~ ! [X204] :
( ~ r1(X0,X204)
| p4(X204)
| p3(X204)
| p2(X204)
| p1(X204)
| ! [X205] :
( ~ r1(X204,X205)
| $false )
| ~ ! [X206] :
( ~ r1(X204,X206)
| ! [X207] :
( ~ r1(X206,X207)
| p4(X207)
| p3(X207)
| p2(X207)
| p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| $false ) )
| ~ ( p4(X206)
| p3(X206)
| p2(X206)
| p1(X206)
| ! [X209] :
( ~ r1(X206,X209)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X210] :
( ~ r1(X0,X210)
| $false )
| ~ ! [X211] :
( ~ r1(X0,X211)
| p3(X211)
| p2(X211)
| p1(X211)
| ! [X212] :
( ~ r1(X211,X212)
| $false )
| ~ ! [X213] :
( ~ r1(X211,X213)
| ! [X214] :
( ~ r1(X213,X214)
| p3(X214)
| p2(X214)
| p1(X214)
| ! [X215] :
( ~ r1(X214,X215)
| $false ) )
| ~ ( p3(X213)
| p2(X213)
| p1(X213)
| ! [X216] :
( ~ r1(X213,X216)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X217] :
( ~ r1(X0,X217)
| $false )
| ~ ! [X218] :
( ~ r1(X0,X218)
| p2(X218)
| p1(X218)
| ! [X219] :
( ~ r1(X218,X219)
| $false )
| ~ ! [X220] :
( ~ r1(X218,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p2(X221)
| p1(X221)
| ! [X222] :
( ~ r1(X221,X222)
| $false ) )
| ~ ( p2(X220)
| p1(X220)
| ! [X223] :
( ~ r1(X220,X223)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X224] :
( ~ r1(X0,X224)
| $false )
| ~ ! [X225] :
( ~ r1(X0,X225)
| p1(X225)
| ! [X226] :
( ~ r1(X225,X226)
| $false )
| ~ ! [X227] :
( ~ r1(X225,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228)
| ! [X229] :
( ~ r1(X228,X229)
| $false ) )
| ~ ( p1(X227)
| ! [X230] :
( ~ r1(X227,X230)
| $false ) ) ) ) )
& ! [X231] :
( ~ r1(X0,X231)
| p2(X231)
| ~ ! [X232] :
( ~ r1(X231,X232)
| p2(X232)
| ~ ! [X233] :
( ~ r1(X232,X233)
| ! [X234] :
( ~ r1(X233,X234)
| p2(X234) )
| ~ p2(X233) ) ) ) ) ),
inference(flattening,[],[f5]) ).
fof(f7,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f8,plain,
! [X0,X1,X2] :
( r1(X0,X2)
| ~ r1(X0,X1)
| ~ r1(X1,X2) ),
inference(flattening,[],[f7]) ).
fof(f9,plain,
? [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p5(X3) ) ) )
| ( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) ) )
& ? [X8] :
( r1(X0,X8)
& ~ p3(X8) )
& ! [X9] :
( ~ r1(X0,X9)
| p3(X9)
| ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ~ p3(X11) )
& p3(X10) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| ? [X13] :
( r1(X12,X13)
& p5(X13) ) )
| ( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ? [X16] :
( r1(X15,X16)
& ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
& p2(X16) ) ) ) )
& ? [X18] :
( r1(X0,X18)
& ~ p1(X18) )
& ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p1(X21) )
& p1(X20) ) )
& ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ? [X24] :
( r1(X23,X24)
& ? [X25] :
( r1(X24,X25)
& ~ p2(X25) )
& p2(X24) ) ) )
| ? [X26] :
( r1(X0,X26)
& ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ? [X29] :
( r1(X0,X29)
& ? [X30] :
( r1(X29,X30)
& ~ p2(X30) )
& p2(X29) ) ) )
| ? [X31] :
( r1(X0,X31)
& ( ( ? [X32] :
( r1(X31,X32)
& ? [X33] :
( r1(X32,X33)
& ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
& ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ? [X37] :
( r1(X36,X37)
& ? [X38] :
( r1(X37,X38)
& ~ p2(X38) )
& p2(X37) ) ) )
| ( ~ p2(X31)
& ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p2(X46) )
& p2(X45) ) ) )
| ? [X47] :
( r1(X42,X47)
& ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ? [X50] :
( r1(X42,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51) )
& p2(X50) ) ) ) )
| ( ? [X52] :
( r1(X41,X52)
& ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
& ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] :
( r1(X57,X58)
& ~ p2(X58) )
& p2(X57) ) ) )
| ( ~ p2(X41)
& ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X61] :
( ~ r1(X0,X61)
| p4(X61)
| p3(X61)
| p2(X61)
| p1(X61)
| ! [X62] :
( ~ r1(X61,X62)
| p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) ) ) )
| ? [X65] :
( r1(X0,X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] :
( r1(X65,X66)
& ~ p4(X66)
& ~ p3(X66)
& ~ p2(X66)
& ~ p1(X66)
& ? [X67] :
( r1(X66,X67)
& ~ p4(X67)
& ~ p3(X67)
& ~ p2(X67)
& ~ p1(X67)
& ? [X68] :
( r1(X67,X68)
& ~ p4(X68)
& ~ p3(X68)
& ~ p2(X68)
& ~ p1(X68)
& ? [X69] :
( r1(X68,X69)
& $true ) ) ) )
& ! [X70] :
( ~ r1(X65,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X73] :
( ~ r1(X72,X73)
| p4(X73)
| p3(X73)
| p2(X73)
| p1(X73)
| ! [X74] :
( ~ r1(X73,X74)
| p4(X74)
| p3(X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false ) ) ) ) )
| ( ~ p2(X70)
& ~ p1(X70)
& ? [X76] :
( r1(X70,X76)
& ~ p4(X76)
& ~ p3(X76)
& ~ p2(X76)
& ~ p1(X76)
& ? [X77] :
( r1(X76,X77)
& ~ p4(X77)
& ~ p3(X77)
& ~ p2(X77)
& ~ p1(X77)
& ? [X78] :
( r1(X77,X78)
& ~ p4(X78)
& ~ p3(X78)
& ~ p2(X78)
& ~ p1(X78)
& ? [X79] :
( r1(X78,X79)
& $true ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| p4(X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| $false ) ) ) )
| ? [X84] :
( r1(X0,X84)
& ~ p1(X84)
& ? [X85] :
( r1(X84,X85)
& ~ p4(X85)
& ~ p3(X85)
& ~ p2(X85)
& ~ p1(X85)
& ? [X86] :
( r1(X85,X86)
& ~ p4(X86)
& ~ p3(X86)
& ~ p2(X86)
& ~ p1(X86)
& ? [X87] :
( r1(X86,X87)
& ~ p4(X87)
& ~ p3(X87)
& ~ p2(X87)
& ~ p1(X87)
& ? [X88] :
( r1(X87,X88)
& $true ) ) ) )
& ! [X89] :
( ~ r1(X84,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| p4(X91)
| p3(X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] :
( ~ r1(X92,X93)
| p4(X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| $false ) ) ) ) )
| ( ~ p1(X89)
& ? [X95] :
( r1(X89,X95)
& ~ p4(X95)
& ~ p3(X95)
& ~ p2(X95)
& ~ p1(X95)
& ? [X96] :
( r1(X95,X96)
& ~ p4(X96)
& ~ p3(X96)
& ~ p2(X96)
& ~ p1(X96)
& ? [X97] :
( r1(X96,X97)
& ~ p4(X97)
& ~ p3(X97)
& ~ p2(X97)
& ~ p1(X97)
& ? [X98] :
( r1(X97,X98)
& $true ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X99] :
( ~ r1(X0,X99)
| p4(X99)
| p3(X99)
| p2(X99)
| p1(X99)
| ! [X100] :
( ~ r1(X99,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| $false ) ) )
| ? [X102] :
( r1(X0,X102)
& ~ p4(X102)
& ~ p3(X102)
& ~ p2(X102)
& ~ p1(X102)
& ? [X103] :
( r1(X102,X103)
& ~ p4(X103)
& ~ p3(X103)
& ~ p2(X103)
& ~ p1(X103)
& ? [X104] :
( r1(X103,X104)
& ~ p4(X104)
& ~ p3(X104)
& ~ p2(X104)
& ~ p1(X104)
& ? [X105] :
( r1(X104,X105)
& $true ) ) )
& ! [X106] :
( ~ r1(X102,X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| p4(X108)
| p3(X108)
| p2(X108)
| p1(X108)
| ! [X109] :
( ~ r1(X108,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) ) ) )
| ( ~ p4(X106)
& ~ p3(X106)
& ~ p2(X106)
& ~ p1(X106)
& ? [X111] :
( r1(X106,X111)
& ~ p4(X111)
& ~ p3(X111)
& ~ p2(X111)
& ~ p1(X111)
& ? [X112] :
( r1(X111,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] :
( r1(X112,X113)
& $true ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X114] :
( ~ r1(X0,X114)
| p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| $false ) ) )
| ? [X117] :
( r1(X0,X117)
& ~ p3(X117)
& ~ p2(X117)
& ~ p1(X117)
& ? [X118] :
( r1(X117,X118)
& ~ p4(X118)
& ~ p3(X118)
& ~ p2(X118)
& ~ p1(X118)
& ? [X119] :
( r1(X118,X119)
& ~ p4(X119)
& ~ p3(X119)
& ~ p2(X119)
& ~ p1(X119)
& ? [X120] :
( r1(X119,X120)
& $true ) ) )
& ! [X121] :
( ~ r1(X117,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] :
( ~ r1(X122,X123)
| p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) ) ) )
| ( ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X126] :
( r1(X121,X126)
& ~ p4(X126)
& ~ p3(X126)
& ~ p2(X126)
& ~ p1(X126)
& ? [X127] :
( r1(X126,X127)
& ~ p4(X127)
& ~ p3(X127)
& ~ p2(X127)
& ~ p1(X127)
& ? [X128] :
( r1(X127,X128)
& $true ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X129] :
( ~ r1(X0,X129)
| p4(X129)
| p3(X129)
| p2(X129)
| p1(X129)
| ! [X130] :
( ~ r1(X129,X130)
| p4(X130)
| p3(X130)
| p2(X130)
| p1(X130)
| ! [X131] :
( ~ r1(X130,X131)
| $false ) ) )
| ? [X132] :
( r1(X0,X132)
& ~ p2(X132)
& ~ p1(X132)
& ? [X133] :
( r1(X132,X133)
& ~ p4(X133)
& ~ p3(X133)
& ~ p2(X133)
& ~ p1(X133)
& ? [X134] :
( r1(X133,X134)
& ~ p4(X134)
& ~ p3(X134)
& ~ p2(X134)
& ~ p1(X134)
& ? [X135] :
( r1(X134,X135)
& $true ) ) )
& ! [X136] :
( ~ r1(X132,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p2(X137)
| p1(X137)
| ! [X138] :
( ~ r1(X137,X138)
| p4(X138)
| p3(X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| p4(X139)
| p3(X139)
| p2(X139)
| p1(X139)
| ! [X140] :
( ~ r1(X139,X140)
| $false ) ) ) )
| ( ~ p2(X136)
& ~ p1(X136)
& ? [X141] :
( r1(X136,X141)
& ~ p4(X141)
& ~ p3(X141)
& ~ p2(X141)
& ~ p1(X141)
& ? [X142] :
( r1(X141,X142)
& ~ p4(X142)
& ~ p3(X142)
& ~ p2(X142)
& ~ p1(X142)
& ? [X143] :
( r1(X142,X143)
& $true ) ) ) ) ) ) )
& ( p1(X0)
| ! [X144] :
( ~ r1(X0,X144)
| p4(X144)
| p3(X144)
| p2(X144)
| p1(X144)
| ! [X145] :
( ~ r1(X144,X145)
| p4(X145)
| p3(X145)
| p2(X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) ) )
| ? [X147] :
( r1(X0,X147)
& ~ p1(X147)
& ? [X148] :
( r1(X147,X148)
& ~ p4(X148)
& ~ p3(X148)
& ~ p2(X148)
& ~ p1(X148)
& ? [X149] :
( r1(X148,X149)
& ~ p4(X149)
& ~ p3(X149)
& ~ p2(X149)
& ~ p1(X149)
& ? [X150] :
( r1(X149,X150)
& $true ) ) )
& ! [X151] :
( ~ r1(X147,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ! [X153] :
( ~ r1(X152,X153)
| p4(X153)
| p3(X153)
| p2(X153)
| p1(X153)
| ! [X154] :
( ~ r1(X153,X154)
| p4(X154)
| p3(X154)
| p2(X154)
| p1(X154)
| ! [X155] :
( ~ r1(X154,X155)
| $false ) ) ) )
| ( ~ p1(X151)
& ? [X156] :
( r1(X151,X156)
& ~ p4(X156)
& ~ p3(X156)
& ~ p2(X156)
& ~ p1(X156)
& ? [X157] :
( r1(X156,X157)
& ~ p4(X157)
& ~ p3(X157)
& ~ p2(X157)
& ~ p1(X157)
& ? [X158] :
( r1(X157,X158)
& $true ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X159] :
( ~ r1(X0,X159)
| p4(X159)
| p3(X159)
| p2(X159)
| p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| $false ) )
| ? [X161] :
( r1(X0,X161)
& ~ p4(X161)
& ~ p3(X161)
& ~ p2(X161)
& ~ p1(X161)
& ? [X162] :
( r1(X161,X162)
& ~ p4(X162)
& ~ p3(X162)
& ~ p2(X162)
& ~ p1(X162)
& ? [X163] :
( r1(X162,X163)
& $true ) )
& ! [X164] :
( ~ r1(X161,X164)
| ! [X165] :
( ~ r1(X164,X165)
| p4(X165)
| p3(X165)
| p2(X165)
| p1(X165)
| ! [X166] :
( ~ r1(X165,X166)
| p4(X166)
| p3(X166)
| p2(X166)
| p1(X166)
| ! [X167] :
( ~ r1(X166,X167)
| $false ) ) )
| ( ~ p4(X164)
& ~ p3(X164)
& ~ p2(X164)
& ~ p1(X164)
& ? [X168] :
( r1(X164,X168)
& ~ p4(X168)
& ~ p3(X168)
& ~ p2(X168)
& ~ p1(X168)
& ? [X169] :
( r1(X168,X169)
& $true ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X170] :
( ~ r1(X0,X170)
| p4(X170)
| p3(X170)
| p2(X170)
| p1(X170)
| ! [X171] :
( ~ r1(X170,X171)
| $false ) )
| ? [X172] :
( r1(X0,X172)
& ~ p3(X172)
& ~ p2(X172)
& ~ p1(X172)
& ? [X173] :
( r1(X172,X173)
& ~ p4(X173)
& ~ p3(X173)
& ~ p2(X173)
& ~ p1(X173)
& ? [X174] :
( r1(X173,X174)
& $true ) )
& ! [X175] :
( ~ r1(X172,X175)
| ! [X176] :
( ~ r1(X175,X176)
| p3(X176)
| p2(X176)
| p1(X176)
| ! [X177] :
( ~ r1(X176,X177)
| p4(X177)
| p3(X177)
| p2(X177)
| p1(X177)
| ! [X178] :
( ~ r1(X177,X178)
| $false ) ) )
| ( ~ p3(X175)
& ~ p2(X175)
& ~ p1(X175)
& ? [X179] :
( r1(X175,X179)
& ~ p4(X179)
& ~ p3(X179)
& ~ p2(X179)
& ~ p1(X179)
& ? [X180] :
( r1(X179,X180)
& $true ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X181] :
( ~ r1(X0,X181)
| p4(X181)
| p3(X181)
| p2(X181)
| p1(X181)
| ! [X182] :
( ~ r1(X181,X182)
| $false ) )
| ? [X183] :
( r1(X0,X183)
& ~ p2(X183)
& ~ p1(X183)
& ? [X184] :
( r1(X183,X184)
& ~ p4(X184)
& ~ p3(X184)
& ~ p2(X184)
& ~ p1(X184)
& ? [X185] :
( r1(X184,X185)
& $true ) )
& ! [X186] :
( ~ r1(X183,X186)
| ! [X187] :
( ~ r1(X186,X187)
| p2(X187)
| p1(X187)
| ! [X188] :
( ~ r1(X187,X188)
| p4(X188)
| p3(X188)
| p2(X188)
| p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| $false ) ) )
| ( ~ p2(X186)
& ~ p1(X186)
& ? [X190] :
( r1(X186,X190)
& ~ p4(X190)
& ~ p3(X190)
& ~ p2(X190)
& ~ p1(X190)
& ? [X191] :
( r1(X190,X191)
& $true ) ) ) ) ) )
& ( p1(X0)
| ! [X192] :
( ~ r1(X0,X192)
| p4(X192)
| p3(X192)
| p2(X192)
| p1(X192)
| ! [X193] :
( ~ r1(X192,X193)
| $false ) )
| ? [X194] :
( r1(X0,X194)
& ~ p1(X194)
& ? [X195] :
( r1(X194,X195)
& ~ p4(X195)
& ~ p3(X195)
& ~ p2(X195)
& ~ p1(X195)
& ? [X196] :
( r1(X195,X196)
& $true ) )
& ! [X197] :
( ~ r1(X194,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198)
| ! [X199] :
( ~ r1(X198,X199)
| p4(X199)
| p3(X199)
| p2(X199)
| p1(X199)
| ! [X200] :
( ~ r1(X199,X200)
| $false ) ) )
| ( ~ p1(X197)
& ? [X201] :
( r1(X197,X201)
& ~ p4(X201)
& ~ p3(X201)
& ~ p2(X201)
& ~ p1(X201)
& ? [X202] :
( r1(X201,X202)
& $true ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X203] :
( ~ r1(X0,X203)
| $false )
| ? [X204] :
( r1(X0,X204)
& ~ p4(X204)
& ~ p3(X204)
& ~ p2(X204)
& ~ p1(X204)
& ? [X205] :
( r1(X204,X205)
& $true )
& ! [X206] :
( ~ r1(X204,X206)
| ! [X207] :
( ~ r1(X206,X207)
| p4(X207)
| p3(X207)
| p2(X207)
| p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| $false ) )
| ( ~ p4(X206)
& ~ p3(X206)
& ~ p2(X206)
& ~ p1(X206)
& ? [X209] :
( r1(X206,X209)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X210] :
( ~ r1(X0,X210)
| $false )
| ? [X211] :
( r1(X0,X211)
& ~ p3(X211)
& ~ p2(X211)
& ~ p1(X211)
& ? [X212] :
( r1(X211,X212)
& $true )
& ! [X213] :
( ~ r1(X211,X213)
| ! [X214] :
( ~ r1(X213,X214)
| p3(X214)
| p2(X214)
| p1(X214)
| ! [X215] :
( ~ r1(X214,X215)
| $false ) )
| ( ~ p3(X213)
& ~ p2(X213)
& ~ p1(X213)
& ? [X216] :
( r1(X213,X216)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X217] :
( ~ r1(X0,X217)
| $false )
| ? [X218] :
( r1(X0,X218)
& ~ p2(X218)
& ~ p1(X218)
& ? [X219] :
( r1(X218,X219)
& $true )
& ! [X220] :
( ~ r1(X218,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p2(X221)
| p1(X221)
| ! [X222] :
( ~ r1(X221,X222)
| $false ) )
| ( ~ p2(X220)
& ~ p1(X220)
& ? [X223] :
( r1(X220,X223)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X224] :
( ~ r1(X0,X224)
| $false )
| ? [X225] :
( r1(X0,X225)
& ~ p1(X225)
& ? [X226] :
( r1(X225,X226)
& $true )
& ! [X227] :
( ~ r1(X225,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228)
| ! [X229] :
( ~ r1(X228,X229)
| $false ) )
| ( ~ p1(X227)
& ? [X230] :
( r1(X227,X230)
& $true ) ) ) ) )
& ! [X231] :
( ~ r1(X0,X231)
| p2(X231)
| ? [X232] :
( r1(X231,X232)
& ~ p2(X232)
& ! [X233] :
( ~ r1(X232,X233)
| ! [X234] :
( ~ r1(X233,X234)
| p2(X234) )
| ~ p2(X233) ) ) ) ),
inference(ennf_transformation,[],[f6]) ).
fof(f10,plain,
? [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ~ p1(X1)
& ? [X2] :
( r1(X1,X2)
& ! [X3] :
( ~ r1(X2,X3)
| ~ p5(X3) ) ) )
| ( ? [X4] :
( r1(X0,X4)
& ~ p2(X4) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) ) )
& ? [X8] :
( r1(X0,X8)
& ~ p3(X8) )
& ! [X9] :
( ~ r1(X0,X9)
| p3(X9)
| ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ~ p3(X11) )
& p3(X10) ) )
& ( ! [X12] :
( ~ r1(X0,X12)
| ? [X13] :
( r1(X12,X13)
& p5(X13) ) )
| ( ? [X14] :
( r1(X0,X14)
& ~ p2(X14) )
& ! [X15] :
( ~ r1(X0,X15)
| p2(X15)
| ? [X16] :
( r1(X15,X16)
& ? [X17] :
( r1(X16,X17)
& ~ p2(X17) )
& p2(X16) ) ) ) )
& ? [X18] :
( r1(X0,X18)
& ~ p1(X18) )
& ! [X19] :
( ~ r1(X0,X19)
| p1(X19)
| ? [X20] :
( r1(X19,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p1(X21) )
& p1(X20) ) )
& ( ( ( ! [X22] :
( ~ r1(X0,X22)
| ! [X23] :
( ~ r1(X22,X23)
| p2(X23)
| ? [X24] :
( r1(X23,X24)
& ? [X25] :
( r1(X24,X25)
& ~ p2(X25) )
& p2(X24) ) ) )
| ? [X26] :
( r1(X0,X26)
& ~ p2(X26)
& ! [X27] :
( ~ r1(X26,X27)
| ! [X28] :
( ~ r1(X27,X28)
| p2(X28) )
| ~ p2(X27) ) ) )
& ( p2(X0)
| ? [X29] :
( r1(X0,X29)
& ? [X30] :
( r1(X29,X30)
& ~ p2(X30) )
& p2(X29) ) ) )
| ? [X31] :
( r1(X0,X31)
& ( ( ? [X32] :
( r1(X31,X32)
& ? [X33] :
( r1(X32,X33)
& ~ p2(X33)
& ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35) )
| ~ p2(X34) ) ) )
& ! [X36] :
( ~ r1(X31,X36)
| p2(X36)
| ? [X37] :
( r1(X36,X37)
& ? [X38] :
( r1(X37,X38)
& ~ p2(X38) )
& p2(X37) ) ) )
| ( ~ p2(X31)
& ! [X39] :
( ~ r1(X31,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ! [X41] :
( ~ r1(X31,X41)
| ! [X42] :
( ~ r1(X41,X42)
| ( ( ! [X43] :
( ~ r1(X42,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ? [X45] :
( r1(X44,X45)
& ? [X46] :
( r1(X45,X46)
& ~ p2(X46) )
& p2(X45) ) ) )
| ? [X47] :
( r1(X42,X47)
& ~ p2(X47)
& ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X42)
| ? [X50] :
( r1(X42,X50)
& ? [X51] :
( r1(X50,X51)
& ~ p2(X51) )
& p2(X50) ) ) ) )
| ( ? [X52] :
( r1(X41,X52)
& ? [X53] :
( r1(X52,X53)
& ~ p2(X53)
& ! [X54] :
( ~ r1(X53,X54)
| ! [X55] :
( ~ r1(X54,X55)
| p2(X55) )
| ~ p2(X54) ) ) )
& ! [X56] :
( ~ r1(X41,X56)
| p2(X56)
| ? [X57] :
( r1(X56,X57)
& ? [X58] :
( r1(X57,X58)
& ~ p2(X58) )
& p2(X57) ) ) )
| ( ~ p2(X41)
& ! [X59] :
( ~ r1(X41,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p2(X60) )
| ~ p2(X59) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X61] :
( ~ r1(X0,X61)
| p4(X61)
| p3(X61)
| p2(X61)
| p1(X61)
| ! [X62] :
( ~ r1(X61,X62)
| p4(X62)
| p3(X62)
| p2(X62)
| p1(X62)
| ! [X63] :
( ~ r1(X62,X63)
| p4(X63)
| p3(X63)
| p2(X63)
| p1(X63)
| ! [X64] :
( ~ r1(X63,X64)
| $false ) ) ) )
| ? [X65] :
( r1(X0,X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] :
( r1(X65,X66)
& ~ p4(X66)
& ~ p3(X66)
& ~ p2(X66)
& ~ p1(X66)
& ? [X67] :
( r1(X66,X67)
& ~ p4(X67)
& ~ p3(X67)
& ~ p2(X67)
& ~ p1(X67)
& ? [X68] :
( r1(X67,X68)
& ~ p4(X68)
& ~ p3(X68)
& ~ p2(X68)
& ~ p1(X68)
& ? [X69] :
( r1(X68,X69)
& $true ) ) ) )
& ! [X70] :
( ~ r1(X65,X70)
| ! [X71] :
( ~ r1(X70,X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X73] :
( ~ r1(X72,X73)
| p4(X73)
| p3(X73)
| p2(X73)
| p1(X73)
| ! [X74] :
( ~ r1(X73,X74)
| p4(X74)
| p3(X74)
| p2(X74)
| p1(X74)
| ! [X75] :
( ~ r1(X74,X75)
| $false ) ) ) ) )
| ( ~ p2(X70)
& ~ p1(X70)
& ? [X76] :
( r1(X70,X76)
& ~ p4(X76)
& ~ p3(X76)
& ~ p2(X76)
& ~ p1(X76)
& ? [X77] :
( r1(X76,X77)
& ~ p4(X77)
& ~ p3(X77)
& ~ p2(X77)
& ~ p1(X77)
& ? [X78] :
( r1(X77,X78)
& ~ p4(X78)
& ~ p3(X78)
& ~ p2(X78)
& ~ p1(X78)
& ? [X79] :
( r1(X78,X79)
& $true ) ) ) ) ) ) ) )
& ( p1(X0)
| ! [X80] :
( ~ r1(X0,X80)
| p4(X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| $false ) ) ) )
| ? [X84] :
( r1(X0,X84)
& ~ p1(X84)
& ? [X85] :
( r1(X84,X85)
& ~ p4(X85)
& ~ p3(X85)
& ~ p2(X85)
& ~ p1(X85)
& ? [X86] :
( r1(X85,X86)
& ~ p4(X86)
& ~ p3(X86)
& ~ p2(X86)
& ~ p1(X86)
& ? [X87] :
( r1(X86,X87)
& ~ p4(X87)
& ~ p3(X87)
& ~ p2(X87)
& ~ p1(X87)
& ? [X88] :
( r1(X87,X88)
& $true ) ) ) )
& ! [X89] :
( ~ r1(X84,X89)
| ! [X90] :
( ~ r1(X89,X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| p4(X91)
| p3(X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] :
( ~ r1(X92,X93)
| p4(X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| $false ) ) ) ) )
| ( ~ p1(X89)
& ? [X95] :
( r1(X89,X95)
& ~ p4(X95)
& ~ p3(X95)
& ~ p2(X95)
& ~ p1(X95)
& ? [X96] :
( r1(X95,X96)
& ~ p4(X96)
& ~ p3(X96)
& ~ p2(X96)
& ~ p1(X96)
& ? [X97] :
( r1(X96,X97)
& ~ p4(X97)
& ~ p3(X97)
& ~ p2(X97)
& ~ p1(X97)
& ? [X98] :
( r1(X97,X98)
& $true ) ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X99] :
( ~ r1(X0,X99)
| p4(X99)
| p3(X99)
| p2(X99)
| p1(X99)
| ! [X100] :
( ~ r1(X99,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| $false ) ) )
| ? [X102] :
( r1(X0,X102)
& ~ p4(X102)
& ~ p3(X102)
& ~ p2(X102)
& ~ p1(X102)
& ? [X103] :
( r1(X102,X103)
& ~ p4(X103)
& ~ p3(X103)
& ~ p2(X103)
& ~ p1(X103)
& ? [X104] :
( r1(X103,X104)
& ~ p4(X104)
& ~ p3(X104)
& ~ p2(X104)
& ~ p1(X104)
& ? [X105] :
( r1(X104,X105)
& $true ) ) )
& ! [X106] :
( ~ r1(X102,X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| p4(X108)
| p3(X108)
| p2(X108)
| p1(X108)
| ! [X109] :
( ~ r1(X108,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) ) ) )
| ( ~ p4(X106)
& ~ p3(X106)
& ~ p2(X106)
& ~ p1(X106)
& ? [X111] :
( r1(X106,X111)
& ~ p4(X111)
& ~ p3(X111)
& ~ p2(X111)
& ~ p1(X111)
& ? [X112] :
( r1(X111,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] :
( r1(X112,X113)
& $true ) ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X114] :
( ~ r1(X0,X114)
| p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| $false ) ) )
| ? [X117] :
( r1(X0,X117)
& ~ p3(X117)
& ~ p2(X117)
& ~ p1(X117)
& ? [X118] :
( r1(X117,X118)
& ~ p4(X118)
& ~ p3(X118)
& ~ p2(X118)
& ~ p1(X118)
& ? [X119] :
( r1(X118,X119)
& ~ p4(X119)
& ~ p3(X119)
& ~ p2(X119)
& ~ p1(X119)
& ? [X120] :
( r1(X119,X120)
& $true ) ) )
& ! [X121] :
( ~ r1(X117,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] :
( ~ r1(X122,X123)
| p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) ) ) )
| ( ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X126] :
( r1(X121,X126)
& ~ p4(X126)
& ~ p3(X126)
& ~ p2(X126)
& ~ p1(X126)
& ? [X127] :
( r1(X126,X127)
& ~ p4(X127)
& ~ p3(X127)
& ~ p2(X127)
& ~ p1(X127)
& ? [X128] :
( r1(X127,X128)
& $true ) ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X129] :
( ~ r1(X0,X129)
| p4(X129)
| p3(X129)
| p2(X129)
| p1(X129)
| ! [X130] :
( ~ r1(X129,X130)
| p4(X130)
| p3(X130)
| p2(X130)
| p1(X130)
| ! [X131] :
( ~ r1(X130,X131)
| $false ) ) )
| ? [X132] :
( r1(X0,X132)
& ~ p2(X132)
& ~ p1(X132)
& ? [X133] :
( r1(X132,X133)
& ~ p4(X133)
& ~ p3(X133)
& ~ p2(X133)
& ~ p1(X133)
& ? [X134] :
( r1(X133,X134)
& ~ p4(X134)
& ~ p3(X134)
& ~ p2(X134)
& ~ p1(X134)
& ? [X135] :
( r1(X134,X135)
& $true ) ) )
& ! [X136] :
( ~ r1(X132,X136)
| ! [X137] :
( ~ r1(X136,X137)
| p2(X137)
| p1(X137)
| ! [X138] :
( ~ r1(X137,X138)
| p4(X138)
| p3(X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| p4(X139)
| p3(X139)
| p2(X139)
| p1(X139)
| ! [X140] :
( ~ r1(X139,X140)
| $false ) ) ) )
| ( ~ p2(X136)
& ~ p1(X136)
& ? [X141] :
( r1(X136,X141)
& ~ p4(X141)
& ~ p3(X141)
& ~ p2(X141)
& ~ p1(X141)
& ? [X142] :
( r1(X141,X142)
& ~ p4(X142)
& ~ p3(X142)
& ~ p2(X142)
& ~ p1(X142)
& ? [X143] :
( r1(X142,X143)
& $true ) ) ) ) ) ) )
& ( p1(X0)
| ! [X144] :
( ~ r1(X0,X144)
| p4(X144)
| p3(X144)
| p2(X144)
| p1(X144)
| ! [X145] :
( ~ r1(X144,X145)
| p4(X145)
| p3(X145)
| p2(X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) ) )
| ? [X147] :
( r1(X0,X147)
& ~ p1(X147)
& ? [X148] :
( r1(X147,X148)
& ~ p4(X148)
& ~ p3(X148)
& ~ p2(X148)
& ~ p1(X148)
& ? [X149] :
( r1(X148,X149)
& ~ p4(X149)
& ~ p3(X149)
& ~ p2(X149)
& ~ p1(X149)
& ? [X150] :
( r1(X149,X150)
& $true ) ) )
& ! [X151] :
( ~ r1(X147,X151)
| ! [X152] :
( ~ r1(X151,X152)
| p1(X152)
| ! [X153] :
( ~ r1(X152,X153)
| p4(X153)
| p3(X153)
| p2(X153)
| p1(X153)
| ! [X154] :
( ~ r1(X153,X154)
| p4(X154)
| p3(X154)
| p2(X154)
| p1(X154)
| ! [X155] :
( ~ r1(X154,X155)
| $false ) ) ) )
| ( ~ p1(X151)
& ? [X156] :
( r1(X151,X156)
& ~ p4(X156)
& ~ p3(X156)
& ~ p2(X156)
& ~ p1(X156)
& ? [X157] :
( r1(X156,X157)
& ~ p4(X157)
& ~ p3(X157)
& ~ p2(X157)
& ~ p1(X157)
& ? [X158] :
( r1(X157,X158)
& $true ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X159] :
( ~ r1(X0,X159)
| p4(X159)
| p3(X159)
| p2(X159)
| p1(X159)
| ! [X160] :
( ~ r1(X159,X160)
| $false ) )
| ? [X161] :
( r1(X0,X161)
& ~ p4(X161)
& ~ p3(X161)
& ~ p2(X161)
& ~ p1(X161)
& ? [X162] :
( r1(X161,X162)
& ~ p4(X162)
& ~ p3(X162)
& ~ p2(X162)
& ~ p1(X162)
& ? [X163] :
( r1(X162,X163)
& $true ) )
& ! [X164] :
( ~ r1(X161,X164)
| ! [X165] :
( ~ r1(X164,X165)
| p4(X165)
| p3(X165)
| p2(X165)
| p1(X165)
| ! [X166] :
( ~ r1(X165,X166)
| p4(X166)
| p3(X166)
| p2(X166)
| p1(X166)
| ! [X167] :
( ~ r1(X166,X167)
| $false ) ) )
| ( ~ p4(X164)
& ~ p3(X164)
& ~ p2(X164)
& ~ p1(X164)
& ? [X168] :
( r1(X164,X168)
& ~ p4(X168)
& ~ p3(X168)
& ~ p2(X168)
& ~ p1(X168)
& ? [X169] :
( r1(X168,X169)
& $true ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X170] :
( ~ r1(X0,X170)
| p4(X170)
| p3(X170)
| p2(X170)
| p1(X170)
| ! [X171] :
( ~ r1(X170,X171)
| $false ) )
| ? [X172] :
( r1(X0,X172)
& ~ p3(X172)
& ~ p2(X172)
& ~ p1(X172)
& ? [X173] :
( r1(X172,X173)
& ~ p4(X173)
& ~ p3(X173)
& ~ p2(X173)
& ~ p1(X173)
& ? [X174] :
( r1(X173,X174)
& $true ) )
& ! [X175] :
( ~ r1(X172,X175)
| ! [X176] :
( ~ r1(X175,X176)
| p3(X176)
| p2(X176)
| p1(X176)
| ! [X177] :
( ~ r1(X176,X177)
| p4(X177)
| p3(X177)
| p2(X177)
| p1(X177)
| ! [X178] :
( ~ r1(X177,X178)
| $false ) ) )
| ( ~ p3(X175)
& ~ p2(X175)
& ~ p1(X175)
& ? [X179] :
( r1(X175,X179)
& ~ p4(X179)
& ~ p3(X179)
& ~ p2(X179)
& ~ p1(X179)
& ? [X180] :
( r1(X179,X180)
& $true ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X181] :
( ~ r1(X0,X181)
| p4(X181)
| p3(X181)
| p2(X181)
| p1(X181)
| ! [X182] :
( ~ r1(X181,X182)
| $false ) )
| ? [X183] :
( r1(X0,X183)
& ~ p2(X183)
& ~ p1(X183)
& ? [X184] :
( r1(X183,X184)
& ~ p4(X184)
& ~ p3(X184)
& ~ p2(X184)
& ~ p1(X184)
& ? [X185] :
( r1(X184,X185)
& $true ) )
& ! [X186] :
( ~ r1(X183,X186)
| ! [X187] :
( ~ r1(X186,X187)
| p2(X187)
| p1(X187)
| ! [X188] :
( ~ r1(X187,X188)
| p4(X188)
| p3(X188)
| p2(X188)
| p1(X188)
| ! [X189] :
( ~ r1(X188,X189)
| $false ) ) )
| ( ~ p2(X186)
& ~ p1(X186)
& ? [X190] :
( r1(X186,X190)
& ~ p4(X190)
& ~ p3(X190)
& ~ p2(X190)
& ~ p1(X190)
& ? [X191] :
( r1(X190,X191)
& $true ) ) ) ) ) )
& ( p1(X0)
| ! [X192] :
( ~ r1(X0,X192)
| p4(X192)
| p3(X192)
| p2(X192)
| p1(X192)
| ! [X193] :
( ~ r1(X192,X193)
| $false ) )
| ? [X194] :
( r1(X0,X194)
& ~ p1(X194)
& ? [X195] :
( r1(X194,X195)
& ~ p4(X195)
& ~ p3(X195)
& ~ p2(X195)
& ~ p1(X195)
& ? [X196] :
( r1(X195,X196)
& $true ) )
& ! [X197] :
( ~ r1(X194,X197)
| ! [X198] :
( ~ r1(X197,X198)
| p1(X198)
| ! [X199] :
( ~ r1(X198,X199)
| p4(X199)
| p3(X199)
| p2(X199)
| p1(X199)
| ! [X200] :
( ~ r1(X199,X200)
| $false ) ) )
| ( ~ p1(X197)
& ? [X201] :
( r1(X197,X201)
& ~ p4(X201)
& ~ p3(X201)
& ~ p2(X201)
& ~ p1(X201)
& ? [X202] :
( r1(X201,X202)
& $true ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X203] :
( ~ r1(X0,X203)
| $false )
| ? [X204] :
( r1(X0,X204)
& ~ p4(X204)
& ~ p3(X204)
& ~ p2(X204)
& ~ p1(X204)
& ? [X205] :
( r1(X204,X205)
& $true )
& ! [X206] :
( ~ r1(X204,X206)
| ! [X207] :
( ~ r1(X206,X207)
| p4(X207)
| p3(X207)
| p2(X207)
| p1(X207)
| ! [X208] :
( ~ r1(X207,X208)
| $false ) )
| ( ~ p4(X206)
& ~ p3(X206)
& ~ p2(X206)
& ~ p1(X206)
& ? [X209] :
( r1(X206,X209)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X210] :
( ~ r1(X0,X210)
| $false )
| ? [X211] :
( r1(X0,X211)
& ~ p3(X211)
& ~ p2(X211)
& ~ p1(X211)
& ? [X212] :
( r1(X211,X212)
& $true )
& ! [X213] :
( ~ r1(X211,X213)
| ! [X214] :
( ~ r1(X213,X214)
| p3(X214)
| p2(X214)
| p1(X214)
| ! [X215] :
( ~ r1(X214,X215)
| $false ) )
| ( ~ p3(X213)
& ~ p2(X213)
& ~ p1(X213)
& ? [X216] :
( r1(X213,X216)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X217] :
( ~ r1(X0,X217)
| $false )
| ? [X218] :
( r1(X0,X218)
& ~ p2(X218)
& ~ p1(X218)
& ? [X219] :
( r1(X218,X219)
& $true )
& ! [X220] :
( ~ r1(X218,X220)
| ! [X221] :
( ~ r1(X220,X221)
| p2(X221)
| p1(X221)
| ! [X222] :
( ~ r1(X221,X222)
| $false ) )
| ( ~ p2(X220)
& ~ p1(X220)
& ? [X223] :
( r1(X220,X223)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X224] :
( ~ r1(X0,X224)
| $false )
| ? [X225] :
( r1(X0,X225)
& ~ p1(X225)
& ? [X226] :
( r1(X225,X226)
& $true )
& ! [X227] :
( ~ r1(X225,X227)
| ! [X228] :
( ~ r1(X227,X228)
| p1(X228)
| ! [X229] :
( ~ r1(X228,X229)
| $false ) )
| ( ~ p1(X227)
& ? [X230] :
( r1(X227,X230)
& $true ) ) ) ) )
& ! [X231] :
( ~ r1(X0,X231)
| p2(X231)
| ? [X232] :
( r1(X231,X232)
& ~ p2(X232)
& ! [X233] :
( ~ r1(X232,X233)
| ! [X234] :
( ~ r1(X233,X234)
| p2(X234) )
| ~ p2(X233) ) ) ) ),
inference(flattening,[],[f9]) ).
fof(f12,plain,
! [X2,X0,X1] :
( ~ r1(X0,X1)
| ~ r1(X1,X2)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f196,plain,
! [X5] :
( ~ p2(sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f197,plain,
! [X5] :
( r1(sK56(X5),sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f198,plain,
! [X5] :
( ~ p2(sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f199,plain,
! [X5] :
( r1(sK56(X5),sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f202,plain,
! [X3,X5] :
( ~ p2(sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f203,plain,
! [X3,X5] :
( r1(sK56(X5),sK89(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f204,plain,
! [X15,X12] :
( ~ p2(sK88(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f205,plain,
! [X15,X12] :
( r1(sK54(X15),sK88(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f206,plain,
! [X15,X12] :
( ~ p2(sK88(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f207,plain,
! [X15,X12] :
( r1(sK54(X15),sK88(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f229,plain,
! [X233,X231,X234] :
( ~ p2(X233)
| p2(X234)
| ~ r1(X233,X234)
| ~ r1(sK19(X231),X233)
| p2(X231)
| ~ r1(sK0,X231) ),
inference(cnf_transformation,[],[f10]) ).
fof(f230,plain,
! [X3] :
( ~ p2(sK23)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f231,plain,
! [X3] :
( r1(sK0,sK23)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f232,plain,
! [X3,X5] :
( r1(X5,sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f233,plain,
! [X3,X5] :
( p2(sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK41,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f300,plain,
! [X5] :
( p2(sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f301,plain,
! [X5] :
( r1(X5,sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f302,plain,
! [X5] :
( p2(sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f303,plain,
! [X5] :
( r1(X5,sK56(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f306,plain,
! [X15,X12] :
( p2(sK54(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f307,plain,
! [X15,X12] :
( r1(X15,sK54(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f308,plain,
! [X15,X12] :
( p2(sK54(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f309,plain,
! [X15,X12] :
( r1(X15,sK54(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f316,plain,
( r1(sK0,sK23)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f317,plain,
( ~ p2(sK23)
| r1(sK18,sK41) ),
inference(cnf_transformation,[],[f10]) ).
fof(f318,plain,
! [X12] :
( r1(sK0,sK21)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f319,plain,
! [X12] :
( r1(sK0,sK21)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f320,plain,
! [X12] :
( ~ p2(sK21)
| p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f321,plain,
! [X12] :
( ~ p2(sK21)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f396,plain,
( ~ p2(sK23)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f397,plain,
( r1(sK0,sK23)
| r1(sK0,sK18) ),
inference(cnf_transformation,[],[f10]) ).
fof(f418,plain,
! [X231] :
( ~ p2(sK19(X231))
| p2(X231)
| ~ r1(sK0,X231) ),
inference(cnf_transformation,[],[f10]) ).
fof(f419,plain,
! [X231] :
( r1(X231,sK19(X231))
| p2(X231)
| ~ r1(sK0,X231) ),
inference(cnf_transformation,[],[f10]) ).
fof(f491,plain,
! [X231] :
( r1(X231,sK19(X231))
| ~ p2(X231)
| ~ r1(sK0,X231) ),
inference(consistent_polarity_flipping,[],[f419]) ).
fof(f492,plain,
! [X231] :
( p2(sK19(X231))
| ~ p2(X231)
| ~ r1(sK0,X231) ),
inference(consistent_polarity_flipping,[],[f418]) ).
fof(f508,plain,
( p2(sK23)
| r1(sK0,sK18) ),
inference(consistent_polarity_flipping,[],[f396]) ).
fof(f580,plain,
! [X12] :
( p2(sK21)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f321]) ).
fof(f581,plain,
! [X12] :
( p2(sK21)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f320]) ).
fof(f582,plain,
! [X12] :
( r1(sK0,sK21)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f318]) ).
fof(f583,plain,
( p2(sK23)
| r1(sK18,sK41) ),
inference(consistent_polarity_flipping,[],[f317]) ).
fof(f588,plain,
! [X15,X12] :
( r1(X15,sK54(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f309]) ).
fof(f589,plain,
! [X15,X12] :
( ~ p2(sK54(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f308]) ).
fof(f590,plain,
! [X15,X12] :
( r1(X15,sK54(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f307]) ).
fof(f591,plain,
! [X15,X12] :
( ~ p2(sK54(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f306]) ).
fof(f594,plain,
! [X5] :
( r1(X5,sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(consistent_polarity_flipping,[],[f303]) ).
fof(f595,plain,
! [X5] :
( ~ p2(sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(consistent_polarity_flipping,[],[f302]) ).
fof(f596,plain,
! [X5] :
( r1(X5,sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(consistent_polarity_flipping,[],[f301]) ).
fof(f597,plain,
! [X5] :
( ~ p2(sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(consistent_polarity_flipping,[],[f300]) ).
fof(f662,plain,
! [X3,X5] :
( ~ p2(sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f233]) ).
fof(f663,plain,
! [X3,X5] :
( r1(X5,sK56(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f232]) ).
fof(f664,plain,
! [X3] :
( r1(sK0,sK23)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f231]) ).
fof(f665,plain,
! [X3] :
( p2(sK23)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f230]) ).
fof(f666,plain,
! [X233,X231,X234] :
( ~ p2(X231)
| ~ p2(X234)
| ~ r1(X233,X234)
| ~ r1(sK19(X231),X233)
| p2(X233)
| ~ r1(sK0,X231) ),
inference(consistent_polarity_flipping,[],[f229]) ).
fof(f688,plain,
! [X15,X12] :
( r1(sK54(X15),sK88(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f207]) ).
fof(f689,plain,
! [X15,X12] :
( p2(sK88(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f206]) ).
fof(f690,plain,
! [X15,X12] :
( r1(sK54(X15),sK88(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f205]) ).
fof(f691,plain,
! [X15,X12] :
( p2(sK88(X15))
| ~ p2(X15)
| ~ r1(sK0,X15)
| ~ p5(sK40(X12))
| ~ r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f204]) ).
fof(f692,plain,
! [X3,X5] :
( r1(sK56(X5),sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f203]) ).
fof(f693,plain,
! [X3,X5] :
( p2(sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| p5(X3)
| ~ r1(sK41,X3) ),
inference(consistent_polarity_flipping,[],[f202]) ).
fof(f696,plain,
! [X5] :
( r1(sK56(X5),sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(consistent_polarity_flipping,[],[f199]) ).
fof(f697,plain,
! [X5] :
( p2(sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK18) ),
inference(consistent_polarity_flipping,[],[f198]) ).
fof(f698,plain,
! [X5] :
( r1(sK56(X5),sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(consistent_polarity_flipping,[],[f197]) ).
fof(f699,plain,
! [X5] :
( p2(sK89(X5))
| ~ p2(X5)
| ~ r1(sK0,X5)
| r1(sK18,sK41) ),
inference(consistent_polarity_flipping,[],[f196]) ).
fof(f1491,definition,
( spl139_150
<=> r1(sK18,sK41) ),
introduced(definition,[new_symbols(definition,[spl139_150])],[avatar_definition]) ).
fof(f1493,plain,
( r1(sK18,sK41)
| ~ spl139_150 ),
inference(avatar_component_clause,[],[f1491]) ).
fof(f1495,definition,
( spl139_151
<=> ! [X5] :
( p2(sK89(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl139_151])],[avatar_definition]) ).
fof(f1496,plain,
( ! [X5] :
( p2(sK89(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) )
| ~ spl139_151 ),
inference(avatar_component_clause,[],[f1495]) ).
fof(f1497,plain,
( spl139_150
| spl139_151 ),
inference(avatar_split_clause,[],[f699,f1495,f1491]) ).
fof(f1499,definition,
( spl139_152
<=> ! [X5] :
( r1(sK56(X5),sK89(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl139_152])],[avatar_definition]) ).
fof(f1500,plain,
( ! [X5] :
( r1(sK56(X5),sK89(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) )
| ~ spl139_152 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1501,plain,
( spl139_150
| spl139_152 ),
inference(avatar_split_clause,[],[f698,f1499,f1491]) ).
fof(f1503,definition,
( spl139_153
<=> r1(sK0,sK18) ),
introduced(definition,[new_symbols(definition,[spl139_153])],[avatar_definition]) ).
fof(f1505,plain,
( r1(sK0,sK18)
| ~ spl139_153 ),
inference(avatar_component_clause,[],[f1503]) ).
fof(f1506,plain,
( spl139_153
| spl139_151 ),
inference(avatar_split_clause,[],[f697,f1495,f1503]) ).
fof(f1507,plain,
( spl139_153
| spl139_152 ),
inference(avatar_split_clause,[],[f696,f1499,f1503]) ).
fof(f1515,definition,
( spl139_155
<=> ! [X3] :
( p5(X3)
| ~ r1(sK41,X3) ) ),
introduced(definition,[new_symbols(definition,[spl139_155])],[avatar_definition]) ).
fof(f1516,plain,
( ! [X3] :
( ~ r1(sK41,X3)
| p5(X3) )
| ~ spl139_155 ),
inference(avatar_component_clause,[],[f1515]) ).
fof(f1517,plain,
( spl139_155
| spl139_151 ),
inference(avatar_split_clause,[],[f693,f1495,f1515]) ).
fof(f1518,plain,
( spl139_155
| spl139_152 ),
inference(avatar_split_clause,[],[f692,f1499,f1515]) ).
fof(f1520,definition,
( spl139_156
<=> ! [X12] :
( ~ p5(sK40(X12))
| ~ r1(sK0,X12) ) ),
introduced(definition,[new_symbols(definition,[spl139_156])],[avatar_definition]) ).
fof(f1521,plain,
( ! [X12] :
( ~ p5(sK40(X12))
| ~ r1(sK0,X12) )
| ~ spl139_156 ),
inference(avatar_component_clause,[],[f1520]) ).
fof(f1523,definition,
( spl139_157
<=> ! [X15] :
( p2(sK88(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl139_157])],[avatar_definition]) ).
fof(f1524,plain,
( ! [X15] :
( ~ p2(X15)
| ~ r1(sK0,X15)
| p2(sK88(X15)) )
| ~ spl139_157 ),
inference(avatar_component_clause,[],[f1523]) ).
fof(f1525,plain,
( spl139_156
| spl139_157 ),
inference(avatar_split_clause,[],[f691,f1523,f1520]) ).
fof(f1527,definition,
( spl139_158
<=> ! [X15] :
( r1(sK54(X15),sK88(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl139_158])],[avatar_definition]) ).
fof(f1528,plain,
( ! [X15] :
( r1(sK54(X15),sK88(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) )
| ~ spl139_158 ),
inference(avatar_component_clause,[],[f1527]) ).
fof(f1529,plain,
( spl139_156
| spl139_158 ),
inference(avatar_split_clause,[],[f690,f1527,f1520]) ).
fof(f1531,definition,
( spl139_159
<=> ! [X12] :
( r1(X12,sK40(X12))
| ~ r1(sK0,X12) ) ),
introduced(definition,[new_symbols(definition,[spl139_159])],[avatar_definition]) ).
fof(f1532,plain,
( ! [X12] :
( r1(X12,sK40(X12))
| ~ r1(sK0,X12) )
| ~ spl139_159 ),
inference(avatar_component_clause,[],[f1531]) ).
fof(f1533,plain,
( spl139_159
| spl139_157 ),
inference(avatar_split_clause,[],[f689,f1523,f1531]) ).
fof(f1534,plain,
( spl139_159
| spl139_158 ),
inference(avatar_split_clause,[],[f688,f1527,f1531]) ).
fof(f1616,definition,
( spl139_180
<=> p2(sK23) ),
introduced(definition,[new_symbols(definition,[spl139_180])],[avatar_definition]) ).
fof(f1618,plain,
( p2(sK23)
| ~ spl139_180 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1619,plain,
( spl139_155
| spl139_180 ),
inference(avatar_split_clause,[],[f665,f1616,f1515]) ).
fof(f1621,definition,
( spl139_181
<=> r1(sK0,sK23) ),
introduced(definition,[new_symbols(definition,[spl139_181])],[avatar_definition]) ).
fof(f1623,plain,
( r1(sK0,sK23)
| ~ spl139_181 ),
inference(avatar_component_clause,[],[f1621]) ).
fof(f1624,plain,
( spl139_155
| spl139_181 ),
inference(avatar_split_clause,[],[f664,f1621,f1515]) ).
fof(f1626,definition,
( spl139_182
<=> ! [X5] :
( r1(X5,sK56(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl139_182])],[avatar_definition]) ).
fof(f1627,plain,
( ! [X5] :
( r1(X5,sK56(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) )
| ~ spl139_182 ),
inference(avatar_component_clause,[],[f1626]) ).
fof(f1628,plain,
( spl139_155
| spl139_182 ),
inference(avatar_split_clause,[],[f663,f1626,f1515]) ).
fof(f1630,definition,
( spl139_183
<=> ! [X5] :
( ~ p2(sK56(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl139_183])],[avatar_definition]) ).
fof(f1631,plain,
( ! [X5] :
( ~ p2(sK56(X5))
| ~ r1(sK0,X5)
| ~ p2(X5) )
| ~ spl139_183 ),
inference(avatar_component_clause,[],[f1630]) ).
fof(f1632,plain,
( spl139_155
| spl139_183 ),
inference(avatar_split_clause,[],[f662,f1630,f1515]) ).
fof(f1873,plain,
( spl139_153
| spl139_183 ),
inference(avatar_split_clause,[],[f597,f1630,f1503]) ).
fof(f1874,plain,
( spl139_153
| spl139_182 ),
inference(avatar_split_clause,[],[f596,f1626,f1503]) ).
fof(f1875,plain,
( spl139_150
| spl139_183 ),
inference(avatar_split_clause,[],[f595,f1630,f1491]) ).
fof(f1876,plain,
( spl139_150
| spl139_182 ),
inference(avatar_split_clause,[],[f594,f1626,f1491]) ).
fof(f1878,definition,
( spl139_232
<=> ! [X15] :
( ~ p2(sK54(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl139_232])],[avatar_definition]) ).
fof(f1879,plain,
( ! [X15] :
( ~ p2(sK54(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) )
| ~ spl139_232 ),
inference(avatar_component_clause,[],[f1878]) ).
fof(f1880,plain,
( spl139_159
| spl139_232 ),
inference(avatar_split_clause,[],[f591,f1878,f1531]) ).
fof(f1882,definition,
( spl139_233
<=> ! [X15] :
( r1(X15,sK54(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl139_233])],[avatar_definition]) ).
fof(f1883,plain,
( ! [X15] :
( r1(X15,sK54(X15))
| ~ r1(sK0,X15)
| ~ p2(X15) )
| ~ spl139_233 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1884,plain,
( spl139_159
| spl139_233 ),
inference(avatar_split_clause,[],[f590,f1882,f1531]) ).
fof(f1885,plain,
( spl139_156
| spl139_232 ),
inference(avatar_split_clause,[],[f589,f1878,f1520]) ).
fof(f1886,plain,
( spl139_156
| spl139_233 ),
inference(avatar_split_clause,[],[f588,f1882,f1520]) ).
fof(f1891,plain,
( spl139_150
| spl139_181 ),
inference(avatar_split_clause,[],[f316,f1621,f1491]) ).
fof(f1892,plain,
( spl139_150
| spl139_180 ),
inference(avatar_split_clause,[],[f583,f1616,f1491]) ).
fof(f1894,definition,
( spl139_234
<=> r1(sK0,sK21) ),
introduced(definition,[new_symbols(definition,[spl139_234])],[avatar_definition]) ).
fof(f1896,plain,
( r1(sK0,sK21)
| ~ spl139_234 ),
inference(avatar_component_clause,[],[f1894]) ).
fof(f1897,plain,
( spl139_156
| spl139_234 ),
inference(avatar_split_clause,[],[f582,f1894,f1520]) ).
fof(f1898,plain,
( spl139_159
| spl139_234 ),
inference(avatar_split_clause,[],[f319,f1894,f1531]) ).
fof(f1900,definition,
( spl139_235
<=> p2(sK21) ),
introduced(definition,[new_symbols(definition,[spl139_235])],[avatar_definition]) ).
fof(f1902,plain,
( p2(sK21)
| ~ spl139_235 ),
inference(avatar_component_clause,[],[f1900]) ).
fof(f1903,plain,
( spl139_156
| spl139_235 ),
inference(avatar_split_clause,[],[f581,f1900,f1520]) ).
fof(f1904,plain,
( spl139_159
| spl139_235 ),
inference(avatar_split_clause,[],[f580,f1900,f1531]) ).
fof(f2195,plain,
( spl139_153
| spl139_180 ),
inference(avatar_split_clause,[],[f508,f1616,f1503]) ).
fof(f2196,plain,
( spl139_153
| spl139_181 ),
inference(avatar_split_clause,[],[f397,f1621,f1503]) ).
fof(f2477,plain,
( p5(sK40(sK41))
| ~ r1(sK0,sK41)
| ~ spl139_155
| ~ spl139_159 ),
inference(resolution,[],[f1516,f1532]) ).
fof(f2495,definition,
( spl139_344
<=> r1(sK0,sK41) ),
introduced(definition,[new_symbols(definition,[spl139_344])],[avatar_definition]) ).
fof(f2503,plain,
( ~ r1(sK0,sK41)
| ~ spl139_155
| ~ spl139_156
| ~ spl139_159 ),
inference(forward_subsumption_resolution,[],[f2477,f1521]) ).
fof(f2527,plain,
( ~ spl139_344
| ~ spl139_155
| ~ spl139_156
| ~ spl139_159 ),
inference(avatar_split_clause,[],[f2503,f1531,f1520,f1515,f2495]) ).
fof(f2556,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK19(sK23),X1)
| p2(X1)
| ~ r1(sK0,sK23) )
| ~ spl139_180 ),
inference(resolution,[],[f666,f1618]) ).
fof(f2560,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK19(sK23),X1)
| p2(X1) )
| ~ spl139_180
| ~ spl139_181 ),
inference(forward_subsumption_resolution,[],[f2556,f1623]) ).
fof(f2696,plain,
( ! [X0] :
( ~ r1(sK18,X0)
| r1(sK0,X0) )
| ~ spl139_153 ),
inference(resolution,[],[f12,f1505]) ).
fof(f2697,plain,
( ! [X0] :
( ~ r1(sK23,X0)
| r1(sK0,X0) )
| ~ spl139_181 ),
inference(resolution,[],[f12,f1623]) ).
fof(f2909,plain,
( r1(sK0,sK41)
| ~ spl139_150
| ~ spl139_153 ),
inference(resolution,[],[f2696,f1493]) ).
fof(f2992,plain,
( r1(sK0,sK19(sK23))
| ~ p2(sK23)
| ~ r1(sK0,sK23)
| ~ spl139_181 ),
inference(resolution,[],[f2697,f491]) ).
fof(f3035,plain,
( spl139_344
| ~ spl139_150
| ~ spl139_153 ),
inference(avatar_split_clause,[],[f2909,f1503,f1491,f2495]) ).
fof(f3043,definition,
( spl139_415
<=> ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK19(sK23),X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl139_415])],[avatar_definition]) ).
fof(f3044,plain,
( ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK19(sK23),X1)
| ~ r1(X1,X0) )
| ~ spl139_415 ),
inference(avatar_component_clause,[],[f3043]) ).
fof(f3099,plain,
( ! [X0] :
( ~ r1(sK21,X0)
| r1(sK0,X0) )
| ~ spl139_234 ),
inference(resolution,[],[f1896,f12]) ).
fof(f3102,plain,
( ~ r1(sK0,sK21)
| p2(sK88(sK21))
| ~ spl139_157
| ~ spl139_235 ),
inference(resolution,[],[f1524,f1902]) ).
fof(f3107,plain,
( p2(sK88(sK21))
| ~ spl139_157
| ~ spl139_234
| ~ spl139_235 ),
inference(forward_subsumption_resolution,[],[f3102,f1896]) ).
fof(f3120,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(sK0,X0)
| ~ r1(sK54(X0),X1)
| r1(X0,X1) )
| ~ spl139_233 ),
inference(resolution,[],[f1883,f12]) ).
fof(f3178,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X1,X0)
| ~ r1(sK19(sK88(sK21)),X1)
| p2(X1)
| ~ r1(sK0,sK88(sK21)) )
| ~ spl139_157
| ~ spl139_234
| ~ spl139_235 ),
inference(resolution,[],[f3107,f666]) ).
fof(f3201,definition,
( spl139_439
<=> r1(sK0,sK88(sK21)) ),
introduced(definition,[new_symbols(definition,[spl139_439])],[avatar_definition]) ).
fof(f3202,plain,
( r1(sK0,sK88(sK21))
| ~ spl139_439 ),
inference(avatar_component_clause,[],[f3201]) ).
fof(f3224,definition,
( spl139_444
<=> ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(sK19(sK88(sK21)),X1)
| ~ r1(X1,X0) ) ),
introduced(definition,[new_symbols(definition,[spl139_444])],[avatar_definition]) ).
fof(f3225,plain,
( ! [X0,X1] :
( ~ r1(sK19(sK88(sK21)),X1)
| p2(X1)
| ~ p2(X0)
| ~ r1(X1,X0) )
| ~ spl139_444 ),
inference(avatar_component_clause,[],[f3224]) ).
fof(f3226,plain,
( ~ spl139_439
| spl139_444
| ~ spl139_157
| ~ spl139_234
| ~ spl139_235 ),
inference(avatar_split_clause,[],[f3178,f1900,f1894,f1523,f3224,f3201]) ).
fof(f3734,plain,
( ! [X0] :
( ~ r1(sK0,sK21)
| ~ r1(sK54(sK21),X0)
| r1(sK21,X0) )
| ~ spl139_233
| ~ spl139_235 ),
inference(resolution,[],[f3120,f1902]) ).
fof(f3754,plain,
( ! [X0] :
( ~ r1(sK54(sK21),X0)
| r1(sK21,X0) )
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(forward_subsumption_resolution,[],[f3734,f1896]) ).
fof(f4708,plain,
( r1(sK21,sK88(sK21))
| ~ r1(sK0,sK21)
| ~ p2(sK21)
| ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(resolution,[],[f3754,f1528]) ).
fof(f4766,plain,
( r1(sK21,sK88(sK21))
| ~ p2(sK21)
| ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(forward_subsumption_resolution,[],[f4708,f1896]) ).
fof(f4795,plain,
( r1(sK21,sK88(sK21))
| ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(forward_subsumption_resolution,[],[f4766,f1902]) ).
fof(f5747,plain,
( spl139_415
| ~ spl139_180
| ~ spl139_181 ),
inference(avatar_split_clause,[],[f2560,f1621,f1616,f3043]) ).
fof(f5782,definition,
( spl139_762
<=> r1(sK0,sK19(sK23)) ),
introduced(definition,[new_symbols(definition,[spl139_762])],[avatar_definition]) ).
fof(f5784,plain,
( r1(sK0,sK19(sK23))
| ~ spl139_762 ),
inference(avatar_component_clause,[],[f5782]) ).
fof(f6034,plain,
( ! [X0,X1] :
( ~ r1(X0,sK89(X1))
| ~ r1(sK19(sK23),X0)
| p2(X0)
| ~ r1(sK0,X1)
| ~ p2(X1) )
| ~ spl139_151
| ~ spl139_415 ),
inference(resolution,[],[f3044,f1496]) ).
fof(f7214,plain,
( r1(sK0,sK88(sK21))
| ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(resolution,[],[f4795,f3099]) ).
fof(f7272,plain,
( spl139_439
| ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235 ),
inference(avatar_split_clause,[],[f7214,f1900,f1894,f1882,f1527,f3201]) ).
fof(f7378,plain,
( ! [X0] :
( ~ r1(sK88(sK21),X0)
| r1(sK0,X0) )
| ~ spl139_439 ),
inference(resolution,[],[f3202,f12]) ).
fof(f7419,definition,
( spl139_998
<=> p2(sK19(sK88(sK21))) ),
introduced(definition,[new_symbols(definition,[spl139_998])],[avatar_definition]) ).
fof(f7421,plain,
( ~ p2(sK19(sK88(sK21)))
| spl139_998 ),
inference(avatar_component_clause,[],[f7419]) ).
fof(f7454,definition,
( spl139_1006
<=> r1(sK0,sK19(sK88(sK21))) ),
introduced(definition,[new_symbols(definition,[spl139_1006])],[avatar_definition]) ).
fof(f8073,plain,
( ! [X0] :
( p2(sK54(sK19(sK88(sK21))))
| ~ p2(X0)
| ~ r1(sK54(sK19(sK88(sK21))),X0)
| ~ r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK19(sK88(sK21))) )
| ~ spl139_233
| ~ spl139_444 ),
inference(resolution,[],[f3225,f1883]) ).
fof(f8195,definition,
( spl139_1144
<=> ! [X0] :
( ~ p2(X0)
| ~ r1(sK54(sK19(sK88(sK21))),X0) ) ),
introduced(definition,[new_symbols(definition,[spl139_1144])],[avatar_definition]) ).
fof(f8196,plain,
( ! [X0] :
( ~ r1(sK54(sK19(sK88(sK21))),X0)
| ~ p2(X0) )
| ~ spl139_1144 ),
inference(avatar_component_clause,[],[f8195]) ).
fof(f13503,plain,
( r1(sK0,sK19(sK23))
| ~ r1(sK0,sK23)
| ~ spl139_180
| ~ spl139_181 ),
inference(forward_subsumption_resolution,[],[f2992,f1618]) ).
fof(f13543,plain,
( ~ spl139_181
| spl139_762
| ~ spl139_180
| ~ spl139_181 ),
inference(avatar_split_clause,[],[f13503,f1621,f1616,f5782,f1621]) ).
fof(f14342,definition,
( spl139_2016
<=> p2(sK19(sK23)) ),
introduced(definition,[new_symbols(definition,[spl139_2016])],[avatar_definition]) ).
fof(f14343,plain,
( p2(sK19(sK23))
| ~ spl139_2016 ),
inference(avatar_component_clause,[],[f14342]) ).
fof(f14344,plain,
( ~ p2(sK19(sK23))
| spl139_2016 ),
inference(avatar_component_clause,[],[f14342]) ).
fof(f15025,plain,
( ~ p2(sK23)
| ~ r1(sK0,sK23)
| spl139_2016 ),
inference(resolution,[],[f14344,f492]) ).
fof(f15026,plain,
( ~ r1(sK0,sK23)
| ~ spl139_180
| spl139_2016 ),
inference(forward_subsumption_resolution,[],[f15025,f1618]) ).
fof(f15027,plain,
( $false
| ~ spl139_180
| ~ spl139_181
| spl139_2016 ),
inference(forward_subsumption_resolution,[],[f15026,f1623]) ).
fof(f15028,plain,
( ~ spl139_180
| ~ spl139_181
| spl139_2016 ),
inference(avatar_contradiction_clause,[],[f15027]) ).
fof(f20655,plain,
( ! [X0] :
( ~ p2(X0)
| ~ r1(sK54(sK19(sK88(sK21))),X0)
| ~ r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK19(sK88(sK21))) )
| ~ spl139_232
| ~ spl139_233
| ~ spl139_444 ),
inference(forward_subsumption_resolution,[],[f8073,f1879]) ).
fof(f20667,plain,
( ~ spl139_998
| ~ spl139_1006
| spl139_1144
| ~ spl139_232
| ~ spl139_233
| ~ spl139_444 ),
inference(avatar_split_clause,[],[f20655,f3224,f1882,f1878,f8195,f7454,f7419]) ).
fof(f20687,plain,
( ~ p2(sK88(sK21))
| ~ r1(sK0,sK88(sK21))
| spl139_998 ),
inference(resolution,[],[f7421,f492]) ).
fof(f21385,plain,
( r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK88(sK21))
| ~ r1(sK0,sK88(sK21))
| ~ spl139_439 ),
inference(resolution,[],[f7378,f491]) ).
fof(f23982,plain,
( ~ p2(sK88(sK19(sK88(sK21))))
| ~ r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK19(sK88(sK21)))
| ~ spl139_158
| ~ spl139_1144 ),
inference(resolution,[],[f8196,f1528]) ).
fof(f24143,plain,
( ~ r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK19(sK88(sK21)))
| ~ spl139_157
| ~ spl139_158
| ~ spl139_1144 ),
inference(forward_subsumption_resolution,[],[f23982,f1524]) ).
fof(f24210,plain,
( ~ p2(sK88(sK21))
| ~ spl139_439
| spl139_998 ),
inference(forward_subsumption_resolution,[],[f20687,f3202]) ).
fof(f24220,definition,
( spl139_3453
<=> p2(sK88(sK21)) ),
introduced(definition,[new_symbols(definition,[spl139_3453])],[avatar_definition]) ).
fof(f24223,plain,
( spl139_3453
| ~ spl139_234
| ~ spl139_157
| ~ spl139_235 ),
inference(avatar_split_clause,[],[f3102,f1900,f1523,f1894,f24220]) ).
fof(f24360,plain,
( ~ spl139_3453
| ~ spl139_439
| spl139_998 ),
inference(avatar_split_clause,[],[f24210,f7419,f3201,f24220]) ).
fof(f24576,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK19(sK23),sK56(X0))
| p2(sK56(X0))
| ~ r1(sK0,X0)
| ~ p2(X0) )
| ~ spl139_151
| ~ spl139_152
| ~ spl139_415 ),
inference(resolution,[],[f1500,f6034]) ).
fof(f24579,plain,
( ! [X0] :
( ~ r1(sK0,X0)
| ~ p2(X0)
| ~ r1(sK19(sK23),sK56(X0))
| p2(sK56(X0)) )
| ~ spl139_151
| ~ spl139_152
| ~ spl139_415 ),
inference(duplicate_literal_removal,[],[f24576]) ).
fof(f24586,plain,
( ! [X0] :
( ~ r1(sK19(sK23),sK56(X0))
| ~ p2(X0)
| ~ r1(sK0,X0) )
| ~ spl139_151
| ~ spl139_152
| ~ spl139_183
| ~ spl139_415 ),
inference(forward_subsumption_resolution,[],[f24579,f1631]) ).
fof(f32603,plain,
( r1(sK0,sK19(sK88(sK21)))
| ~ p2(sK88(sK21))
| ~ spl139_439 ),
inference(forward_subsumption_resolution,[],[f21385,f3202]) ).
fof(f32605,plain,
( ~ spl139_998
| ~ spl139_1006
| ~ spl139_157
| ~ spl139_158
| ~ spl139_1144 ),
inference(avatar_split_clause,[],[f24143,f8195,f1527,f1523,f7454,f7419]) ).
fof(f32774,plain,
( ~ spl139_3453
| spl139_1006
| ~ spl139_439 ),
inference(avatar_split_clause,[],[f32603,f3201,f7454,f24220]) ).
fof(f45319,plain,
( ~ p2(sK19(sK23))
| ~ r1(sK0,sK19(sK23))
| ~ r1(sK0,sK19(sK23))
| ~ p2(sK19(sK23))
| ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415 ),
inference(resolution,[],[f24586,f1627]) ).
fof(f45320,plain,
( ~ p2(sK19(sK23))
| ~ r1(sK0,sK19(sK23))
| ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415 ),
inference(duplicate_literal_removal,[],[f45319]) ).
fof(f45321,plain,
( ~ r1(sK0,sK19(sK23))
| ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415
| ~ spl139_2016 ),
inference(forward_subsumption_resolution,[],[f45320,f14343]) ).
fof(f45322,plain,
( $false
| ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415
| ~ spl139_762
| ~ spl139_2016 ),
inference(forward_subsumption_resolution,[],[f45321,f5784]) ).
fof(f45323,plain,
( ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415
| ~ spl139_762
| ~ spl139_2016 ),
inference(avatar_contradiction_clause,[],[f45322]) ).
cnf(s133,plain,
( spl139_150
| spl139_151 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s134,plain,
( spl139_150
| spl139_152 ),
inference(sat_conversion,[],[f1501]) ).
cnf(s135,plain,
( spl139_151
| spl139_153 ),
inference(sat_conversion,[],[f1506]) ).
cnf(s136,plain,
( spl139_152
| spl139_153 ),
inference(sat_conversion,[],[f1507]) ).
cnf(s139,plain,
( spl139_151
| spl139_155 ),
inference(sat_conversion,[],[f1517]) ).
cnf(s140,plain,
( spl139_152
| spl139_155 ),
inference(sat_conversion,[],[f1518]) ).
cnf(s141,plain,
( spl139_156
| spl139_157 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s142,plain,
( spl139_156
| spl139_158 ),
inference(sat_conversion,[],[f1529]) ).
cnf(s143,plain,
( spl139_157
| spl139_159 ),
inference(sat_conversion,[],[f1533]) ).
cnf(s144,plain,
( spl139_158
| spl139_159 ),
inference(sat_conversion,[],[f1534]) ).
cnf(s165,plain,
( spl139_155
| spl139_180 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s166,plain,
( spl139_155
| spl139_181 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s167,plain,
( spl139_155
| spl139_182 ),
inference(sat_conversion,[],[f1628]) ).
cnf(s168,plain,
( spl139_155
| spl139_183 ),
inference(sat_conversion,[],[f1632]) ).
cnf(s231,plain,
( spl139_153
| spl139_183 ),
inference(sat_conversion,[],[f1873]) ).
cnf(s232,plain,
( spl139_153
| spl139_182 ),
inference(sat_conversion,[],[f1874]) ).
cnf(s233,plain,
( spl139_150
| spl139_183 ),
inference(sat_conversion,[],[f1875]) ).
cnf(s234,plain,
( spl139_150
| spl139_182 ),
inference(sat_conversion,[],[f1876]) ).
cnf(s235,plain,
( spl139_159
| spl139_232 ),
inference(sat_conversion,[],[f1880]) ).
cnf(s236,plain,
( spl139_159
| spl139_233 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s237,plain,
( spl139_156
| spl139_232 ),
inference(sat_conversion,[],[f1885]) ).
cnf(s238,plain,
( spl139_156
| spl139_233 ),
inference(sat_conversion,[],[f1886]) ).
cnf(s243,plain,
( spl139_150
| spl139_181 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s244,plain,
( spl139_150
| spl139_180 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s245,plain,
( spl139_156
| spl139_234 ),
inference(sat_conversion,[],[f1897]) ).
cnf(s246,plain,
( spl139_159
| spl139_234 ),
inference(sat_conversion,[],[f1898]) ).
cnf(s247,plain,
( spl139_156
| spl139_235 ),
inference(sat_conversion,[],[f1903]) ).
cnf(s248,plain,
( spl139_159
| spl139_235 ),
inference(sat_conversion,[],[f1904]) ).
cnf(s323,plain,
( spl139_153
| spl139_180 ),
inference(sat_conversion,[],[f2195]) ).
cnf(s324,plain,
( spl139_153
| spl139_181 ),
inference(sat_conversion,[],[f2196]) ).
cnf(s382,plain,
( ~ spl139_155
| ~ spl139_156
| ~ spl139_159
| ~ spl139_344 ),
inference(sat_conversion,[],[f2527]) ).
cnf(s437,plain,
( ~ spl139_150
| ~ spl139_153
| spl139_344 ),
inference(sat_conversion,[],[f3035]) ).
cnf(s467,plain,
( ~ spl139_157
| ~ spl139_234
| ~ spl139_235
| ~ spl139_439
| spl139_444 ),
inference(sat_conversion,[],[f3226]) ).
cnf(s712,plain,
( ~ spl139_180
| ~ spl139_181
| spl139_415 ),
inference(sat_conversion,[],[f5747]) ).
cnf(s916,plain,
( ~ spl139_158
| ~ spl139_233
| ~ spl139_234
| ~ spl139_235
| spl139_439 ),
inference(sat_conversion,[],[f7272]) ).
cnf(s1643,plain,
( ~ spl139_181
| ~ spl139_180
| ~ spl139_181
| spl139_762 ),
inference(sat_conversion,[],[f13543]) ).
cnf(s1644,plain,
( ~ spl139_180
| ~ spl139_181
| spl139_762 ),
inference(rat,[],[s1643]) ).
cnf(s1861,plain,
( ~ spl139_180
| ~ spl139_181
| spl139_2016 ),
inference(sat_conversion,[],[f15028]) ).
cnf(s2530,plain,
( ~ spl139_232
| ~ spl139_233
| ~ spl139_444
| ~ spl139_998
| ~ spl139_1006
| spl139_1144 ),
inference(sat_conversion,[],[f20667]) ).
cnf(s2907,plain,
( ~ spl139_157
| ~ spl139_234
| ~ spl139_235
| spl139_3453 ),
inference(sat_conversion,[],[f24223]) ).
cnf(s2936,plain,
( ~ spl139_439
| spl139_998
| ~ spl139_3453 ),
inference(sat_conversion,[],[f24360]) ).
cnf(s4142,plain,
( ~ spl139_157
| ~ spl139_158
| ~ spl139_998
| ~ spl139_1006
| ~ spl139_1144 ),
inference(sat_conversion,[],[f32605]) ).
cnf(s4195,plain,
( ~ spl139_439
| spl139_1006
| ~ spl139_3453 ),
inference(sat_conversion,[],[f32774]) ).
cnf(s5484,plain,
( ~ spl139_151
| ~ spl139_152
| ~ spl139_182
| ~ spl139_183
| ~ spl139_415
| ~ spl139_762
| ~ spl139_2016 ),
inference(sat_conversion,[],[f45323]) ).
cnf(s5495,plain,
spl139_150,
inference(rat,[],[s5484,s712,s1644,s1861,s133,s134,s233,s234,s243,s244]) ).
cnf(s5496,plain,
( spl139_153
| ~ spl139_152
| ~ spl139_151 ),
inference(rat,[],[s5484,s712,s1644,s1861,s231,s232,s323,s324]) ).
cnf(s5500,plain,
( spl139_152
| ~ spl139_159
| ~ spl139_156 ),
inference(rat,[],[s437,s382,s136,s140,s5495]) ).
cnf(s5504,plain,
spl139_156,
inference(rat,[],[s2530,s4142,s467,s2936,s4195,s2907,s916,s141,s142,s237,s238,s245,s247]) ).
cnf(s5505,plain,
spl139_159,
inference(rat,[],[s2530,s4142,s467,s2936,s4195,s2907,s916,s143,s144,s235,s236,s246,s248]) ).
cnf(s5509,plain,
spl139_152,
inference(rat,[],[s5500,s5504,s5505]) ).
cnf(s5510,plain,
spl139_155,
inference(rat,[],[s5484,s712,s1644,s1861,s139,s165,s166,s167,s168,s5509]) ).
cnf(s5511,plain,
~ spl139_344,
inference(rat,[],[s382,s5505,s5504,s5510]) ).
cnf(s5512,plain,
~ spl139_153,
inference(rat,[],[s437,s5495,s5511]) ).
cnf(s5517,plain,
spl139_151,
inference(rat,[],[s135,s5512]) ).
cnf(s5518,plain,
$false,
inference(rat,[],[s5496,s5509,s5517,s5512]) ).
fof(f45324,plain,
$false,
inference(avatar_sat_refutation,[],[s5518]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL676+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n008.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 16:33:55 UTC 2026
% 0.12/0.40 % CPUTime :
% 0.12/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.43 Running first-order model finding
% 0.12/0.43 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
% 5.79/1.37 % (1433236)Will run a generic schedule for satisfiability detection.
% 5.79/1.37 % (1433241)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1898032938_2999 on theBenchmark for (2999ds/0Mi)
% 5.79/1.37 % (1433242)% WARNING: option uhcvi not known.
% 5.79/1.37 % (1433244)dis+10_1_sil=32000:sp=arity:random_seed=1869257663:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.79/1.37 % (1433242)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1137869686:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.79/1.37 % (1433243)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=553150595:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.79/1.37 % (1433245)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2854587648:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.79/1.37 % (1433246)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3313022815:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.79/1.37 % (1433247)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2367752617:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.79/1.37 % TRYING [1]
% 5.79/1.37 % TRYING [2]
% 5.79/1.37 % TRYING [3]
% 5.79/1.37 % TRYING [4]
% 5.79/1.37 % TRYING [5]
% 5.79/1.37 % (1433244)Instruction limit reached!
% 5.79/1.37 % (1433244)------------------------------
% 5.79/1.37 % (1433244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433244)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433244)Termination reason: Instruction limit
% 5.79/1.37 % (1433244)Termination phase: Saturation
% 5.79/1.37 % (1433244)Time elapsed: 0.057 s
% 5.79/1.37 % (1433244)Peak memory usage: 14 MB
% 5.79/1.37 % (1433244)Instructions burned: 105 (million)
% 5.79/1.37 % (1433245)Instruction limit reached!
% 5.79/1.37 % (1433245)------------------------------
% 5.79/1.37 % (1433245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433245)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433245)Termination reason: Instruction limit
% 5.79/1.37 % (1433245)Termination phase: Saturation
% 5.79/1.37 % (1433245)Time elapsed: 0.060 s
% 5.79/1.37 % (1433245)Peak memory usage: 13 MB
% 5.79/1.37 % (1433245)Instructions burned: 116 (million)
% 5.79/1.37 % (1433246)Instruction limit reached!
% 5.79/1.37 % (1433246)------------------------------
% 5.79/1.37 % (1433246)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433246)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433246)Termination reason: Instruction limit
% 5.79/1.37 % (1433246)Termination phase: Saturation
% 5.79/1.37 % (1433246)Time elapsed: 0.074 s
% 5.79/1.37 % (1433246)Peak memory usage: 14 MB
% 5.79/1.37 % (1433246)Instructions burned: 132 (million)
% 5.79/1.37 % (1433255)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2327225060:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.79/1.37 % (1433247)Instruction limit reached!
% 5.79/1.37 % (1433247)------------------------------
% 5.79/1.37 % (1433247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433247)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433247)Termination reason: Instruction limit
% 5.79/1.37 % (1433247)Termination phase: Saturation
% 5.79/1.37 % (1433247)Time elapsed: 0.079 s
% 5.79/1.37 % (1433247)Peak memory usage: 15 MB
% 5.79/1.37 % (1433247)Instructions burned: 160 (million)
% 5.79/1.37 % (1433256)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4102393407:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 5.79/1.37 % TRYING [1]
% 5.79/1.37 % (1433258)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=3424081011:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 5.79/1.37 % TRYING [2]
% 5.79/1.37 % (1433260)ott-21_1_sil=16000:fs=off:random_seed=3004250333:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 5.79/1.37 % TRYING [3]
% 5.79/1.37 % TRYING [6]
% 5.79/1.37 % TRYING [4]
% 5.79/1.37 % TRYING [5]
% 5.79/1.37 % (1433256)Instruction limit reached!
% 5.79/1.37 % (1433256)------------------------------
% 5.79/1.37 % (1433256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433256)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433256)Termination reason: Instruction limit
% 5.79/1.37 % (1433256)Termination phase: Saturation
% 5.79/1.37 % (1433256)Time elapsed: 0.067 s
% 5.79/1.37 % (1433256)Peak memory usage: 13 MB
% 5.79/1.37 % (1433256)Instructions burned: 132 (million)
% 5.79/1.37 % (1433263)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2592711229:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.79/1.37 % (1433260)Instruction limit reached!
% 5.79/1.37 % (1433260)------------------------------
% 5.79/1.37 % (1433260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433260)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433260)Termination reason: Instruction limit
% 5.79/1.37 % (1433260)Termination phase: Saturation
% 5.79/1.37 % (1433260)Time elapsed: 0.094 s
% 5.79/1.37 % (1433260)Peak memory usage: 15 MB
% 5.79/1.37 % (1433260)Instructions burned: 180 (million)
% 5.79/1.37 % (1433265)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1590753644:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 5.79/1.37 % TRYING [6]
% 5.79/1.37 % TRYING [7]
% 5.79/1.37 % TRYING [1]
% 5.79/1.37 % TRYING [2]
% 5.79/1.37 % TRYING [3]
% 5.79/1.37 % TRYING [4]
% 5.79/1.37 % TRYING [5]
% 5.79/1.37 % (1433258)Instruction limit reached!
% 5.79/1.37 % (1433258)------------------------------
% 5.79/1.37 % (1433258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433258)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433258)Termination reason: Instruction limit
% 5.79/1.37 % (1433258)Termination phase: Saturation
% 5.79/1.37 % (1433258)Time elapsed: 0.336 s
% 5.79/1.37 % (1433258)Peak memory usage: 22 MB
% 5.79/1.37 % (1433258)Instructions burned: 686 (million)
% 5.79/1.37 % (1433255)Instruction limit reached!
% 5.79/1.37 % (1433255)------------------------------
% 5.79/1.37 % (1433255)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433255)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433255)Termination reason: Instruction limit
% 5.79/1.37 % (1433255)Termination phase: Finite model building SAT solving
% 5.79/1.37 % (1433255)Time elapsed: 0.363 s
% 5.79/1.37 % (1433255)Peak memory usage: 23 MB
% 5.79/1.37 % (1433255)Instructions burned: 715 (million)
% 5.79/1.37 % (1433267)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2172900365:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 5.79/1.37 % (1433268)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1021546706:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 5.79/1.37 % (1433263)Instruction limit reached!
% 5.79/1.37 % (1433263)------------------------------
% 5.79/1.37 % (1433263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433263)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433263)Termination reason: Instruction limit
% 5.79/1.37 % (1433263)Termination phase: Saturation
% 5.79/1.37 % (1433263)Time elapsed: 0.295 s
% 5.79/1.37 % (1433263)Peak memory usage: 19 MB
% 5.79/1.37 % (1433263)Instructions burned: 477 (million)
% 5.79/1.37 % (1433271)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=608332811:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 5.79/1.37 % TRYING [14]
% 5.79/1.37 % TRYING [6]
% 5.79/1.37 % (1433265)Instruction limit reached!
% 5.79/1.37 % (1433265)------------------------------
% 5.79/1.37 % (1433265)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433265)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433265)Termination reason: Instruction limit
% 5.79/1.37 % (1433265)Termination phase: Finite model building constraint generation
% 5.79/1.37 % (1433265)Time elapsed: 0.350 s
% 5.79/1.37 % (1433265)Peak memory usage: 19 MB
% 5.79/1.37 % (1433265)Instructions burned: 866 (million)
% 5.79/1.37 % (1433273)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3287825392:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 5.79/1.37 % (1433268)Instruction limit reached!
% 5.79/1.37 % (1433268)------------------------------
% 5.79/1.37 % (1433268)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433268)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433268)Termination reason: Instruction limit
% 5.79/1.37 % (1433268)Termination phase: Finite model building SAT solving
% 5.79/1.37 % (1433268)Time elapsed: 0.363 s
% 5.79/1.37 % (1433268)Peak memory usage: 57 MB
% 5.79/1.37 % (1433268)Instructions burned: 889 (million)
% 5.79/1.37 % (1433275)fmb+10_1_sil=64000:random_seed=3194381795:i=22061:nm=2:gsp=on_2991 on theBenchmark for (2991ds/22061Mi)
% 5.79/1.37 % TRYING [1]
% 5.79/1.37 % TRYING [2]
% 5.79/1.37 % (1433271)Instruction limit reached!
% 5.79/1.37 % (1433271)------------------------------
% 5.79/1.37 % (1433271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.37 % (1433271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.37 % (1433271)CaDiCaL version: 2.1.3
% 5.79/1.37 % (1433271)Termination reason: Instruction limit
% 5.79/1.37 % (1433271)Termination phase: Saturation
% 5.79/1.37 % (1433271)Time elapsed: 0.387 s
% 5.79/1.37 % (1433271)Peak memory usage: 23 MB
% 5.79/1.37 % (1433271)Instructions burned: 693 (million)
% 5.79/1.37 % (1433242) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1433236-1433242"...
% 5.79/1.37 % TRYING [3]
% 5.79/1.37 % (1433242)...printing done.
% 5.79/1.37 % (1433242)Refutation found. Thanks to Tanya!
% 5.79/1.37 % SZS status Theorem for theBenchmark
% 5.79/1.37 % SZS output start Proof for theBenchmark
% See solution above
% 5.79/1.38 % (1433242)------------------------------
% 5.79/1.38 % (1433242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.79/1.38 % (1433242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.79/1.38 % (1433242)CaDiCaL version: 2.1.3
% 5.79/1.38 % (1433242)Termination reason: Refutation
% 5.79/1.38 % (1433242)Time elapsed: 0.885 s
% 5.79/1.38 % (1433242)Peak memory usage: 35 MB
% 5.79/1.38 % (1433242)Instructions burned: 1642 (million)
% 5.79/1.38 % (1433236)Success in time 0.935 s
% 5.79/1.38 % Vampire exiting
%------------------------------------------------------------------------------