%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL676+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n009.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 19.24s 3.19s
% Output : Refutation 19.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 21
% Syntax : Number of formulae : 232 ( 11 unt; 19 def)
% Number of atoms : 3336 ( 0 equ)
% Maximal formula atoms : 426 ( 14 avg)
% Number of connectives : 4740 (1636 ~;2591 |; 493 &)
% ( 19 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 27 ( 25 usr; 21 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-1 aty)
% Number of variables : 1072 ( 0 sgn 918 !; 154 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( r1(X0,X1)
& r1(X1,X2) )
=> r1(X0,X2) ),
file('/export/starexec/sandbox/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) ) ) ) ) ) )
& ( 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/sandbox/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) ) ) ) ) ) )
& ( 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) ) ) ) ) ) )
& ( 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)
| $false ) ) )
| ~ ! [X64] :
( ~ r1(X0,X64)
| p1(X64)
| ! [X65] :
( ~ r1(X64,X65)
| p4(X65)
| p3(X65)
| p2(X65)
| p1(X65)
| ! [X66] :
( ~ r1(X65,X66)
| p4(X66)
| p3(X66)
| p2(X66)
| p1(X66)
| ! [X67] :
( ~ r1(X66,X67)
| $false ) ) )
| ~ ! [X68] :
( ~ r1(X64,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| p4(X71)
| p3(X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| $false ) ) ) )
| ~ ( p1(X68)
| ! [X73] :
( ~ r1(X68,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 ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X76] :
( ~ r1(X0,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| $false ) )
| ~ ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] :
( ~ r1(X78,X79)
| p4(X79)
| p3(X79)
| p2(X79)
| p1(X79)
| ! [X80] :
( ~ r1(X79,X80)
| $false ) )
| ~ ! [X81] :
( ~ r1(X78,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| p4(X83)
| p3(X83)
| p2(X83)
| p1(X83)
| ! [X84] :
( ~ r1(X83,X84)
| $false ) ) )
| ~ ( p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X85] :
( ~ r1(X81,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] :
( ~ r1(X85,X86)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X87] :
( ~ r1(X0,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) )
| ~ ! [X89] :
( ~ r1(X0,X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] :
( ~ r1(X89,X90)
| p4(X90)
| p3(X90)
| p2(X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| $false ) )
| ~ ! [X92] :
( ~ r1(X89,X92)
| ! [X93] :
( ~ r1(X92,X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| p4(X94)
| p3(X94)
| p2(X94)
| p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| $false ) ) )
| ~ ( p3(X92)
| p2(X92)
| p1(X92)
| ! [X96] :
( ~ r1(X92,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X98] :
( ~ r1(X0,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] :
( ~ r1(X98,X99)
| $false ) )
| ~ ! [X100] :
( ~ r1(X0,X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| p4(X101)
| p3(X101)
| p2(X101)
| p1(X101)
| ! [X102] :
( ~ r1(X101,X102)
| $false ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| p4(X105)
| p3(X105)
| p2(X105)
| p1(X105)
| ! [X106] :
( ~ r1(X105,X106)
| $false ) ) )
| ~ ( p2(X103)
| p1(X103)
| ! [X107] :
( ~ r1(X103,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X109] :
( ~ r1(X0,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) )
| ~ ! [X111] :
( ~ r1(X0,X111)
| p1(X111)
| ! [X112] :
( ~ r1(X111,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] :
( ~ r1(X112,X113)
| $false ) )
| ~ ! [X114] :
( ~ r1(X111,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| p4(X116)
| p3(X116)
| p2(X116)
| p1(X116)
| ! [X117] :
( ~ r1(X116,X117)
| $false ) ) )
| ~ ( p1(X114)
| ! [X118] :
( ~ r1(X114,X118)
| p4(X118)
| p3(X118)
| p2(X118)
| p1(X118)
| ! [X119] :
( ~ r1(X118,X119)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X120] :
( ~ r1(X0,X120)
| $false )
| ~ ! [X121] :
( ~ r1(X0,X121)
| p4(X121)
| p3(X121)
| p2(X121)
| p1(X121)
| ! [X122] :
( ~ r1(X121,X122)
| $false )
| ~ ! [X123] :
( ~ r1(X121,X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) )
| ~ ( p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X126] :
( ~ r1(X123,X126)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X127] :
( ~ r1(X0,X127)
| $false )
| ~ ! [X128] :
( ~ r1(X0,X128)
| p3(X128)
| p2(X128)
| p1(X128)
| ! [X129] :
( ~ r1(X128,X129)
| $false )
| ~ ! [X130] :
( ~ r1(X128,X130)
| ! [X131] :
( ~ r1(X130,X131)
| p3(X131)
| p2(X131)
| p1(X131)
| ! [X132] :
( ~ r1(X131,X132)
| $false ) )
| ~ ( p3(X130)
| p2(X130)
| p1(X130)
| ! [X133] :
( ~ r1(X130,X133)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X134] :
( ~ r1(X0,X134)
| $false )
| ~ ! [X135] :
( ~ r1(X0,X135)
| p2(X135)
| p1(X135)
| ! [X136] :
( ~ r1(X135,X136)
| $false )
| ~ ! [X137] :
( ~ r1(X135,X137)
| ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| $false ) )
| ~ ( p2(X137)
| p1(X137)
| ! [X140] :
( ~ r1(X137,X140)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X141] :
( ~ r1(X0,X141)
| $false )
| ~ ! [X142] :
( ~ r1(X0,X142)
| p1(X142)
| ! [X143] :
( ~ r1(X142,X143)
| $false )
| ~ ! [X144] :
( ~ r1(X142,X144)
| ! [X145] :
( ~ r1(X144,X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) )
| ~ ( p1(X144)
| ! [X147] :
( ~ r1(X144,X147)
| $false ) ) ) ) )
& ! [X148] :
( ~ r1(X0,X148)
| p2(X148)
| ~ ! [X149] :
( ~ r1(X148,X149)
| p2(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p2(X151) )
| ~ p2(X150) ) ) ) ) ),
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) ) ) ) ) ) )
& ( 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)
| $false ) ) )
| ~ ! [X64] :
( ~ r1(X0,X64)
| p1(X64)
| ! [X65] :
( ~ r1(X64,X65)
| p4(X65)
| p3(X65)
| p2(X65)
| p1(X65)
| ! [X66] :
( ~ r1(X65,X66)
| p4(X66)
| p3(X66)
| p2(X66)
| p1(X66)
| ! [X67] :
( ~ r1(X66,X67)
| $false ) ) )
| ~ ! [X68] :
( ~ r1(X64,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| p4(X71)
| p3(X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| $false ) ) ) )
| ~ ( p1(X68)
| ! [X73] :
( ~ r1(X68,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 ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X76] :
( ~ r1(X0,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| $false ) )
| ~ ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] :
( ~ r1(X78,X79)
| p4(X79)
| p3(X79)
| p2(X79)
| p1(X79)
| ! [X80] :
( ~ r1(X79,X80)
| $false ) )
| ~ ! [X81] :
( ~ r1(X78,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| p4(X83)
| p3(X83)
| p2(X83)
| p1(X83)
| ! [X84] :
( ~ r1(X83,X84)
| $false ) ) )
| ~ ( p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X85] :
( ~ r1(X81,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] :
( ~ r1(X85,X86)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X87] :
( ~ r1(X0,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) )
| ~ ! [X89] :
( ~ r1(X0,X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] :
( ~ r1(X89,X90)
| p4(X90)
| p3(X90)
| p2(X90)
| p1(X90)
| ! [X91] :
( ~ r1(X90,X91)
| $false ) )
| ~ ! [X92] :
( ~ r1(X89,X92)
| ! [X93] :
( ~ r1(X92,X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| p4(X94)
| p3(X94)
| p2(X94)
| p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| $false ) ) )
| ~ ( p3(X92)
| p2(X92)
| p1(X92)
| ! [X96] :
( ~ r1(X92,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X98] :
( ~ r1(X0,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] :
( ~ r1(X98,X99)
| $false ) )
| ~ ! [X100] :
( ~ r1(X0,X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| p4(X101)
| p3(X101)
| p2(X101)
| p1(X101)
| ! [X102] :
( ~ r1(X101,X102)
| $false ) )
| ~ ! [X103] :
( ~ r1(X100,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| p4(X105)
| p3(X105)
| p2(X105)
| p1(X105)
| ! [X106] :
( ~ r1(X105,X106)
| $false ) ) )
| ~ ( p2(X103)
| p1(X103)
| ! [X107] :
( ~ r1(X103,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X109] :
( ~ r1(X0,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) )
| ~ ! [X111] :
( ~ r1(X0,X111)
| p1(X111)
| ! [X112] :
( ~ r1(X111,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] :
( ~ r1(X112,X113)
| $false ) )
| ~ ! [X114] :
( ~ r1(X111,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| p4(X116)
| p3(X116)
| p2(X116)
| p1(X116)
| ! [X117] :
( ~ r1(X116,X117)
| $false ) ) )
| ~ ( p1(X114)
| ! [X118] :
( ~ r1(X114,X118)
| p4(X118)
| p3(X118)
| p2(X118)
| p1(X118)
| ! [X119] :
( ~ r1(X118,X119)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X120] :
( ~ r1(X0,X120)
| $false )
| ~ ! [X121] :
( ~ r1(X0,X121)
| p4(X121)
| p3(X121)
| p2(X121)
| p1(X121)
| ! [X122] :
( ~ r1(X121,X122)
| $false )
| ~ ! [X123] :
( ~ r1(X121,X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) )
| ~ ( p4(X123)
| p3(X123)
| p2(X123)
| p1(X123)
| ! [X126] :
( ~ r1(X123,X126)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X127] :
( ~ r1(X0,X127)
| $false )
| ~ ! [X128] :
( ~ r1(X0,X128)
| p3(X128)
| p2(X128)
| p1(X128)
| ! [X129] :
( ~ r1(X128,X129)
| $false )
| ~ ! [X130] :
( ~ r1(X128,X130)
| ! [X131] :
( ~ r1(X130,X131)
| p3(X131)
| p2(X131)
| p1(X131)
| ! [X132] :
( ~ r1(X131,X132)
| $false ) )
| ~ ( p3(X130)
| p2(X130)
| p1(X130)
| ! [X133] :
( ~ r1(X130,X133)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X134] :
( ~ r1(X0,X134)
| $false )
| ~ ! [X135] :
( ~ r1(X0,X135)
| p2(X135)
| p1(X135)
| ! [X136] :
( ~ r1(X135,X136)
| $false )
| ~ ! [X137] :
( ~ r1(X135,X137)
| ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| $false ) )
| ~ ( p2(X137)
| p1(X137)
| ! [X140] :
( ~ r1(X137,X140)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X141] :
( ~ r1(X0,X141)
| $false )
| ~ ! [X142] :
( ~ r1(X0,X142)
| p1(X142)
| ! [X143] :
( ~ r1(X142,X143)
| $false )
| ~ ! [X144] :
( ~ r1(X142,X144)
| ! [X145] :
( ~ r1(X144,X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) )
| ~ ( p1(X144)
| ! [X147] :
( ~ r1(X144,X147)
| $false ) ) ) ) )
& ! [X148] :
( ~ r1(X0,X148)
| p2(X148)
| ~ ! [X149] :
( ~ r1(X148,X149)
| p2(X149)
| ~ ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p2(X151) )
| ~ p2(X150) ) ) ) ) ),
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) ) ) ) ) )
& ( 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)
| $false ) ) )
| ? [X64] :
( r1(X0,X64)
& ~ p1(X64)
& ? [X65] :
( r1(X64,X65)
& ~ p4(X65)
& ~ p3(X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] :
( r1(X65,X66)
& ~ p4(X66)
& ~ p3(X66)
& ~ p2(X66)
& ~ p1(X66)
& ? [X67] :
( r1(X66,X67)
& $true ) ) )
& ! [X68] :
( ~ r1(X64,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| p4(X71)
| p3(X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| $false ) ) ) )
| ( ~ p1(X68)
& ? [X73] :
( r1(X68,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)
& $true ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X76] :
( ~ r1(X0,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| $false ) )
| ? [X78] :
( r1(X0,X78)
& ~ p4(X78)
& ~ p3(X78)
& ~ p2(X78)
& ~ p1(X78)
& ? [X79] :
( r1(X78,X79)
& ~ p4(X79)
& ~ p3(X79)
& ~ p2(X79)
& ~ p1(X79)
& ? [X80] :
( r1(X79,X80)
& $true ) )
& ! [X81] :
( ~ r1(X78,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| p4(X83)
| p3(X83)
| p2(X83)
| p1(X83)
| ! [X84] :
( ~ r1(X83,X84)
| $false ) ) )
| ( ~ p4(X81)
& ~ p3(X81)
& ~ p2(X81)
& ~ p1(X81)
& ? [X85] :
( r1(X81,X85)
& ~ p4(X85)
& ~ p3(X85)
& ~ p2(X85)
& ~ p1(X85)
& ? [X86] :
( r1(X85,X86)
& $true ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X87] :
( ~ r1(X0,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) )
| ? [X89] :
( r1(X0,X89)
& ~ p3(X89)
& ~ p2(X89)
& ~ p1(X89)
& ? [X90] :
( r1(X89,X90)
& ~ p4(X90)
& ~ p3(X90)
& ~ p2(X90)
& ~ p1(X90)
& ? [X91] :
( r1(X90,X91)
& $true ) )
& ! [X92] :
( ~ r1(X89,X92)
| ! [X93] :
( ~ r1(X92,X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| p4(X94)
| p3(X94)
| p2(X94)
| p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| $false ) ) )
| ( ~ p3(X92)
& ~ p2(X92)
& ~ p1(X92)
& ? [X96] :
( r1(X92,X96)
& ~ p4(X96)
& ~ p3(X96)
& ~ p2(X96)
& ~ p1(X96)
& ? [X97] :
( r1(X96,X97)
& $true ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X98] :
( ~ r1(X0,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] :
( ~ r1(X98,X99)
| $false ) )
| ? [X100] :
( r1(X0,X100)
& ~ p2(X100)
& ~ p1(X100)
& ? [X101] :
( r1(X100,X101)
& ~ p4(X101)
& ~ p3(X101)
& ~ p2(X101)
& ~ p1(X101)
& ? [X102] :
( r1(X101,X102)
& $true ) )
& ! [X103] :
( ~ r1(X100,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| p4(X105)
| p3(X105)
| p2(X105)
| p1(X105)
| ! [X106] :
( ~ r1(X105,X106)
| $false ) ) )
| ( ~ p2(X103)
& ~ p1(X103)
& ? [X107] :
( r1(X103,X107)
& ~ p4(X107)
& ~ p3(X107)
& ~ p2(X107)
& ~ p1(X107)
& ? [X108] :
( r1(X107,X108)
& $true ) ) ) ) ) )
& ( p1(X0)
| ! [X109] :
( ~ r1(X0,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) )
| ? [X111] :
( r1(X0,X111)
& ~ p1(X111)
& ? [X112] :
( r1(X111,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] :
( r1(X112,X113)
& $true ) )
& ! [X114] :
( ~ r1(X111,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| p4(X116)
| p3(X116)
| p2(X116)
| p1(X116)
| ! [X117] :
( ~ r1(X116,X117)
| $false ) ) )
| ( ~ p1(X114)
& ? [X118] :
( r1(X114,X118)
& ~ p4(X118)
& ~ p3(X118)
& ~ p2(X118)
& ~ p1(X118)
& ? [X119] :
( r1(X118,X119)
& $true ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X120] :
( ~ r1(X0,X120)
| $false )
| ? [X121] :
( r1(X0,X121)
& ~ p4(X121)
& ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X122] :
( r1(X121,X122)
& $true )
& ! [X123] :
( ~ r1(X121,X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) )
| ( ~ p4(X123)
& ~ p3(X123)
& ~ p2(X123)
& ~ p1(X123)
& ? [X126] :
( r1(X123,X126)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X127] :
( ~ r1(X0,X127)
| $false )
| ? [X128] :
( r1(X0,X128)
& ~ p3(X128)
& ~ p2(X128)
& ~ p1(X128)
& ? [X129] :
( r1(X128,X129)
& $true )
& ! [X130] :
( ~ r1(X128,X130)
| ! [X131] :
( ~ r1(X130,X131)
| p3(X131)
| p2(X131)
| p1(X131)
| ! [X132] :
( ~ r1(X131,X132)
| $false ) )
| ( ~ p3(X130)
& ~ p2(X130)
& ~ p1(X130)
& ? [X133] :
( r1(X130,X133)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X134] :
( ~ r1(X0,X134)
| $false )
| ? [X135] :
( r1(X0,X135)
& ~ p2(X135)
& ~ p1(X135)
& ? [X136] :
( r1(X135,X136)
& $true )
& ! [X137] :
( ~ r1(X135,X137)
| ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| $false ) )
| ( ~ p2(X137)
& ~ p1(X137)
& ? [X140] :
( r1(X137,X140)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X141] :
( ~ r1(X0,X141)
| $false )
| ? [X142] :
( r1(X0,X142)
& ~ p1(X142)
& ? [X143] :
( r1(X142,X143)
& $true )
& ! [X144] :
( ~ r1(X142,X144)
| ! [X145] :
( ~ r1(X144,X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) )
| ( ~ p1(X144)
& ? [X147] :
( r1(X144,X147)
& $true ) ) ) ) )
& ! [X148] :
( ~ r1(X0,X148)
| p2(X148)
| ? [X149] :
( r1(X148,X149)
& ~ p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p2(X151) )
| ~ p2(X150) ) ) ) ),
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) ) ) ) ) )
& ( 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)
| $false ) ) )
| ? [X64] :
( r1(X0,X64)
& ~ p1(X64)
& ? [X65] :
( r1(X64,X65)
& ~ p4(X65)
& ~ p3(X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] :
( r1(X65,X66)
& ~ p4(X66)
& ~ p3(X66)
& ~ p2(X66)
& ~ p1(X66)
& ? [X67] :
( r1(X66,X67)
& $true ) ) )
& ! [X68] :
( ~ r1(X64,X68)
| ! [X69] :
( ~ r1(X68,X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| p4(X71)
| p3(X71)
| p2(X71)
| p1(X71)
| ! [X72] :
( ~ r1(X71,X72)
| $false ) ) ) )
| ( ~ p1(X68)
& ? [X73] :
( r1(X68,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)
& $true ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X76] :
( ~ r1(X0,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| $false ) )
| ? [X78] :
( r1(X0,X78)
& ~ p4(X78)
& ~ p3(X78)
& ~ p2(X78)
& ~ p1(X78)
& ? [X79] :
( r1(X78,X79)
& ~ p4(X79)
& ~ p3(X79)
& ~ p2(X79)
& ~ p1(X79)
& ? [X80] :
( r1(X79,X80)
& $true ) )
& ! [X81] :
( ~ r1(X78,X81)
| ! [X82] :
( ~ r1(X81,X82)
| p4(X82)
| p3(X82)
| p2(X82)
| p1(X82)
| ! [X83] :
( ~ r1(X82,X83)
| p4(X83)
| p3(X83)
| p2(X83)
| p1(X83)
| ! [X84] :
( ~ r1(X83,X84)
| $false ) ) )
| ( ~ p4(X81)
& ~ p3(X81)
& ~ p2(X81)
& ~ p1(X81)
& ? [X85] :
( r1(X81,X85)
& ~ p4(X85)
& ~ p3(X85)
& ~ p2(X85)
& ~ p1(X85)
& ? [X86] :
( r1(X85,X86)
& $true ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X87] :
( ~ r1(X0,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) )
| ? [X89] :
( r1(X0,X89)
& ~ p3(X89)
& ~ p2(X89)
& ~ p1(X89)
& ? [X90] :
( r1(X89,X90)
& ~ p4(X90)
& ~ p3(X90)
& ~ p2(X90)
& ~ p1(X90)
& ? [X91] :
( r1(X90,X91)
& $true ) )
& ! [X92] :
( ~ r1(X89,X92)
| ! [X93] :
( ~ r1(X92,X93)
| p3(X93)
| p2(X93)
| p1(X93)
| ! [X94] :
( ~ r1(X93,X94)
| p4(X94)
| p3(X94)
| p2(X94)
| p1(X94)
| ! [X95] :
( ~ r1(X94,X95)
| $false ) ) )
| ( ~ p3(X92)
& ~ p2(X92)
& ~ p1(X92)
& ? [X96] :
( r1(X92,X96)
& ~ p4(X96)
& ~ p3(X96)
& ~ p2(X96)
& ~ p1(X96)
& ? [X97] :
( r1(X96,X97)
& $true ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X98] :
( ~ r1(X0,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] :
( ~ r1(X98,X99)
| $false ) )
| ? [X100] :
( r1(X0,X100)
& ~ p2(X100)
& ~ p1(X100)
& ? [X101] :
( r1(X100,X101)
& ~ p4(X101)
& ~ p3(X101)
& ~ p2(X101)
& ~ p1(X101)
& ? [X102] :
( r1(X101,X102)
& $true ) )
& ! [X103] :
( ~ r1(X100,X103)
| ! [X104] :
( ~ r1(X103,X104)
| p2(X104)
| p1(X104)
| ! [X105] :
( ~ r1(X104,X105)
| p4(X105)
| p3(X105)
| p2(X105)
| p1(X105)
| ! [X106] :
( ~ r1(X105,X106)
| $false ) ) )
| ( ~ p2(X103)
& ~ p1(X103)
& ? [X107] :
( r1(X103,X107)
& ~ p4(X107)
& ~ p3(X107)
& ~ p2(X107)
& ~ p1(X107)
& ? [X108] :
( r1(X107,X108)
& $true ) ) ) ) ) )
& ( p1(X0)
| ! [X109] :
( ~ r1(X0,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) )
| ? [X111] :
( r1(X0,X111)
& ~ p1(X111)
& ? [X112] :
( r1(X111,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] :
( r1(X112,X113)
& $true ) )
& ! [X114] :
( ~ r1(X111,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| p4(X116)
| p3(X116)
| p2(X116)
| p1(X116)
| ! [X117] :
( ~ r1(X116,X117)
| $false ) ) )
| ( ~ p1(X114)
& ? [X118] :
( r1(X114,X118)
& ~ p4(X118)
& ~ p3(X118)
& ~ p2(X118)
& ~ p1(X118)
& ? [X119] :
( r1(X118,X119)
& $true ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X120] :
( ~ r1(X0,X120)
| $false )
| ? [X121] :
( r1(X0,X121)
& ~ p4(X121)
& ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X122] :
( r1(X121,X122)
& $true )
& ! [X123] :
( ~ r1(X121,X123)
| ! [X124] :
( ~ r1(X123,X124)
| p4(X124)
| p3(X124)
| p2(X124)
| p1(X124)
| ! [X125] :
( ~ r1(X124,X125)
| $false ) )
| ( ~ p4(X123)
& ~ p3(X123)
& ~ p2(X123)
& ~ p1(X123)
& ? [X126] :
( r1(X123,X126)
& $true ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X127] :
( ~ r1(X0,X127)
| $false )
| ? [X128] :
( r1(X0,X128)
& ~ p3(X128)
& ~ p2(X128)
& ~ p1(X128)
& ? [X129] :
( r1(X128,X129)
& $true )
& ! [X130] :
( ~ r1(X128,X130)
| ! [X131] :
( ~ r1(X130,X131)
| p3(X131)
| p2(X131)
| p1(X131)
| ! [X132] :
( ~ r1(X131,X132)
| $false ) )
| ( ~ p3(X130)
& ~ p2(X130)
& ~ p1(X130)
& ? [X133] :
( r1(X130,X133)
& $true ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X134] :
( ~ r1(X0,X134)
| $false )
| ? [X135] :
( r1(X0,X135)
& ~ p2(X135)
& ~ p1(X135)
& ? [X136] :
( r1(X135,X136)
& $true )
& ! [X137] :
( ~ r1(X135,X137)
| ! [X138] :
( ~ r1(X137,X138)
| p2(X138)
| p1(X138)
| ! [X139] :
( ~ r1(X138,X139)
| $false ) )
| ( ~ p2(X137)
& ~ p1(X137)
& ? [X140] :
( r1(X137,X140)
& $true ) ) ) ) )
& ( p1(X0)
| ! [X141] :
( ~ r1(X0,X141)
| $false )
| ? [X142] :
( r1(X0,X142)
& ~ p1(X142)
& ? [X143] :
( r1(X142,X143)
& $true )
& ! [X144] :
( ~ r1(X142,X144)
| ! [X145] :
( ~ r1(X144,X145)
| p1(X145)
| ! [X146] :
( ~ r1(X145,X146)
| $false ) )
| ( ~ p1(X144)
& ? [X147] :
( r1(X144,X147)
& $true ) ) ) ) )
& ! [X148] :
( ~ r1(X0,X148)
| p2(X148)
| ? [X149] :
( r1(X148,X149)
& ~ p2(X149)
& ! [X150] :
( ~ r1(X149,X150)
| ! [X151] :
( ~ r1(X150,X151)
| p2(X151) )
| ~ p2(X150) ) ) ) ),
inference(flattening,[],[f9]) ).
fof(f12,plain,
! [X2,X0,X1] :
( ~ r1(X1,X2)
| ~ r1(X0,X1)
| r1(X0,X2) ),
inference(cnf_transformation,[],[f8]) ).
fof(f111,plain,
! [X5] :
( ~ p2(sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f112,plain,
! [X5] :
( r1(sK41(X5),sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f113,plain,
! [X5] :
( ~ p2(sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f114,plain,
! [X5] :
( r1(sK41(X5),sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f117,plain,
! [X3,X5] :
( ~ p2(sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f118,plain,
! [X3,X5] :
( r1(sK41(X5),sK64(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f119,plain,
! [X15,X12] :
( ~ p2(sK63(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f120,plain,
! [X15,X12] :
( r1(sK39(X15),sK63(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f121,plain,
! [X15,X12] :
( ~ p2(sK63(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f122,plain,
! [X15,X12] :
( r1(sK39(X15),sK63(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f134,plain,
! [X150,X151,X148] :
( ~ p2(X150)
| p2(X151)
| ~ r1(X150,X151)
| ~ r1(sK14(X148),X150)
| p2(X148)
| ~ r1(sK0,X148) ),
inference(cnf_transformation,[],[f10]) ).
fof(f135,plain,
! [X3] :
( ~ p2(sK18)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f136,plain,
! [X3] :
( r1(sK0,sK18)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f137,plain,
! [X3,X5] :
( r1(X5,sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f138,plain,
! [X3,X5] :
( p2(sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| ~ p5(X3)
| ~ r1(sK31,X3) ),
inference(cnf_transformation,[],[f10]) ).
fof(f173,plain,
! [X5] :
( p2(sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f174,plain,
! [X5] :
( r1(X5,sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f175,plain,
! [X5] :
( p2(sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f176,plain,
! [X5] :
( r1(X5,sK41(X5))
| p2(X5)
| ~ r1(sK0,X5)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f179,plain,
! [X15,X12] :
( p2(sK39(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f180,plain,
! [X15,X12] :
( r1(X15,sK39(X15))
| p2(X15)
| ~ r1(sK0,X15)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f181,plain,
! [X15,X12] :
( p2(sK39(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f182,plain,
! [X15,X12] :
( r1(X15,sK39(X15))
| p2(X15)
| ~ r1(sK0,X15)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f189,plain,
( r1(sK0,sK18)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f190,plain,
( ~ p2(sK18)
| r1(sK13,sK31) ),
inference(cnf_transformation,[],[f10]) ).
fof(f191,plain,
! [X12] :
( r1(sK0,sK16)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f192,plain,
! [X12] :
( r1(sK0,sK16)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f193,plain,
! [X12] :
( ~ p2(sK16)
| p5(sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f194,plain,
! [X12] :
( ~ p2(sK16)
| r1(X12,sK30(X12))
| ~ r1(sK0,X12) ),
inference(cnf_transformation,[],[f10]) ).
fof(f244,plain,
( ~ p2(sK18)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f245,plain,
( r1(sK0,sK18)
| r1(sK0,sK13) ),
inference(cnf_transformation,[],[f10]) ).
fof(f266,plain,
! [X148] :
( ~ p2(sK14(X148))
| p2(X148)
| ~ r1(sK0,X148) ),
inference(cnf_transformation,[],[f10]) ).
fof(f267,plain,
! [X148] :
( r1(X148,sK14(X148))
| p2(X148)
| ~ r1(sK0,X148) ),
inference(cnf_transformation,[],[f10]) ).
fof(f289,plain,
! [X2,X0,X1] :
( ~ r1(X0,X2)
| r1(X0,X1)
| r1(X1,X2) ),
inference(consistent_polarity_flipping,[],[f12]) ).
fof(f310,plain,
! [X148] :
( ~ r1(X148,sK14(X148))
| p2(X148)
| r1(sK0,X148) ),
inference(consistent_polarity_flipping,[],[f267]) ).
fof(f311,plain,
! [X148] :
( ~ p2(sK14(X148))
| p2(X148)
| r1(sK0,X148) ),
inference(consistent_polarity_flipping,[],[f266]) ).
fof(f332,plain,
( ~ r1(sK0,sK18)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f245]) ).
fof(f333,plain,
( ~ p2(sK18)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f244]) ).
fof(f381,plain,
! [X12] :
( ~ p2(sK16)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f194]) ).
fof(f382,plain,
! [X12] :
( ~ p2(sK16)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f193]) ).
fof(f383,plain,
! [X12] :
( ~ r1(sK0,sK16)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f192]) ).
fof(f384,plain,
! [X12] :
( ~ r1(sK0,sK16)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f191]) ).
fof(f385,plain,
( ~ p2(sK18)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f190]) ).
fof(f386,plain,
( ~ r1(sK0,sK18)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f189]) ).
fof(f393,plain,
! [X15,X12] :
( ~ r1(X15,sK39(X15))
| p2(X15)
| r1(sK0,X15)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f182]) ).
fof(f394,plain,
! [X15,X12] :
( p2(sK39(X15))
| p2(X15)
| r1(sK0,X15)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f181]) ).
fof(f395,plain,
! [X15,X12] :
( ~ r1(X15,sK39(X15))
| p2(X15)
| r1(sK0,X15)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f180]) ).
fof(f396,plain,
! [X15,X12] :
( p2(sK39(X15))
| p2(X15)
| r1(sK0,X15)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f179]) ).
fof(f399,plain,
! [X5] :
( ~ r1(X5,sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f176]) ).
fof(f400,plain,
! [X5] :
( p2(sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f175]) ).
fof(f401,plain,
! [X5] :
( ~ r1(X5,sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f174]) ).
fof(f402,plain,
! [X5] :
( p2(sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f173]) ).
fof(f436,plain,
! [X3,X5] :
( p2(sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f138]) ).
fof(f437,plain,
! [X3,X5] :
( ~ r1(X5,sK41(X5))
| p2(X5)
| r1(sK0,X5)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f137]) ).
fof(f438,plain,
! [X3] :
( ~ r1(sK0,sK18)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f136]) ).
fof(f439,plain,
! [X3] :
( ~ p2(sK18)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f135]) ).
fof(f440,plain,
! [X150,X151,X148] :
( ~ p2(X150)
| p2(X151)
| r1(X150,X151)
| r1(sK14(X148),X150)
| p2(X148)
| r1(sK0,X148) ),
inference(consistent_polarity_flipping,[],[f134]) ).
fof(f452,plain,
! [X15,X12] :
( ~ r1(sK39(X15),sK63(X15))
| p2(X15)
| r1(sK0,X15)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f453,plain,
! [X15,X12] :
( ~ p2(sK63(X15))
| p2(X15)
| r1(sK0,X15)
| ~ r1(X12,sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f454,plain,
! [X15,X12] :
( ~ r1(sK39(X15),sK63(X15))
| p2(X15)
| r1(sK0,X15)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f455,plain,
! [X15,X12] :
( ~ p2(sK63(X15))
| p2(X15)
| r1(sK0,X15)
| p5(sK30(X12))
| r1(sK0,X12) ),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f456,plain,
! [X3,X5] :
( ~ r1(sK41(X5),sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f457,plain,
! [X3,X5] :
( ~ p2(sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ p5(X3)
| r1(sK31,X3) ),
inference(consistent_polarity_flipping,[],[f117]) ).
fof(f460,plain,
! [X5] :
( ~ r1(sK41(X5),sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f461,plain,
! [X5] :
( ~ p2(sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK0,sK13) ),
inference(consistent_polarity_flipping,[],[f113]) ).
fof(f462,plain,
! [X5] :
( ~ r1(sK41(X5),sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f463,plain,
! [X5] :
( ~ p2(sK64(X5))
| p2(X5)
| r1(sK0,X5)
| ~ r1(sK13,sK31) ),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f841,definition,
( spl90_70
<=> r1(sK13,sK31) ),
introduced(definition,[new_symbols(definition,[spl90_70])],[avatar_definition]) ).
fof(f843,plain,
( ~ r1(sK13,sK31)
| spl90_70 ),
inference(avatar_component_clause,[],[f841]) ).
fof(f845,definition,
( spl90_71
<=> ! [X5] :
( ~ p2(sK64(X5))
| r1(sK0,X5)
| p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl90_71])],[avatar_definition]) ).
fof(f846,plain,
( ! [X5] :
( ~ p2(sK64(X5))
| r1(sK0,X5)
| p2(X5) )
| ~ spl90_71 ),
inference(avatar_component_clause,[],[f845]) ).
fof(f847,plain,
( ~ spl90_70
| spl90_71 ),
inference(avatar_split_clause,[],[f463,f845,f841]) ).
fof(f849,definition,
( spl90_72
<=> ! [X5] :
( ~ r1(sK41(X5),sK64(X5))
| r1(sK0,X5)
| p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl90_72])],[avatar_definition]) ).
fof(f850,plain,
( ! [X5] :
( ~ r1(sK41(X5),sK64(X5))
| r1(sK0,X5)
| p2(X5) )
| ~ spl90_72 ),
inference(avatar_component_clause,[],[f849]) ).
fof(f851,plain,
( ~ spl90_70
| spl90_72 ),
inference(avatar_split_clause,[],[f462,f849,f841]) ).
fof(f853,definition,
( spl90_73
<=> r1(sK0,sK13) ),
introduced(definition,[new_symbols(definition,[spl90_73])],[avatar_definition]) ).
fof(f855,plain,
( ~ r1(sK0,sK13)
| spl90_73 ),
inference(avatar_component_clause,[],[f853]) ).
fof(f856,plain,
( ~ spl90_73
| spl90_71 ),
inference(avatar_split_clause,[],[f461,f845,f853]) ).
fof(f857,plain,
( ~ spl90_73
| spl90_72 ),
inference(avatar_split_clause,[],[f460,f849,f853]) ).
fof(f865,definition,
( spl90_75
<=> ! [X3] :
( ~ p5(X3)
| r1(sK31,X3) ) ),
introduced(definition,[new_symbols(definition,[spl90_75])],[avatar_definition]) ).
fof(f866,plain,
( ! [X3] :
( r1(sK31,X3)
| ~ p5(X3) )
| ~ spl90_75 ),
inference(avatar_component_clause,[],[f865]) ).
fof(f867,plain,
( spl90_75
| spl90_71 ),
inference(avatar_split_clause,[],[f457,f845,f865]) ).
fof(f868,plain,
( spl90_75
| spl90_72 ),
inference(avatar_split_clause,[],[f456,f849,f865]) ).
fof(f870,definition,
( spl90_76
<=> ! [X12] :
( p5(sK30(X12))
| r1(sK0,X12) ) ),
introduced(definition,[new_symbols(definition,[spl90_76])],[avatar_definition]) ).
fof(f871,plain,
( ! [X12] :
( p5(sK30(X12))
| r1(sK0,X12) )
| ~ spl90_76 ),
inference(avatar_component_clause,[],[f870]) ).
fof(f873,definition,
( spl90_77
<=> ! [X15] :
( ~ p2(sK63(X15))
| r1(sK0,X15)
| p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl90_77])],[avatar_definition]) ).
fof(f874,plain,
( ! [X15] :
( ~ p2(sK63(X15))
| r1(sK0,X15)
| p2(X15) )
| ~ spl90_77 ),
inference(avatar_component_clause,[],[f873]) ).
fof(f875,plain,
( spl90_76
| spl90_77 ),
inference(avatar_split_clause,[],[f455,f873,f870]) ).
fof(f877,definition,
( spl90_78
<=> ! [X15] :
( ~ r1(sK39(X15),sK63(X15))
| r1(sK0,X15)
| p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl90_78])],[avatar_definition]) ).
fof(f878,plain,
( ! [X15] :
( ~ r1(sK39(X15),sK63(X15))
| r1(sK0,X15)
| p2(X15) )
| ~ spl90_78 ),
inference(avatar_component_clause,[],[f877]) ).
fof(f879,plain,
( spl90_76
| spl90_78 ),
inference(avatar_split_clause,[],[f454,f877,f870]) ).
fof(f881,definition,
( spl90_79
<=> ! [X12] :
( ~ r1(X12,sK30(X12))
| r1(sK0,X12) ) ),
introduced(definition,[new_symbols(definition,[spl90_79])],[avatar_definition]) ).
fof(f882,plain,
( ! [X12] :
( ~ r1(X12,sK30(X12))
| r1(sK0,X12) )
| ~ spl90_79 ),
inference(avatar_component_clause,[],[f881]) ).
fof(f883,plain,
( spl90_79
| spl90_77 ),
inference(avatar_split_clause,[],[f453,f873,f881]) ).
fof(f884,plain,
( spl90_79
| spl90_78 ),
inference(avatar_split_clause,[],[f452,f877,f881]) ).
fof(f926,definition,
( spl90_90
<=> p2(sK18) ),
introduced(definition,[new_symbols(definition,[spl90_90])],[avatar_definition]) ).
fof(f928,plain,
( ~ p2(sK18)
| spl90_90 ),
inference(avatar_component_clause,[],[f926]) ).
fof(f929,plain,
( spl90_75
| ~ spl90_90 ),
inference(avatar_split_clause,[],[f439,f926,f865]) ).
fof(f931,definition,
( spl90_91
<=> r1(sK0,sK18) ),
introduced(definition,[new_symbols(definition,[spl90_91])],[avatar_definition]) ).
fof(f933,plain,
( ~ r1(sK0,sK18)
| spl90_91 ),
inference(avatar_component_clause,[],[f931]) ).
fof(f934,plain,
( spl90_75
| ~ spl90_91 ),
inference(avatar_split_clause,[],[f438,f931,f865]) ).
fof(f936,definition,
( spl90_92
<=> ! [X5] :
( ~ r1(X5,sK41(X5))
| r1(sK0,X5)
| p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl90_92])],[avatar_definition]) ).
fof(f937,plain,
( ! [X5] :
( ~ r1(X5,sK41(X5))
| r1(sK0,X5)
| p2(X5) )
| ~ spl90_92 ),
inference(avatar_component_clause,[],[f936]) ).
fof(f938,plain,
( spl90_75
| spl90_92 ),
inference(avatar_split_clause,[],[f437,f936,f865]) ).
fof(f940,definition,
( spl90_93
<=> ! [X5] :
( p2(sK41(X5))
| r1(sK0,X5)
| p2(X5) ) ),
introduced(definition,[new_symbols(definition,[spl90_93])],[avatar_definition]) ).
fof(f941,plain,
( ! [X5] :
( p2(sK41(X5))
| r1(sK0,X5)
| p2(X5) )
| ~ spl90_93 ),
inference(avatar_component_clause,[],[f940]) ).
fof(f942,plain,
( spl90_75
| spl90_93 ),
inference(avatar_split_clause,[],[f436,f940,f865]) ).
fof(f1030,plain,
( ~ spl90_73
| spl90_93 ),
inference(avatar_split_clause,[],[f402,f940,f853]) ).
fof(f1031,plain,
( ~ spl90_73
| spl90_92 ),
inference(avatar_split_clause,[],[f401,f936,f853]) ).
fof(f1032,plain,
( ~ spl90_70
| spl90_93 ),
inference(avatar_split_clause,[],[f400,f940,f841]) ).
fof(f1033,plain,
( ~ spl90_70
| spl90_92 ),
inference(avatar_split_clause,[],[f399,f936,f841]) ).
fof(f1035,definition,
( spl90_110
<=> ! [X15] :
( p2(sK39(X15))
| r1(sK0,X15)
| p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl90_110])],[avatar_definition]) ).
fof(f1036,plain,
( ! [X15] :
( p2(sK39(X15))
| r1(sK0,X15)
| p2(X15) )
| ~ spl90_110 ),
inference(avatar_component_clause,[],[f1035]) ).
fof(f1037,plain,
( spl90_79
| spl90_110 ),
inference(avatar_split_clause,[],[f396,f1035,f881]) ).
fof(f1039,definition,
( spl90_111
<=> ! [X15] :
( ~ r1(X15,sK39(X15))
| r1(sK0,X15)
| p2(X15) ) ),
introduced(definition,[new_symbols(definition,[spl90_111])],[avatar_definition]) ).
fof(f1040,plain,
( ! [X15] :
( ~ r1(X15,sK39(X15))
| r1(sK0,X15)
| p2(X15) )
| ~ spl90_111 ),
inference(avatar_component_clause,[],[f1039]) ).
fof(f1041,plain,
( spl90_79
| spl90_111 ),
inference(avatar_split_clause,[],[f395,f1039,f881]) ).
fof(f1042,plain,
( spl90_76
| spl90_110 ),
inference(avatar_split_clause,[],[f394,f1035,f870]) ).
fof(f1043,plain,
( spl90_76
| spl90_111 ),
inference(avatar_split_clause,[],[f393,f1039,f870]) ).
fof(f1048,plain,
( ~ spl90_70
| ~ spl90_91 ),
inference(avatar_split_clause,[],[f386,f931,f841]) ).
fof(f1049,plain,
( ~ spl90_70
| ~ spl90_90 ),
inference(avatar_split_clause,[],[f385,f926,f841]) ).
fof(f1051,definition,
( spl90_112
<=> r1(sK0,sK16) ),
introduced(definition,[new_symbols(definition,[spl90_112])],[avatar_definition]) ).
fof(f1053,plain,
( ~ r1(sK0,sK16)
| spl90_112 ),
inference(avatar_component_clause,[],[f1051]) ).
fof(f1054,plain,
( spl90_76
| ~ spl90_112 ),
inference(avatar_split_clause,[],[f384,f1051,f870]) ).
fof(f1055,plain,
( spl90_79
| ~ spl90_112 ),
inference(avatar_split_clause,[],[f383,f1051,f881]) ).
fof(f1057,definition,
( spl90_113
<=> p2(sK16) ),
introduced(definition,[new_symbols(definition,[spl90_113])],[avatar_definition]) ).
fof(f1059,plain,
( ~ p2(sK16)
| spl90_113 ),
inference(avatar_component_clause,[],[f1057]) ).
fof(f1060,plain,
( spl90_76
| ~ spl90_113 ),
inference(avatar_split_clause,[],[f382,f1057,f870]) ).
fof(f1061,plain,
( spl90_79
| ~ spl90_113 ),
inference(avatar_split_clause,[],[f381,f1057,f881]) ).
fof(f1227,plain,
( ~ spl90_73
| ~ spl90_90 ),
inference(avatar_split_clause,[],[f333,f926,f853]) ).
fof(f1228,plain,
( ~ spl90_73
| ~ spl90_91 ),
inference(avatar_split_clause,[],[f332,f931,f853]) ).
fof(f1386,plain,
( r1(sK0,sK31)
| ~ p5(sK30(sK31))
| ~ spl90_75
| ~ spl90_79 ),
inference(resolution,[],[f882,f866]) ).
fof(f1387,plain,
( r1(sK0,sK31)
| ~ spl90_75
| ~ spl90_76
| ~ spl90_79 ),
inference(forward_subsumption_resolution,[],[f1386,f871]) ).
fof(f1425,definition,
( spl90_177
<=> ! [X0] :
( p2(X0)
| r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl90_177])],[avatar_definition]) ).
fof(f1426,plain,
( ! [X0] :
( r1(sK0,X0)
| p2(X0) )
| ~ spl90_177 ),
inference(avatar_component_clause,[],[f1425]) ).
fof(f1483,definition,
( spl90_181
<=> ! [X0] :
( r1(X0,sK31)
| r1(sK0,X0) ) ),
introduced(definition,[new_symbols(definition,[spl90_181])],[avatar_definition]) ).
fof(f1484,plain,
( ! [X0] :
( r1(X0,sK31)
| r1(sK0,X0) )
| ~ spl90_181 ),
inference(avatar_component_clause,[],[f1483]) ).
fof(f1572,plain,
( ! [X2,X0,X1] :
( r1(sK41(X0),X1)
| r1(sK14(X2),sK41(X0))
| p2(X1)
| r1(sK0,X0)
| p2(X0)
| p2(X2)
| r1(sK0,X2) )
| ~ spl90_93 ),
inference(resolution,[],[f941,f440]) ).
fof(f1621,plain,
( ! [X0] :
( r1(sK0,X0)
| r1(X0,sK31) )
| ~ spl90_75
| ~ spl90_76
| ~ spl90_79 ),
inference(resolution,[],[f289,f1387]) ).
fof(f1622,plain,
( spl90_181
| ~ spl90_75
| ~ spl90_76
| ~ spl90_79 ),
inference(avatar_split_clause,[],[f1621,f881,f870,f865,f1483]) ).
fof(f1668,plain,
( r1(sK0,sK13)
| spl90_70
| ~ spl90_181 ),
inference(resolution,[],[f1484,f843]) ).
fof(f1670,plain,
( $false
| spl90_70
| spl90_73
| ~ spl90_181 ),
inference(forward_subsumption_resolution,[],[f1668,f855]) ).
fof(f1671,plain,
( spl90_70
| spl90_73
| ~ spl90_181 ),
inference(avatar_contradiction_clause,[],[f1670]) ).
fof(f1923,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK41(X0))
| p2(sK64(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1)
| r1(sK0,X0)
| p2(X0) )
| ~ spl90_72
| ~ spl90_93 ),
inference(resolution,[],[f1572,f850]) ).
fof(f1934,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK41(X0))
| p2(sK64(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1) )
| ~ spl90_72
| ~ spl90_93 ),
inference(duplicate_literal_removal,[],[f1923]) ).
fof(f1936,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK41(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_93 ),
inference(forward_subsumption_resolution,[],[f1934,f846]) ).
fof(f2259,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(sK14(X0))
| p2(X0)
| r1(sK0,X0)
| r1(sK0,sK14(X0))
| p2(sK14(X0)) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(resolution,[],[f1936,f937]) ).
fof(f2261,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(sK14(X0))
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(duplicate_literal_removal,[],[f2259]) ).
fof(f2262,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(forward_subsumption_resolution,[],[f2261,f311]) ).
fof(f3477,plain,
( ! [X2,X0,X1] :
( r1(sK39(X0),X1)
| r1(sK14(X2),sK39(X0))
| p2(X1)
| r1(sK0,X0)
| p2(X0)
| p2(X2)
| r1(sK0,X2) )
| ~ spl90_110 ),
inference(resolution,[],[f1036,f440]) ).
fof(f3638,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK39(X0))
| p2(sK63(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1)
| r1(sK0,X0)
| p2(X0) )
| ~ spl90_78
| ~ spl90_110 ),
inference(resolution,[],[f3477,f878]) ).
fof(f3649,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK39(X0))
| p2(sK63(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1) )
| ~ spl90_78
| ~ spl90_110 ),
inference(duplicate_literal_removal,[],[f3638]) ).
fof(f3651,plain,
( ! [X0,X1] :
( r1(sK14(X1),sK39(X0))
| r1(sK0,X0)
| p2(X0)
| p2(X1)
| r1(sK0,X1) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110 ),
inference(forward_subsumption_resolution,[],[f3649,f874]) ).
fof(f3717,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(sK14(X0))
| p2(X0)
| r1(sK0,X0)
| r1(sK0,sK14(X0))
| p2(sK14(X0)) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(resolution,[],[f3651,f1040]) ).
fof(f3719,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(sK14(X0))
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(duplicate_literal_removal,[],[f3717]) ).
fof(f3720,plain,
( ! [X0] :
( r1(sK0,sK14(X0))
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(forward_subsumption_resolution,[],[f3719,f311]) ).
fof(f4560,plain,
( p2(sK16)
| spl90_112
| ~ spl90_177 ),
inference(resolution,[],[f1426,f1053]) ).
fof(f4561,plain,
( p2(sK18)
| spl90_91
| ~ spl90_177 ),
inference(resolution,[],[f1426,f933]) ).
fof(f4575,plain,
( $false
| spl90_90
| spl90_91
| ~ spl90_177 ),
inference(forward_subsumption_resolution,[],[f4561,f928]) ).
fof(f4576,plain,
( spl90_90
| spl90_91
| ~ spl90_177 ),
inference(avatar_contradiction_clause,[],[f4575]) ).
fof(f4577,plain,
( $false
| spl90_112
| spl90_113
| ~ spl90_177 ),
inference(forward_subsumption_resolution,[],[f4560,f1059]) ).
fof(f4578,plain,
( spl90_112
| spl90_113
| ~ spl90_177 ),
inference(avatar_contradiction_clause,[],[f4577]) ).
fof(f7944,plain,
( ! [X0,X1] :
( r1(X1,sK14(X0))
| r1(sK0,X0)
| r1(sK0,X1)
| p2(X0) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(resolution,[],[f2262,f289]) ).
fof(f40855,plain,
( ! [X0] :
( r1(sK0,X0)
| r1(sK0,X0)
| p2(X0)
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(resolution,[],[f7944,f310]) ).
fof(f40858,plain,
( ! [X0] :
( r1(sK0,X0)
| p2(X0) )
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(duplicate_literal_removal,[],[f40855]) ).
fof(f40859,plain,
( spl90_177
| ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93 ),
inference(avatar_split_clause,[],[f40858,f940,f936,f849,f845,f1425]) ).
fof(f41762,plain,
( ! [X0,X1] :
( r1(X1,sK14(X0))
| r1(sK0,X0)
| r1(sK0,X1)
| p2(X0) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(resolution,[],[f3720,f289]) ).
fof(f44592,plain,
( ! [X0] :
( r1(sK0,X0)
| r1(sK0,X0)
| p2(X0)
| p2(X0)
| r1(sK0,X0) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(resolution,[],[f41762,f310]) ).
fof(f44595,plain,
( ! [X0] :
( r1(sK0,X0)
| p2(X0) )
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(duplicate_literal_removal,[],[f44592]) ).
fof(f44596,plain,
( spl90_177
| ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111 ),
inference(avatar_split_clause,[],[f44595,f1039,f1035,f877,f873,f1425]) ).
cnf(s58,plain,
( ~ spl90_70
| spl90_71 ),
inference(sat_conversion,[],[f847]) ).
cnf(s59,plain,
( ~ spl90_70
| spl90_72 ),
inference(sat_conversion,[],[f851]) ).
cnf(s60,plain,
( spl90_71
| ~ spl90_73 ),
inference(sat_conversion,[],[f856]) ).
cnf(s61,plain,
( spl90_72
| ~ spl90_73 ),
inference(sat_conversion,[],[f857]) ).
cnf(s64,plain,
( spl90_71
| spl90_75 ),
inference(sat_conversion,[],[f867]) ).
cnf(s65,plain,
( spl90_72
| spl90_75 ),
inference(sat_conversion,[],[f868]) ).
cnf(s66,plain,
( spl90_76
| spl90_77 ),
inference(sat_conversion,[],[f875]) ).
cnf(s67,plain,
( spl90_76
| spl90_78 ),
inference(sat_conversion,[],[f879]) ).
cnf(s68,plain,
( spl90_77
| spl90_79 ),
inference(sat_conversion,[],[f883]) ).
cnf(s69,plain,
( spl90_78
| spl90_79 ),
inference(sat_conversion,[],[f884]) ).
cnf(s80,plain,
( spl90_75
| ~ spl90_90 ),
inference(sat_conversion,[],[f929]) ).
cnf(s81,plain,
( spl90_75
| ~ spl90_91 ),
inference(sat_conversion,[],[f934]) ).
cnf(s82,plain,
( spl90_75
| spl90_92 ),
inference(sat_conversion,[],[f938]) ).
cnf(s83,plain,
( spl90_75
| spl90_93 ),
inference(sat_conversion,[],[f942]) ).
cnf(s114,plain,
( ~ spl90_73
| spl90_93 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s115,plain,
( ~ spl90_73
| spl90_92 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s116,plain,
( ~ spl90_70
| spl90_93 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s117,plain,
( ~ spl90_70
| spl90_92 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s118,plain,
( spl90_79
| spl90_110 ),
inference(sat_conversion,[],[f1037]) ).
cnf(s119,plain,
( spl90_79
| spl90_111 ),
inference(sat_conversion,[],[f1041]) ).
cnf(s120,plain,
( spl90_76
| spl90_110 ),
inference(sat_conversion,[],[f1042]) ).
cnf(s121,plain,
( spl90_76
| spl90_111 ),
inference(sat_conversion,[],[f1043]) ).
cnf(s126,plain,
( ~ spl90_70
| ~ spl90_91 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s127,plain,
( ~ spl90_70
| ~ spl90_90 ),
inference(sat_conversion,[],[f1049]) ).
cnf(s128,plain,
( spl90_76
| ~ spl90_112 ),
inference(sat_conversion,[],[f1054]) ).
cnf(s129,plain,
( spl90_79
| ~ spl90_112 ),
inference(sat_conversion,[],[f1055]) ).
cnf(s130,plain,
( spl90_76
| ~ spl90_113 ),
inference(sat_conversion,[],[f1060]) ).
cnf(s131,plain,
( spl90_79
| ~ spl90_113 ),
inference(sat_conversion,[],[f1061]) ).
cnf(s181,plain,
( ~ spl90_73
| ~ spl90_90 ),
inference(sat_conversion,[],[f1227]) ).
cnf(s182,plain,
( ~ spl90_73
| ~ spl90_91 ),
inference(sat_conversion,[],[f1228]) ).
cnf(s231,plain,
( ~ spl90_75
| ~ spl90_76
| ~ spl90_79
| spl90_181 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s232,plain,
( spl90_70
| spl90_73
| ~ spl90_181 ),
inference(sat_conversion,[],[f1671]) ).
cnf(s389,plain,
( spl90_90
| spl90_91
| ~ spl90_177 ),
inference(sat_conversion,[],[f4576]) ).
cnf(s390,plain,
( spl90_112
| spl90_113
| ~ spl90_177 ),
inference(sat_conversion,[],[f4578]) ).
cnf(s2748,plain,
( ~ spl90_71
| ~ spl90_72
| ~ spl90_92
| ~ spl90_93
| spl90_177 ),
inference(sat_conversion,[],[f40859]) ).
cnf(s3096,plain,
( ~ spl90_77
| ~ spl90_78
| ~ spl90_110
| ~ spl90_111
| spl90_177 ),
inference(sat_conversion,[],[f44596]) ).
cnf(s3131,plain,
( spl90_76
| spl90_177 ),
inference(rat,[],[s3096,s66,s67,s120,s121]) ).
cnf(s3132,plain,
( spl90_79
| spl90_177 ),
inference(rat,[],[s3096,s68,s69,s118,s119]) ).
cnf(s3133,plain,
( spl90_71
| spl90_70
| spl90_177 ),
inference(rat,[],[s232,s231,s60,s64,s3131,s3132]) ).
cnf(s3134,plain,
( spl90_75
| ~ spl90_71
| spl90_177 ),
inference(rat,[],[s2748,s65,s82,s83]) ).
cnf(s3135,plain,
( spl90_70
| spl90_177 ),
inference(rat,[],[s2748,s61,s114,s115,s232,s231,s3134,s3133,s3131,s3132]) ).
cnf(s3136,plain,
spl90_177,
inference(rat,[],[s2748,s58,s59,s116,s117,s3135]) ).
cnf(s3139,plain,
spl90_76,
inference(rat,[],[s390,s128,s130,s3136]) ).
cnf(s3140,plain,
spl90_79,
inference(rat,[],[s390,s129,s131,s3136]) ).
cnf(s3144,plain,
~ spl90_73,
inference(rat,[],[s389,s181,s182,s3136]) ).
cnf(s3147,plain,
~ spl90_70,
inference(rat,[],[s389,s126,s127,s3136]) ).
cnf(s3149,plain,
~ spl90_181,
inference(rat,[],[s232,s3144,s3147]) ).
cnf(s3151,plain,
~ spl90_75,
inference(rat,[],[s231,s3140,s3139,s3149]) ).
cnf(s3154,plain,
~ spl90_91,
inference(rat,[],[s81,s3151]) ).
cnf(s3155,plain,
~ spl90_90,
inference(rat,[],[s80,s3151]) ).
cnf(s3157,plain,
$false,
inference(rat,[],[s389,s3136,s3155,s3154]) ).
fof(f44597,plain,
$false,
inference(avatar_sat_refutation,[],[s3157]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL676+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.38 % Computer : n009.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sun Sep 27 16:33:15 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.41 Running first-order model finding
% 0.10/0.41 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.45/2.64 % (2233202)Will run a generic schedule for satisfiability detection.
% 15.45/2.64 % (2233213)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=366036707:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.45/2.64 % (2233208)% WARNING: option uhcvi not known.
% 15.45/2.64 % (2233207)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=739727754_2999 on theBenchmark for (2999ds/0Mi)
% 15.45/2.64 % (2233208)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1488517394:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.45/2.64 % (2233212)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4244477384:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.45/2.64 % (2233209)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3830863680:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.45/2.64 % (2233210)dis+10_1_sil=32000:sp=arity:random_seed=2957064777:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.45/2.64 % (2233211)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=753618087:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.45/2.64 % TRYING [1]
% 15.45/2.64 % TRYING [2]
% 15.45/2.64 % TRYING [3]
% 15.45/2.64 % (2233213)Instruction limit reached!
% 15.45/2.64 % (2233213)------------------------------
% 15.45/2.64 % (2233213)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.64 % (2233213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.64 % (2233213)CaDiCaL version: 2.1.3
% 15.45/2.64 % (2233213)Termination reason: Instruction limit
% 15.45/2.64 % (2233213)Termination phase: Saturation
% 15.45/2.64 % (2233213)Time elapsed: 0.047 s
% 15.45/2.64 % (2233213)Peak memory usage: 14 MB
% 15.45/2.64 % (2233213)Instructions burned: 163 (million)
% 15.45/2.64 % TRYING [4]
% 15.45/2.64 % (2233221)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2229549996:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.45/2.64 % (2233210)Instruction limit reached!
% 15.45/2.64 % (2233210)------------------------------
% 15.45/2.64 % (2233210)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.64 % (2233210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.64 % (2233210)CaDiCaL version: 2.1.3
% 15.45/2.64 % (2233210)Termination reason: Instruction limit
% 15.45/2.64 % (2233210)Termination phase: Saturation
% 15.45/2.64 % (2233210)Time elapsed: 0.056 s
% 15.45/2.64 % (2233210)Peak memory usage: 13 MB
% 15.45/2.64 % (2233210)Instructions burned: 104 (million)
% 15.45/2.64 % TRYING [1]
% 15.45/2.64 % TRYING [2]
% 15.45/2.64 % TRYING [3]
% 15.45/2.64 % (2233211)Instruction limit reached!
% 15.45/2.64 % (2233211)------------------------------
% 15.45/2.64 % (2233211)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.64 % (2233211)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.64 % (2233211)CaDiCaL version: 2.1.3
% 15.45/2.64 % (2233211)Termination reason: Instruction limit
% 15.45/2.64 % (2233211)Termination phase: Saturation
% 15.45/2.64 % (2233211)Time elapsed: 0.063 s
% 15.45/2.64 % (2233211)Peak memory usage: 13 MB
% 15.45/2.64 % (2233211)Instructions burned: 116 (million)
% 15.45/2.64 % TRYING [5]
% 15.45/2.64 % TRYING [4]
% 15.45/2.64 % (2233223)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1871192396:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.45/2.64 % TRYING [5]
% 15.45/2.64 % (2233224)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=991534298:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.45/2.64 % (2233212)Instruction limit reached!
% 15.45/2.64 % (2233212)------------------------------
% 15.45/2.64 % (2233212)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.45/2.64 % (2233212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.45/2.64 % (2233212)CaDiCaL version: 2.1.3
% 15.45/2.64 % (2233212)Termination reason: Instruction limit
% 15.45/2.64 % (2233212)Termination phase: Saturation
% 15.45/2.64 % (2233212)Time elapsed: 0.083 s
% 15.45/2.64 % (2233212)Peak memory usage: 15 MB
% 15.45/2.64 % (2233212)Instructions burned: 136 (million)
% 15.45/2.64 % (2233227)ott-21_1_sil=16000:fs=off:random_seed=3820412989:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.45/2.64 % TRYING [6]
% 15.45/2.64 % TRYING [6]
% 15.45/2.64 % (2233223)Instruction limit reached!
% 15.45/2.64 % (2233223)------------------------------
% 15.45/2.64 % (2233223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233223)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233223)Termination reason: Instruction limit
% 19.24/3.19 % (2233223)Termination phase: Saturation
% 19.24/3.19 % (2233223)Time elapsed: 0.078 s
% 19.24/3.19 % (2233223)Peak memory usage: 14 MB
% 19.24/3.19 % (2233223)Instructions burned: 133 (million)
% 19.24/3.19 % (2233229)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=614489479:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 19.24/3.19 % (2233227)Instruction limit reached!
% 19.24/3.19 % (2233227)------------------------------
% 19.24/3.19 % (2233227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233227)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233227)Termination reason: Instruction limit
% 19.24/3.19 % (2233227)Termination phase: Saturation
% 19.24/3.19 % (2233227)Time elapsed: 0.093 s
% 19.24/3.19 % (2233227)Peak memory usage: 15 MB
% 19.24/3.19 % (2233227)Instructions burned: 182 (million)
% 19.24/3.19 % (2233231)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3286616690:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 19.24/3.19 % TRYING [1]
% 19.24/3.19 % TRYING [2]
% 19.24/3.19 % TRYING [3]
% 19.24/3.19 % (2233221)Instruction limit reached!
% 19.24/3.19 % (2233221)------------------------------
% 19.24/3.19 % (2233221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233221)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233221)Termination reason: Instruction limit
% 19.24/3.19 % (2233221)Termination phase: Finite model building SAT solving
% 19.24/3.19 % (2233221)Time elapsed: 0.195 s
% 19.24/3.19 % (2233221)Peak memory usage: 19 MB
% 19.24/3.19 % (2233221)Instructions burned: 715 (million)
% 19.24/3.19 % (2233233)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3574385233:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 19.24/3.19 % TRYING [4]
% 19.24/3.19 % TRYING [5]
% 19.24/3.19 % TRYING [7]
% 19.24/3.19 % TRYING [6]
% 19.24/3.19 % (2233224)Instruction limit reached!
% 19.24/3.19 % (2233224)------------------------------
% 19.24/3.19 % (2233224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233224)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233224)Termination reason: Instruction limit
% 19.24/3.19 % (2233224)Termination phase: Saturation
% 19.24/3.19 % (2233224)Time elapsed: 0.340 s
% 19.24/3.19 % (2233224)Peak memory usage: 21 MB
% 19.24/3.19 % (2233224)Instructions burned: 685 (million)
% 19.24/3.19 % (2233235)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=359375543:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 19.24/3.19 % (2233229)Instruction limit reached!
% 19.24/3.19 % (2233229)------------------------------
% 19.24/3.19 % (2233229)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233229)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233229)Termination reason: Instruction limit
% 19.24/3.19 % (2233229)Termination phase: Saturation
% 19.24/3.19 % (2233229)Time elapsed: 0.281 s
% 19.24/3.19 % (2233229)Peak memory usage: 17 MB
% 19.24/3.19 % (2233229)Instructions burned: 477 (million)
% 19.24/3.19 % TRYING [14]
% 19.24/3.19 % (2233237)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=1771119859:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 19.24/3.19 % TRYING [7]
% 19.24/3.19 % (2233231)Instruction limit reached!
% 19.24/3.19 % (2233231)------------------------------
% 19.24/3.19 % (2233231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233231)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233231)Termination reason: Instruction limit
% 19.24/3.19 % (2233231)Termination phase: Finite model building SAT solving
% 19.24/3.19 % (2233231)Time elapsed: 0.357 s
% 19.24/3.19 % (2233231)Peak memory usage: 17 MB
% 19.24/3.19 % (2233231)Instructions burned: 866 (million)
% 19.24/3.19 % (2233233)Instruction limit reached!
% 19.24/3.19 % (2233233)------------------------------
% 19.24/3.19 % (2233233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233233)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233233)Termination reason: Instruction limit
% 19.24/3.19 % (2233233)Termination phase: Saturation
% 19.24/3.19 % (2233233)Time elapsed: 0.325 s
% 19.24/3.19 % (2233233)Peak memory usage: 20 MB
% 19.24/3.19 % (2233233)Instructions burned: 1181 (million)
% 19.24/3.19 % (2233239)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3190392723:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 19.24/3.19 % (2233240)fmb+10_1_sil=64000:random_seed=3396084578:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 19.24/3.19 % TRYING [1]
% 19.24/3.19 % TRYING [2]
% 19.24/3.19 % TRYING [3]
% 19.24/3.19 % TRYING [4]
% 19.24/3.19 % TRYING [5]
% 19.24/3.19 % TRYING [6]
% 19.24/3.19 % TRYING [7]
% 19.24/3.19 % (2233235)Instruction limit reached!
% 19.24/3.19 % (2233235)------------------------------
% 19.24/3.19 % (2233235)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233235)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233235)Termination reason: Instruction limit
% 19.24/3.19 % (2233235)Termination phase: Finite model building SAT solving
% 19.24/3.19 % (2233235)Time elapsed: 0.339 s
% 19.24/3.19 % (2233235)Peak memory usage: 43 MB
% 19.24/3.19 % (2233235)Instructions burned: 891 (million)
% 19.24/3.19 % (2233243)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1274544380:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 19.24/3.19 % TRYING [20]
% 19.24/3.19 % (2233237)Instruction limit reached!
% 19.24/3.19 % (2233237)------------------------------
% 19.24/3.19 % (2233237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233237)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233237)Termination reason: Instruction limit
% 19.24/3.19 % (2233237)Termination phase: Saturation
% 19.24/3.19 % (2233237)Time elapsed: 0.388 s
% 19.24/3.19 % (2233237)Peak memory usage: 24 MB
% 19.24/3.19 % (2233237)Instructions burned: 693 (million)
% 19.24/3.19 % (2233245)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1047321899:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 19.24/3.19 % TRYING [8]
% 19.24/3.19 % TRYING [8]
% 19.24/3.19 % (2233239)Instruction limit reached!
% 19.24/3.19 % (2233239)------------------------------
% 19.24/3.19 % (2233239)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233239)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233239)Termination reason: Instruction limit
% 19.24/3.19 % (2233239)Termination phase: Saturation
% 19.24/3.19 % (2233239)Time elapsed: 0.423 s
% 19.24/3.19 % (2233239)Peak memory usage: 19 MB
% 19.24/3.19 % (2233239)Instructions burned: 881 (million)
% 19.24/3.19 % (2233247)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1435746183:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 19.24/3.19 % TRYING [8]
% 19.24/3.19 % TRYING [9]
% 19.24/3.19 % (2233245)Instruction limit reached!
% 19.24/3.19 % (2233245)------------------------------
% 19.24/3.19 % (2233245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233245)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233245)Termination reason: Instruction limit
% 19.24/3.19 % (2233245)Termination phase: Finite model building SAT solving
% 19.24/3.19 % (2233245)Time elapsed: 0.441 s
% 19.24/3.19 % (2233245)Peak memory usage: 28 MB
% 19.24/3.19 % (2233245)Instructions burned: 922 (million)
% 19.24/3.19 % (2233249)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4157747544:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 19.24/3.19 % (2233249)Instruction limit reached!
% 19.24/3.19 % (2233249)------------------------------
% 19.24/3.19 % (2233249)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233249)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233249)Termination reason: Instruction limit
% 19.24/3.19 % (2233249)Termination phase: Saturation
% 19.24/3.19 % (2233249)Time elapsed: 0.815 s
% 19.24/3.19 % (2233249)Peak memory usage: 28 MB
% 19.24/3.19 % (2233249)Instructions burned: 1473 (million)
% 19.24/3.19 % (2233251)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=661983239:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 19.24/3.19 % TRYING [77]
% 19.24/3.19 % (2233208) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2233202-2233208"...
% 19.24/3.19 % TRYING [10]
% 19.24/3.19 % (2233208)...printing done.
% 19.24/3.19 % (2233208)Refutation found. Thanks to Tanya!
% 19.24/3.19 % SZS status Theorem for theBenchmark
% 19.24/3.19 % SZS output start Proof for theBenchmark
% See solution above
% 19.24/3.19 % (2233208)------------------------------
% 19.24/3.19 % (2233208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.24/3.19 % (2233208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.24/3.19 % (2233208)CaDiCaL version: 2.1.3
% 19.24/3.19 % (2233208)Termination reason: Refutation
% 19.24/3.19 % (2233208)Time elapsed: 2.709 s
% 19.24/3.19 % (2233208)Peak memory usage: 30 MB
% 19.24/3.19 % (2233208)Instructions burned: 4525 (million)
% 19.24/3.19 % (2233202)Success in time 2.773 s
% 19.24/3.19 % Vampire exiting
%------------------------------------------------------------------------------