%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n003.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 : Fri Sep 25 02:07:00 PM UTC 2026
% Result : Theorem 44.14s 6.92s
% Output : CNFRefutation 44.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 5
% Syntax : Number of formulae : 243 ( 19 unt; 4 def)
% Number of atoms : 3722 ( 0 equ)
% Maximal formula atoms : 239 ( 15 avg)
% Number of connectives : 6298 (2847 ~;2957 |; 494 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 41 ( 11 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-2 aty)
% Number of functors : 44 ( 44 usr; 9 con; 0-1 aty)
% Number of variables : 1936 ( 0 sgn1739 !; 197 ?; 428 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ~ ( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
& ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) )
| ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ~ ( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
& ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ ( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) )
| ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ( ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ( ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ( ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| p1(X0)
| ~ r1(X1,X0) )
| ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| p1(X1) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ~ ( ! [X146] :
( ( ! [X152] :
( ~ ! [X155] :
( p1(X155)
| ~ r1(X152,X155) )
| ! [X153] :
( ! [X154] :
( p1(X154)
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X146,X152) )
& ( ~ ! [X149] :
( ~ ! [X150] :
( ~ p1(X150)
| ! [X151] :
( p1(X151)
| ~ r1(X150,X151) )
| ~ r1(X149,X150) )
| p1(X149)
| ~ r1(X146,X149) )
| ! [X147] :
( ~ ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
| ~ r1(X146,X147) )
| p1(X146) ) )
| ~ r1(X0,X146) )
& ! [X135] :
( ! [X136] :
( ( ! [X142] :
( ~ ! [X145] :
( p1(X145)
| ~ r1(X142,X145) )
| ! [X143] :
( ! [X144] :
( p1(X144)
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X136,X142) )
& ( ~ ! [X139] :
( ~ ! [X140] :
( ~ p1(X140)
| ! [X141] :
( p1(X141)
| ~ r1(X140,X141) )
| ~ r1(X139,X140) )
| p1(X139)
| ~ r1(X136,X139) )
| ! [X137] :
( ~ ! [X138] :
( p1(X138)
| ~ r1(X137,X138) )
| ~ r1(X136,X137) )
| p1(X136) ) )
| ~ r1(X135,X136) )
| ~ r1(X0,X135) )
& ! [X123] :
( ! [X124] :
( ! [X125] :
( ( ! [X131] :
( ~ ! [X134] :
( p1(X134)
| ~ r1(X131,X134) )
| ! [X132] :
( ! [X133] :
( p1(X133)
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X125,X131) )
& ( ~ ! [X128] :
( ~ ! [X129] :
( ~ p1(X129)
| ! [X130] :
( p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
| p1(X128)
| ~ r1(X125,X128) )
| ! [X126] :
( ~ ! [X127] :
( p1(X127)
| ~ r1(X126,X127) )
| ~ r1(X125,X126) )
| p1(X125) ) )
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X0,X123) )
& ! [X110] :
( ! [X111] :
( ! [X112] :
( ! [X113] :
( ( ! [X119] :
( ~ ! [X122] :
( p1(X122)
| ~ r1(X119,X122) )
| ! [X120] :
( ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X113,X119) )
& ( ~ ! [X116] :
( ~ ! [X117] :
( ~ p1(X117)
| ! [X118] :
( p1(X118)
| ~ r1(X117,X118) )
| ~ r1(X116,X117) )
| p1(X116)
| ~ r1(X113,X116) )
| ! [X114] :
( ~ ! [X115] :
( p1(X115)
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| p1(X113) ) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X0,X110) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( ! [X100] :
( ( ! [X106] :
( ~ ! [X109] :
( p1(X109)
| ~ r1(X106,X109) )
| ! [X107] :
( ! [X108] :
( p1(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X100,X106) )
& ( ~ ! [X103] :
( ~ ! [X104] :
( ~ p1(X104)
| ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| p1(X103)
| ~ r1(X100,X103) )
| ! [X101] :
( ~ ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| p1(X100) ) )
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X0,X96) )
& ~ ! [X84] :
( ! [X85] :
( ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ~ ! [X93] :
( ~ ! [X94] :
( ~ p1(X94)
| ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| p1(X93)
| ~ r1(X89,X93) )
| ! [X91] :
( ~ ! [X92] :
( p1(X92)
| ~ r1(X91,X92) )
| ~ r1(X89,X91) )
| ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) ) )
| ~ ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ~ ! [X81] :
( ~ ! [X82] :
( ~ p1(X82)
| ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| p1(X81)
| ~ r1(X57,X81) )
| ! [X77] :
( ! [X78] :
( ~ ! [X79] :
( ~ p1(X79)
| ! [X80] :
( p1(X80)
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) )
& ! [X73] :
( ~ ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X57,X73) )
& ( ~ ! [X70] :
( ~ ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| p1(X70)
| ~ r1(X57,X70) )
| ! [X68] :
( ~ ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) )
& ( ~ ! [X62] :
( ~ ! [X64] :
( ~ ( ~ p1(X64)
| ! [X67] :
( p1(X67)
| ~ r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
| ~ p1(X62)
| ! [X63] :
( p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X57,X62) )
| ! [X59] :
( ~ ! [X60] :
( ~ p1(X60)
| ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
| ~ ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ~ ! [X51] :
( p1(X51)
| ~ r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ~ ! [X45] :
( ~ ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
| ~ ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ~ ! [X35] :
( p1(X35)
| ~ r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ~ ! [X29] :
( ~ ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| p1(X29)
| ~ r1(X26,X29) )
| ! [X27] :
( ~ ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ~ ! [X18] :
( p1(X18)
| ~ r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ~ ! [X12] :
( ~ ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| p1(X12)
| ~ r1(X9,X12) )
| ! [X10] :
( ~ ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f2]) ).
fof(f4,plain,
? [X0] :
~ ( ~ ( ! [X146] :
( ( ! [X152] :
( ~ ! [X155] :
( p1(X155)
| ~ r1(X152,X155) )
| ! [X153] :
( ! [X154] :
( p1(X154)
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X146,X152) )
& ( ~ ! [X149] :
( ~ ! [X150] :
( ~ p1(X150)
| ! [X151] :
( p1(X151)
| ~ r1(X150,X151) )
| ~ r1(X149,X150) )
| p1(X149)
| ~ r1(X146,X149) )
| ! [X147] :
( ~ ! [X148] :
( p1(X148)
| ~ r1(X147,X148) )
| ~ r1(X146,X147) )
| p1(X146) ) )
| ~ r1(X0,X146) )
& ! [X135] :
( ! [X136] :
( ( ! [X142] :
( ~ ! [X145] :
( p1(X145)
| ~ r1(X142,X145) )
| ! [X143] :
( ! [X144] :
( p1(X144)
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X136,X142) )
& ( ~ ! [X139] :
( ~ ! [X140] :
( ~ p1(X140)
| ! [X141] :
( p1(X141)
| ~ r1(X140,X141) )
| ~ r1(X139,X140) )
| p1(X139)
| ~ r1(X136,X139) )
| ! [X137] :
( ~ ! [X138] :
( p1(X138)
| ~ r1(X137,X138) )
| ~ r1(X136,X137) )
| p1(X136) ) )
| ~ r1(X135,X136) )
| ~ r1(X0,X135) )
& ! [X123] :
( ! [X124] :
( ! [X125] :
( ( ! [X131] :
( ~ ! [X134] :
( p1(X134)
| ~ r1(X131,X134) )
| ! [X132] :
( ! [X133] :
( p1(X133)
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X125,X131) )
& ( ~ ! [X128] :
( ~ ! [X129] :
( ~ p1(X129)
| ! [X130] :
( p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
| p1(X128)
| ~ r1(X125,X128) )
| ! [X126] :
( ~ ! [X127] :
( p1(X127)
| ~ r1(X126,X127) )
| ~ r1(X125,X126) )
| p1(X125) ) )
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X0,X123) )
& ! [X110] :
( ! [X111] :
( ! [X112] :
( ! [X113] :
( ( ! [X119] :
( ~ ! [X122] :
( p1(X122)
| ~ r1(X119,X122) )
| ! [X120] :
( ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X113,X119) )
& ( ~ ! [X116] :
( ~ ! [X117] :
( ~ p1(X117)
| ! [X118] :
( p1(X118)
| ~ r1(X117,X118) )
| ~ r1(X116,X117) )
| p1(X116)
| ~ r1(X113,X116) )
| ! [X114] :
( ~ ! [X115] :
( p1(X115)
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| p1(X113) ) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X0,X110) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( ! [X100] :
( ( ! [X106] :
( ~ ! [X109] :
( p1(X109)
| ~ r1(X106,X109) )
| ! [X107] :
( ! [X108] :
( p1(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X100,X106) )
& ( ~ ! [X103] :
( ~ ! [X104] :
( ~ p1(X104)
| ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| p1(X103)
| ~ r1(X100,X103) )
| ! [X101] :
( ~ ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| p1(X100) ) )
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X0,X96) )
& ~ ! [X84] :
( ! [X85] :
( ! [X86] :
( ! [X87] :
( ! [X88] :
( ! [X89] :
( ~ ! [X93] :
( ~ ! [X94] :
( ~ p1(X94)
| ! [X95] :
( p1(X95)
| ~ r1(X94,X95) )
| ~ r1(X93,X94) )
| p1(X93)
| ~ r1(X89,X93) )
| ! [X91] :
( ~ ! [X92] :
( p1(X92)
| ~ r1(X91,X92) )
| ~ r1(X89,X91) )
| ! [X90] :
( p1(X90)
| ~ r1(X89,X90) )
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) ) )
| ~ ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ~ ! [X81] :
( ~ ! [X82] :
( ~ p1(X82)
| ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
| p1(X81)
| ~ r1(X57,X81) )
| ! [X77] :
( ! [X78] :
( ~ ! [X79] :
( ~ p1(X79)
| ! [X80] :
( p1(X80)
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) )
& ! [X73] :
( ~ ! [X76] :
( p1(X76)
| ~ r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X57,X73) )
& ( ~ ! [X70] :
( ~ ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
| p1(X70)
| ~ r1(X57,X70) )
| ! [X68] :
( ~ ! [X69] :
( p1(X69)
| ~ r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) )
& ( ~ ! [X62] :
( ~ ! [X64] :
( ~ ( ~ p1(X64)
| ! [X67] :
( p1(X67)
| ~ r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
| ~ p1(X62)
| ! [X63] :
( p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X57,X62) )
| ! [X59] :
( ~ ! [X60] :
( ~ p1(X60)
| ! [X61] :
( p1(X61)
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
| ~ ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ~ ! [X51] :
( p1(X51)
| ~ r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ~ ! [X45] :
( ~ ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| p1(X45)
| ~ r1(X42,X45) )
| ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
| ~ ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ~ ! [X35] :
( p1(X35)
| ~ r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ~ ! [X29] :
( ~ ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| p1(X29)
| ~ r1(X26,X29) )
| ! [X27] :
( ~ ! [X28] :
( p1(X28)
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ~ ! [X18] :
( p1(X18)
| ~ r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ~ ! [X12] :
( ~ ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
| p1(X12)
| ~ r1(X9,X12) )
| ! [X10] :
( ~ ! [X11] :
( p1(X11)
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f3]) ).
fof(f5,plain,
? [X0] :
( ! [X146] :
( ( ! [X152] :
( ? [X155] :
( ~ p1(X155)
& r1(X152,X155) )
| ! [X153] :
( ! [X154] :
( p1(X154)
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X146,X152) )
& ( ? [X149] :
( ! [X150] :
( ~ p1(X150)
| ! [X151] :
( p1(X151)
| ~ r1(X150,X151) )
| ~ r1(X149,X150) )
& ~ p1(X149)
& r1(X146,X149) )
| ! [X147] :
( ? [X148] :
( ~ p1(X148)
& r1(X147,X148) )
| ~ r1(X146,X147) )
| p1(X146) ) )
| ~ r1(X0,X146) )
& ! [X135] :
( ! [X136] :
( ( ! [X142] :
( ? [X145] :
( ~ p1(X145)
& r1(X142,X145) )
| ! [X143] :
( ! [X144] :
( p1(X144)
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X136,X142) )
& ( ? [X139] :
( ! [X140] :
( ~ p1(X140)
| ! [X141] :
( p1(X141)
| ~ r1(X140,X141) )
| ~ r1(X139,X140) )
& ~ p1(X139)
& r1(X136,X139) )
| ! [X137] :
( ? [X138] :
( ~ p1(X138)
& r1(X137,X138) )
| ~ r1(X136,X137) )
| p1(X136) ) )
| ~ r1(X135,X136) )
| ~ r1(X0,X135) )
& ! [X123] :
( ! [X124] :
( ! [X125] :
( ( ! [X131] :
( ? [X134] :
( ~ p1(X134)
& r1(X131,X134) )
| ! [X132] :
( ! [X133] :
( p1(X133)
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X125,X131) )
& ( ? [X128] :
( ! [X129] :
( ~ p1(X129)
| ! [X130] :
( p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
& ~ p1(X128)
& r1(X125,X128) )
| ! [X126] :
( ? [X127] :
( ~ p1(X127)
& r1(X126,X127) )
| ~ r1(X125,X126) )
| p1(X125) ) )
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X0,X123) )
& ! [X110] :
( ! [X111] :
( ! [X112] :
( ! [X113] :
( ( ! [X119] :
( ? [X122] :
( ~ p1(X122)
& r1(X119,X122) )
| ! [X120] :
( ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X113,X119) )
& ( ? [X116] :
( ! [X117] :
( ~ p1(X117)
| ! [X118] :
( p1(X118)
| ~ r1(X117,X118) )
| ~ r1(X116,X117) )
& ~ p1(X116)
& r1(X113,X116) )
| ! [X114] :
( ? [X115] :
( ~ p1(X115)
& r1(X114,X115) )
| ~ r1(X113,X114) )
| p1(X113) ) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X0,X110) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( ! [X100] :
( ( ! [X106] :
( ? [X109] :
( ~ p1(X109)
& r1(X106,X109) )
| ! [X107] :
( ! [X108] :
( p1(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X100,X106) )
& ( ? [X103] :
( ! [X104] :
( ~ p1(X104)
| ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
& ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ? [X102] :
( ~ p1(X102)
& r1(X101,X102) )
| ~ r1(X100,X101) )
| p1(X100) ) )
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X0,X96) )
& ? [X84] :
( ? [X85] :
( ? [X86] :
( ? [X87] :
( ? [X88] :
( ? [X89] :
( ! [X93] :
( ? [X94] :
( p1(X94)
& ? [X95] :
( ~ p1(X95)
& r1(X94,X95) )
& r1(X93,X94) )
| p1(X93)
| ~ r1(X89,X93) )
& ? [X91] :
( ! [X92] :
( p1(X92)
| ~ r1(X91,X92) )
& r1(X89,X91) )
& ? [X90] :
( ~ p1(X90)
& r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X86,X87) )
& r1(X85,X86) )
& r1(X84,X85) )
& r1(X0,X84) )
& ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ? [X81] :
( ! [X82] :
( ~ p1(X82)
| ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
& ~ p1(X81)
& r1(X57,X81) )
| ! [X77] :
( ! [X78] :
( ? [X79] :
( p1(X79)
& ? [X80] :
( ~ p1(X80)
& r1(X79,X80) )
& r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) )
& ! [X73] :
( ? [X76] :
( ~ p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X57,X73) )
& ( ? [X70] :
( ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
& ~ p1(X70)
& r1(X57,X70) )
| ! [X68] :
( ? [X69] :
( ~ p1(X69)
& r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) )
& ( ? [X62] :
( ! [X64] :
( ( p1(X64)
& ? [X67] :
( ~ p1(X67)
& r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
& p1(X62)
& ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
& r1(X57,X62) )
| ! [X59] :
( ? [X60] :
( p1(X60)
& ? [X61] :
( ~ p1(X61)
& r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
& ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ? [X51] :
( ~ p1(X51)
& r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ? [X45] :
( ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p1(X45)
& r1(X42,X45) )
| ! [X43] :
( ? [X44] :
( ~ p1(X44)
& r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
& ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ? [X35] :
( ~ p1(X35)
& r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ? [X29] :
( ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
& ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ? [X28] :
( ~ p1(X28)
& r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ? [X18] :
( ~ p1(X18)
& r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ? [X12] :
( ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
& ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ? [X11] :
( ~ p1(X11)
& r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(ennf_transformation,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ! [X146] :
( ( ! [X152] :
( ? [X155] :
( ~ p1(X155)
& r1(X152,X155) )
| ! [X153] :
( ! [X154] :
( p1(X154)
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X146,X152) )
& ( ? [X149] :
( ! [X150] :
( ~ p1(X150)
| ! [X151] :
( p1(X151)
| ~ r1(X150,X151) )
| ~ r1(X149,X150) )
& ~ p1(X149)
& r1(X146,X149) )
| ! [X147] :
( ? [X148] :
( ~ p1(X148)
& r1(X147,X148) )
| ~ r1(X146,X147) )
| p1(X146) ) )
| ~ r1(X0,X146) )
& ! [X135] :
( ! [X136] :
( ( ! [X142] :
( ? [X145] :
( ~ p1(X145)
& r1(X142,X145) )
| ! [X143] :
( ! [X144] :
( p1(X144)
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X136,X142) )
& ( ? [X139] :
( ! [X140] :
( ~ p1(X140)
| ! [X141] :
( p1(X141)
| ~ r1(X140,X141) )
| ~ r1(X139,X140) )
& ~ p1(X139)
& r1(X136,X139) )
| ! [X137] :
( ? [X138] :
( ~ p1(X138)
& r1(X137,X138) )
| ~ r1(X136,X137) )
| p1(X136) ) )
| ~ r1(X135,X136) )
| ~ r1(X0,X135) )
& ! [X123] :
( ! [X124] :
( ! [X125] :
( ( ! [X131] :
( ? [X134] :
( ~ p1(X134)
& r1(X131,X134) )
| ! [X132] :
( ! [X133] :
( p1(X133)
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X125,X131) )
& ( ? [X128] :
( ! [X129] :
( ~ p1(X129)
| ! [X130] :
( p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
& ~ p1(X128)
& r1(X125,X128) )
| ! [X126] :
( ? [X127] :
( ~ p1(X127)
& r1(X126,X127) )
| ~ r1(X125,X126) )
| p1(X125) ) )
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X0,X123) )
& ! [X110] :
( ! [X111] :
( ! [X112] :
( ! [X113] :
( ( ! [X119] :
( ? [X122] :
( ~ p1(X122)
& r1(X119,X122) )
| ! [X120] :
( ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X113,X119) )
& ( ? [X116] :
( ! [X117] :
( ~ p1(X117)
| ! [X118] :
( p1(X118)
| ~ r1(X117,X118) )
| ~ r1(X116,X117) )
& ~ p1(X116)
& r1(X113,X116) )
| ! [X114] :
( ? [X115] :
( ~ p1(X115)
& r1(X114,X115) )
| ~ r1(X113,X114) )
| p1(X113) ) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X0,X110) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( ! [X100] :
( ( ! [X106] :
( ? [X109] :
( ~ p1(X109)
& r1(X106,X109) )
| ! [X107] :
( ! [X108] :
( p1(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X100,X106) )
& ( ? [X103] :
( ! [X104] :
( ~ p1(X104)
| ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
& ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ? [X102] :
( ~ p1(X102)
& r1(X101,X102) )
| ~ r1(X100,X101) )
| p1(X100) ) )
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X0,X96) )
& ? [X84] :
( ? [X85] :
( ? [X86] :
( ? [X87] :
( ? [X88] :
( ? [X89] :
( ! [X93] :
( ? [X94] :
( p1(X94)
& ? [X95] :
( ~ p1(X95)
& r1(X94,X95) )
& r1(X93,X94) )
| p1(X93)
| ~ r1(X89,X93) )
& ? [X91] :
( ! [X92] :
( p1(X92)
| ~ r1(X91,X92) )
& r1(X89,X91) )
& ? [X90] :
( ~ p1(X90)
& r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X86,X87) )
& r1(X85,X86) )
& r1(X84,X85) )
& r1(X0,X84) )
& ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ? [X81] :
( ! [X82] :
( ~ p1(X82)
| ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
& ~ p1(X81)
& r1(X57,X81) )
| ! [X77] :
( ! [X78] :
( ? [X79] :
( p1(X79)
& ? [X80] :
( ~ p1(X80)
& r1(X79,X80) )
& r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) )
& ! [X73] :
( ? [X76] :
( ~ p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X57,X73) )
& ( ? [X70] :
( ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
& ~ p1(X70)
& r1(X57,X70) )
| ! [X68] :
( ? [X69] :
( ~ p1(X69)
& r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) )
& ( ? [X62] :
( ! [X64] :
( ( p1(X64)
& ? [X67] :
( ~ p1(X67)
& r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
& p1(X62)
& ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
& r1(X57,X62) )
| ! [X59] :
( ? [X60] :
( p1(X60)
& ? [X61] :
( ~ p1(X61)
& r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
& ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ? [X51] :
( ~ p1(X51)
& r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ? [X45] :
( ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p1(X45)
& r1(X42,X45) )
| ! [X43] :
( ? [X44] :
( ~ p1(X44)
& r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
& ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ? [X35] :
( ~ p1(X35)
& r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ? [X29] :
( ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
& ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ? [X28] :
( ~ p1(X28)
& r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ? [X18] :
( ~ p1(X18)
& r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ? [X12] :
( ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
& ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ? [X11] :
( ~ p1(X11)
& r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f5]) ).
fof(f12,plain,
! [X57] :
( ~ sP3(X57)
| sP1(X57)
| ! [X59] :
( ? [X60] :
( p1(X60)
& ? [X61] :
( ~ p1(X61)
& r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f13,plain,
! [X0] :
( ~ sP3(X0)
| sP1(X0)
| ! [X2] :
( ? [X3] :
( p1(X3)
& ? [X4] :
( ~ p1(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| ~ r1(X0,X2) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f12]) ).
fof(f14,plain,
! [X0] :
( ~ sP3(X0)
| sP1(X0)
| ! [X2] :
( ( p1(sK4(X2))
& ~ p1(sK5(X2))
& r1(sK4(X2),sK5(X2))
& r1(X2,sK4(X2)) )
| ~ r1(X0,X2) )
| ~ p1(X0)
| ! [X1] :
( p1(X1)
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X2)),skolemize(X4,sK5(X2))],[f13]) ).
fof(f15,plain,
! [X57] :
( ~ sP2(X57)
| ? [X70] :
( ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
& ~ p1(X70)
& r1(X57,X70) )
| ! [X68] :
( ? [X69] :
( ~ p1(X69)
& r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) ),
inference(nnf_transformation,[],[f9]) ).
fof(f16,plain,
! [X0] :
( ~ sP2(X0)
| ? [X3] :
( ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
& ~ p1(X3)
& r1(X0,X3) )
| ! [X1] :
( ? [X2] :
( ~ p1(X2)
& r1(X1,X2) )
| ~ r1(X0,X1) )
| p1(X0) ),
inference(rectify,[],[f15]) ).
fof(f17,plain,
! [X0] :
( ~ sP2(X0)
| ( ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(sK7(X0),X4) )
& ~ p1(sK7(X0))
& r1(X0,sK7(X0)) )
| ! [X1] :
( ( ~ p1(sK6(X1))
& r1(X1,sK6(X1)) )
| ~ r1(X0,X1) )
| p1(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6,sK7]),skolemize(X2,sK6(X1)),skolemize(X3,sK7(X0))],[f16]) ).
fof(f18,plain,
! [X57] :
( ~ sP1(X57)
| ? [X62] :
( ! [X64] :
( ( p1(X64)
& ? [X67] :
( ~ p1(X67)
& r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
& p1(X62)
& ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
& r1(X57,X62) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f19,plain,
! [X0] :
( ~ sP1(X0)
| ? [X1] :
( ! [X3] :
( ( p1(X3)
& ? [X6] :
( ~ p1(X6)
& r1(X3,X6) ) )
| ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X1,X3) )
& p1(X1)
& ? [X2] :
( ~ p1(X2)
& r1(X1,X2) )
& r1(X0,X1) ) ),
inference(rectify,[],[f18]) ).
fof(f20,plain,
! [X0] :
( ~ sP1(X0)
| ( ! [X3] :
( ( p1(X3)
& ~ p1(sK10(X3))
& r1(X3,sK10(X3)) )
| ! [X4] :
( ~ p1(X4)
| ! [X5] :
( p1(X5)
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(sK8(X0),X3) )
& p1(sK8(X0))
& ~ p1(sK9(X0))
& r1(sK8(X0),sK9(X0))
& r1(X0,sK8(X0)) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8,sK9,sK10]),skolemize(X1,sK8(X0)),skolemize(X2,sK9(X0)),skolemize(X6,sK10(X3))],[f19]) ).
fof(f24,plain,
? [X0] :
( ! [X127] :
( ( ! [X133] :
( ? [X136] :
( ~ p1(X136)
& r1(X133,X136) )
| ! [X134] :
( ! [X135] :
( p1(X135)
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X127,X133) )
& ( ? [X130] :
( ! [X131] :
( ~ p1(X131)
| ! [X132] :
( p1(X132)
| ~ r1(X131,X132) )
| ~ r1(X130,X131) )
& ~ p1(X130)
& r1(X127,X130) )
| ! [X128] :
( ? [X129] :
( ~ p1(X129)
& r1(X128,X129) )
| ~ r1(X127,X128) )
| p1(X127) ) )
| ~ r1(X0,X127) )
& ! [X116] :
( ! [X117] :
( ( ! [X123] :
( ? [X126] :
( ~ p1(X126)
& r1(X123,X126) )
| ! [X124] :
( ! [X125] :
( p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X117,X123) )
& ( ? [X120] :
( ! [X121] :
( ~ p1(X121)
| ! [X122] :
( p1(X122)
| ~ r1(X121,X122) )
| ~ r1(X120,X121) )
& ~ p1(X120)
& r1(X117,X120) )
| ! [X118] :
( ? [X119] :
( ~ p1(X119)
& r1(X118,X119) )
| ~ r1(X117,X118) )
| p1(X117) ) )
| ~ r1(X116,X117) )
| ~ r1(X0,X116) )
& ! [X104] :
( ! [X105] :
( ! [X106] :
( ( ! [X112] :
( ? [X115] :
( ~ p1(X115)
& r1(X112,X115) )
| ! [X113] :
( ! [X114] :
( p1(X114)
| ~ r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X106,X112) )
& ( ? [X109] :
( ! [X110] :
( ~ p1(X110)
| ! [X111] :
( p1(X111)
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
& ~ p1(X109)
& r1(X106,X109) )
| ! [X107] :
( ? [X108] :
( ~ p1(X108)
& r1(X107,X108) )
| ~ r1(X106,X107) )
| p1(X106) ) )
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X0,X104) )
& ! [X91] :
( ! [X92] :
( ! [X93] :
( ! [X94] :
( ( ! [X100] :
( ? [X103] :
( ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X94,X100) )
& ( ? [X97] :
( ! [X98] :
( ~ p1(X98)
| ! [X99] :
( p1(X99)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
& ~ p1(X97)
& r1(X94,X97) )
| ! [X95] :
( ? [X96] :
( ~ p1(X96)
& r1(X95,X96) )
| ~ r1(X94,X95) )
| p1(X94) ) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(X0,X91) )
& ! [X77] :
( ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ( ! [X87] :
( ? [X90] :
( ~ p1(X90)
& r1(X87,X90) )
| ! [X88] :
( ! [X89] :
( p1(X89)
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X81,X87) )
& ( ? [X84] :
( ! [X85] :
( ~ p1(X85)
| ! [X86] :
( p1(X86)
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
& ~ p1(X84)
& r1(X81,X84) )
| ! [X82] :
( ? [X83] :
( ~ p1(X83)
& r1(X82,X83) )
| ~ r1(X81,X82) )
| p1(X81) ) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(X0,X77) )
& ? [X65] :
( ? [X66] :
( ? [X67] :
( ? [X68] :
( ? [X69] :
( ? [X70] :
( ! [X74] :
( ? [X75] :
( p1(X75)
& ? [X76] :
( ~ p1(X76)
& r1(X75,X76) )
& r1(X74,X75) )
| p1(X74)
| ~ r1(X70,X74) )
& ? [X72] :
( ! [X73] :
( p1(X73)
| ~ r1(X72,X73) )
& r1(X70,X72) )
& ? [X71] :
( ~ p1(X71)
& r1(X70,X71) )
& r1(X69,X70) )
& r1(X68,X69) )
& r1(X67,X68) )
& r1(X66,X67) )
& r1(X65,X66) )
& r1(X0,X65) )
& ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ? [X62] :
( ! [X63] :
( ~ p1(X63)
| ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(X62,X63) )
& ~ p1(X62)
& r1(X57,X62) )
| sP0(X57) )
& ! [X58] :
( ? [X61] :
( ~ p1(X61)
& r1(X58,X61) )
| ! [X59] :
( ! [X60] :
( p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
& sP2(X57)
& sP3(X57) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
& ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ? [X51] :
( ~ p1(X51)
& r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ? [X45] :
( ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p1(X45)
& r1(X42,X45) )
| ! [X43] :
( ? [X44] :
( ~ p1(X44)
& r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
& ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ? [X35] :
( ~ p1(X35)
& r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ? [X29] :
( ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
& ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ? [X28] :
( ~ p1(X28)
& r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ? [X18] :
( ~ p1(X18)
& r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ? [X12] :
( ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
& ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ? [X11] :
( ~ p1(X11)
& r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f11]) ).
fof(f25,plain,
( ! [X127] :
( ( ! [X133] :
( ( ~ p1(sK49(X133))
& r1(X133,sK49(X133)) )
| ! [X134] :
( ! [X135] :
( p1(X135)
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X127,X133) )
& ( ( ! [X131] :
( ~ p1(X131)
| ! [X132] :
( p1(X132)
| ~ r1(X131,X132) )
| ~ r1(sK48(X127),X131) )
& ~ p1(sK48(X127))
& r1(X127,sK48(X127)) )
| ! [X128] :
( ( ~ p1(sK47(X128))
& r1(X128,sK47(X128)) )
| ~ r1(X127,X128) )
| p1(X127) ) )
| ~ r1(sK13,X127) )
& ! [X116] :
( ! [X117] :
( ( ! [X123] :
( ( ~ p1(sK46(X123))
& r1(X123,sK46(X123)) )
| ! [X124] :
( ! [X125] :
( p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X117,X123) )
& ( ( ! [X121] :
( ~ p1(X121)
| ! [X122] :
( p1(X122)
| ~ r1(X121,X122) )
| ~ r1(sK45(X117),X121) )
& ~ p1(sK45(X117))
& r1(X117,sK45(X117)) )
| ! [X118] :
( ( ~ p1(sK44(X118))
& r1(X118,sK44(X118)) )
| ~ r1(X117,X118) )
| p1(X117) ) )
| ~ r1(X116,X117) )
| ~ r1(sK13,X116) )
& ! [X104] :
( ! [X105] :
( ! [X106] :
( ( ! [X112] :
( ( ~ p1(sK43(X112))
& r1(X112,sK43(X112)) )
| ! [X113] :
( ! [X114] :
( p1(X114)
| ~ r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X106,X112) )
& ( ( ! [X110] :
( ~ p1(X110)
| ! [X111] :
( p1(X111)
| ~ r1(X110,X111) )
| ~ r1(sK42(X106),X110) )
& ~ p1(sK42(X106))
& r1(X106,sK42(X106)) )
| ! [X107] :
( ( ~ p1(sK41(X107))
& r1(X107,sK41(X107)) )
| ~ r1(X106,X107) )
| p1(X106) ) )
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(sK13,X104) )
& ! [X91] :
( ! [X92] :
( ! [X93] :
( ! [X94] :
( ( ! [X100] :
( ( ~ p1(sK40(X100))
& r1(X100,sK40(X100)) )
| ! [X101] :
( ! [X102] :
( p1(X102)
| ~ r1(X101,X102) )
| ~ r1(X100,X101) )
| ~ r1(X94,X100) )
& ( ( ! [X98] :
( ~ p1(X98)
| ! [X99] :
( p1(X99)
| ~ r1(X98,X99) )
| ~ r1(sK39(X94),X98) )
& ~ p1(sK39(X94))
& r1(X94,sK39(X94)) )
| ! [X95] :
( ( ~ p1(sK38(X95))
& r1(X95,sK38(X95)) )
| ~ r1(X94,X95) )
| p1(X94) ) )
| ~ r1(X93,X94) )
| ~ r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(sK13,X91) )
& ! [X77] :
( ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ( ! [X87] :
( ( ~ p1(sK37(X87))
& r1(X87,sK37(X87)) )
| ! [X88] :
( ! [X89] :
( p1(X89)
| ~ r1(X88,X89) )
| ~ r1(X87,X88) )
| ~ r1(X81,X87) )
& ( ( ! [X85] :
( ~ p1(X85)
| ! [X86] :
( p1(X86)
| ~ r1(X85,X86) )
| ~ r1(sK36(X81),X85) )
& ~ p1(sK36(X81))
& r1(X81,sK36(X81)) )
| ! [X82] :
( ( ~ p1(sK35(X82))
& r1(X82,sK35(X82)) )
| ~ r1(X81,X82) )
| p1(X81) ) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X77,X78) )
| ~ r1(sK13,X77) )
& ! [X74] :
( ( p1(sK33(X74))
& ~ p1(sK34(X74))
& r1(sK33(X74),sK34(X74))
& r1(X74,sK33(X74)) )
| p1(X74)
| ~ r1(sK30,X74) )
& ! [X73] :
( p1(X73)
| ~ r1(sK32,X73) )
& r1(sK30,sK32)
& ~ p1(sK31)
& r1(sK30,sK31)
& r1(sK29,sK30)
& r1(sK28,sK29)
& r1(sK27,sK28)
& r1(sK26,sK27)
& r1(sK25,sK26)
& r1(sK13,sK25)
& ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ( ! [X63] :
( ~ p1(X63)
| ! [X64] :
( p1(X64)
| ~ r1(X63,X64) )
| ~ r1(sK24(X57),X63) )
& ~ p1(sK24(X57))
& r1(X57,sK24(X57)) )
| sP0(X57) )
& ! [X58] :
( ( ~ p1(sK23(X58))
& r1(X58,sK23(X58)) )
| ! [X59] :
( ! [X60] :
( p1(X60)
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
& sP2(X57)
& sP3(X57) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(sK13,X52) )
& ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ( ~ p1(sK22(X48))
& r1(X48,sK22(X48)) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ( ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(sK21(X42),X46) )
& ~ p1(sK21(X42))
& r1(X42,sK21(X42)) )
| ! [X43] :
( ( ~ p1(sK20(X43))
& r1(X43,sK20(X43)) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(sK13,X36) )
& ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ( ~ p1(sK19(X32))
& r1(X32,sK19(X32)) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ( ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(sK18(X26),X30) )
& ~ p1(sK18(X26))
& r1(X26,sK18(X26)) )
| ! [X27] :
( ( ~ p1(sK17(X27))
& r1(X27,sK17(X27)) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(sK13,X19) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ( ~ p1(sK16(X15))
& r1(X15,sK16(X15)) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ( ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(sK15(X9),X13) )
& ~ p1(sK15(X9))
& r1(X9,sK15(X9)) )
| ! [X10] :
( ( ~ p1(sK14(X10))
& r1(X10,sK14(X10)) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK13,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13,sK14,sK15,sK16,sK17,sK18,sK19,sK20,sK21,sK22,sK23,sK24,sK25,sK26,sK27,sK28,sK29,sK30,sK31,sK32,sK33,sK34,sK35,sK36,sK37,sK38,sK39,sK40,sK41,sK42,sK43,sK44,sK45,sK46,sK47,sK48,sK49]),skolemize(X0,sK13),skolemize(X11,sK14(X10)),skolemize(X12,sK15(X9)),skolemize(X18,sK16(X15)),skolemize(X28,sK17(X27)),skolemize(X29,sK18(X26)),skolemize(X35,sK19(X32)),skolemize(X44,sK20(X43)),skolemize(X45,sK21(X42)),skolemize(X51,sK22(X48)),skolemize(X61,sK23(X58)),skolemize(X62,sK24(X57)),skolemize(X65,sK25),skolemize(X66,sK26),skolemize(X67,sK27),skolemize(X68,sK28),skolemize(X69,sK29),skolemize(X70,sK30),skolemize(X71,sK31),skolemize(X72,sK32),skolemize(X75,sK33(X74)),skolemize(X76,sK34(X74)),skolemize(X83,sK35(X82)),skolemize(X84,sK36(X81)),skolemize(X90,sK37(X87)),skolemize(X96,sK38(X95)),skolemize(X97,sK39(X94)),skolemize(X103,sK40(X100)),skolemize(X108,sK41(X107)),skolemize(X109,sK42(X106)),skolemize(X115,sK43(X112)),skolemize(X119,sK44(X118)),skolemize(X120,sK45(X117)),skolemize(X126,sK46(X123)),skolemize(X129,sK47(X128)),skolemize(X130,sK48(X127)),skolemize(X136,sK49(X133))],[f24]) ).
fof(f27,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| ~ p1(sK5(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| r1(sK4(X2),sK5(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ sP3(X0)
| sP1(X0)
| r1(X2,sK4(X2))
| ~ r1(X0,X2)
| ~ p1(X0)
| p1(X1)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f14]) ).
fof(f30,plain,
! [X0,X1,X4,X5] :
( ~ sP2(X0)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK7(X0),X4)
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f31,plain,
! [X0,X1] :
( ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f32,plain,
! [X0,X1] :
( ~ sP2(X0)
| r1(X0,sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f33,plain,
! [X0,X1,X4,X5] :
( ~ sP2(X0)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(sK7(X0),X4)
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f34,plain,
! [X0,X1] :
( ~ sP2(X0)
| ~ p1(sK7(X0))
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f35,plain,
! [X0,X1] :
( ~ sP2(X0)
| r1(X0,sK7(X0))
| r1(X1,sK6(X1))
| ~ r1(X0,X1)
| p1(X0) ),
inference(cnf_transformation,[],[f17]) ).
fof(f36,plain,
! [X3,X0,X4,X5] :
( ~ sP1(X0)
| p1(X3)
| ~ p1(X4)
| p1(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(sK8(X0),X3) ),
inference(cnf_transformation,[],[f20]) ).
fof(f40,plain,
! [X0] :
( ~ sP1(X0)
| ~ p1(sK9(X0)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f41,plain,
! [X0] :
( ~ sP1(X0)
| r1(sK8(X0),sK9(X0)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f42,plain,
! [X0] :
( ~ sP1(X0)
| r1(X0,sK8(X0)) ),
inference(cnf_transformation,[],[f20]) ).
fof(f79,plain,
! [X80,X78,X81,X79,X88,X89,X87,X77] :
( ~ p1(sK37(X87))
| p1(X89)
| ~ r1(X88,X89)
| ~ r1(X87,X88)
| ~ r1(X81,X87)
| ~ r1(X80,X81)
| ~ r1(X79,X80)
| ~ r1(X78,X79)
| ~ r1(X77,X78)
| ~ r1(sK13,X77) ),
inference(cnf_transformation,[],[f25]) ).
fof(f80,plain,
! [X80,X78,X81,X79,X88,X89,X87,X77] :
( r1(X87,sK37(X87))
| p1(X89)
| ~ r1(X88,X89)
| ~ r1(X87,X88)
| ~ r1(X81,X87)
| ~ r1(X80,X81)
| ~ r1(X79,X80)
| ~ r1(X78,X79)
| ~ r1(X77,X78)
| ~ r1(sK13,X77) ),
inference(cnf_transformation,[],[f25]) ).
fof(f87,plain,
! [X74] :
( p1(sK33(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f88,plain,
! [X74] :
( ~ p1(sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f89,plain,
! [X74] :
( r1(sK33(X74),sK34(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f90,plain,
! [X74] :
( r1(X74,sK33(X74))
| p1(X74)
| ~ r1(sK30,X74) ),
inference(cnf_transformation,[],[f25]) ).
fof(f91,plain,
! [X73] :
( p1(X73)
| ~ r1(sK32,X73) ),
inference(cnf_transformation,[],[f25]) ).
fof(f92,plain,
r1(sK30,sK32),
inference(cnf_transformation,[],[f25]) ).
fof(f93,plain,
~ p1(sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f94,plain,
r1(sK30,sK31),
inference(cnf_transformation,[],[f25]) ).
fof(f95,plain,
r1(sK29,sK30),
inference(cnf_transformation,[],[f25]) ).
fof(f96,plain,
r1(sK28,sK29),
inference(cnf_transformation,[],[f25]) ).
fof(f97,plain,
r1(sK27,sK28),
inference(cnf_transformation,[],[f25]) ).
fof(f98,plain,
r1(sK26,sK27),
inference(cnf_transformation,[],[f25]) ).
fof(f99,plain,
r1(sK25,sK26),
inference(cnf_transformation,[],[f25]) ).
fof(f100,plain,
r1(sK13,sK25),
inference(cnf_transformation,[],[f25]) ).
fof(f101,plain,
! [X56,X54,X57,X55,X52,X63,X53,X64] :
( ~ p1(X63)
| p1(X64)
| ~ r1(X63,X64)
| ~ r1(sK24(X57),X63)
| sP0(X57)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f102,plain,
! [X56,X54,X57,X55,X52,X53] :
( ~ p1(sK24(X57))
| sP0(X57)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f103,plain,
! [X56,X54,X57,X55,X52,X53] :
( r1(X57,sK24(X57))
| sP0(X57)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f104,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( ~ p1(sK23(X58))
| p1(X60)
| ~ r1(X59,X60)
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f105,plain,
! [X58,X59,X56,X54,X57,X55,X52,X53,X60] :
( r1(X58,sK23(X58))
| p1(X60)
| ~ r1(X59,X60)
| ~ r1(X58,X59)
| ~ r1(X57,X58)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f106,plain,
! [X56,X54,X57,X55,X52,X53] :
( sP2(X57)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
fof(f107,plain,
! [X56,X54,X57,X55,X52,X53] :
( sP3(X57)
| ~ r1(X56,X57)
| ~ r1(X55,X56)
| ~ r1(X54,X55)
| ~ r1(X53,X54)
| ~ r1(X52,X53)
| ~ r1(sK13,X52) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| r1(X2,sK4(X2))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| r1(sK4(X2),sK5(X2))
| ~ sP3(X0)
| ~ p1(X0)
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP1(X0)
| p1(X1)
| ~ sP3(X0)
| ~ p1(X0)
| ~ p1(sK5(X2))
| ~ r1(X0,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X1,sK6(X1))
| r1(X0,sK7(X0))
| ~ sP2(X0)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_54,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X1,sK6(X1))
| ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_55,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X0)
| r1(X2,sK6(X2))
| ~ sP2(X0)
| ~ p1(X1)
| ~ r1(X1,X3)
| ~ r1(X0,X2)
| ~ r1(sK7(X0),X1) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X0,sK7(X0))
| ~ sP2(X0)
| ~ p1(sK6(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| ~ sP2(X0)
| ~ p1(sK7(X0))
| ~ p1(sK6(X1))
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_58,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X0)
| ~ sP2(X0)
| ~ p1(X1)
| ~ p1(sK6(X2))
| ~ r1(X1,X3)
| ~ r1(X0,X2)
| ~ r1(sK7(X0),X1) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_59,plain,
! [X0: $i] :
( r1(X0,sK8(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_60,plain,
! [X0: $i] :
( r1(sK8(X0),sK9(X0))
| ~ sP1(X0) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_61,plain,
! [X0: $i] :
( ~ sP1(X0)
| ~ p1(sK9(X0)) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| p1(X1)
| ~ sP1(X0)
| ~ p1(X2)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK8(X0),X1) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_94,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP3(X5)
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_95,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP2(X5)
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_96,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( p1(X8)
| r1(X6,sK23(X6))
| ~ r1(sK13,X0)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_97,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] :
( p1(X8)
| ~ p1(sK23(X6))
| ~ r1(sK13,X0)
| ~ r1(X7,X8)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_98,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(X5)
| r1(X5,sK24(X5))
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_99,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(X5)
| ~ p1(sK24(X5))
| ~ r1(sK13,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_100,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( sP0(X0)
| p1(X7)
| ~ p1(X1)
| ~ r1(sK13,X2)
| ~ r1(X6,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X7)
| ~ r1(sK24(X0),X1) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_101,negated_conjecture,
r1(sK13,sK25),
inference(cnf_transformation,[],[f100]) ).
tcf(c_102,negated_conjecture,
r1(sK25,sK26),
inference(cnf_transformation,[],[f99]) ).
tcf(c_103,negated_conjecture,
r1(sK26,sK27),
inference(cnf_transformation,[],[f98]) ).
tcf(c_104,negated_conjecture,
r1(sK27,sK28),
inference(cnf_transformation,[],[f97]) ).
tcf(c_105,negated_conjecture,
r1(sK28,sK29),
inference(cnf_transformation,[],[f96]) ).
tcf(c_106,negated_conjecture,
r1(sK29,sK30),
inference(cnf_transformation,[],[f95]) ).
tcf(c_107,negated_conjecture,
r1(sK30,sK31),
inference(cnf_transformation,[],[f94]) ).
tcf(c_108,negated_conjecture,
~ p1(sK31),
inference(cnf_transformation,[],[f93]) ).
tcf(c_109,negated_conjecture,
r1(sK30,sK32),
inference(cnf_transformation,[],[f92]) ).
tcf(c_110,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ r1(sK32,X0) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_111,negated_conjecture,
! [X0: $i] :
( p1(X0)
| r1(X0,sK33(X0))
| ~ r1(sK30,X0) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_112,negated_conjecture,
! [X0: $i] :
( p1(X0)
| r1(sK33(X0),sK34(X0))
| ~ r1(sK30,X0) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_113,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ p1(sK34(X0))
| ~ r1(sK30,X0) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_114,negated_conjecture,
! [X0: $i] :
( p1(X0)
| p1(sK33(X0))
| ~ r1(sK30,X0) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_121,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| r1(X5,sK37(X5))
| ~ r1(sK13,X0)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_122,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| ~ p1(sK37(X5))
| ~ r1(sK13,X0)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_3646,plain,
( p1(sK31)
| r1(sK31,sK33(sK31))
| ~ r1(sK30,sK31) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_3648,plain,
( p1(sK31)
| r1(sK33(sK31),sK34(sK31))
| ~ r1(sK30,sK31) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_3707,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP3(X4)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_94]) ).
tcf(c_3708,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP2(X4)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_95]) ).
tcf(c_3711,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(X4)
| r1(X4,sK24(X4))
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_98]) ).
tcf(c_3716,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK37(X4))
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_121]) ).
tcf(c_3718,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| r1(X5,sK23(X5))
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_3730,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP3(X3)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3707]) ).
tcf(c_3732,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP2(X3)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3708]) ).
tcf(c_3738,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(X3)
| r1(X3,sK24(X3))
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3711]) ).
tcf(c_3748,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK37(X3))
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3716]) ).
tcf(c_3752,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK23(X4))
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3718]) ).
tcf(c_3767,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP3(X2)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3730]) ).
tcf(c_3768,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP2(X2)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3732]) ).
tcf(c_3773,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(X2)
| r1(X2,sK24(X2))
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3738]) ).
tcf(c_3778,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK37(X2))
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3748]) ).
tcf(c_3780,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK23(X3))
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3752]) ).
tcf(c_3812,plain,
! [X0: $i,X1: $i] :
( sP3(X1)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3767]) ).
tcf(c_3813,plain,
! [X0: $i,X1: $i] :
( sP2(X1)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3768]) ).
tcf(c_3814,plain,
! [X0: $i,X1: $i] :
( sP0(X1)
| r1(X1,sK24(X1))
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3773]) ).
tcf(c_3821,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK37(X1))
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3778]) ).
tcf(c_3823,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK23(X2))
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3780]) ).
tcf(c_3873,plain,
! [X0: $i] :
( sP3(X0)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0) ),
inference(instantiation,[status(thm)],[c_3812]) ).
tcf(c_3875,plain,
! [X0: $i] :
( sP2(X0)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0) ),
inference(instantiation,[status(thm)],[c_3813]) ).
tcf(c_3879,plain,
! [X0: $i] :
( sP0(X0)
| r1(X0,sK24(X0))
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0) ),
inference(instantiation,[status(thm)],[c_3814]) ).
tcf(c_3885,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK37(X0))
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3821]) ).
tcf(c_3887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK23(X1))
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3823]) ).
tcf(c_3913,plain,
( sP3(sK30)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25) ),
inference(instantiation,[status(thm)],[c_3873]) ).
tcf(c_3914,plain,
( sP2(sK30)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25) ),
inference(instantiation,[status(thm)],[c_3875]) ).
tcf(c_3917,plain,
( sP0(sK30)
| r1(sK30,sK24(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25) ),
inference(instantiation,[status(thm)],[c_3879]) ).
tcf(c_3920,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK30,sK37(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3885]) ).
tcf(c_3924,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK23(X0))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3887]) ).
tcf(c_3980,plain,
! [X0: $i] :
( p1(sK30)
| r1(sK30,sK7(sK30))
| r1(X0,sK6(X0))
| ~ sP2(sK30)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_53]) ).
tcf(c_3985,plain,
( p1(sK24(sK30))
| r1(sK33(sK24(sK30)),sK34(sK24(sK30)))
| ~ r1(sK30,sK24(sK30)) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_3986,plain,
( p1(sK24(sK30))
| r1(sK24(sK30),sK33(sK24(sK30)))
| ~ r1(sK30,sK24(sK30)) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_3987,plain,
( p1(sK24(sK30))
| p1(sK33(sK24(sK30)))
| ~ r1(sK30,sK24(sK30)) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_4000,plain,
! [X0: $i] :
( p1(X0)
| r1(sK30,sK37(sK30))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X0) ),
inference(instantiation,[status(thm)],[c_3920]) ).
tcf(c_4009,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK31,sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3924]) ).
tcf(c_4076,plain,
! [X0: $i] :
( p1(X0)
| r1(sK31,sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK33(sK31))
| ~ r1(sK33(sK31),X0) ),
inference(instantiation,[status(thm)],[c_4009]) ).
tcf(c_4086,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30))
| ~ sP2(sK30)
| ~ r1(sK30,sK32) ),
inference(instantiation,[status(thm)],[c_3980]) ).
tcf(c_4126,plain,
( p1(sK6(sK32))
| ~ r1(sK32,sK6(sK32)) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_4182,plain,
( p1(sK34(sK31))
| r1(sK31,sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK33(sK31))
| ~ r1(sK33(sK31),sK34(sK31)) ),
inference(instantiation,[status(thm)],[c_4076]) ).
tcf(c_4201,plain,
( r1(sK8(sK30),sK9(sK30))
| ~ sP1(sK30) ),
inference(instantiation,[status(thm)],[c_60]) ).
tcf(c_4202,plain,
( r1(sK30,sK8(sK30))
| ~ sP1(sK30) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_4204,plain,
( ~ sP1(sK30)
| ~ p1(sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_61]) ).
tcf(c_4217,plain,
( p1(sK31)
| ~ p1(sK34(sK31))
| ~ r1(sK30,sK31) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_4264,plain,
( p1(sK23(sK31))
| r1(sK30,sK37(sK30))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK23(sK31)) ),
inference(instantiation,[status(thm)],[c_4000]) ).
tcf(c_4304,plain,
( p1(sK7(sK30))
| r1(sK33(sK7(sK30)),sK34(sK7(sK30)))
| ~ r1(sK30,sK7(sK30)) ),
inference(instantiation,[status(thm)],[c_112]) ).
tcf(c_4305,plain,
( p1(sK7(sK30))
| r1(sK7(sK30),sK33(sK7(sK30)))
| ~ r1(sK30,sK7(sK30)) ),
inference(instantiation,[status(thm)],[c_111]) ).
tcf(c_4306,plain,
( p1(sK7(sK30))
| p1(sK33(sK7(sK30)))
| ~ r1(sK30,sK7(sK30)) ),
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_4409,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| r1(X5,sK23(X5))
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X6,X7)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_96]) ).
tcf(c_4441,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK23(X4))
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK26,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4409]) ).
tcf(c_4486,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK23(X3))
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK27,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4441]) ).
tcf(c_4531,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK23(X2))
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK28,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4486]) ).
tcf(c_4557,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK23(X1))
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK29,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4531]) ).
tcf(c_4570,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK23(X0))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4557]) ).
tcf(c_4576,plain,
! [X0: $i,X1: $i] :
( sP1(sK30)
| p1(X0)
| r1(sK4(X1),sK5(X1))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,X1)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_4577,plain,
! [X0: $i,X1: $i] :
( sP1(sK30)
| p1(X0)
| r1(X1,sK4(X1))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,X1)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_4593,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK32,sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4570]) ).
tcf(c_4610,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK13,X0)
| ~ r1(X4,sK30)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_99]) ).
tcf(c_4647,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X3,sK30)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4610]) ).
tcf(c_4692,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X2,sK29)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4647]) ).
tcf(c_4732,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| ~ p1(sK37(sK30))
| ~ r1(sK30,X5)
| ~ r1(sK13,X0)
| ~ r1(X4,sK30)
| ~ r1(X5,X6)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_122]) ).
tcf(c_4736,plain,
! [X0: $i,X1: $i] :
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X1,sK28)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4692]) ).
tcf(c_4777,plain,
! [X0: $i] :
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X0)
| ~ r1(X0,sK27) ),
inference(instantiation,[status(thm)],[c_4736]) ).
tcf(c_4781,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| ~ p1(sK37(sK30))
| ~ r1(sK13,sK25)
| ~ r1(sK30,X4)
| ~ r1(sK25,X0)
| ~ r1(X3,sK30)
| ~ r1(X4,X5)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4732]) ).
tcf(c_4789,plain,
( sP0(sK30)
| ~ p1(sK24(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25) ),
inference(instantiation,[status(thm)],[c_4777]) ).
tcf(c_4792,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| ~ p1(sK37(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X3)
| ~ r1(sK25,X0)
| ~ r1(X2,sK29)
| ~ r1(X3,X4)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4781]) ).
tcf(c_4794,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK13,X1)
| ~ r1(X5,sK30)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_100]) ).
tcf(c_4824,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| ~ p1(sK37(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X2)
| ~ r1(sK25,X0)
| ~ r1(X1,sK28)
| ~ r1(X2,X3)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4792]) ).
tcf(c_4831,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X1)
| ~ p1(sK37(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X0)
| ~ r1(sK25,X2)
| ~ r1(X2,sK27)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4824]) ).
tcf(c_4833,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X1)
| ~ r1(X4,sK30)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_4794]) ).
tcf(c_4865,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| ~ p1(sK37(sK30))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK30,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_4831]) ).
tcf(c_4867,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK29,sK30)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X1)
| ~ r1(X3,sK29)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_4833]) ).
tcf(c_4869,plain,
( p1(sK24(sK30))
| ~ p1(sK34(sK24(sK30)))
| ~ r1(sK30,sK24(sK30)) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_4891,plain,
! [X0: $i] :
( p1(X0)
| ~ p1(sK37(sK30))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X0) ),
inference(instantiation,[status(thm)],[c_4865]) ).
tcf(c_4900,plain,
! [X0: $i,X1: $i,X2: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X1)
| ~ r1(X2,sK28)
| ~ r1(X1,X2)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_4867]) ).
tcf(c_4999,plain,
( p1(sK23(sK31))
| ~ p1(sK37(sK30))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK23(sK31)) ),
inference(instantiation,[status(thm)],[c_4891]) ).
tcf(c_5000,plain,
! [X0: $i,X1: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK13,sK25)
| ~ r1(sK25,X1)
| ~ r1(X1,sK27)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_4900]) ).
tcf(c_5232,plain,
! [X0: $i] :
( sP0(sK30)
| p1(X0)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),X0)
| ~ r1(sK24(sK30),sK33(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_5000]) ).
tcf(c_5303,plain,
( sP0(sK30)
| p1(sK34(sK24(sK30)))
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ p1(sK33(sK24(sK30)))
| ~ r1(sK24(sK30),sK33(sK24(sK30)))
| ~ r1(sK33(sK24(sK30)),sK34(sK24(sK30))) ),
inference(instantiation,[status(thm)],[c_5232]) ).
tcf(c_5324,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| ~ p1(sK23(sK31))
| ~ r1(sK31,X6)
| ~ r1(sK13,X0)
| ~ r1(X5,sK31)
| ~ r1(X6,X7)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_5332,plain,
! [X0: $i] :
( sP1(sK30)
| p1(X0)
| r1(sK4(sK32),sK5(sK32))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,sK32)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_4576]) ).
tcf(c_5337,plain,
! [X0: $i] :
( sP1(sK30)
| p1(X0)
| r1(sK32,sK4(sK32))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,sK32)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_4577]) ).
tcf(c_5385,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| ~ p1(sK23(sK31))
| ~ r1(sK13,sK25)
| ~ r1(sK31,X5)
| ~ r1(sK25,X0)
| ~ r1(X4,sK31)
| ~ r1(X5,X6)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5324]) ).
tcf(c_5444,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| r1(sK30,sK7(sK30))
| ~ sP2(sK30) ),
inference(superposition,[status(thm)],[c_109,c_53]) ).
tcf(c_5455,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X4)
| ~ r1(sK25,X0)
| ~ r1(X3,sK30)
| ~ r1(X4,X5)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5385]) ).
tcf(c_5510,plain,
( p1(sK30)
| r1(sK32,sK6(sK32))
| ~ sP2(sK30)
| ~ p1(sK7(sK30)) ),
inference(superposition,[status(thm)],[c_109,c_54]) ).
tcf(c_5536,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X3)
| ~ r1(sK25,X0)
| ~ r1(X2,sK29)
| ~ r1(X3,X4)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5455]) ).
tcf(c_5609,plain,
( p1(sK30)
| r1(sK30,sK7(sK30))
| ~ sP2(sK30)
| ~ p1(sK6(sK32)) ),
inference(superposition,[status(thm)],[c_109,c_56]) ).
tcf(c_5645,plain,
! [X0: $i] :
( p1(sK30)
| ~ sP2(sK30)
| ~ p1(sK7(sK30))
| ~ p1(sK6(X0))
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_5665,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X2)
| ~ r1(sK25,X0)
| ~ r1(X1,sK28)
| ~ r1(X2,X3)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5536]) ).
tcf(c_5774,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X1)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X0)
| ~ r1(sK25,X2)
| ~ r1(X2,sK27)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5665]) ).
tcf(c_5777,plain,
( p1(sK30)
| ~ sP2(sK30)
| ~ p1(sK7(sK30))
| ~ p1(sK6(sK32))
| ~ r1(sK30,sK32) ),
inference(instantiation,[status(thm)],[c_5645]) ).
tcf(c_6069,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_5774]) ).
tcf(c_6112,plain,
! [X0: $i] :
( p1(X0)
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK33(sK31))
| ~ r1(sK33(sK31),X0) ),
inference(instantiation,[status(thm)],[c_6069]) ).
tcf(c_6302,plain,
( p1(sK7(sK30))
| ~ p1(sK34(sK7(sK30)))
| ~ r1(sK30,sK7(sK30)) ),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_6303,plain,
( p1(sK34(sK31))
| ~ p1(sK23(sK31))
| ~ r1(sK30,sK31)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK31,sK33(sK31))
| ~ r1(sK33(sK31),sK34(sK31)) ),
inference(instantiation,[status(thm)],[c_6112]) ).
tcf(c_6493,plain,
! [X0: $i] :
( p1(X0)
| r1(sK32,sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,sK4(sK32))
| ~ r1(sK4(sK32),X0) ),
inference(instantiation,[status(thm)],[c_4593]) ).
tcf(c_6849,plain,
( sP1(sK30)
| p1(sK37(sK30))
| r1(sK32,sK4(sK32))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,sK32)
| ~ r1(sK30,sK37(sK30)) ),
inference(instantiation,[status(thm)],[c_5337]) ).
tcf(c_6851,plain,
( sP1(sK30)
| p1(sK37(sK30))
| r1(sK4(sK32),sK5(sK32))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ r1(sK30,sK32)
| ~ r1(sK30,sK37(sK30)) ),
inference(instantiation,[status(thm)],[c_5332]) ).
tcf(c_7837,plain,
( p1(sK5(sK32))
| r1(sK32,sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,sK4(sK32))
| ~ r1(sK4(sK32),sK5(sK32)) ),
inference(instantiation,[status(thm)],[c_6493]) ).
tcf(c_8781,plain,
! [X0: $i,X1: $i] :
( sP1(X0)
| p1(X1)
| ~ sP3(X0)
| ~ p1(X0)
| ~ p1(sK5(sK32))
| ~ r1(X0,sK32)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_8792,plain,
( p1(sK30)
| ~ sP2(sK30)
| ~ p1(sK7(sK30))
| ~ p1(sK6(sK32)) ),
inference(superposition,[status(thm)],[c_109,c_57]) ).
tcf(c_9164,plain,
! [X0: $i] :
( sP1(sK30)
| p1(X0)
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ p1(sK5(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK30,X0) ),
inference(instantiation,[status(thm)],[c_8781]) ).
tcf(c_9439,plain,
( sP1(sK30)
| p1(sK37(sK30))
| ~ sP3(sK30)
| ~ p1(sK30)
| ~ p1(sK5(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK30,sK37(sK30)) ),
inference(instantiation,[status(thm)],[c_9164]) ).
tcf(c_9528,plain,
( p1(sK23(sK32))
| ~ r1(sK32,sK23(sK32)) ),
inference(instantiation,[status(thm)],[c_110]) ).
tcf(c_11962,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( p1(X7)
| ~ p1(sK23(sK32))
| ~ r1(sK32,X6)
| ~ r1(sK13,X0)
| ~ r1(X5,sK32)
| ~ r1(X6,X7)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_97]) ).
tcf(c_12023,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| ~ p1(sK23(sK32))
| ~ r1(sK13,sK25)
| ~ r1(sK32,X5)
| ~ r1(sK25,X0)
| ~ r1(X4,sK32)
| ~ r1(X5,X6)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_11962]) ).
tcf(c_12049,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X4)
| ~ r1(sK25,X0)
| ~ r1(X3,sK30)
| ~ r1(X4,X5)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_12023]) ).
tcf(c_12100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X3)
| ~ r1(sK25,X0)
| ~ r1(X2,sK29)
| ~ r1(X3,X4)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_12049]) ).
tcf(c_12116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X2)
| ~ r1(sK25,X0)
| ~ r1(X1,sK28)
| ~ r1(X2,X3)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_12100]) ).
tcf(c_12134,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X1)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X0)
| ~ r1(sK25,X2)
| ~ r1(X2,sK27)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_12116]) ).
tcf(c_12145,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_12134]) ).
tcf(c_12149,plain,
! [X0: $i] :
( p1(X0)
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,sK4(sK32))
| ~ r1(sK4(sK32),X0) ),
inference(instantiation,[status(thm)],[c_12145]) ).
tcf(c_12154,plain,
( p1(sK5(sK32))
| ~ p1(sK23(sK32))
| ~ r1(sK30,sK32)
| ~ r1(sK29,sK30)
| ~ r1(sK28,sK29)
| ~ r1(sK27,sK28)
| ~ r1(sK26,sK27)
| ~ r1(sK25,sK26)
| ~ r1(sK13,sK25)
| ~ r1(sK32,sK4(sK32))
| ~ r1(sK4(sK32),sK5(sK32)) ),
inference(instantiation,[status(thm)],[c_12149]) ).
tcf(c_12170,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK9(sK30))
| ~ sP1(sK30)
| ~ p1(X0)
| ~ r1(X0,X1)
| ~ r1(sK9(sK30),X0)
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_65]) ).
tcf(c_12347,plain,
! [X0: $i] :
( p1(X0)
| p1(sK9(sK30))
| ~ sP1(sK30)
| ~ p1(sK11(sK9(sK30)))
| ~ r1(sK8(sK30),sK9(sK30))
| ~ r1(sK11(sK9(sK30)),X0)
| ~ r1(sK9(sK30),sK11(sK9(sK30))) ),
inference(instantiation,[status(thm)],[c_12170]) ).
tcf(c_12364,plain,
( p1(sK9(sK30))
| p1(sK12(sK9(sK30)))
| ~ sP1(sK30)
| ~ p1(sK11(sK9(sK30)))
| ~ r1(sK8(sK30),sK9(sK30))
| ~ r1(sK9(sK30),sK11(sK9(sK30)))
| ~ r1(sK11(sK9(sK30)),sK12(sK9(sK30))) ),
inference(instantiation,[status(thm)],[c_12347]) ).
tcf(c_12716,plain,
! [X0: $i,X1: $i] :
( p1(sK30)
| p1(X0)
| r1(X1,sK6(X1))
| ~ sP2(sK30)
| ~ r1(sK30,X1)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),X0)
| ~ r1(sK7(sK30),sK33(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_55]) ).
tcf(c_12717,plain,
! [X0: $i,X1: $i] :
( p1(sK30)
| p1(X0)
| ~ sP2(sK30)
| ~ p1(sK6(X1))
| ~ r1(sK30,X1)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),X0)
| ~ r1(sK7(sK30),sK33(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_12795,plain,
! [X0: $i] :
( p1(sK30)
| p1(sK34(sK7(sK30)))
| ~ sP2(sK30)
| ~ p1(sK6(X0))
| ~ r1(sK30,X0)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK7(sK30),sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),sK34(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_12717]) ).
tcf(c_12799,plain,
! [X0: $i] :
( p1(sK30)
| p1(sK34(sK7(sK30)))
| r1(X0,sK6(X0))
| ~ sP2(sK30)
| ~ r1(sK30,X0)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK7(sK30),sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),sK34(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_12716]) ).
tcf(c_12930,plain,
( p1(sK30)
| p1(sK34(sK7(sK30)))
| ~ sP2(sK30)
| ~ p1(sK6(sK32))
| ~ r1(sK30,sK32)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK7(sK30),sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),sK34(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_12795]) ).
tcf(c_12933,plain,
( p1(sK30)
| p1(sK34(sK7(sK30)))
| r1(sK32,sK6(sK32))
| ~ sP2(sK30)
| ~ r1(sK30,sK32)
| ~ p1(sK33(sK7(sK30)))
| ~ r1(sK7(sK30),sK33(sK7(sK30)))
| ~ r1(sK33(sK7(sK30)),sK34(sK7(sK30))) ),
inference(instantiation,[status(thm)],[c_12799]) ).
fof(f7,definition,
! [X57] :
( ~ sP0(X57)
| ! [X77] :
( ! [X78] :
( ? [X79] :
( p1(X79)
& ? [X80] :
( ~ p1(X80)
& r1(X79,X80) )
& r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f8,definition,
! [X57] :
( ~ sP1(X57)
| ? [X62] :
( ! [X64] :
( ( p1(X64)
& ? [X67] :
( ~ p1(X67)
& r1(X64,X67) ) )
| ! [X65] :
( ~ p1(X65)
| ! [X66] :
( p1(X66)
| ~ r1(X65,X66) )
| ~ r1(X64,X65) )
| ~ r1(X62,X64) )
& p1(X62)
& ? [X63] :
( ~ p1(X63)
& r1(X62,X63) )
& r1(X57,X62) ) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f9,definition,
! [X57] :
( ~ sP2(X57)
| ? [X70] :
( ! [X71] :
( ~ p1(X71)
| ! [X72] :
( p1(X72)
| ~ r1(X71,X72) )
| ~ r1(X70,X71) )
& ~ p1(X70)
& r1(X57,X70) )
| ! [X68] :
( ? [X69] :
( ~ p1(X69)
& r1(X68,X69) )
| ~ r1(X57,X68) )
| p1(X57) ),
introduced(definition,[new_symbols(definition,[sP2])],[predicate_definition_introduction]) ).
fof(f10,definition,
! [X57] :
( ~ sP3(X57)
| sP1(X57)
| ! [X59] :
( ? [X60] :
( p1(X60)
& ? [X61] :
( ~ p1(X61)
& r1(X60,X61) )
& r1(X59,X60) )
| ~ r1(X57,X59) )
| ~ p1(X57)
| ! [X58] :
( p1(X58)
| ~ r1(X57,X58) ) ),
introduced(definition,[new_symbols(definition,[sP3])],[predicate_definition_introduction]) ).
fof(f11,plain,
? [X0] :
( ! [X146] :
( ( ! [X152] :
( ? [X155] :
( ~ p1(X155)
& r1(X152,X155) )
| ! [X153] :
( ! [X154] :
( p1(X154)
| ~ r1(X153,X154) )
| ~ r1(X152,X153) )
| ~ r1(X146,X152) )
& ( ? [X149] :
( ! [X150] :
( ~ p1(X150)
| ! [X151] :
( p1(X151)
| ~ r1(X150,X151) )
| ~ r1(X149,X150) )
& ~ p1(X149)
& r1(X146,X149) )
| ! [X147] :
( ? [X148] :
( ~ p1(X148)
& r1(X147,X148) )
| ~ r1(X146,X147) )
| p1(X146) ) )
| ~ r1(X0,X146) )
& ! [X135] :
( ! [X136] :
( ( ! [X142] :
( ? [X145] :
( ~ p1(X145)
& r1(X142,X145) )
| ! [X143] :
( ! [X144] :
( p1(X144)
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X136,X142) )
& ( ? [X139] :
( ! [X140] :
( ~ p1(X140)
| ! [X141] :
( p1(X141)
| ~ r1(X140,X141) )
| ~ r1(X139,X140) )
& ~ p1(X139)
& r1(X136,X139) )
| ! [X137] :
( ? [X138] :
( ~ p1(X138)
& r1(X137,X138) )
| ~ r1(X136,X137) )
| p1(X136) ) )
| ~ r1(X135,X136) )
| ~ r1(X0,X135) )
& ! [X123] :
( ! [X124] :
( ! [X125] :
( ( ! [X131] :
( ? [X134] :
( ~ p1(X134)
& r1(X131,X134) )
| ! [X132] :
( ! [X133] :
( p1(X133)
| ~ r1(X132,X133) )
| ~ r1(X131,X132) )
| ~ r1(X125,X131) )
& ( ? [X128] :
( ! [X129] :
( ~ p1(X129)
| ! [X130] :
( p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
& ~ p1(X128)
& r1(X125,X128) )
| ! [X126] :
( ? [X127] :
( ~ p1(X127)
& r1(X126,X127) )
| ~ r1(X125,X126) )
| p1(X125) ) )
| ~ r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X0,X123) )
& ! [X110] :
( ! [X111] :
( ! [X112] :
( ! [X113] :
( ( ! [X119] :
( ? [X122] :
( ~ p1(X122)
& r1(X119,X122) )
| ! [X120] :
( ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X113,X119) )
& ( ? [X116] :
( ! [X117] :
( ~ p1(X117)
| ! [X118] :
( p1(X118)
| ~ r1(X117,X118) )
| ~ r1(X116,X117) )
& ~ p1(X116)
& r1(X113,X116) )
| ! [X114] :
( ? [X115] :
( ~ p1(X115)
& r1(X114,X115) )
| ~ r1(X113,X114) )
| p1(X113) ) )
| ~ r1(X112,X113) )
| ~ r1(X111,X112) )
| ~ r1(X110,X111) )
| ~ r1(X0,X110) )
& ! [X96] :
( ! [X97] :
( ! [X98] :
( ! [X99] :
( ! [X100] :
( ( ! [X106] :
( ? [X109] :
( ~ p1(X109)
& r1(X106,X109) )
| ! [X107] :
( ! [X108] :
( p1(X108)
| ~ r1(X107,X108) )
| ~ r1(X106,X107) )
| ~ r1(X100,X106) )
& ( ? [X103] :
( ! [X104] :
( ~ p1(X104)
| ! [X105] :
( p1(X105)
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
& ~ p1(X103)
& r1(X100,X103) )
| ! [X101] :
( ? [X102] :
( ~ p1(X102)
& r1(X101,X102) )
| ~ r1(X100,X101) )
| p1(X100) ) )
| ~ r1(X99,X100) )
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X0,X96) )
& ? [X84] :
( ? [X85] :
( ? [X86] :
( ? [X87] :
( ? [X88] :
( ? [X89] :
( ! [X93] :
( ? [X94] :
( p1(X94)
& ? [X95] :
( ~ p1(X95)
& r1(X94,X95) )
& r1(X93,X94) )
| p1(X93)
| ~ r1(X89,X93) )
& ? [X91] :
( ! [X92] :
( p1(X92)
| ~ r1(X91,X92) )
& r1(X89,X91) )
& ? [X90] :
( ~ p1(X90)
& r1(X89,X90) )
& r1(X88,X89) )
& r1(X87,X88) )
& r1(X86,X87) )
& r1(X85,X86) )
& r1(X84,X85) )
& r1(X0,X84) )
& ! [X52] :
( ! [X53] :
( ! [X54] :
( ! [X55] :
( ! [X56] :
( ! [X57] :
( ( ( ? [X81] :
( ! [X82] :
( ~ p1(X82)
| ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| ~ r1(X81,X82) )
& ~ p1(X81)
& r1(X57,X81) )
| sP0(X57) )
& ! [X73] :
( ? [X76] :
( ~ p1(X76)
& r1(X73,X76) )
| ! [X74] :
( ! [X75] :
( p1(X75)
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X57,X73) )
& sP2(X57)
& sP3(X57) )
| ~ r1(X56,X57) )
| ~ r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X0,X52) )
& ! [X36] :
( ! [X37] :
( ! [X38] :
( ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ( ! [X48] :
( ? [X51] :
( ~ p1(X51)
& r1(X48,X51) )
| ! [X49] :
( ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X42,X48) )
& ( ? [X45] :
( ! [X46] :
( ~ p1(X46)
| ! [X47] :
( p1(X47)
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
& ~ p1(X45)
& r1(X42,X45) )
| ! [X43] :
( ? [X44] :
( ~ p1(X44)
& r1(X43,X44) )
| ~ r1(X42,X43) )
| p1(X42) ) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X38,X39) )
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X0,X36) )
& ! [X19] :
( ! [X20] :
( ! [X21] :
( ! [X22] :
( ! [X23] :
( ! [X24] :
( ! [X25] :
( ! [X26] :
( ( ! [X32] :
( ? [X35] :
( ~ p1(X35)
& r1(X32,X35) )
| ! [X33] :
( ! [X34] :
( p1(X34)
| ~ r1(X33,X34) )
| ~ r1(X32,X33) )
| ~ r1(X26,X32) )
& ( ? [X29] :
( ! [X30] :
( ~ p1(X30)
| ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
& ~ p1(X29)
& r1(X26,X29) )
| ! [X27] :
( ? [X28] :
( ~ p1(X28)
& r1(X27,X28) )
| ~ r1(X26,X27) )
| p1(X26) ) )
| ~ r1(X25,X26) )
| ~ r1(X24,X25) )
| ~ r1(X23,X24) )
| ~ r1(X22,X23) )
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X0,X19) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( ! [X7] :
( ! [X8] :
( ! [X9] :
( ( ! [X15] :
( ? [X18] :
( ~ p1(X18)
& r1(X15,X18) )
| ! [X16] :
( ! [X17] :
( p1(X17)
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X9,X15) )
& ( ? [X12] :
( ! [X13] :
( ~ p1(X13)
| ! [X14] :
( p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) )
& ~ p1(X12)
& r1(X9,X12) )
| ! [X10] :
( ? [X11] :
( ~ p1(X11)
& r1(X10,X11) )
| ~ r1(X9,X10) )
| p1(X9) ) )
| ~ r1(X8,X9) )
| ~ r1(X7,X8) )
| ~ r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(definition_folding,[],[f6,f10,f9,f8,f7]) ).
fof(f21,plain,
! [X57] :
( ~ sP0(X57)
| ! [X77] :
( ! [X78] :
( ? [X79] :
( p1(X79)
& ? [X80] :
( ~ p1(X80)
& r1(X79,X80) )
& r1(X78,X79) )
| p1(X78)
| ~ r1(X77,X78) )
| ~ r1(X57,X77) ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ! [X2] :
( ? [X3] :
( p1(X3)
& ? [X4] :
( ~ p1(X4)
& r1(X3,X4) )
& r1(X2,X3) )
| p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0] :
( ~ sP0(X0)
| ! [X1] :
( ! [X2] :
( ( p1(sK11(X2))
& ~ p1(sK12(X2))
& r1(sK11(X2),sK12(X2))
& r1(X2,sK11(X2)) )
| p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11,sK12]),skolemize(X3,sK11(X2)),skolemize(X4,sK12(X2))],[f22]) ).
fof(f43,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| p1(sK11(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f44,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| ~ p1(sK12(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f45,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(sK11(X2),sK12(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
fof(f46,plain,
! [X2,X0,X1] :
( ~ sP0(X0)
| r1(X2,sK11(X2))
| p1(X2)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X2,sK11(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(sK11(X2),sK12(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_68,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| ~ sP0(X0)
| ~ p1(sK12(X2))
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| p1(sK11(X2))
| ~ sP0(X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_12019,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK11(X1),sK12(X1))
| ~ sP0(sK30)
| ~ r1(sK30,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_67]) ).
tcf(c_12020,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(X1,sK11(X1))
| ~ sP0(sK30)
| ~ r1(sK30,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_66]) ).
tcf(c_12021,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| p1(sK11(X1))
| ~ sP0(sK30)
| ~ r1(sK30,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_69]) ).
tcf(c_12173,plain,
! [X0: $i] :
( p1(X0)
| r1(X0,sK11(X0))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),X0) ),
inference(instantiation,[status(thm)],[c_12020]) ).
tcf(c_12174,plain,
! [X0: $i] :
( p1(X0)
| r1(sK11(X0),sK12(X0))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),X0) ),
inference(instantiation,[status(thm)],[c_12019]) ).
tcf(c_12175,plain,
! [X0: $i] :
( p1(X0)
| p1(sK11(X0))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),X0) ),
inference(instantiation,[status(thm)],[c_12021]) ).
tcf(c_12318,plain,
( p1(sK9(sK30))
| p1(sK11(sK9(sK30)))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_12175]) ).
tcf(c_12319,plain,
( p1(sK9(sK30))
| r1(sK9(sK30),sK11(sK9(sK30)))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_12173]) ).
tcf(c_12320,plain,
( p1(sK9(sK30))
| r1(sK11(sK9(sK30)),sK12(sK9(sK30)))
| ~ sP0(sK30)
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_12174]) ).
tcf(c_12386,plain,
! [X0: $i,X1: $i] :
( p1(sK9(sK30))
| ~ sP0(X1)
| ~ r1(X1,X0)
| ~ p1(sK12(sK9(sK30)))
| ~ r1(X0,sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_68]) ).
tcf(c_12439,plain,
! [X0: $i] :
( p1(sK9(sK30))
| ~ sP0(X0)
| ~ p1(sK12(sK9(sK30)))
| ~ r1(X0,sK8(sK30))
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_12386]) ).
tcf(c_12442,plain,
( p1(sK9(sK30))
| ~ sP0(sK30)
| ~ p1(sK12(sK9(sK30)))
| ~ r1(sK30,sK8(sK30))
| ~ r1(sK8(sK30),sK9(sK30)) ),
inference(instantiation,[status(thm)],[c_12439]) ).
tcf(c_12950,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_12933,c_12930,c_12442,c_12364,c_12320,c_12319,c_12318,c_12154,c_9528,c_9439,c_8792,c_7837,c_6849,c_6851,c_6303,c_6302,c_5777,c_5609,c_5510,c_5444,c_5303,c_4999,c_4869,c_4789,c_4304,c_4305,c_4306,c_4264,c_4217,c_4201,c_4202,c_4204,c_4182,c_4126,c_4086,c_3985,c_3986,c_3987,c_3917,c_3914,c_3913,c_3648,c_3646,c_101,c_102,c_103,c_104,c_105,c_106,c_107,c_108,c_109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL640+1.010 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.37 % Computer : n003.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 23:53:35 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.42
% 0.09/0.42 % ======== iProver multi-core TPTP/SMT =========
% 0.09/0.42
% 0.09/0.42 % Detected problem language: tptp
% 0.09/0.43 % Proving...
% 44.14/6.92 % SZS status Started for theBenchmark.p
% 44.14/6.92 % SZS status Theorem for theBenchmark.p
% 44.14/6.92
% 44.14/6.92 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 44.14/6.92
% 44.14/6.92 % ------ iProver source info
% 44.14/6.92
% 44.14/6.92 % git: date: 2026-07-19 20:42:38 +0200
% 44.14/6.92 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 44.14/6.92 % git: non_committed_changes: false
% 44.14/6.92
% 44.14/6.92 % ------ Parsing...
% 44.14/6.92 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 44.14/6.92
% 44.14/6.92 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 44.14/6.92
% 44.14/6.92 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e
% 44.14/6.92 % ------ Proving...
% 44.14/6.92 % ------ Problem Properties
% 44.14/6.92
% 44.14/6.92 %
% 44.14/6.92 % clauses 106
% 44.14/6.92 % conjectures 85
% 44.14/6.92 % EPR 12
% 44.14/6.92 % Horn 38
% 44.14/6.92 % unary 9
% 44.14/6.92 % binary 5
% 44.14/6.92 % lits 831
% 44.14/6.92 % lits eq 0
% 44.14/6.92 % fd_pure 0
% 44.14/6.92 % fd_pseudo 0
% 44.14/6.92 % fd_cond 0
% 44.14/6.92 % fd_pseudo_cond 0
% 44.14/6.92 % AC symbols 0
% 44.14/6.92
% 44.14/6.92 % ------ Input Options Time Limit: Unbounded
% 44.14/6.92
% 44.14/6.92
% 44.14/6.92 % ------
% 44.14/6.92 % Current options:
% 44.14/6.92 % ------
% 44.14/6.92
% 44.14/6.92
% 44.14/6.92 %
% 44.14/6.92
% 44.14/6.92 % ------ Proving...
% 44.14/6.92 %
% 44.14/6.92
% 44.14/6.92 % SZS status Theorem for theBenchmark.p
% 44.14/6.92
% 44.14/6.92 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 44.14/6.93
% 44.14/6.93
%------------------------------------------------------------------------------