%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : LCL642+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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:59:08 AM UTC 2026
% Result : Theorem 0.17s 0.73s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 50
% Syntax : Number of formulae : 320 ( 16 unt; 49 def)
% Number of atoms : 4590 ( 0 equ)
% Maximal formula atoms : 410 ( 14 avg)
% Number of connectives : 6662 (2392 ~;3376 |; 867 &)
% ( 27 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 40 ( 6 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 55 ( 54 usr; 28 prp; 0-2 aty)
% Number of functors : 43 ( 43 usr; 18 con; 0-1 aty)
% Number of variables : 1471 ( 0 sgn1200 !; 271 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [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)
| 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(f2,negated_conjecture,
~ ~ ? [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)
| 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)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p3(X4) )
| ~ p3(X3) ) )
| ! [X5] :
( ~ r1(X0,X5)
| p2(X5) )
| ~ ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p2(X8) )
| ~ p2(X7) ) )
| ! [X9] :
( ~ r1(X0,X9)
| p1(X9) )
| ~ ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) )
| ~ p1(X11) ) )
| ~ ( ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p2(X16) )
| ~ p2(X15) ) ) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ~ ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21) )
| ~ p2(X20) ) ) )
| ~ ! [X22] :
( ~ r1(X0,X22)
| ( ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
| ~ ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p2(X29) )
| ~ p2(X28) ) ) )
& ( p2(X22)
| ~ ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
| ~ ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ~ ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p2(X37) )
| ~ p2(X36) ) ) )
| ~ ! [X38] :
( ~ r1(X33,X38)
| p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ~ ! [X41] :
( ~ r1(X33,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42) )
| ~ p2(X41) ) ) ) )
| ~ ( ( ! [X43] :
( ~ r1(X32,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X32)
| ~ ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] :
( ~ r1(X53,X54)
| $false ) ) )
| ~ ! [X55] :
( ~ r1(X0,X55)
| p1(X55)
| ! [X56] :
( ~ r1(X55,X56)
| p4(X56)
| p3(X56)
| p2(X56)
| p1(X56)
| ! [X57] :
( ~ r1(X56,X57)
| p4(X57)
| p3(X57)
| p2(X57)
| p1(X57)
| ! [X58] :
( ~ r1(X57,X58)
| $false ) ) )
| ~ ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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 ) ) ) )
| ~ ( p1(X59)
| ! [X64] :
( ~ r1(X59,X64)
| p4(X64)
| p3(X64)
| p2(X64)
| p1(X64)
| ! [X65] :
( ~ r1(X64,X65)
| p4(X65)
| p3(X65)
| p2(X65)
| p1(X65)
| ! [X66] :
( ~ r1(X65,X66)
| $false ) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] :
( ~ r1(X67,X68)
| $false ) )
| ~ ! [X69] :
( ~ r1(X0,X69)
| p4(X69)
| p3(X69)
| p2(X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] :
( ~ r1(X70,X71)
| $false ) )
| ~ ! [X72] :
( ~ r1(X69,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 ) ) )
| ~ ( p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X76] :
( ~ r1(X72,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] :
( ~ r1(X76,X77)
| $false ) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] :
( ~ r1(X78,X79)
| $false ) )
| ~ ! [X80] :
( ~ r1(X0,X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] :
( ~ r1(X81,X82)
| $false ) )
| ~ ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] :
( ~ r1(X85,X86)
| $false ) ) )
| ~ ( p3(X83)
| p2(X83)
| p1(X83)
| ! [X87] :
( ~ r1(X83,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] :
( ~ r1(X87,X88)
| $false ) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] :
( ~ r1(X89,X90)
| $false ) )
| ~ ! [X91] :
( ~ r1(X0,X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] :
( ~ r1(X92,X93)
| $false ) )
| ~ ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] :
( ~ r1(X96,X97)
| $false ) ) )
| ~ ( p2(X94)
| p1(X94)
| ! [X98] :
( ~ r1(X94,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] :
( ~ r1(X98,X99)
| $false ) ) ) ) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] :
( ~ r1(X100,X101)
| $false ) )
| ~ ! [X102] :
( ~ r1(X0,X102)
| p1(X102)
| ! [X103] :
( ~ r1(X102,X103)
| p4(X103)
| p3(X103)
| p2(X103)
| p1(X103)
| ! [X104] :
( ~ r1(X103,X104)
| $false ) )
| ~ ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] :
( ~ r1(X107,X108)
| $false ) ) )
| ~ ( p1(X105)
| ! [X109] :
( ~ r1(X105,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] :
( ~ r1(X109,X110)
| $false ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] :
( ~ r1(X0,X111)
| $false )
| ~ ! [X112] :
( ~ r1(X0,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] :
( ~ r1(X112,X113)
| $false )
| ~ ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] :
( ~ r1(X115,X116)
| $false ) )
| ~ ( p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X117] :
( ~ r1(X114,X117)
| $false ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] :
( ~ r1(X0,X118)
| $false )
| ~ ! [X119] :
( ~ r1(X0,X119)
| p3(X119)
| p2(X119)
| p1(X119)
| ! [X120] :
( ~ r1(X119,X120)
| $false )
| ~ ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] :
( ~ r1(X122,X123)
| $false ) )
| ~ ( p3(X121)
| p2(X121)
| p1(X121)
| ! [X124] :
( ~ r1(X121,X124)
| $false ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] :
( ~ r1(X0,X125)
| $false )
| ~ ! [X126] :
( ~ r1(X0,X126)
| p2(X126)
| p1(X126)
| ! [X127] :
( ~ r1(X126,X127)
| $false )
| ~ ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] :
( ~ r1(X129,X130)
| $false ) )
| ~ ( p2(X128)
| p1(X128)
| ! [X131] :
( ~ r1(X128,X131)
| $false ) ) ) ) )
& ( p1(X0)
| ! [X132] :
( ~ r1(X0,X132)
| $false )
| ~ ! [X133] :
( ~ r1(X0,X133)
| p1(X133)
| ! [X134] :
( ~ r1(X133,X134)
| $false )
| ~ ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] :
( ~ r1(X136,X137)
| $false ) )
| ~ ( p1(X135)
| ! [X138] :
( ~ r1(X135,X138)
| $false ) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| p2(X140)
| ~ ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
~ ~ ? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p3(X4) )
| ~ p3(X3) ) )
| ! [X5] :
( ~ r1(X0,X5)
| p2(X5) )
| ~ ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p2(X8) )
| ~ p2(X7) ) )
| ! [X9] :
( ~ r1(X0,X9)
| p1(X9) )
| ~ ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) )
| ~ p1(X11) ) )
| ~ ( ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p2(X16) )
| ~ p2(X15) ) ) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ~ ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21) )
| ~ p2(X20) ) ) )
| ~ ! [X22] :
( ~ r1(X0,X22)
| ( ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
| ~ ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p2(X29) )
| ~ p2(X28) ) ) )
& ( p2(X22)
| ~ ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
| ~ ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ~ ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p2(X37) )
| ~ p2(X36) ) ) )
| ~ ! [X38] :
( ~ r1(X33,X38)
| p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ~ ! [X41] :
( ~ r1(X33,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42) )
| ~ p2(X41) ) ) ) )
| ~ ( ( ! [X43] :
( ~ r1(X32,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X32)
| ~ ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] : ~ r1(X53,X54) ) )
| ~ ! [X55] :
( ~ r1(X0,X55)
| p1(X55)
| ! [X56] :
( ~ r1(X55,X56)
| p4(X56)
| p3(X56)
| p2(X56)
| p1(X56)
| ! [X57] :
( ~ r1(X56,X57)
| p4(X57)
| p3(X57)
| p2(X57)
| p1(X57)
| ! [X58] : ~ r1(X57,X58) ) )
| ~ ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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) ) ) )
| ~ ( p1(X59)
| ! [X64] :
( ~ r1(X59,X64)
| p4(X64)
| p3(X64)
| p2(X64)
| p1(X64)
| ! [X65] :
( ~ r1(X64,X65)
| p4(X65)
| p3(X65)
| p2(X65)
| p1(X65)
| ! [X66] : ~ r1(X65,X66) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] : ~ r1(X67,X68) )
| ~ ! [X69] :
( ~ r1(X0,X69)
| p4(X69)
| p3(X69)
| p2(X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] : ~ r1(X70,X71) )
| ~ ! [X72] :
( ~ r1(X69,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) ) )
| ~ ( p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X76] :
( ~ r1(X72,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] : ~ r1(X76,X77) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] : ~ r1(X78,X79) )
| ~ ! [X80] :
( ~ r1(X0,X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] : ~ r1(X81,X82) )
| ~ ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] : ~ r1(X85,X86) ) )
| ~ ( p3(X83)
| p2(X83)
| p1(X83)
| ! [X87] :
( ~ r1(X83,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] : ~ r1(X87,X88) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] : ~ r1(X89,X90) )
| ~ ! [X91] :
( ~ r1(X0,X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] : ~ r1(X92,X93) )
| ~ ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] : ~ r1(X96,X97) ) )
| ~ ( p2(X94)
| p1(X94)
| ! [X98] :
( ~ r1(X94,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] : ~ r1(X98,X99) ) ) ) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] : ~ r1(X100,X101) )
| ~ ! [X102] :
( ~ r1(X0,X102)
| p1(X102)
| ! [X103] :
( ~ r1(X102,X103)
| p4(X103)
| p3(X103)
| p2(X103)
| p1(X103)
| ! [X104] : ~ r1(X103,X104) )
| ~ ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] : ~ r1(X107,X108) ) )
| ~ ( p1(X105)
| ! [X109] :
( ~ r1(X105,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] : ~ r1(X109,X110) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] : ~ r1(X0,X111)
| ~ ! [X112] :
( ~ r1(X0,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] : ~ r1(X112,X113)
| ~ ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] : ~ r1(X115,X116) )
| ~ ( p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X117] : ~ r1(X114,X117) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] : ~ r1(X0,X118)
| ~ ! [X119] :
( ~ r1(X0,X119)
| p3(X119)
| p2(X119)
| p1(X119)
| ! [X120] : ~ r1(X119,X120)
| ~ ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] : ~ r1(X122,X123) )
| ~ ( p3(X121)
| p2(X121)
| p1(X121)
| ! [X124] : ~ r1(X121,X124) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] : ~ r1(X0,X125)
| ~ ! [X126] :
( ~ r1(X0,X126)
| p2(X126)
| p1(X126)
| ! [X127] : ~ r1(X126,X127)
| ~ ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] : ~ r1(X129,X130) )
| ~ ( p2(X128)
| p1(X128)
| ! [X131] : ~ r1(X128,X131) ) ) ) )
& ( p1(X0)
| ! [X132] : ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X0,X133)
| p1(X133)
| ! [X134] : ~ r1(X133,X134)
| ~ ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] : ~ r1(X136,X137) )
| ~ ( p1(X135)
| ! [X138] : ~ r1(X135,X138) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| p2(X140)
| ~ ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ) ),
inference(true_and_false_elimination,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ! [X1] :
( ~ r1(X0,X1)
| p3(X1) )
| ~ ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ~ ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p3(X4) )
| ~ p3(X3) ) )
| ! [X5] :
( ~ r1(X0,X5)
| p2(X5) )
| ~ ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ~ ! [X7] :
( ~ r1(X6,X7)
| ! [X8] :
( ~ r1(X7,X8)
| p2(X8) )
| ~ p2(X7) ) )
| ! [X9] :
( ~ r1(X0,X9)
| p1(X9) )
| ~ ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ~ ! [X11] :
( ~ r1(X10,X11)
| ! [X12] :
( ~ r1(X11,X12)
| p1(X12) )
| ~ p1(X11) ) )
| ~ ( ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ~ ! [X15] :
( ~ r1(X14,X15)
| ! [X16] :
( ~ r1(X15,X16)
| p2(X16) )
| ~ p2(X15) ) ) )
| ~ ! [X17] :
( ~ r1(X0,X17)
| p2(X17)
| ~ ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ~ ! [X20] :
( ~ r1(X0,X20)
| ! [X21] :
( ~ r1(X20,X21)
| p2(X21) )
| ~ p2(X20) ) ) )
| ~ ! [X22] :
( ~ r1(X0,X22)
| ( ( ! [X23] :
( ~ r1(X22,X23)
| ! [X24] :
( ~ r1(X23,X24)
| p2(X24)
| ~ ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
| ~ ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ~ ! [X28] :
( ~ r1(X27,X28)
| ! [X29] :
( ~ r1(X28,X29)
| p2(X29) )
| ~ p2(X28) ) ) )
& ( p2(X22)
| ~ ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
| ~ ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ~ ! [X36] :
( ~ r1(X35,X36)
| ! [X37] :
( ~ r1(X36,X37)
| p2(X37) )
| ~ p2(X36) ) ) )
| ~ ! [X38] :
( ~ r1(X33,X38)
| p2(X38)
| ~ ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ~ ! [X41] :
( ~ r1(X33,X41)
| ! [X42] :
( ~ r1(X41,X42)
| p2(X42) )
| ~ p2(X41) ) ) ) )
| ~ ( ( ! [X43] :
( ~ r1(X32,X43)
| ! [X44] :
( ~ r1(X43,X44)
| p2(X44)
| ~ ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
| ~ ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ~ ! [X48] :
( ~ r1(X47,X48)
| ! [X49] :
( ~ r1(X48,X49)
| p2(X49) )
| ~ p2(X48) ) ) )
& ( p2(X32)
| ~ ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] : ~ r1(X53,X54) ) )
| ~ ! [X55] :
( ~ r1(X0,X55)
| p1(X55)
| ! [X56] :
( ~ r1(X55,X56)
| p4(X56)
| p3(X56)
| p2(X56)
| p1(X56)
| ! [X57] :
( ~ r1(X56,X57)
| p4(X57)
| p3(X57)
| p2(X57)
| p1(X57)
| ! [X58] : ~ r1(X57,X58) ) )
| ~ ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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) ) ) )
| ~ ( p1(X59)
| ! [X64] :
( ~ r1(X59,X64)
| p4(X64)
| p3(X64)
| p2(X64)
| p1(X64)
| ! [X65] :
( ~ r1(X64,X65)
| p4(X65)
| p3(X65)
| p2(X65)
| p1(X65)
| ! [X66] : ~ r1(X65,X66) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] : ~ r1(X67,X68) )
| ~ ! [X69] :
( ~ r1(X0,X69)
| p4(X69)
| p3(X69)
| p2(X69)
| p1(X69)
| ! [X70] :
( ~ r1(X69,X70)
| p4(X70)
| p3(X70)
| p2(X70)
| p1(X70)
| ! [X71] : ~ r1(X70,X71) )
| ~ ! [X72] :
( ~ r1(X69,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) ) )
| ~ ( p4(X72)
| p3(X72)
| p2(X72)
| p1(X72)
| ! [X76] :
( ~ r1(X72,X76)
| p4(X76)
| p3(X76)
| p2(X76)
| p1(X76)
| ! [X77] : ~ r1(X76,X77) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] : ~ r1(X78,X79) )
| ~ ! [X80] :
( ~ r1(X0,X80)
| p3(X80)
| p2(X80)
| p1(X80)
| ! [X81] :
( ~ r1(X80,X81)
| p4(X81)
| p3(X81)
| p2(X81)
| p1(X81)
| ! [X82] : ~ r1(X81,X82) )
| ~ ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] : ~ r1(X85,X86) ) )
| ~ ( p3(X83)
| p2(X83)
| p1(X83)
| ! [X87] :
( ~ r1(X83,X87)
| p4(X87)
| p3(X87)
| p2(X87)
| p1(X87)
| ! [X88] : ~ r1(X87,X88) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] : ~ r1(X89,X90) )
| ~ ! [X91] :
( ~ r1(X0,X91)
| p2(X91)
| p1(X91)
| ! [X92] :
( ~ r1(X91,X92)
| p4(X92)
| p3(X92)
| p2(X92)
| p1(X92)
| ! [X93] : ~ r1(X92,X93) )
| ~ ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] : ~ r1(X96,X97) ) )
| ~ ( p2(X94)
| p1(X94)
| ! [X98] :
( ~ r1(X94,X98)
| p4(X98)
| p3(X98)
| p2(X98)
| p1(X98)
| ! [X99] : ~ r1(X98,X99) ) ) ) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] : ~ r1(X100,X101) )
| ~ ! [X102] :
( ~ r1(X0,X102)
| p1(X102)
| ! [X103] :
( ~ r1(X102,X103)
| p4(X103)
| p3(X103)
| p2(X103)
| p1(X103)
| ! [X104] : ~ r1(X103,X104) )
| ~ ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] : ~ r1(X107,X108) ) )
| ~ ( p1(X105)
| ! [X109] :
( ~ r1(X105,X109)
| p4(X109)
| p3(X109)
| p2(X109)
| p1(X109)
| ! [X110] : ~ r1(X109,X110) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] : ~ r1(X0,X111)
| ~ ! [X112] :
( ~ r1(X0,X112)
| p4(X112)
| p3(X112)
| p2(X112)
| p1(X112)
| ! [X113] : ~ r1(X112,X113)
| ~ ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] : ~ r1(X115,X116) )
| ~ ( p4(X114)
| p3(X114)
| p2(X114)
| p1(X114)
| ! [X117] : ~ r1(X114,X117) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] : ~ r1(X0,X118)
| ~ ! [X119] :
( ~ r1(X0,X119)
| p3(X119)
| p2(X119)
| p1(X119)
| ! [X120] : ~ r1(X119,X120)
| ~ ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] : ~ r1(X122,X123) )
| ~ ( p3(X121)
| p2(X121)
| p1(X121)
| ! [X124] : ~ r1(X121,X124) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] : ~ r1(X0,X125)
| ~ ! [X126] :
( ~ r1(X0,X126)
| p2(X126)
| p1(X126)
| ! [X127] : ~ r1(X126,X127)
| ~ ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] : ~ r1(X129,X130) )
| ~ ( p2(X128)
| p1(X128)
| ! [X131] : ~ r1(X128,X131) ) ) ) )
& ( p1(X0)
| ! [X132] : ~ r1(X0,X132)
| ~ ! [X133] :
( ~ r1(X0,X133)
| p1(X133)
| ! [X134] : ~ r1(X133,X134)
| ~ ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] : ~ r1(X136,X137) )
| ~ ( p1(X135)
| ! [X138] : ~ r1(X135,X138) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ~ ! [X140] :
( ~ r1(X139,X140)
| p2(X140)
| ~ ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ? [X22] :
( r1(X0,X22)
& ( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] : ~ r1(X53,X54) ) )
| ? [X55] :
( r1(X0,X55)
& ~ p1(X55)
& ? [X56] :
( r1(X55,X56)
& ~ p4(X56)
& ~ p3(X56)
& ~ p2(X56)
& ~ p1(X56)
& ? [X57] :
( r1(X56,X57)
& ~ p4(X57)
& ~ p3(X57)
& ~ p2(X57)
& ~ p1(X57)
& ? [X58] : r1(X57,X58) ) )
& ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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) ) ) )
| ( ~ p1(X59)
& ? [X64] :
( r1(X59,X64)
& ~ p4(X64)
& ~ p3(X64)
& ~ p2(X64)
& ~ p1(X64)
& ? [X65] :
( r1(X64,X65)
& ~ p4(X65)
& ~ p3(X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] : r1(X65,X66) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] : ~ r1(X67,X68) )
| ? [X69] :
( r1(X0,X69)
& ~ p4(X69)
& ~ p3(X69)
& ~ p2(X69)
& ~ p1(X69)
& ? [X70] :
( r1(X69,X70)
& ~ p4(X70)
& ~ p3(X70)
& ~ p2(X70)
& ~ p1(X70)
& ? [X71] : r1(X70,X71) )
& ! [X72] :
( ~ r1(X69,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) ) )
| ( ~ p4(X72)
& ~ p3(X72)
& ~ p2(X72)
& ~ p1(X72)
& ? [X76] :
( r1(X72,X76)
& ~ p4(X76)
& ~ p3(X76)
& ~ p2(X76)
& ~ p1(X76)
& ? [X77] : r1(X76,X77) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] : ~ r1(X78,X79) )
| ? [X80] :
( r1(X0,X80)
& ~ p3(X80)
& ~ p2(X80)
& ~ p1(X80)
& ? [X81] :
( r1(X80,X81)
& ~ p4(X81)
& ~ p3(X81)
& ~ p2(X81)
& ~ p1(X81)
& ? [X82] : r1(X81,X82) )
& ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] : ~ r1(X85,X86) ) )
| ( ~ p3(X83)
& ~ p2(X83)
& ~ p1(X83)
& ? [X87] :
( r1(X83,X87)
& ~ p4(X87)
& ~ p3(X87)
& ~ p2(X87)
& ~ p1(X87)
& ? [X88] : r1(X87,X88) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] : ~ r1(X89,X90) )
| ? [X91] :
( r1(X0,X91)
& ~ p2(X91)
& ~ p1(X91)
& ? [X92] :
( r1(X91,X92)
& ~ p4(X92)
& ~ p3(X92)
& ~ p2(X92)
& ~ p1(X92)
& ? [X93] : r1(X92,X93) )
& ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] : ~ r1(X96,X97) ) )
| ( ~ p2(X94)
& ~ p1(X94)
& ? [X98] :
( r1(X94,X98)
& ~ p4(X98)
& ~ p3(X98)
& ~ p2(X98)
& ~ p1(X98)
& ? [X99] : r1(X98,X99) ) ) ) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] : ~ r1(X100,X101) )
| ? [X102] :
( r1(X0,X102)
& ~ p1(X102)
& ? [X103] :
( r1(X102,X103)
& ~ p4(X103)
& ~ p3(X103)
& ~ p2(X103)
& ~ p1(X103)
& ? [X104] : r1(X103,X104) )
& ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] : ~ r1(X107,X108) ) )
| ( ~ p1(X105)
& ? [X109] :
( r1(X105,X109)
& ~ p4(X109)
& ~ p3(X109)
& ~ p2(X109)
& ~ p1(X109)
& ? [X110] : r1(X109,X110) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] : ~ r1(X0,X111)
| ? [X112] :
( r1(X0,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] : r1(X112,X113)
& ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] : ~ r1(X115,X116) )
| ( ~ p4(X114)
& ~ p3(X114)
& ~ p2(X114)
& ~ p1(X114)
& ? [X117] : r1(X114,X117) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] : ~ r1(X0,X118)
| ? [X119] :
( r1(X0,X119)
& ~ p3(X119)
& ~ p2(X119)
& ~ p1(X119)
& ? [X120] : r1(X119,X120)
& ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] : ~ r1(X122,X123) )
| ( ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X124] : r1(X121,X124) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] : ~ r1(X0,X125)
| ? [X126] :
( r1(X0,X126)
& ~ p2(X126)
& ~ p1(X126)
& ? [X127] : r1(X126,X127)
& ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] : ~ r1(X129,X130) )
| ( ~ p2(X128)
& ~ p1(X128)
& ? [X131] : r1(X128,X131) ) ) ) )
& ( p1(X0)
| ! [X132] : ~ r1(X0,X132)
| ? [X133] :
( r1(X0,X133)
& ~ p1(X133)
& ? [X134] : r1(X133,X134)
& ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] : ~ r1(X136,X137) )
| ( ~ p1(X135)
& ? [X138] : r1(X135,X138) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ? [X140] :
( r1(X139,X140)
& ~ p2(X140)
& ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( ( ( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ? [X22] :
( r1(X0,X22)
& ( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| ! [X33] :
( ~ r1(X32,X33)
| ( ( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] : ~ r1(X53,X54) ) )
| ? [X55] :
( r1(X0,X55)
& ~ p1(X55)
& ? [X56] :
( r1(X55,X56)
& ~ p4(X56)
& ~ p3(X56)
& ~ p2(X56)
& ~ p1(X56)
& ? [X57] :
( r1(X56,X57)
& ~ p4(X57)
& ~ p3(X57)
& ~ p2(X57)
& ~ p1(X57)
& ? [X58] : r1(X57,X58) ) )
& ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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) ) ) )
| ( ~ p1(X59)
& ? [X64] :
( r1(X59,X64)
& ~ p4(X64)
& ~ p3(X64)
& ~ p2(X64)
& ~ p1(X64)
& ? [X65] :
( r1(X64,X65)
& ~ p4(X65)
& ~ p3(X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] : r1(X65,X66) ) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] : ~ r1(X67,X68) )
| ? [X69] :
( r1(X0,X69)
& ~ p4(X69)
& ~ p3(X69)
& ~ p2(X69)
& ~ p1(X69)
& ? [X70] :
( r1(X69,X70)
& ~ p4(X70)
& ~ p3(X70)
& ~ p2(X70)
& ~ p1(X70)
& ? [X71] : r1(X70,X71) )
& ! [X72] :
( ~ r1(X69,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) ) )
| ( ~ p4(X72)
& ~ p3(X72)
& ~ p2(X72)
& ~ p1(X72)
& ? [X76] :
( r1(X72,X76)
& ~ p4(X76)
& ~ p3(X76)
& ~ p2(X76)
& ~ p1(X76)
& ? [X77] : r1(X76,X77) ) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] : ~ r1(X78,X79) )
| ? [X80] :
( r1(X0,X80)
& ~ p3(X80)
& ~ p2(X80)
& ~ p1(X80)
& ? [X81] :
( r1(X80,X81)
& ~ p4(X81)
& ~ p3(X81)
& ~ p2(X81)
& ~ p1(X81)
& ? [X82] : r1(X81,X82) )
& ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] : ~ r1(X85,X86) ) )
| ( ~ p3(X83)
& ~ p2(X83)
& ~ p1(X83)
& ? [X87] :
( r1(X83,X87)
& ~ p4(X87)
& ~ p3(X87)
& ~ p2(X87)
& ~ p1(X87)
& ? [X88] : r1(X87,X88) ) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] : ~ r1(X89,X90) )
| ? [X91] :
( r1(X0,X91)
& ~ p2(X91)
& ~ p1(X91)
& ? [X92] :
( r1(X91,X92)
& ~ p4(X92)
& ~ p3(X92)
& ~ p2(X92)
& ~ p1(X92)
& ? [X93] : r1(X92,X93) )
& ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] : ~ r1(X96,X97) ) )
| ( ~ p2(X94)
& ~ p1(X94)
& ? [X98] :
( r1(X94,X98)
& ~ p4(X98)
& ~ p3(X98)
& ~ p2(X98)
& ~ p1(X98)
& ? [X99] : r1(X98,X99) ) ) ) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] : ~ r1(X100,X101) )
| ? [X102] :
( r1(X0,X102)
& ~ p1(X102)
& ? [X103] :
( r1(X102,X103)
& ~ p4(X103)
& ~ p3(X103)
& ~ p2(X103)
& ~ p1(X103)
& ? [X104] : r1(X103,X104) )
& ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] : ~ r1(X107,X108) ) )
| ( ~ p1(X105)
& ? [X109] :
( r1(X105,X109)
& ~ p4(X109)
& ~ p3(X109)
& ~ p2(X109)
& ~ p1(X109)
& ? [X110] : r1(X109,X110) ) ) ) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] : ~ r1(X0,X111)
| ? [X112] :
( r1(X0,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] : r1(X112,X113)
& ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] : ~ r1(X115,X116) )
| ( ~ p4(X114)
& ~ p3(X114)
& ~ p2(X114)
& ~ p1(X114)
& ? [X117] : r1(X114,X117) ) ) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] : ~ r1(X0,X118)
| ? [X119] :
( r1(X0,X119)
& ~ p3(X119)
& ~ p2(X119)
& ~ p1(X119)
& ? [X120] : r1(X119,X120)
& ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] : ~ r1(X122,X123) )
| ( ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X124] : r1(X121,X124) ) ) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] : ~ r1(X0,X125)
| ? [X126] :
( r1(X0,X126)
& ~ p2(X126)
& ~ p1(X126)
& ? [X127] : r1(X126,X127)
& ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] : ~ r1(X129,X130) )
| ( ~ p2(X128)
& ~ p1(X128)
& ? [X131] : r1(X128,X131) ) ) ) )
& ( p1(X0)
| ! [X132] : ~ r1(X0,X132)
| ? [X133] :
( r1(X0,X133)
& ~ p1(X133)
& ? [X134] : r1(X133,X134)
& ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] : ~ r1(X136,X137) )
| ( ~ p1(X135)
& ? [X138] : r1(X135,X138) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ? [X140] :
( r1(X139,X140)
& ~ p2(X140)
& ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ),
inference(flattening,[],[f6]) ).
fof(f8,definition,
! [X119] :
( ! [X121] :
( ~ r1(X119,X121)
| ! [X122] :
( ~ r1(X121,X122)
| p3(X122)
| p2(X122)
| p1(X122)
| ! [X123] : ~ r1(X122,X123) )
| ( ~ p3(X121)
& ~ p2(X121)
& ~ p1(X121)
& ? [X124] : r1(X121,X124) ) )
| ~ sP0(X119) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X112] :
( ! [X114] :
( ~ r1(X112,X114)
| ! [X115] :
( ~ r1(X114,X115)
| p4(X115)
| p3(X115)
| p2(X115)
| p1(X115)
| ! [X116] : ~ r1(X115,X116) )
| ( ~ p4(X114)
& ~ p3(X114)
& ~ p2(X114)
& ~ p1(X114)
& ? [X117] : r1(X114,X117) ) )
| ~ sP1(X112) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X102] :
( ! [X105] :
( ~ r1(X102,X105)
| ! [X106] :
( ~ r1(X105,X106)
| p1(X106)
| ! [X107] :
( ~ r1(X106,X107)
| p4(X107)
| p3(X107)
| p2(X107)
| p1(X107)
| ! [X108] : ~ r1(X107,X108) ) )
| ( ~ p1(X105)
& ? [X109] :
( r1(X105,X109)
& ~ p4(X109)
& ~ p3(X109)
& ~ p2(X109)
& ~ p1(X109)
& ? [X110] : r1(X109,X110) ) ) )
| ~ sP2(X102) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f11,definition,
! [X102] :
( ? [X103] :
( r1(X102,X103)
& ~ p4(X103)
& ~ p3(X103)
& ~ p2(X103)
& ~ p1(X103)
& ? [X104] : r1(X103,X104) )
| ~ sP3(X102) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f12,definition,
! [X91] :
( ! [X94] :
( ~ r1(X91,X94)
| ! [X95] :
( ~ r1(X94,X95)
| p2(X95)
| p1(X95)
| ! [X96] :
( ~ r1(X95,X96)
| p4(X96)
| p3(X96)
| p2(X96)
| p1(X96)
| ! [X97] : ~ r1(X96,X97) ) )
| ( ~ p2(X94)
& ~ p1(X94)
& ? [X98] :
( r1(X94,X98)
& ~ p4(X98)
& ~ p3(X98)
& ~ p2(X98)
& ~ p1(X98)
& ? [X99] : r1(X98,X99) ) ) )
| ~ sP4(X91) ),
introduced(definition,[new_symbols(definition,[sP4])],[predicate_definition_introduction]) ).
fof(f13,definition,
! [X91] :
( ? [X92] :
( r1(X91,X92)
& ~ p4(X92)
& ~ p3(X92)
& ~ p2(X92)
& ~ p1(X92)
& ? [X93] : r1(X92,X93) )
| ~ sP5(X91) ),
introduced(definition,[new_symbols(definition,[sP5])],[predicate_definition_introduction]) ).
fof(f14,definition,
! [X83] :
( ? [X87] :
( r1(X83,X87)
& ~ p4(X87)
& ~ p3(X87)
& ~ p2(X87)
& ~ p1(X87)
& ? [X88] : r1(X87,X88) )
| ~ sP6(X83) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f15,definition,
! [X80] :
( ? [X81] :
( r1(X80,X81)
& ~ p4(X81)
& ~ p3(X81)
& ~ p2(X81)
& ~ p1(X81)
& ? [X82] : r1(X81,X82) )
| ~ sP7(X80) ),
introduced(definition,[new_symbols(definition,[sP7])],[predicate_definition_introduction]) ).
fof(f16,definition,
! [X80] :
( ! [X83] :
( ~ r1(X80,X83)
| ! [X84] :
( ~ r1(X83,X84)
| p3(X84)
| p2(X84)
| p1(X84)
| ! [X85] :
( ~ r1(X84,X85)
| p4(X85)
| p3(X85)
| p2(X85)
| p1(X85)
| ! [X86] : ~ r1(X85,X86) ) )
| ( ~ p3(X83)
& ~ p2(X83)
& ~ p1(X83)
& sP6(X83) ) )
| ~ sP8(X80) ),
introduced(definition,[new_symbols(definition,[sP8])],[predicate_definition_introduction]) ).
fof(f17,definition,
! [X72] :
( ? [X76] :
( r1(X72,X76)
& ~ p4(X76)
& ~ p3(X76)
& ~ p2(X76)
& ~ p1(X76)
& ? [X77] : r1(X76,X77) )
| ~ sP9(X72) ),
introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction]) ).
fof(f18,definition,
! [X69] :
( ? [X70] :
( r1(X69,X70)
& ~ p4(X70)
& ~ p3(X70)
& ~ p2(X70)
& ~ p1(X70)
& ? [X71] : r1(X70,X71) )
| ~ sP10(X69) ),
introduced(definition,[new_symbols(definition,[sP10])],[predicate_definition_introduction]) ).
fof(f19,definition,
! [X69] :
( ! [X72] :
( ~ r1(X69,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) ) )
| ( ~ p4(X72)
& ~ p3(X72)
& ~ p2(X72)
& ~ p1(X72)
& sP9(X72) ) )
| ~ sP11(X69) ),
introduced(definition,[new_symbols(definition,[sP11])],[predicate_definition_introduction]) ).
fof(f20,definition,
! [X64] :
( ? [X65] :
( r1(X64,X65)
& ~ p4(X65)
& ~ p3(X65)
& ~ p2(X65)
& ~ p1(X65)
& ? [X66] : r1(X65,X66) )
| ~ sP12(X64) ),
introduced(definition,[new_symbols(definition,[sP12])],[predicate_definition_introduction]) ).
fof(f21,definition,
! [X56] :
( ? [X57] :
( r1(X56,X57)
& ~ p4(X57)
& ~ p3(X57)
& ~ p2(X57)
& ~ p1(X57)
& ? [X58] : r1(X57,X58) )
| ~ sP13(X56) ),
introduced(definition,[new_symbols(definition,[sP13])],[predicate_definition_introduction]) ).
fof(f22,definition,
! [X55] :
( ! [X59] :
( ~ r1(X55,X59)
| ! [X60] :
( ~ r1(X59,X60)
| p1(X60)
| ! [X61] :
( ~ r1(X60,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) ) ) )
| ( ~ p1(X59)
& ? [X64] :
( r1(X59,X64)
& ~ p4(X64)
& ~ p3(X64)
& ~ p2(X64)
& ~ p1(X64)
& sP12(X64) ) ) )
| ~ sP14(X55) ),
introduced(definition,[new_symbols(definition,[sP14])],[predicate_definition_introduction]) ).
fof(f23,definition,
! [X55] :
( ? [X56] :
( r1(X55,X56)
& ~ p4(X56)
& ~ p3(X56)
& ~ p2(X56)
& ~ p1(X56)
& sP13(X56) )
| ~ sP15(X55) ),
introduced(definition,[new_symbols(definition,[sP15])],[predicate_definition_introduction]) ).
fof(f24,definition,
! [X33] :
( ! [X34] :
( ~ r1(X33,X34)
| ! [X35] :
( ~ r1(X34,X35)
| p2(X35)
| ? [X36] :
( r1(X35,X36)
& ? [X37] :
( r1(X36,X37)
& ~ p2(X37) )
& p2(X36) ) ) )
| ~ sP16(X33) ),
introduced(definition,[new_symbols(definition,[sP16])],[predicate_definition_introduction]) ).
fof(f25,definition,
! [X32] :
( ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ~ sP17(X32) ),
introduced(definition,[new_symbols(definition,[sP17])],[predicate_definition_introduction]) ).
fof(f26,definition,
! [X32] :
( ! [X33] :
( ~ r1(X32,X33)
| ( ( sP16(X33)
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ~ sP18(X32) ),
introduced(definition,[new_symbols(definition,[sP18])],[predicate_definition_introduction]) ).
fof(f27,definition,
! [X22] :
( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ~ sP19(X22) ),
introduced(definition,[new_symbols(definition,[sP19])],[predicate_definition_introduction]) ).
fof(f28,definition,
! [X0] :
( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ~ sP20(X0) ),
introduced(definition,[new_symbols(definition,[sP20])],[predicate_definition_introduction]) ).
fof(f29,definition,
! [X0] :
( ( ( sP20(X0)
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ~ sP21(X0) ),
introduced(definition,[new_symbols(definition,[sP21])],[predicate_definition_introduction]) ).
fof(f30,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( sP21(X0)
| ? [X22] :
( r1(X0,X22)
& ( sP19(X22)
| ( ~ p2(X22)
& ! [X30] :
( ~ r1(X22,X30)
| ! [X31] :
( ~ r1(X30,X31)
| p2(X31) )
| ~ p2(X30) ) ) )
& ! [X32] :
( ~ r1(X22,X32)
| sP18(X32)
| sP17(X32)
| ( ~ p2(X32)
& ! [X50] :
( ~ r1(X32,X50)
| ! [X51] :
( ~ r1(X50,X51)
| p2(X51) )
| ~ p2(X50) ) ) ) ) )
& ( p1(X0)
| ! [X52] :
( ~ r1(X0,X52)
| p4(X52)
| p3(X52)
| p2(X52)
| p1(X52)
| ! [X53] :
( ~ r1(X52,X53)
| p4(X53)
| p3(X53)
| p2(X53)
| p1(X53)
| ! [X54] : ~ r1(X53,X54) ) )
| ? [X55] :
( r1(X0,X55)
& ~ p1(X55)
& sP15(X55)
& sP14(X55) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X67] :
( ~ r1(X0,X67)
| p4(X67)
| p3(X67)
| p2(X67)
| p1(X67)
| ! [X68] : ~ r1(X67,X68) )
| ? [X69] :
( r1(X0,X69)
& ~ p4(X69)
& ~ p3(X69)
& ~ p2(X69)
& ~ p1(X69)
& sP10(X69)
& sP11(X69) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X78] :
( ~ r1(X0,X78)
| p4(X78)
| p3(X78)
| p2(X78)
| p1(X78)
| ! [X79] : ~ r1(X78,X79) )
| ? [X80] :
( r1(X0,X80)
& ~ p3(X80)
& ~ p2(X80)
& ~ p1(X80)
& sP7(X80)
& sP8(X80) ) )
& ( p2(X0)
| p1(X0)
| ! [X89] :
( ~ r1(X0,X89)
| p4(X89)
| p3(X89)
| p2(X89)
| p1(X89)
| ! [X90] : ~ r1(X89,X90) )
| ? [X91] :
( r1(X0,X91)
& ~ p2(X91)
& ~ p1(X91)
& sP5(X91)
& sP4(X91) ) )
& ( p1(X0)
| ! [X100] :
( ~ r1(X0,X100)
| p4(X100)
| p3(X100)
| p2(X100)
| p1(X100)
| ! [X101] : ~ r1(X100,X101) )
| ? [X102] :
( r1(X0,X102)
& ~ p1(X102)
& sP3(X102)
& sP2(X102) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X111] : ~ r1(X0,X111)
| ? [X112] :
( r1(X0,X112)
& ~ p4(X112)
& ~ p3(X112)
& ~ p2(X112)
& ~ p1(X112)
& ? [X113] : r1(X112,X113)
& sP1(X112) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X118] : ~ r1(X0,X118)
| ? [X119] :
( r1(X0,X119)
& ~ p3(X119)
& ~ p2(X119)
& ~ p1(X119)
& ? [X120] : r1(X119,X120)
& sP0(X119) ) )
& ( p2(X0)
| p1(X0)
| ! [X125] : ~ r1(X0,X125)
| ? [X126] :
( r1(X0,X126)
& ~ p2(X126)
& ~ p1(X126)
& ? [X127] : r1(X126,X127)
& ! [X128] :
( ~ r1(X126,X128)
| ! [X129] :
( ~ r1(X128,X129)
| p2(X129)
| p1(X129)
| ! [X130] : ~ r1(X129,X130) )
| ( ~ p2(X128)
& ~ p1(X128)
& ? [X131] : r1(X128,X131) ) ) ) )
& ( p1(X0)
| ! [X132] : ~ r1(X0,X132)
| ? [X133] :
( r1(X0,X133)
& ~ p1(X133)
& ? [X134] : r1(X133,X134)
& ! [X135] :
( ~ r1(X133,X135)
| ! [X136] :
( ~ r1(X135,X136)
| p1(X136)
| ! [X137] : ~ r1(X136,X137) )
| ( ~ p1(X135)
& ? [X138] : r1(X135,X138) ) ) ) )
& ! [X139] :
( ~ r1(X0,X139)
| p2(X139)
| ? [X140] :
( r1(X139,X140)
& ~ p2(X140)
& ! [X141] :
( ~ r1(X140,X141)
| ! [X142] :
( ~ r1(X141,X142)
| p2(X142) )
| ~ p2(X141) ) ) ) ),
inference(definition_folding,[],[f7,f29,f28,f27,f26,f25,f24,f23,f22,f21,f20,f19,f18,f17,f16,f15,f14,f13,f12,f11,f10,f9,f8]) ).
fof(f31,plain,
! [X0] :
( ( ( sP20(X0)
| ? [X17] :
( r1(X0,X17)
& ~ p2(X17)
& ! [X18] :
( ~ r1(X17,X18)
| ! [X19] :
( ~ r1(X18,X19)
| p2(X19) )
| ~ p2(X18) ) ) )
& ( p2(X0)
| ? [X20] :
( r1(X0,X20)
& ? [X21] :
( r1(X20,X21)
& ~ p2(X21) )
& p2(X20) ) ) )
| ~ sP21(X0) ),
inference(nnf_transformation,[],[f29]) ).
fof(f32,plain,
! [X0] :
( ( ( sP20(X0)
| ? [X1] :
( r1(X0,X1)
& ~ p2(X1)
& ! [X2] :
( ~ r1(X1,X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) ) )
& ( p2(X0)
| ? [X4] :
( r1(X0,X4)
& ? [X5] :
( r1(X4,X5)
& ~ p2(X5) )
& p2(X4) ) ) )
| ~ sP21(X0) ),
inference(rectify,[],[f31]) ).
fof(f33,plain,
! [X0] :
( ( ( sP20(X0)
| ( r1(X0,sK22(X0))
& ~ p2(sK22(X0))
& ! [X2] :
( ~ r1(sK22(X0),X2)
| ! [X3] :
( ~ r1(X2,X3)
| p2(X3) )
| ~ p2(X2) ) ) )
& ( p2(X0)
| ( r1(X0,sK23(X0))
& r1(sK23(X0),sK24(X0))
& ~ p2(sK24(X0))
& p2(sK23(X0)) ) ) )
| ~ sP21(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22,sK23,sK24]),skolemize(X1,sK22(X0)),skolemize(X4,sK23(X0)),skolemize(X5,sK24(X0))],[f32]) ).
fof(f34,plain,
! [X0] :
( ! [X13] :
( ~ r1(X0,X13)
| ! [X14] :
( ~ r1(X13,X14)
| p2(X14)
| ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& ~ p2(X16) )
& p2(X15) ) ) )
| ~ sP20(X0) ),
inference(nnf_transformation,[],[f28]) ).
fof(f35,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p2(X4) )
& p2(X3) ) ) )
| ~ sP20(X0) ),
inference(rectify,[],[f34]) ).
fof(f36,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2)
| ( r1(X2,sK25(X2))
& r1(sK25(X2),sK26(X2))
& ~ p2(sK26(X2))
& p2(sK25(X2)) ) ) )
| ~ sP20(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25,sK26]),skolemize(X3,sK25(X2)),skolemize(X4,sK26(X2))],[f35]) ).
fof(f37,plain,
! [X22] :
( ( ? [X23] :
( r1(X22,X23)
& ? [X24] :
( r1(X23,X24)
& ~ p2(X24)
& ! [X25] :
( ~ r1(X24,X25)
| ! [X26] :
( ~ r1(X25,X26)
| p2(X26) )
| ~ p2(X25) ) ) )
& ! [X27] :
( ~ r1(X22,X27)
| p2(X27)
| ? [X28] :
( r1(X27,X28)
& ? [X29] :
( r1(X28,X29)
& ~ p2(X29) )
& p2(X28) ) ) )
| ~ sP19(X22) ),
inference(nnf_transformation,[],[f27]) ).
fof(f38,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) )
| ~ sP19(X0) ),
inference(rectify,[],[f37]) ).
fof(f39,plain,
! [X0] :
( ( r1(X0,sK27(X0))
& r1(sK27(X0),sK28(X0))
& ~ p2(sK28(X0))
& ! [X3] :
( ~ r1(sK28(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ( r1(X5,sK29(X5))
& r1(sK29(X5),sK30(X5))
& ~ p2(sK30(X5))
& p2(sK29(X5)) ) ) )
| ~ sP19(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK27,sK28,sK29,sK30]),skolemize(X1,sK27(X0)),skolemize(X2,sK28(X0)),skolemize(X6,sK29(X5)),skolemize(X7,sK30(X5))],[f38]) ).
fof(f40,plain,
! [X32] :
( ! [X33] :
( ~ r1(X32,X33)
| ( ( sP16(X33)
| ? [X38] :
( r1(X33,X38)
& ~ p2(X38)
& ! [X39] :
( ~ r1(X38,X39)
| ! [X40] :
( ~ r1(X39,X40)
| p2(X40) )
| ~ p2(X39) ) ) )
& ( p2(X33)
| ? [X41] :
( r1(X33,X41)
& ? [X42] :
( r1(X41,X42)
& ~ p2(X42) )
& p2(X41) ) ) ) )
| ~ sP18(X32) ),
inference(nnf_transformation,[],[f26]) ).
fof(f41,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( sP16(X1)
| ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ( p2(X1)
| ? [X5] :
( r1(X1,X5)
& ? [X6] :
( r1(X5,X6)
& ~ p2(X6) )
& p2(X5) ) ) ) )
| ~ sP18(X0) ),
inference(rectify,[],[f40]) ).
fof(f42,plain,
! [X0] :
( ! [X1] :
( ~ r1(X0,X1)
| ( ( sP16(X1)
| ( r1(X1,sK31(X1))
& ~ p2(sK31(X1))
& ! [X3] :
( ~ r1(sK31(X1),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ( p2(X1)
| ( r1(X1,sK32(X1))
& r1(sK32(X1),sK33(X1))
& ~ p2(sK33(X1))
& p2(sK32(X1)) ) ) ) )
| ~ sP18(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK31,sK32,sK33]),skolemize(X2,sK31(X1)),skolemize(X5,sK32(X1)),skolemize(X6,sK33(X1))],[f41]) ).
fof(f43,plain,
! [X32] :
( ( ? [X43] :
( r1(X32,X43)
& ? [X44] :
( r1(X43,X44)
& ~ p2(X44)
& ! [X45] :
( ~ r1(X44,X45)
| ! [X46] :
( ~ r1(X45,X46)
| p2(X46) )
| ~ p2(X45) ) ) )
& ! [X47] :
( ~ r1(X32,X47)
| p2(X47)
| ? [X48] :
( r1(X47,X48)
& ? [X49] :
( r1(X48,X49)
& ~ p2(X49) )
& p2(X48) ) ) )
| ~ sP17(X32) ),
inference(nnf_transformation,[],[f25]) ).
fof(f44,plain,
! [X0] :
( ( ? [X1] :
( r1(X0,X1)
& ? [X2] :
( r1(X1,X2)
& ~ p2(X2)
& ! [X3] :
( ~ r1(X2,X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) ) ) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ~ p2(X7) )
& p2(X6) ) ) )
| ~ sP17(X0) ),
inference(rectify,[],[f43]) ).
fof(f45,plain,
! [X0] :
( ( r1(X0,sK34(X0))
& r1(sK34(X0),sK35(X0))
& ~ p2(sK35(X0))
& ! [X3] :
( ~ r1(sK35(X0),X3)
| ! [X4] :
( ~ r1(X3,X4)
| p2(X4) )
| ~ p2(X3) )
& ! [X5] :
( ~ r1(X0,X5)
| p2(X5)
| ( r1(X5,sK36(X5))
& r1(sK36(X5),sK37(X5))
& ~ p2(sK37(X5))
& p2(sK36(X5)) ) ) )
| ~ sP17(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35,sK36,sK37]),skolemize(X1,sK34(X0)),skolemize(X2,sK35(X0)),skolemize(X6,sK36(X5)),skolemize(X7,sK37(X5))],[f44]) ).
fof(f95,plain,
? [X0] :
( ? [X1] :
( r1(X0,X1)
& ~ p3(X1) )
& ! [X2] :
( ~ r1(X0,X2)
| p3(X2)
| ? [X3] :
( r1(X2,X3)
& ? [X4] :
( r1(X3,X4)
& ~ p3(X4) )
& p3(X3) ) )
& ? [X5] :
( r1(X0,X5)
& ~ p2(X5) )
& ! [X6] :
( ~ r1(X0,X6)
| p2(X6)
| ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ~ p2(X8) )
& p2(X7) ) )
& ? [X9] :
( r1(X0,X9)
& ~ p1(X9) )
& ! [X10] :
( ~ r1(X0,X10)
| p1(X10)
| ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ~ p1(X12) )
& p1(X11) ) )
& ( sP21(X0)
| ? [X13] :
( r1(X0,X13)
& ( sP19(X13)
| ( ~ p2(X13)
& ! [X14] :
( ~ r1(X13,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(X13,X16)
| sP18(X16)
| sP17(X16)
| ( ~ p2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| p2(X18) )
| ~ p2(X17) ) ) ) ) )
& ( p1(X0)
| ! [X19] :
( ~ r1(X0,X19)
| p4(X19)
| p3(X19)
| p2(X19)
| p1(X19)
| ! [X20] :
( ~ r1(X19,X20)
| p4(X20)
| p3(X20)
| p2(X20)
| p1(X20)
| ! [X21] : ~ r1(X20,X21) ) )
| ? [X22] :
( r1(X0,X22)
& ~ p1(X22)
& sP15(X22)
& sP14(X22) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X23] :
( ~ r1(X0,X23)
| p4(X23)
| p3(X23)
| p2(X23)
| p1(X23)
| ! [X24] : ~ r1(X23,X24) )
| ? [X25] :
( r1(X0,X25)
& ~ p4(X25)
& ~ p3(X25)
& ~ p2(X25)
& ~ p1(X25)
& sP10(X25)
& sP11(X25) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X26] :
( ~ r1(X0,X26)
| p4(X26)
| p3(X26)
| p2(X26)
| p1(X26)
| ! [X27] : ~ r1(X26,X27) )
| ? [X28] :
( r1(X0,X28)
& ~ p3(X28)
& ~ p2(X28)
& ~ p1(X28)
& sP7(X28)
& sP8(X28) ) )
& ( p2(X0)
| p1(X0)
| ! [X29] :
( ~ r1(X0,X29)
| p4(X29)
| p3(X29)
| p2(X29)
| p1(X29)
| ! [X30] : ~ r1(X29,X30) )
| ? [X31] :
( r1(X0,X31)
& ~ p2(X31)
& ~ p1(X31)
& sP5(X31)
& sP4(X31) ) )
& ( p1(X0)
| ! [X32] :
( ~ r1(X0,X32)
| p4(X32)
| p3(X32)
| p2(X32)
| p1(X32)
| ! [X33] : ~ r1(X32,X33) )
| ? [X34] :
( r1(X0,X34)
& ~ p1(X34)
& sP3(X34)
& sP2(X34) ) )
& ( p4(X0)
| p3(X0)
| p2(X0)
| p1(X0)
| ! [X35] : ~ r1(X0,X35)
| ? [X36] :
( r1(X0,X36)
& ~ p4(X36)
& ~ p3(X36)
& ~ p2(X36)
& ~ p1(X36)
& ? [X37] : r1(X36,X37)
& sP1(X36) ) )
& ( p3(X0)
| p2(X0)
| p1(X0)
| ! [X38] : ~ r1(X0,X38)
| ? [X39] :
( r1(X0,X39)
& ~ p3(X39)
& ~ p2(X39)
& ~ p1(X39)
& ? [X40] : r1(X39,X40)
& sP0(X39) ) )
& ( p2(X0)
| p1(X0)
| ! [X41] : ~ r1(X0,X41)
| ? [X42] :
( r1(X0,X42)
& ~ p2(X42)
& ~ p1(X42)
& ? [X43] : r1(X42,X43)
& ! [X44] :
( ~ r1(X42,X44)
| ! [X45] :
( ~ r1(X44,X45)
| p2(X45)
| p1(X45)
| ! [X46] : ~ r1(X45,X46) )
| ( ~ p2(X44)
& ~ p1(X44)
& ? [X47] : r1(X44,X47) ) ) ) )
& ( p1(X0)
| ! [X48] : ~ r1(X0,X48)
| ? [X49] :
( r1(X0,X49)
& ~ p1(X49)
& ? [X50] : r1(X49,X50)
& ! [X51] :
( ~ r1(X49,X51)
| ! [X52] :
( ~ r1(X51,X52)
| p1(X52)
| ! [X53] : ~ r1(X52,X53) )
| ( ~ p1(X51)
& ? [X54] : r1(X51,X54) ) ) ) )
& ! [X55] :
( ~ r1(X0,X55)
| p2(X55)
| ? [X56] :
( r1(X55,X56)
& ~ p2(X56)
& ! [X57] :
( ~ r1(X56,X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ),
inference(rectify,[],[f30]) ).
fof(f96,plain,
( r1(sK64,sK65)
& ~ p3(sK65)
& ! [X2] :
( ~ r1(sK64,X2)
| p3(X2)
| ( r1(X2,sK66(X2))
& r1(sK66(X2),sK67(X2))
& ~ p3(sK67(X2))
& p3(sK66(X2)) ) )
& r1(sK64,sK68)
& ~ p2(sK68)
& ! [X6] :
( ~ r1(sK64,X6)
| p2(X6)
| ( r1(X6,sK69(X6))
& r1(sK69(X6),sK70(X6))
& ~ p2(sK70(X6))
& p2(sK69(X6)) ) )
& r1(sK64,sK71)
& ~ p1(sK71)
& ! [X10] :
( ~ r1(sK64,X10)
| p1(X10)
| ( r1(X10,sK72(X10))
& r1(sK72(X10),sK73(X10))
& ~ p1(sK73(X10))
& p1(sK72(X10)) ) )
& ( sP21(sK64)
| ( r1(sK64,sK74)
& ( sP19(sK74)
| ( ~ p2(sK74)
& ! [X14] :
( ~ r1(sK74,X14)
| ! [X15] :
( ~ r1(X14,X15)
| p2(X15) )
| ~ p2(X14) ) ) )
& ! [X16] :
( ~ r1(sK74,X16)
| sP18(X16)
| sP17(X16)
| ( ~ p2(X16)
& ! [X17] :
( ~ r1(X16,X17)
| ! [X18] :
( ~ r1(X17,X18)
| p2(X18) )
| ~ p2(X17) ) ) ) ) )
& ( p1(sK64)
| ! [X19] :
( ~ r1(sK64,X19)
| p4(X19)
| p3(X19)
| p2(X19)
| p1(X19)
| ! [X20] :
( ~ r1(X19,X20)
| p4(X20)
| p3(X20)
| p2(X20)
| p1(X20)
| ! [X21] : ~ r1(X20,X21) ) )
| ( r1(sK64,sK75)
& ~ p1(sK75)
& sP15(sK75)
& sP14(sK75) ) )
& ( p4(sK64)
| p3(sK64)
| p2(sK64)
| p1(sK64)
| ! [X23] :
( ~ r1(sK64,X23)
| p4(X23)
| p3(X23)
| p2(X23)
| p1(X23)
| ! [X24] : ~ r1(X23,X24) )
| ( r1(sK64,sK76)
& ~ p4(sK76)
& ~ p3(sK76)
& ~ p2(sK76)
& ~ p1(sK76)
& sP10(sK76)
& sP11(sK76) ) )
& ( p3(sK64)
| p2(sK64)
| p1(sK64)
| ! [X26] :
( ~ r1(sK64,X26)
| p4(X26)
| p3(X26)
| p2(X26)
| p1(X26)
| ! [X27] : ~ r1(X26,X27) )
| ( r1(sK64,sK77)
& ~ p3(sK77)
& ~ p2(sK77)
& ~ p1(sK77)
& sP7(sK77)
& sP8(sK77) ) )
& ( p2(sK64)
| p1(sK64)
| ! [X29] :
( ~ r1(sK64,X29)
| p4(X29)
| p3(X29)
| p2(X29)
| p1(X29)
| ! [X30] : ~ r1(X29,X30) )
| ( r1(sK64,sK78)
& ~ p2(sK78)
& ~ p1(sK78)
& sP5(sK78)
& sP4(sK78) ) )
& ( p1(sK64)
| ! [X32] :
( ~ r1(sK64,X32)
| p4(X32)
| p3(X32)
| p2(X32)
| p1(X32)
| ! [X33] : ~ r1(X32,X33) )
| ( r1(sK64,sK79)
& ~ p1(sK79)
& sP3(sK79)
& sP2(sK79) ) )
& ( p4(sK64)
| p3(sK64)
| p2(sK64)
| p1(sK64)
| ! [X35] : ~ r1(sK64,X35)
| ( r1(sK64,sK80)
& ~ p4(sK80)
& ~ p3(sK80)
& ~ p2(sK80)
& ~ p1(sK80)
& r1(sK80,sK81)
& sP1(sK80) ) )
& ( p3(sK64)
| p2(sK64)
| p1(sK64)
| ! [X38] : ~ r1(sK64,X38)
| ( r1(sK64,sK82)
& ~ p3(sK82)
& ~ p2(sK82)
& ~ p1(sK82)
& r1(sK82,sK83)
& sP0(sK82) ) )
& ( p2(sK64)
| p1(sK64)
| ! [X41] : ~ r1(sK64,X41)
| ( r1(sK64,sK84)
& ~ p2(sK84)
& ~ p1(sK84)
& r1(sK84,sK85)
& ! [X44] :
( ~ r1(sK84,X44)
| ! [X45] :
( ~ r1(X44,X45)
| p2(X45)
| p1(X45)
| ! [X46] : ~ r1(X45,X46) )
| ( ~ p2(X44)
& ~ p1(X44)
& r1(X44,sK86(X44)) ) ) ) )
& ( p1(sK64)
| ! [X48] : ~ r1(sK64,X48)
| ( r1(sK64,sK87)
& ~ p1(sK87)
& r1(sK87,sK88)
& ! [X51] :
( ~ r1(sK87,X51)
| ! [X52] :
( ~ r1(X51,X52)
| p1(X52)
| ! [X53] : ~ r1(X52,X53) )
| ( ~ p1(X51)
& r1(X51,sK89(X51)) ) ) ) )
& ! [X55] :
( ~ r1(sK64,X55)
| p2(X55)
| ( r1(X55,sK90(X55))
& ~ p2(sK90(X55))
& ! [X57] :
( ~ r1(sK90(X55),X57)
| ! [X58] :
( ~ r1(X57,X58)
| p2(X58) )
| ~ p2(X57) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64,sK65,sK66,sK67,sK68,sK69,sK70,sK71,sK72,sK73,sK74,sK75,sK76,sK77,sK78,sK79,sK80,sK81,sK82,sK83,sK84,sK85,sK86,sK87,sK88,sK89,sK90]),skolemize(X0,sK64),skolemize(X1,sK65),skolemize(X3,sK66(X2)),skolemize(X4,sK67(X2)),skolemize(X5,sK68),skolemize(X7,sK69(X6)),skolemize(X8,sK70(X6)),skolemize(X9,sK71),skolemize(X11,sK72(X10)),skolemize(X12,sK73(X10)),skolemize(X13,sK74),skolemize(X22,sK75),skolemize(X25,sK76),skolemize(X28,sK77),skolemize(X31,sK78),skolemize(X34,sK79),skolemize(X36,sK80),skolemize(X37,sK81),skolemize(X39,sK82),skolemize(X40,sK83),skolemize(X42,sK84),skolemize(X43,sK85),skolemize(X47,sK86(X44)),skolemize(X49,sK87),skolemize(X50,sK88),skolemize(X54,sK89(X51)),skolemize(X56,sK90(X55))],[f95]) ).
fof(f101,plain,
! [X2,X3,X0] :
( ~ sP21(X0)
| ~ r1(sK22(X0),X2)
| ~ r1(X2,X3)
| p2(X3)
| ~ p2(X2)
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f102,plain,
! [X0] :
( ~ sP21(X0)
| ~ p2(sK22(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f103,plain,
! [X0] :
( ~ sP21(X0)
| r1(X0,sK22(X0))
| sP20(X0) ),
inference(cnf_transformation,[],[f33]) ).
fof(f104,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| p2(sK25(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f105,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| ~ p2(sK26(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f106,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(sK25(X2),sK26(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f107,plain,
! [X2,X0,X1] :
( ~ sP20(X0)
| ~ r1(X1,X2)
| p2(X2)
| r1(X2,sK25(X2))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f36]) ).
fof(f108,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(X5)
| p2(sK29(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f109,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(X5)
| ~ p2(sK30(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f110,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(X5)
| r1(sK29(X5),sK30(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f111,plain,
! [X0,X5] :
( ~ sP19(X0)
| p2(X5)
| r1(X5,sK29(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f39]) ).
fof(f112,plain,
! [X3,X0,X4] :
( ~ sP19(X0)
| ~ r1(X3,X4)
| p2(X4)
| ~ p2(X3)
| ~ r1(sK28(X0),X3) ),
inference(cnf_transformation,[],[f39]) ).
fof(f113,plain,
! [X0] :
( ~ sP19(X0)
| ~ p2(sK28(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f114,plain,
! [X0] :
( ~ sP19(X0)
| r1(sK27(X0),sK28(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f115,plain,
! [X0] :
( ~ sP19(X0)
| r1(X0,sK27(X0)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f116,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(X1)
| p2(sK32(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f117,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(X1)
| ~ p2(sK33(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f118,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(X1)
| r1(sK32(X1),sK33(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f119,plain,
! [X0,X1] :
( ~ sP18(X0)
| p2(X1)
| r1(X1,sK32(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f42]) ).
fof(f123,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(X5)
| p2(sK36(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f124,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(X5)
| ~ p2(sK37(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f125,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(X5)
| r1(sK36(X5),sK37(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f126,plain,
! [X0,X5] :
( ~ sP17(X0)
| p2(X5)
| r1(X5,sK36(X5))
| ~ r1(X0,X5) ),
inference(cnf_transformation,[],[f45]) ).
fof(f229,plain,
! [X58,X57,X55] :
( ~ p2(X57)
| p2(X55)
| ~ r1(sK90(X55),X57)
| ~ r1(X57,X58)
| p2(X58)
| ~ r1(sK64,X55) ),
inference(cnf_transformation,[],[f96]) ).
fof(f230,plain,
! [X55] :
( ~ p2(sK90(X55))
| p2(X55)
| ~ r1(sK64,X55) ),
inference(cnf_transformation,[],[f96]) ).
fof(f231,plain,
! [X55] :
( ~ r1(sK64,X55)
| p2(X55)
| r1(X55,sK90(X55)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f283,plain,
! [X18,X16,X17] :
( sP21(sK64)
| ~ r1(sK74,X16)
| sP18(X16)
| sP17(X16)
| ~ r1(X16,X17)
| ~ r1(X17,X18)
| p2(X18)
| ~ p2(X17) ),
inference(cnf_transformation,[],[f96]) ).
fof(f284,plain,
! [X16] :
( sP21(sK64)
| ~ r1(sK74,X16)
| sP18(X16)
| sP17(X16)
| ~ p2(X16) ),
inference(cnf_transformation,[],[f96]) ).
fof(f285,plain,
! [X14,X15] :
( sP21(sK64)
| sP19(sK74)
| ~ r1(sK74,X14)
| ~ r1(X14,X15)
| p2(X15)
| ~ p2(X14) ),
inference(cnf_transformation,[],[f96]) ).
fof(f286,plain,
( sP21(sK64)
| sP19(sK74)
| ~ p2(sK74) ),
inference(cnf_transformation,[],[f96]) ).
fof(f287,plain,
( sP21(sK64)
| r1(sK64,sK74) ),
inference(cnf_transformation,[],[f96]) ).
fof(f294,plain,
! [X6] :
( ~ r1(sK64,X6)
| p2(X6)
| p2(sK69(X6)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f295,plain,
! [X6] :
( ~ p2(sK70(X6))
| p2(X6)
| ~ r1(sK64,X6) ),
inference(cnf_transformation,[],[f96]) ).
fof(f296,plain,
! [X6] :
( ~ r1(sK64,X6)
| p2(X6)
| r1(sK69(X6),sK70(X6)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f297,plain,
! [X6] :
( ~ r1(sK64,X6)
| p2(X6)
| r1(X6,sK69(X6)) ),
inference(cnf_transformation,[],[f96]) ).
fof(f298,plain,
~ p2(sK68),
inference(cnf_transformation,[],[f96]) ).
fof(f299,plain,
r1(sK64,sK68),
inference(cnf_transformation,[],[f96]) ).
fof(f582,definition,
( spl91_59
<=> ! [X18,X16,X17] :
( ~ r1(sK74,X16)
| ~ p2(X17)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP17(X16)
| sP18(X16) ) ),
introduced(definition,[new_symbols(definition,[spl91_59])],[avatar_definition]) ).
fof(f583,plain,
( ! [X18,X16,X17] :
( ~ p2(X17)
| ~ r1(sK74,X16)
| p2(X18)
| ~ r1(X17,X18)
| ~ r1(X16,X17)
| sP17(X16)
| sP18(X16) )
| ~ spl91_59 ),
inference(avatar_component_clause,[],[f582]) ).
fof(f585,definition,
( spl91_60
<=> sP21(sK64) ),
introduced(definition,[new_symbols(definition,[spl91_60])],[avatar_definition]) ).
fof(f587,plain,
( sP21(sK64)
| ~ spl91_60 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f588,plain,
( spl91_59
| spl91_60 ),
inference(avatar_split_clause,[],[f283,f585,f582]) ).
fof(f590,definition,
( spl91_61
<=> ! [X16] :
( ~ r1(sK74,X16)
| ~ p2(X16)
| sP17(X16)
| sP18(X16) ) ),
introduced(definition,[new_symbols(definition,[spl91_61])],[avatar_definition]) ).
fof(f591,plain,
( ! [X16] :
( ~ p2(X16)
| ~ r1(sK74,X16)
| sP17(X16)
| sP18(X16) )
| ~ spl91_61 ),
inference(avatar_component_clause,[],[f590]) ).
fof(f592,plain,
( spl91_61
| spl91_60 ),
inference(avatar_split_clause,[],[f284,f585,f590]) ).
fof(f594,definition,
( spl91_62
<=> ! [X14,X15] :
( ~ r1(sK74,X14)
| ~ p2(X14)
| p2(X15)
| ~ r1(X14,X15) ) ),
introduced(definition,[new_symbols(definition,[spl91_62])],[avatar_definition]) ).
fof(f595,plain,
( ! [X14,X15] :
( ~ p2(X14)
| ~ r1(sK74,X14)
| p2(X15)
| ~ r1(X14,X15) )
| ~ spl91_62 ),
inference(avatar_component_clause,[],[f594]) ).
fof(f597,definition,
( spl91_63
<=> sP19(sK74) ),
introduced(definition,[new_symbols(definition,[spl91_63])],[avatar_definition]) ).
fof(f599,plain,
( sP19(sK74)
| ~ spl91_63 ),
inference(avatar_component_clause,[],[f597]) ).
fof(f600,plain,
( spl91_62
| spl91_63
| spl91_60 ),
inference(avatar_split_clause,[],[f285,f585,f597,f594]) ).
fof(f602,definition,
( spl91_64
<=> p2(sK74) ),
introduced(definition,[new_symbols(definition,[spl91_64])],[avatar_definition]) ).
fof(f604,plain,
( ~ p2(sK74)
| spl91_64 ),
inference(avatar_component_clause,[],[f602]) ).
fof(f605,plain,
( ~ spl91_64
| spl91_63
| spl91_60 ),
inference(avatar_split_clause,[],[f286,f585,f597,f602]) ).
fof(f607,definition,
( spl91_65
<=> r1(sK64,sK74) ),
introduced(definition,[new_symbols(definition,[spl91_65])],[avatar_definition]) ).
fof(f609,plain,
( r1(sK64,sK74)
| ~ spl91_65 ),
inference(avatar_component_clause,[],[f607]) ).
fof(f610,plain,
( spl91_65
| spl91_60 ),
inference(avatar_split_clause,[],[f287,f585,f607]) ).
fof(f678,plain,
( p2(sK68)
| r1(sK68,sK90(sK68)) ),
inference(resolution,[],[f231,f299]) ).
fof(f685,plain,
r1(sK68,sK90(sK68)),
inference(forward_subsumption_resolution,[],[f678,f298]) ).
fof(f836,plain,
( p2(sK74)
| p2(sK69(sK74))
| ~ spl91_65 ),
inference(resolution,[],[f609,f294]) ).
fof(f869,plain,
( p2(sK69(sK74))
| spl91_64
| ~ spl91_65 ),
inference(forward_subsumption_resolution,[],[f836,f604]) ).
fof(f991,plain,
( ~ p2(sK22(sK64))
| sP20(sK64)
| ~ spl91_60 ),
inference(resolution,[],[f102,f587]) ).
fof(f993,definition,
( spl91_131
<=> sP20(sK64) ),
introduced(definition,[new_symbols(definition,[spl91_131])],[avatar_definition]) ).
fof(f994,plain,
( ~ sP20(sK64)
| spl91_131 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f995,plain,
( sP20(sK64)
| ~ spl91_131 ),
inference(avatar_component_clause,[],[f993]) ).
fof(f997,definition,
( spl91_132
<=> p2(sK22(sK64)) ),
introduced(definition,[new_symbols(definition,[spl91_132])],[avatar_definition]) ).
fof(f999,plain,
( ~ p2(sK22(sK64))
| spl91_132 ),
inference(avatar_component_clause,[],[f997]) ).
fof(f1000,plain,
( spl91_131
| ~ spl91_132
| ~ spl91_60 ),
inference(avatar_split_clause,[],[f991,f585,f997,f993]) ).
fof(f1011,plain,
( r1(sK64,sK22(sK64))
| sP20(sK64)
| ~ spl91_60 ),
inference(resolution,[],[f103,f587]) ).
fof(f1013,definition,
( spl91_133
<=> r1(sK64,sK22(sK64)) ),
introduced(definition,[new_symbols(definition,[spl91_133])],[avatar_definition]) ).
fof(f1015,plain,
( r1(sK64,sK22(sK64))
| ~ spl91_133 ),
inference(avatar_component_clause,[],[f1013]) ).
fof(f1016,plain,
( spl91_131
| spl91_133
| ~ spl91_60 ),
inference(avatar_split_clause,[],[f1011,f585,f1013,f993]) ).
fof(f1041,plain,
( p2(sK74)
| r1(sK74,sK69(sK74))
| ~ spl91_65 ),
inference(resolution,[],[f609,f297]) ).
fof(f1050,plain,
( r1(sK74,sK69(sK74))
| spl91_64
| ~ spl91_65 ),
inference(forward_subsumption_resolution,[],[f1041,f604]) ).
fof(f1089,plain,
( ! [X0] :
( ~ r1(sK74,sK69(sK74))
| p2(X0)
| ~ r1(sK69(sK74),X0) )
| ~ spl91_62
| spl91_64
| ~ spl91_65 ),
inference(resolution,[],[f869,f595]) ).
fof(f1093,definition,
( spl91_141
<=> ! [X1] :
( ~ r1(sK69(sK74),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_141])],[avatar_definition]) ).
fof(f1094,plain,
( ! [X1] :
( ~ r1(sK69(sK74),X1)
| p2(X1) )
| ~ spl91_141 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1100,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK69(sK74),X0) )
| ~ spl91_62
| spl91_64
| ~ spl91_65 ),
inference(forward_subsumption_resolution,[],[f1089,f1050]) ).
fof(f1114,plain,
( spl91_141
| ~ spl91_62
| spl91_64
| ~ spl91_65 ),
inference(avatar_split_clause,[],[f1100,f607,f602,f594,f1093]) ).
fof(f1116,plain,
( ! [X0] :
( ~ r1(sK74,X0)
| p2(sK29(X0))
| p2(X0) )
| ~ spl91_63 ),
inference(resolution,[],[f599,f108]) ).
fof(f1118,plain,
( r1(sK74,sK27(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f599,f115]) ).
fof(f1219,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| p2(sK25(X1))
| ~ r1(sK64,X0) )
| ~ spl91_131 ),
inference(resolution,[],[f104,f995]) ).
fof(f1283,plain,
( p2(sK29(sK27(sK74)))
| p2(sK27(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f1116,f1118]) ).
fof(f1285,definition,
( spl91_170
<=> p2(sK27(sK74)) ),
introduced(definition,[new_symbols(definition,[spl91_170])],[avatar_definition]) ).
fof(f1286,plain,
( ~ p2(sK27(sK74))
| spl91_170 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1287,plain,
( p2(sK27(sK74))
| ~ spl91_170 ),
inference(avatar_component_clause,[],[f1285]) ).
fof(f1289,definition,
( spl91_171
<=> p2(sK29(sK27(sK74))) ),
introduced(definition,[new_symbols(definition,[spl91_171])],[avatar_definition]) ).
fof(f1291,plain,
( p2(sK29(sK27(sK74)))
| ~ spl91_171 ),
inference(avatar_component_clause,[],[f1289]) ).
fof(f1292,plain,
( spl91_170
| spl91_171
| ~ spl91_63 ),
inference(avatar_split_clause,[],[f1283,f597,f1289,f1285]) ).
fof(f1312,plain,
( p2(sK90(sK68))
| p2(sK25(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ spl91_131 ),
inference(resolution,[],[f1219,f685]) ).
fof(f1375,plain,
( p2(sK90(sK68))
| p2(sK25(sK90(sK68)))
| ~ spl91_131 ),
inference(forward_subsumption_resolution,[],[f1312,f299]) ).
fof(f1413,definition,
( spl91_191
<=> p2(sK25(sK90(sK68))) ),
introduced(definition,[new_symbols(definition,[spl91_191])],[avatar_definition]) ).
fof(f1415,plain,
( p2(sK25(sK90(sK68)))
| ~ spl91_191 ),
inference(avatar_component_clause,[],[f1413]) ).
fof(f1417,definition,
( spl91_192
<=> p2(sK90(sK68)) ),
introduced(definition,[new_symbols(definition,[spl91_192])],[avatar_definition]) ).
fof(f1418,plain,
( ~ p2(sK90(sK68))
| spl91_192 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1419,plain,
( p2(sK90(sK68))
| ~ spl91_192 ),
inference(avatar_component_clause,[],[f1417]) ).
fof(f1420,plain,
( spl91_191
| spl91_192
| ~ spl91_131 ),
inference(avatar_split_clause,[],[f1375,f993,f1417,f1413]) ).
fof(f1463,plain,
( p2(sK22(sK64))
| p2(sK69(sK22(sK64)))
| ~ spl91_133 ),
inference(resolution,[],[f1015,f294]) ).
fof(f1502,plain,
( p2(sK69(sK22(sK64)))
| spl91_132
| ~ spl91_133 ),
inference(forward_subsumption_resolution,[],[f1463,f999]) ).
fof(f1548,plain,
( p2(sK74)
| r1(sK69(sK74),sK70(sK74))
| ~ spl91_65 ),
inference(resolution,[],[f609,f296]) ).
fof(f1562,plain,
( r1(sK69(sK74),sK70(sK74))
| spl91_64
| ~ spl91_65 ),
inference(forward_subsumption_resolution,[],[f1548,f604]) ).
fof(f1585,plain,
( p2(sK70(sK74))
| spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(resolution,[],[f1094,f1562]) ).
fof(f1586,plain,
( p2(sK74)
| ~ r1(sK64,sK74)
| spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(resolution,[],[f1585,f295]) ).
fof(f1616,plain,
( ~ r1(sK64,sK74)
| spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(forward_subsumption_resolution,[],[f1586,f604]) ).
fof(f1617,plain,
( $false
| spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(forward_subsumption_resolution,[],[f1616,f609]) ).
fof(f1618,plain,
( spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(avatar_contradiction_clause,[],[f1617]) ).
fof(f1623,plain,
( ! [X0] :
( ~ p2(sK30(X0))
| p2(X0)
| ~ r1(sK74,X0) )
| ~ spl91_63 ),
inference(resolution,[],[f599,f109]) ).
fof(f1624,plain,
( ! [X0] :
( ~ r1(sK74,X0)
| r1(sK29(X0),sK30(X0))
| p2(X0) )
| ~ spl91_63 ),
inference(resolution,[],[f599,f110]) ).
fof(f1625,plain,
( ! [X0] :
( ~ r1(sK74,X0)
| r1(X0,sK29(X0))
| p2(X0) )
| ~ spl91_63 ),
inference(resolution,[],[f599,f111]) ).
fof(f1626,plain,
( ! [X0,X1] :
( ~ p2(X0)
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK28(sK74),X0) )
| ~ spl91_63 ),
inference(resolution,[],[f599,f112]) ).
fof(f1627,plain,
( ~ p2(sK28(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f599,f113]) ).
fof(f1628,plain,
( r1(sK27(sK74),sK28(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f599,f114]) ).
fof(f1629,plain,
( r1(sK74,sK27(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f599,f115]) ).
fof(f1636,plain,
( ~ r1(sK74,sK27(sK74))
| sP17(sK27(sK74))
| sP18(sK27(sK74))
| ~ spl91_61
| ~ spl91_170 ),
inference(resolution,[],[f1287,f591]) ).
fof(f1645,plain,
( sP17(sK27(sK74))
| sP18(sK27(sK74))
| ~ spl91_61
| ~ spl91_63
| ~ spl91_170 ),
inference(forward_subsumption_resolution,[],[f1636,f1629]) ).
fof(f1652,definition,
( spl91_220
<=> sP18(sK27(sK74)) ),
introduced(definition,[new_symbols(definition,[spl91_220])],[avatar_definition]) ).
fof(f1653,plain,
( ~ sP18(sK27(sK74))
| spl91_220 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1654,plain,
( sP18(sK27(sK74))
| ~ spl91_220 ),
inference(avatar_component_clause,[],[f1652]) ).
fof(f1656,definition,
( spl91_221
<=> sP17(sK27(sK74)) ),
introduced(definition,[new_symbols(definition,[spl91_221])],[avatar_definition]) ).
fof(f1658,plain,
( sP17(sK27(sK74))
| ~ spl91_221 ),
inference(avatar_component_clause,[],[f1656]) ).
fof(f1659,plain,
( spl91_220
| spl91_221
| ~ spl91_61
| ~ spl91_63
| ~ spl91_170 ),
inference(avatar_split_clause,[],[f1645,f1285,f597,f590,f1656,f1652]) ).
fof(f1661,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| p2(sK32(X0))
| p2(X0) )
| ~ spl91_220 ),
inference(resolution,[],[f1654,f116]) ).
fof(f1664,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| r1(X0,sK32(X0))
| p2(X0) )
| ~ spl91_220 ),
inference(resolution,[],[f1654,f119]) ).
fof(f1677,plain,
( ! [X0,X1] :
( ~ r1(sK74,X0)
| p2(X1)
| ~ r1(sK29(sK27(sK74)),X1)
| ~ r1(X0,sK29(sK27(sK74)))
| sP17(X0)
| sP18(X0) )
| ~ spl91_59
| ~ spl91_171 ),
inference(resolution,[],[f1291,f583]) ).
fof(f1682,definition,
( spl91_222
<=> ! [X1] :
( ~ r1(sK29(sK27(sK74)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_222])],[avatar_definition]) ).
fof(f1683,plain,
( ! [X1] :
( ~ r1(sK29(sK27(sK74)),X1)
| p2(X1) )
| ~ spl91_222 ),
inference(avatar_component_clause,[],[f1682]) ).
fof(f1703,definition,
( spl91_227
<=> ! [X0] :
( ~ r1(sK74,X0)
| sP18(X0)
| sP17(X0)
| ~ r1(X0,sK29(sK27(sK74))) ) ),
introduced(definition,[new_symbols(definition,[spl91_227])],[avatar_definition]) ).
fof(f1704,plain,
( ! [X0] :
( ~ r1(sK74,X0)
| sP18(X0)
| sP17(X0)
| ~ r1(X0,sK29(sK27(sK74))) )
| ~ spl91_227 ),
inference(avatar_component_clause,[],[f1703]) ).
fof(f1705,plain,
( spl91_222
| spl91_227
| ~ spl91_59
| ~ spl91_171 ),
inference(avatar_split_clause,[],[f1677,f1289,f582,f1703,f1682]) ).
fof(f1711,plain,
( r1(sK27(sK74),sK29(sK27(sK74)))
| p2(sK27(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f1625,f1629]) ).
fof(f1712,plain,
( r1(sK27(sK74),sK29(sK27(sK74)))
| ~ spl91_63
| spl91_170 ),
inference(forward_subsumption_resolution,[],[f1711,f1286]) ).
fof(f1714,plain,
( r1(sK29(sK27(sK74)),sK30(sK27(sK74)))
| p2(sK27(sK74))
| ~ spl91_63 ),
inference(resolution,[],[f1624,f1629]) ).
fof(f1715,plain,
( r1(sK29(sK27(sK74)),sK30(sK27(sK74)))
| ~ spl91_63
| spl91_170 ),
inference(forward_subsumption_resolution,[],[f1714,f1286]) ).
fof(f1789,plain,
( p2(sK30(sK27(sK74)))
| ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(resolution,[],[f1683,f1715]) ).
fof(f1790,plain,
( p2(sK27(sK74))
| ~ r1(sK74,sK27(sK74))
| ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(resolution,[],[f1789,f1623]) ).
fof(f1826,plain,
( ~ r1(sK74,sK27(sK74))
| ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(forward_subsumption_resolution,[],[f1790,f1286]) ).
fof(f1827,plain,
( $false
| ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(forward_subsumption_resolution,[],[f1826,f1629]) ).
fof(f1828,plain,
( ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(avatar_contradiction_clause,[],[f1827]) ).
fof(f1834,plain,
( p2(sK32(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_220 ),
inference(resolution,[],[f1661,f1628]) ).
fof(f1836,plain,
( p2(sK32(sK28(sK74)))
| ~ spl91_63
| ~ spl91_220 ),
inference(forward_subsumption_resolution,[],[f1834,f1627]) ).
fof(f1837,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK32(sK28(sK74)),X0)
| ~ r1(sK28(sK74),sK32(sK28(sK74))) )
| ~ spl91_63
| ~ spl91_220 ),
inference(resolution,[],[f1836,f1626]) ).
fof(f1843,definition,
( spl91_248
<=> ! [X1] :
( ~ r1(sK32(sK28(sK74)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_248])],[avatar_definition]) ).
fof(f1844,plain,
( ! [X1] :
( ~ r1(sK32(sK28(sK74)),X1)
| p2(X1) )
| ~ spl91_248 ),
inference(avatar_component_clause,[],[f1843]) ).
fof(f1868,definition,
( spl91_254
<=> r1(sK28(sK74),sK32(sK28(sK74))) ),
introduced(definition,[new_symbols(definition,[spl91_254])],[avatar_definition]) ).
fof(f1871,plain,
( ~ spl91_254
| spl91_248
| ~ spl91_63
| ~ spl91_220 ),
inference(avatar_split_clause,[],[f1837,f1652,f597,f1843,f1868]) ).
fof(f1877,plain,
( sP18(sK27(sK74))
| sP17(sK27(sK74))
| ~ r1(sK27(sK74),sK29(sK27(sK74)))
| ~ spl91_63
| ~ spl91_227 ),
inference(resolution,[],[f1704,f1629]) ).
fof(f1911,plain,
( r1(sK28(sK74),sK32(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_220 ),
inference(resolution,[],[f1664,f1628]) ).
fof(f1913,plain,
( r1(sK28(sK74),sK32(sK28(sK74)))
| ~ spl91_63
| ~ spl91_220 ),
inference(forward_subsumption_resolution,[],[f1911,f1627]) ).
fof(f1914,plain,
( spl91_254
| ~ spl91_63
| ~ spl91_220 ),
inference(avatar_split_clause,[],[f1913,f1652,f597,f1868]) ).
fof(f1980,plain,
( sP17(sK27(sK74))
| ~ r1(sK27(sK74),sK29(sK27(sK74)))
| ~ spl91_63
| spl91_220
| ~ spl91_227 ),
inference(forward_subsumption_resolution,[],[f1877,f1653]) ).
fof(f2006,plain,
( sP17(sK27(sK74))
| ~ spl91_63
| spl91_170
| spl91_220
| ~ spl91_227 ),
inference(forward_subsumption_resolution,[],[f1980,f1712]) ).
fof(f2007,plain,
( spl91_221
| ~ spl91_63
| spl91_170
| spl91_220
| ~ spl91_227 ),
inference(avatar_split_clause,[],[f2006,f1703,f1652,f1285,f597,f1656]) ).
fof(f2040,plain,
( ! [X0] :
( ~ p2(sK33(X0))
| p2(X0)
| ~ r1(sK27(sK74),X0) )
| ~ spl91_220 ),
inference(resolution,[],[f1654,f117]) ).
fof(f2041,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| r1(sK32(X0),sK33(X0))
| p2(X0) )
| ~ spl91_220 ),
inference(resolution,[],[f1654,f118]) ).
fof(f2064,plain,
( r1(sK32(sK28(sK74)),sK33(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_220 ),
inference(resolution,[],[f2041,f1628]) ).
fof(f2066,plain,
( r1(sK32(sK28(sK74)),sK33(sK28(sK74)))
| ~ spl91_63
| ~ spl91_220 ),
inference(forward_subsumption_resolution,[],[f2064,f1627]) ).
fof(f2067,plain,
( p2(sK33(sK28(sK74)))
| ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(resolution,[],[f2066,f1844]) ).
fof(f2082,plain,
( p2(sK28(sK74))
| ~ r1(sK27(sK74),sK28(sK74))
| ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(resolution,[],[f2067,f2040]) ).
fof(f2123,plain,
( ~ r1(sK27(sK74),sK28(sK74))
| ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(forward_subsumption_resolution,[],[f2082,f1627]) ).
fof(f2124,plain,
( $false
| ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(forward_subsumption_resolution,[],[f2123,f1628]) ).
fof(f2125,plain,
( ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(avatar_contradiction_clause,[],[f2124]) ).
fof(f2132,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| p2(sK36(X0))
| p2(X0) )
| ~ spl91_221 ),
inference(resolution,[],[f1658,f123]) ).
fof(f2133,plain,
( ! [X0] :
( ~ p2(sK37(X0))
| p2(X0)
| ~ r1(sK27(sK74),X0) )
| ~ spl91_221 ),
inference(resolution,[],[f1658,f124]) ).
fof(f2134,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| r1(sK36(X0),sK37(X0))
| p2(X0) )
| ~ spl91_221 ),
inference(resolution,[],[f1658,f125]) ).
fof(f2135,plain,
( ! [X0] :
( ~ r1(sK27(sK74),X0)
| r1(X0,sK36(X0))
| p2(X0) )
| ~ spl91_221 ),
inference(resolution,[],[f1658,f126]) ).
fof(f2140,plain,
( p2(sK36(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_221 ),
inference(resolution,[],[f2132,f1628]) ).
fof(f2152,plain,
( p2(sK36(sK28(sK74)))
| ~ spl91_63
| ~ spl91_221 ),
inference(forward_subsumption_resolution,[],[f2140,f1627]) ).
fof(f2153,plain,
( ! [X0] :
( p2(X0)
| ~ r1(sK36(sK28(sK74)),X0)
| ~ r1(sK28(sK74),sK36(sK28(sK74))) )
| ~ spl91_63
| ~ spl91_221 ),
inference(resolution,[],[f2152,f1626]) ).
fof(f2159,definition,
( spl91_292
<=> ! [X1] :
( ~ r1(sK36(sK28(sK74)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_292])],[avatar_definition]) ).
fof(f2160,plain,
( ! [X1] :
( ~ r1(sK36(sK28(sK74)),X1)
| p2(X1) )
| ~ spl91_292 ),
inference(avatar_component_clause,[],[f2159]) ).
fof(f2184,definition,
( spl91_298
<=> r1(sK28(sK74),sK36(sK28(sK74))) ),
introduced(definition,[new_symbols(definition,[spl91_298])],[avatar_definition]) ).
fof(f2187,plain,
( ~ spl91_298
| spl91_292
| ~ spl91_63
| ~ spl91_221 ),
inference(avatar_split_clause,[],[f2153,f1656,f597,f2159,f2184]) ).
fof(f2188,plain,
( r1(sK28(sK74),sK36(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_221 ),
inference(resolution,[],[f2135,f1628]) ).
fof(f2196,plain,
( r1(sK28(sK74),sK36(sK28(sK74)))
| ~ spl91_63
| ~ spl91_221 ),
inference(forward_subsumption_resolution,[],[f2188,f1627]) ).
fof(f2197,plain,
( spl91_298
| ~ spl91_63
| ~ spl91_221 ),
inference(avatar_split_clause,[],[f2196,f1656,f597,f2184]) ).
fof(f2233,plain,
( r1(sK36(sK28(sK74)),sK37(sK28(sK74)))
| p2(sK28(sK74))
| ~ spl91_63
| ~ spl91_221 ),
inference(resolution,[],[f2134,f1628]) ).
fof(f2241,plain,
( r1(sK36(sK28(sK74)),sK37(sK28(sK74)))
| ~ spl91_63
| ~ spl91_221 ),
inference(forward_subsumption_resolution,[],[f2233,f1627]) ).
fof(f2283,plain,
( p2(sK37(sK28(sK74)))
| ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(resolution,[],[f2160,f2241]) ).
fof(f2284,plain,
( p2(sK28(sK74))
| ~ r1(sK27(sK74),sK28(sK74))
| ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(resolution,[],[f2283,f2133]) ).
fof(f2326,plain,
( ~ r1(sK27(sK74),sK28(sK74))
| ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(forward_subsumption_resolution,[],[f2284,f1627]) ).
fof(f2327,plain,
( $false
| ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(forward_subsumption_resolution,[],[f2326,f1628]) ).
fof(f2328,plain,
( ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(avatar_contradiction_clause,[],[f2327]) ).
fof(f2336,plain,
( ! [X0,X1] :
( ~ r1(sK22(sK64),X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ p2(X0)
| sP20(sK64) )
| ~ spl91_60 ),
inference(resolution,[],[f587,f101]) ).
fof(f2339,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| r1(sK25(X1),sK26(X1))
| ~ r1(sK64,X0) )
| ~ spl91_131 ),
inference(resolution,[],[f995,f106]) ).
fof(f2341,plain,
( ! [X0,X1] :
( ~ p2(sK26(X1))
| p2(X1)
| ~ r1(X0,X1)
| ~ r1(sK64,X0) )
| ~ spl91_131 ),
inference(resolution,[],[f995,f105]) ).
fof(f2351,plain,
( p2(sK68)
| ~ r1(sK64,sK68)
| ~ spl91_192 ),
inference(resolution,[],[f1419,f230]) ).
fof(f2371,plain,
( ~ r1(sK64,sK68)
| ~ spl91_192 ),
inference(forward_subsumption_resolution,[],[f2351,f298]) ).
fof(f2372,plain,
( $false
| ~ spl91_192 ),
inference(forward_subsumption_resolution,[],[f2371,f299]) ).
fof(f2373,plain,
~ spl91_192,
inference(avatar_contradiction_clause,[],[f2372]) ).
fof(f2490,plain,
( p2(sK90(sK68))
| r1(sK25(sK90(sK68)),sK26(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ spl91_131 ),
inference(resolution,[],[f2339,f685]) ).
fof(f2496,plain,
( r1(sK25(sK90(sK68)),sK26(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ spl91_131
| spl91_192 ),
inference(forward_subsumption_resolution,[],[f2490,f1418]) ).
fof(f2498,plain,
( r1(sK25(sK90(sK68)),sK26(sK90(sK68)))
| ~ spl91_131
| spl91_192 ),
inference(forward_subsumption_resolution,[],[f2496,f299]) ).
fof(f2526,plain,
( ! [X0,X1] :
( p2(X0)
| ~ r1(sK90(X0),sK25(sK90(sK68)))
| ~ r1(sK25(sK90(sK68)),X1)
| p2(X1)
| ~ r1(sK64,X0) )
| ~ spl91_191 ),
inference(resolution,[],[f1415,f229]) ).
fof(f2528,definition,
( spl91_345
<=> ! [X1] :
( ~ r1(sK25(sK90(sK68)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_345])],[avatar_definition]) ).
fof(f2529,plain,
( ! [X1] :
( ~ r1(sK25(sK90(sK68)),X1)
| p2(X1) )
| ~ spl91_345 ),
inference(avatar_component_clause,[],[f2528]) ).
fof(f2531,definition,
( spl91_346
<=> ! [X0] :
( p2(X0)
| ~ r1(sK64,X0)
| ~ r1(sK90(X0),sK25(sK90(sK68))) ) ),
introduced(definition,[new_symbols(definition,[spl91_346])],[avatar_definition]) ).
fof(f2532,plain,
( ! [X0] :
( ~ r1(sK64,X0)
| p2(X0)
| ~ r1(sK90(X0),sK25(sK90(sK68))) )
| ~ spl91_346 ),
inference(avatar_component_clause,[],[f2531]) ).
fof(f2533,plain,
( spl91_345
| spl91_346
| ~ spl91_191 ),
inference(avatar_split_clause,[],[f2526,f1413,f2531,f2528]) ).
fof(f2580,definition,
( spl91_355
<=> p2(sK26(sK90(sK68))) ),
introduced(definition,[new_symbols(definition,[spl91_355])],[avatar_definition]) ).
fof(f2582,plain,
( p2(sK26(sK90(sK68)))
| ~ spl91_355 ),
inference(avatar_component_clause,[],[f2580]) ).
fof(f2628,plain,
( p2(sK26(sK90(sK68)))
| ~ spl91_131
| spl91_192
| ~ spl91_345 ),
inference(resolution,[],[f2529,f2498]) ).
fof(f2629,plain,
( spl91_355
| ~ spl91_131
| spl91_192
| ~ spl91_345 ),
inference(avatar_split_clause,[],[f2628,f2528,f1417,f993,f2580]) ).
fof(f2630,plain,
( ! [X0] :
( p2(sK90(sK68))
| ~ r1(X0,sK90(sK68))
| ~ r1(sK64,X0) )
| ~ spl91_131
| ~ spl91_355 ),
inference(resolution,[],[f2582,f2341]) ).
fof(f2650,plain,
( ! [X0] :
( ~ r1(X0,sK90(sK68))
| ~ r1(sK64,X0) )
| ~ spl91_131
| spl91_192
| ~ spl91_355 ),
inference(forward_subsumption_resolution,[],[f2630,f1418]) ).
fof(f2659,plain,
( ~ r1(sK64,sK68)
| ~ spl91_131
| spl91_192
| ~ spl91_355 ),
inference(resolution,[],[f2650,f685]) ).
fof(f2660,plain,
( $false
| ~ spl91_131
| spl91_192
| ~ spl91_355 ),
inference(forward_subsumption_resolution,[],[f2659,f299]) ).
fof(f2661,plain,
( ~ spl91_131
| spl91_192
| ~ spl91_355 ),
inference(avatar_contradiction_clause,[],[f2660]) ).
fof(f2665,plain,
( ! [X0,X1] :
( ~ p2(X0)
| ~ r1(X0,X1)
| p2(X1)
| ~ r1(sK22(sK64),X0) )
| ~ spl91_60
| spl91_131 ),
inference(forward_subsumption_resolution,[],[f2336,f994]) ).
fof(f2671,plain,
( p2(sK22(sK64))
| r1(sK69(sK22(sK64)),sK70(sK22(sK64)))
| ~ spl91_133 ),
inference(resolution,[],[f1015,f296]) ).
fof(f2672,plain,
( p2(sK22(sK64))
| r1(sK22(sK64),sK69(sK22(sK64)))
| ~ spl91_133 ),
inference(resolution,[],[f1015,f297]) ).
fof(f2690,plain,
( r1(sK22(sK64),sK69(sK22(sK64)))
| spl91_132
| ~ spl91_133 ),
inference(forward_subsumption_resolution,[],[f2672,f999]) ).
fof(f2691,plain,
( r1(sK69(sK22(sK64)),sK70(sK22(sK64)))
| spl91_132
| ~ spl91_133 ),
inference(forward_subsumption_resolution,[],[f2671,f999]) ).
fof(f2738,plain,
( ! [X0] :
( ~ r1(sK69(sK22(sK64)),X0)
| p2(X0)
| ~ r1(sK22(sK64),sK69(sK22(sK64))) )
| ~ spl91_60
| spl91_131
| spl91_132
| ~ spl91_133 ),
inference(resolution,[],[f1502,f2665]) ).
fof(f2743,definition,
( spl91_373
<=> ! [X1] :
( ~ r1(sK69(sK22(sK64)),X1)
| p2(X1) ) ),
introduced(definition,[new_symbols(definition,[spl91_373])],[avatar_definition]) ).
fof(f2744,plain,
( ! [X1] :
( ~ r1(sK69(sK22(sK64)),X1)
| p2(X1) )
| ~ spl91_373 ),
inference(avatar_component_clause,[],[f2743]) ).
fof(f2758,plain,
( ! [X0] :
( ~ r1(sK69(sK22(sK64)),X0)
| p2(X0) )
| ~ spl91_60
| spl91_131
| spl91_132
| ~ spl91_133 ),
inference(forward_subsumption_resolution,[],[f2738,f2690]) ).
fof(f2759,plain,
( spl91_373
| ~ spl91_60
| spl91_131
| spl91_132
| ~ spl91_133 ),
inference(avatar_split_clause,[],[f2758,f1013,f997,f993,f585,f2743]) ).
fof(f2760,plain,
( p2(sK70(sK22(sK64)))
| spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(resolution,[],[f2744,f2691]) ).
fof(f2761,plain,
( p2(sK22(sK64))
| ~ r1(sK64,sK22(sK64))
| spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(resolution,[],[f2760,f295]) ).
fof(f2787,plain,
( ~ r1(sK64,sK22(sK64))
| spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(forward_subsumption_resolution,[],[f2761,f999]) ).
fof(f2788,plain,
( $false
| spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(forward_subsumption_resolution,[],[f2787,f1015]) ).
fof(f2789,plain,
( spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(avatar_contradiction_clause,[],[f2788]) ).
fof(f2791,plain,
( ! [X0,X1] :
( ~ r1(X0,X1)
| p2(X1)
| r1(X1,sK25(X1))
| ~ r1(sK64,X0) )
| ~ spl91_131 ),
inference(resolution,[],[f995,f107]) ).
fof(f2827,plain,
( p2(sK90(sK68))
| r1(sK90(sK68),sK25(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ spl91_131 ),
inference(resolution,[],[f2791,f685]) ).
fof(f2834,plain,
( r1(sK90(sK68),sK25(sK90(sK68)))
| ~ r1(sK64,sK68)
| ~ spl91_131
| spl91_192 ),
inference(forward_subsumption_resolution,[],[f2827,f1418]) ).
fof(f2835,plain,
( r1(sK90(sK68),sK25(sK90(sK68)))
| ~ spl91_131
| spl91_192 ),
inference(forward_subsumption_resolution,[],[f2834,f299]) ).
fof(f2865,plain,
( p2(sK68)
| ~ r1(sK90(sK68),sK25(sK90(sK68)))
| ~ spl91_346 ),
inference(resolution,[],[f2532,f299]) ).
fof(f2868,plain,
( ~ r1(sK90(sK68),sK25(sK90(sK68)))
| ~ spl91_346 ),
inference(forward_subsumption_resolution,[],[f2865,f298]) ).
fof(f2869,plain,
( $false
| ~ spl91_131
| spl91_192
| ~ spl91_346 ),
inference(forward_subsumption_resolution,[],[f2868,f2835]) ).
fof(f2870,plain,
( ~ spl91_131
| spl91_192
| ~ spl91_346 ),
inference(avatar_contradiction_clause,[],[f2869]) ).
cnf(s52,plain,
( spl91_59
| spl91_60 ),
inference(sat_conversion,[],[f588]) ).
cnf(s53,plain,
( spl91_60
| spl91_61 ),
inference(sat_conversion,[],[f592]) ).
cnf(s54,plain,
( spl91_60
| spl91_62
| spl91_63 ),
inference(sat_conversion,[],[f600]) ).
cnf(s55,plain,
( spl91_60
| spl91_63
| ~ spl91_64 ),
inference(sat_conversion,[],[f605]) ).
cnf(s56,plain,
( spl91_60
| spl91_65 ),
inference(sat_conversion,[],[f610]) ).
cnf(s95,plain,
( ~ spl91_60
| spl91_131
| ~ spl91_132 ),
inference(sat_conversion,[],[f1000]) ).
cnf(s97,plain,
( ~ spl91_60
| spl91_131
| spl91_133 ),
inference(sat_conversion,[],[f1016]) ).
cnf(s105,plain,
( ~ spl91_62
| spl91_64
| ~ spl91_65
| spl91_141 ),
inference(sat_conversion,[],[f1114]) ).
cnf(s124,plain,
( ~ spl91_63
| spl91_170
| spl91_171 ),
inference(sat_conversion,[],[f1292]) ).
cnf(s132,plain,
( ~ spl91_131
| spl91_191
| spl91_192 ),
inference(sat_conversion,[],[f1420]) ).
cnf(s158,plain,
( spl91_64
| ~ spl91_65
| ~ spl91_141 ),
inference(sat_conversion,[],[f1618]) ).
cnf(s164,plain,
( ~ spl91_61
| ~ spl91_63
| ~ spl91_170
| spl91_220
| spl91_221 ),
inference(sat_conversion,[],[f1659]) ).
cnf(s171,plain,
( ~ spl91_59
| ~ spl91_171
| spl91_222
| spl91_227 ),
inference(sat_conversion,[],[f1705]) ).
cnf(s189,plain,
( ~ spl91_63
| spl91_170
| ~ spl91_222 ),
inference(sat_conversion,[],[f1828]) ).
cnf(s195,plain,
( ~ spl91_63
| ~ spl91_220
| spl91_248
| ~ spl91_254 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s202,plain,
( ~ spl91_63
| ~ spl91_220
| spl91_254 ),
inference(sat_conversion,[],[f1914]) ).
cnf(s216,plain,
( ~ spl91_63
| spl91_170
| spl91_220
| spl91_221
| ~ spl91_227 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s230,plain,
( ~ spl91_63
| ~ spl91_220
| ~ spl91_248 ),
inference(sat_conversion,[],[f2125]) ).
cnf(s242,plain,
( ~ spl91_63
| ~ spl91_221
| spl91_292
| ~ spl91_298 ),
inference(sat_conversion,[],[f2187]) ).
cnf(s244,plain,
( ~ spl91_63
| ~ spl91_221
| spl91_298 ),
inference(sat_conversion,[],[f2197]) ).
cnf(s263,plain,
( ~ spl91_63
| ~ spl91_221
| ~ spl91_292 ),
inference(sat_conversion,[],[f2328]) ).
cnf(s269,plain,
~ spl91_192,
inference(sat_conversion,[],[f2373]) ).
cnf(s280,plain,
( ~ spl91_191
| spl91_345
| spl91_346 ),
inference(sat_conversion,[],[f2533]) ).
cnf(s292,plain,
( ~ spl91_131
| spl91_192
| ~ spl91_345
| spl91_355 ),
inference(sat_conversion,[],[f2629]) ).
cnf(s298,plain,
( ~ spl91_131
| spl91_192
| ~ spl91_355 ),
inference(sat_conversion,[],[f2661]) ).
cnf(s308,plain,
( ~ spl91_60
| spl91_131
| spl91_132
| ~ spl91_133
| spl91_373 ),
inference(sat_conversion,[],[f2759]) ).
cnf(s313,plain,
( spl91_132
| ~ spl91_133
| ~ spl91_373 ),
inference(sat_conversion,[],[f2789]) ).
cnf(s314,plain,
( ~ spl91_131
| spl91_192
| ~ spl91_346 ),
inference(sat_conversion,[],[f2870]) ).
cnf(s315,plain,
( ~ spl91_131
| spl91_191 ),
inference(rat,[],[s132,s269]) ).
cnf(s318,plain,
( spl91_131
| ~ spl91_60 ),
inference(rat,[],[s308,s313,s95,s97]) ).
cnf(s319,plain,
~ spl91_131,
inference(rat,[],[s280,s315,s292,s298,s314,s269]) ).
cnf(s320,plain,
~ spl91_60,
inference(rat,[],[s318,s319]) ).
cnf(s321,plain,
spl91_65,
inference(rat,[],[s56,s320]) ).
cnf(s322,plain,
spl91_61,
inference(rat,[],[s53,s320]) ).
cnf(s323,plain,
spl91_59,
inference(rat,[],[s52,s320]) ).
cnf(s325,plain,
( ~ spl91_221
| ~ spl91_63 ),
inference(rat,[],[s242,s244,s263]) ).
cnf(s326,plain,
( ~ spl91_220
| ~ spl91_63 ),
inference(rat,[],[s195,s202,s230]) ).
cnf(s327,plain,
( spl91_220
| spl91_221
| ~ spl91_63 ),
inference(rat,[],[s171,s216,s189,s124,s164,s322,s323]) ).
cnf(s328,plain,
~ spl91_63,
inference(rat,[],[s327,s326,s325]) ).
cnf(s329,plain,
~ spl91_64,
inference(rat,[],[s55,s320,s328]) ).
cnf(s330,plain,
spl91_62,
inference(rat,[],[s54,s320,s328]) ).
cnf(s331,plain,
~ spl91_141,
inference(rat,[],[s158,s321,s329]) ).
cnf(s332,plain,
$false,
inference(rat,[],[s105,s329,s321,s331,s330]) ).
fof(f2871,plain,
$false,
inference(avatar_sat_refutation,[],[s332]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL642+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.14/0.60 % Computer : n026.cluster.edu
% 0.14/0.60 % Model : x86_64 x86_64
% 0.14/0.60 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.60 % Memory : 8046.5625MB
% 0.14/0.60 % OS : Linux 6.8.0-71-generic
% 0.14/0.60 % CPULimit : 300
% 0.14/0.60 % WCLimit : 300
% 0.14/0.60 % DateTime : Sun Sep 27 16:13:12 UTC 2026
% 0.14/0.60 % CPUTime :
% 0.14/0.60 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.17/0.63 Running first-order model finding
% 0.17/0.63 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
% 0.17/0.73 % (3039197)Will run a generic schedule for satisfiability detection.
% 0.17/0.73 % (3039208)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2243219304:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.73 % (3039203)% WARNING: option uhcvi not known.
% 0.17/0.73 % (3039207)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3839585077:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.73 % (3039202)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2377164384_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.73 % (3039203)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3923478745:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.73 % (3039204)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3747849411:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.73 % (3039205)dis+10_1_sil=32000:sp=arity:random_seed=2677029280:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.73 % (3039206)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1180927659:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.73 % TRYING [1]
% 0.17/0.73 % TRYING [2]
% 0.17/0.73 % TRYING [3]
% 0.17/0.73 % (3039208)Instruction limit reached!
% 0.17/0.73 % (3039208)------------------------------
% 0.17/0.73 % (3039208)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.73 % (3039208)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.73 % (3039208)CaDiCaL version: 2.1.3
% 0.17/0.73 % (3039208)Termination reason: Instruction limit
% 0.17/0.73 % (3039208)Termination phase: Saturation
% 0.17/0.73 % (3039208)Time elapsed: 0.045 s
% 0.17/0.73 % (3039208)Peak memory usage: 14 MB
% 0.17/0.73 % (3039208)Instructions burned: 159 (million)
% 0.17/0.73 % (3039207) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3039197-3039207"...
% 0.17/0.73 % TRYING [4]
% 0.17/0.73 % (3039207)...printing done.
% 0.17/0.73 % (3039207)Refutation found. Thanks to Tanya!
% 0.17/0.73 % SZS status Theorem for theBenchmark
% 0.17/0.73 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.74 % (3039207)------------------------------
% 0.17/0.74 % (3039207)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.74 % (3039207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.74 % (3039207)CaDiCaL version: 2.1.3
% 0.17/0.74 % (3039207)Termination reason: Refutation
% 0.17/0.74 % (3039207)Time elapsed: 0.048 s
% 0.17/0.74 % (3039207)Peak memory usage: 14 MB
% 0.17/0.74 % (3039207)Instructions burned: 79 (million)
% 0.17/0.74 % (3039197)Success in time 0.089 s
% 0.17/0.74 % Vampire exiting
%------------------------------------------------------------------------------