%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LCL638+1.005 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n013.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:06:59 PM UTC 2026
% Result : Theorem 112.85s 16.64s
% Output : CNFRefutation 112.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 1
% Syntax : Number of formulae : 65 ( 13 unt; 0 def)
% Number of atoms : 2126 ( 0 equ)
% Maximal formula atoms : 225 ( 32 avg)
% Number of connectives : 4197 (2136 ~;1709 |; 352 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 63 ( 14 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 : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 26 con; 0-1 aty)
% Number of variables : 1458 ( 0 sgn1341 !; 117 ?; 114 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,conjecture,
~ ? [X0] :
~ ( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ! [X0] :
( $false
| ~ 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] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ 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) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ 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] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ 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) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [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] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ 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] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ 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) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ 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] :
( ~ ( p1(X1)
& ~ ! [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] :
( ~ ( ~ p1(X1)
& ~ ! [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) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(f2,negated_conjecture,
~ ~ ? [X0] :
~ ( ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ! [X0] :
( $false
| ~ 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] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ~ ( ~ p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ 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) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ~ p1(X1)
& ~ ! [X0] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) ) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ 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] :
( $false
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ 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) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
& ~ ! [X1] :
( ! [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] :
( ~ ( p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( ~ p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ~ ( ~ p1(X0)
& ~ ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ r1(X1,X0) )
| ~ r1(X0,X1) ) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( p1(X0)
| ~ 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] :
( $false
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ 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) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
| ~ r1(X0,X1) )
| ~ ! [X1] :
( ! [X0] :
( ! [X1] :
( ! [X0] :
( ! [X1] :
( ~ ( ! [X0] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X0,X1) )
| ~ r1(X1,X0) )
& ~ ! [X0] :
( ! [X1] :
( ~ ! [X0] :
( ~ 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] :
( ~ ( p1(X1)
& ~ ! [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] :
( ~ ( ~ p1(X1)
& ~ ! [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) ) ),
inference(negated_conjecture,[status(cth)],[f1]) ).
fof(f3,plain,
~ ~ ? [X0] :
~ ( ! [X165] :
( ! [X166] :
( ! [X167] :
( ! [X168] :
( ! [X169] :
( ~ ! [X170] :
( p1(X170)
| ~ r1(X169,X170) )
| p1(X169)
| ~ r1(X168,X169) )
| ~ r1(X167,X168) )
| ~ r1(X166,X167) )
| ~ r1(X165,X166) )
| ~ r1(X0,X165) )
| ~ ! [X163] :
( ~ ! [X164] :
( $false
| ~ r1(X163,X164) )
| ~ r1(X0,X163) )
| ~ ! [X159] :
( ~ ( ! [X162] :
( p1(X162)
| ~ r1(X159,X162) )
& ~ ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) ) )
| ~ r1(X0,X159) )
| ~ ! [X153] :
( ~ ( ! [X157] :
( ~ ! [X158] :
( ~ p1(X158)
| ~ r1(X157,X158) )
| ~ r1(X153,X157) )
& ~ ! [X154] :
( ! [X155] :
( ~ ! [X156] :
( ~ p1(X156)
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) ) )
| ~ r1(X0,X153) )
| ~ ! [X150] :
( ~ ( p1(X150)
& ~ ! [X151] :
( ~ ! [X152] :
( ~ p1(X152)
| ~ r1(X151,X152) )
| ~ r1(X150,X151) ) )
| ~ r1(X0,X150) )
| ~ ! [X147] :
( ~ ( ~ p1(X147)
& ~ ! [X148] :
( ~ ! [X149] :
( p1(X149)
| ~ r1(X148,X149) )
| ~ r1(X147,X148) ) )
| ~ r1(X0,X147) )
| ! [X141] :
( ! [X142] :
( ! [X143] :
( ! [X144] :
( ! [X145] :
( ~ ! [X146] :
( p1(X146)
| ~ r1(X145,X146) )
| p1(X145)
| ~ r1(X144,X145) )
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X141,X142) )
| ~ r1(X0,X141) )
| ~ ! [X138] :
( ! [X139] :
( ~ ! [X140] :
( $false
| ~ r1(X139,X140) )
| ~ r1(X138,X139) )
| ~ r1(X0,X138) )
| ~ ! [X133] :
( ! [X134] :
( ~ ( ! [X137] :
( p1(X137)
| ~ r1(X134,X137) )
& ~ ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) ) )
| ~ r1(X133,X134) )
| ~ r1(X0,X133) )
| ~ ! [X126] :
( ! [X127] :
( ~ ( ! [X131] :
( ~ ! [X132] :
( ~ p1(X132)
| ~ r1(X131,X132) )
| ~ r1(X127,X131) )
& ~ ! [X128] :
( ! [X129] :
( ~ ! [X130] :
( ~ p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) ) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X122] :
( ! [X123] :
( ~ ( p1(X123)
& ~ ! [X124] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X123,X124) ) )
| ~ r1(X122,X123) )
| ~ r1(X0,X122) )
| ~ ! [X118] :
( ! [X119] :
( ~ ( ~ p1(X119)
& ~ ! [X120] :
( ~ ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) ) )
| ~ r1(X118,X119) )
| ~ r1(X0,X118) )
| ! [X112] :
( ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X0,X112) )
| ~ ! [X108] :
( ! [X109] :
( ! [X110] :
( ~ ! [X111] :
( $false
| ~ r1(X110,X111) )
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X0,X108) )
| ~ ! [X102] :
( ! [X103] :
( ! [X104] :
( ~ ( ! [X107] :
( p1(X107)
| ~ r1(X104,X107) )
& ~ ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) ) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X0,X102) )
| ~ ! [X94] :
( ! [X95] :
( ! [X96] :
( ~ ( ! [X100] :
( ~ ! [X101] :
( ~ p1(X101)
| ~ r1(X100,X101) )
| ~ r1(X96,X100) )
& ~ ! [X97] :
( ! [X98] :
( ~ ! [X99] :
( ~ p1(X99)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) ) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X0,X94) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( p1(X91)
& ~ ! [X92] :
( ~ ! [X93] :
( ~ p1(X93)
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X84] :
( ! [X85] :
( ! [X86] :
( ~ ( ~ p1(X86)
& ~ ! [X87] :
( ~ ! [X88] :
( p1(X88)
| ~ r1(X87,X88) )
| ~ r1(X86,X87) ) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) )
| ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ~ ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| p1(X82)
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
| ~ ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( ~ ! [X77] :
( $false
| ~ r1(X76,X77) )
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X0,X73) )
| ~ ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ~ ( ! [X72] :
( p1(X72)
| ~ r1(X69,X72) )
& ~ ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) ) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) )
| ~ ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ~ ( ! [X64] :
( ~ ! [X65] :
( ~ p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X60,X64) )
& ~ ! [X61] :
( ! [X62] :
( ~ ! [X63] :
( ~ p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) ) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X0,X57) )
| ~ ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ ( p1(X54)
& ~ ! [X55] :
( ~ ! [X56] :
( ~ p1(X56)
| ~ r1(X55,X56) )
| ~ r1(X54,X55) ) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X0,X51) )
| ~ ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( ~ ( ~ p1(X48)
& ~ ! [X49] :
( ~ ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) ) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X0,X45) )
| ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X0,X39) )
| ~ ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X38] :
( $false
| ~ r1(X37,X38) )
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ~ ( ! [X32] :
( p1(X32)
| ~ r1(X29,X32) )
& ~ ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X0,X25) )
| ~ ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ~ ( ! [X23] :
( ~ ! [X24] :
( ~ p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X19,X23) )
& ~ ! [X20] :
( ! [X21] :
( ~ ! [X22] :
( ~ p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) ) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ ( p1(X12)
& ~ ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) ) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( ~ p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( p1(X7)
| ~ 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] :
~ ( ! [X165] :
( ! [X166] :
( ! [X167] :
( ! [X168] :
( ! [X169] :
( ~ ! [X170] :
( p1(X170)
| ~ r1(X169,X170) )
| p1(X169)
| ~ r1(X168,X169) )
| ~ r1(X167,X168) )
| ~ r1(X166,X167) )
| ~ r1(X165,X166) )
| ~ r1(X0,X165) )
| ~ ! [X163] :
( ~ ! [X164] : ~ r1(X163,X164)
| ~ r1(X0,X163) )
| ~ ! [X159] :
( ~ ( ! [X162] :
( p1(X162)
| ~ r1(X159,X162) )
& ~ ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) ) )
| ~ r1(X0,X159) )
| ~ ! [X153] :
( ~ ( ! [X157] :
( ~ ! [X158] :
( ~ p1(X158)
| ~ r1(X157,X158) )
| ~ r1(X153,X157) )
& ~ ! [X154] :
( ! [X155] :
( ~ ! [X156] :
( ~ p1(X156)
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) ) )
| ~ r1(X0,X153) )
| ~ ! [X150] :
( ~ ( p1(X150)
& ~ ! [X151] :
( ~ ! [X152] :
( ~ p1(X152)
| ~ r1(X151,X152) )
| ~ r1(X150,X151) ) )
| ~ r1(X0,X150) )
| ~ ! [X147] :
( ~ ( ~ p1(X147)
& ~ ! [X148] :
( ~ ! [X149] :
( p1(X149)
| ~ r1(X148,X149) )
| ~ r1(X147,X148) ) )
| ~ r1(X0,X147) )
| ! [X141] :
( ! [X142] :
( ! [X143] :
( ! [X144] :
( ! [X145] :
( ~ ! [X146] :
( p1(X146)
| ~ r1(X145,X146) )
| p1(X145)
| ~ r1(X144,X145) )
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X141,X142) )
| ~ r1(X0,X141) )
| ~ ! [X138] :
( ! [X139] :
( ~ ! [X140] : ~ r1(X139,X140)
| ~ r1(X138,X139) )
| ~ r1(X0,X138) )
| ~ ! [X133] :
( ! [X134] :
( ~ ( ! [X137] :
( p1(X137)
| ~ r1(X134,X137) )
& ~ ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) ) )
| ~ r1(X133,X134) )
| ~ r1(X0,X133) )
| ~ ! [X126] :
( ! [X127] :
( ~ ( ! [X131] :
( ~ ! [X132] :
( ~ p1(X132)
| ~ r1(X131,X132) )
| ~ r1(X127,X131) )
& ~ ! [X128] :
( ! [X129] :
( ~ ! [X130] :
( ~ p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) ) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X122] :
( ! [X123] :
( ~ ( p1(X123)
& ~ ! [X124] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X123,X124) ) )
| ~ r1(X122,X123) )
| ~ r1(X0,X122) )
| ~ ! [X118] :
( ! [X119] :
( ~ ( ~ p1(X119)
& ~ ! [X120] :
( ~ ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) ) )
| ~ r1(X118,X119) )
| ~ r1(X0,X118) )
| ! [X112] :
( ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X0,X112) )
| ~ ! [X108] :
( ! [X109] :
( ! [X110] :
( ~ ! [X111] : ~ r1(X110,X111)
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X0,X108) )
| ~ ! [X102] :
( ! [X103] :
( ! [X104] :
( ~ ( ! [X107] :
( p1(X107)
| ~ r1(X104,X107) )
& ~ ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) ) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X0,X102) )
| ~ ! [X94] :
( ! [X95] :
( ! [X96] :
( ~ ( ! [X100] :
( ~ ! [X101] :
( ~ p1(X101)
| ~ r1(X100,X101) )
| ~ r1(X96,X100) )
& ~ ! [X97] :
( ! [X98] :
( ~ ! [X99] :
( ~ p1(X99)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) ) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X0,X94) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( p1(X91)
& ~ ! [X92] :
( ~ ! [X93] :
( ~ p1(X93)
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X84] :
( ! [X85] :
( ! [X86] :
( ~ ( ~ p1(X86)
& ~ ! [X87] :
( ~ ! [X88] :
( p1(X88)
| ~ r1(X87,X88) )
| ~ r1(X86,X87) ) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) )
| ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ~ ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| p1(X82)
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
| ~ ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( ~ ! [X77] : ~ r1(X76,X77)
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X0,X73) )
| ~ ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ~ ( ! [X72] :
( p1(X72)
| ~ r1(X69,X72) )
& ~ ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) ) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) )
| ~ ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ~ ( ! [X64] :
( ~ ! [X65] :
( ~ p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X60,X64) )
& ~ ! [X61] :
( ! [X62] :
( ~ ! [X63] :
( ~ p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) ) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X0,X57) )
| ~ ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ ( p1(X54)
& ~ ! [X55] :
( ~ ! [X56] :
( ~ p1(X56)
| ~ r1(X55,X56) )
| ~ r1(X54,X55) ) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X0,X51) )
| ~ ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( ~ ( ~ p1(X48)
& ~ ! [X49] :
( ~ ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) ) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X0,X45) )
| ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X0,X39) )
| ~ ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X38] : ~ r1(X37,X38)
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ~ ( ! [X32] :
( p1(X32)
| ~ r1(X29,X32) )
& ~ ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X0,X25) )
| ~ ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ~ ( ! [X23] :
( ~ ! [X24] :
( ~ p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X19,X23) )
& ~ ! [X20] :
( ! [X21] :
( ~ ! [X22] :
( ~ p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) ) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ ( p1(X12)
& ~ ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) ) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( ~ p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(true_and_false_elimination,[],[f3]) ).
fof(f5,plain,
? [X0] :
~ ( ! [X165] :
( ! [X166] :
( ! [X167] :
( ! [X168] :
( ! [X169] :
( ~ ! [X170] :
( p1(X170)
| ~ r1(X169,X170) )
| p1(X169)
| ~ r1(X168,X169) )
| ~ r1(X167,X168) )
| ~ r1(X166,X167) )
| ~ r1(X165,X166) )
| ~ r1(X0,X165) )
| ~ ! [X163] :
( ~ ! [X164] : ~ r1(X163,X164)
| ~ r1(X0,X163) )
| ~ ! [X159] :
( ~ ( ! [X162] :
( p1(X162)
| ~ r1(X159,X162) )
& ~ ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) ) )
| ~ r1(X0,X159) )
| ~ ! [X153] :
( ~ ( ! [X157] :
( ~ ! [X158] :
( ~ p1(X158)
| ~ r1(X157,X158) )
| ~ r1(X153,X157) )
& ~ ! [X154] :
( ! [X155] :
( ~ ! [X156] :
( ~ p1(X156)
| ~ r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) ) )
| ~ r1(X0,X153) )
| ~ ! [X150] :
( ~ ( p1(X150)
& ~ ! [X151] :
( ~ ! [X152] :
( ~ p1(X152)
| ~ r1(X151,X152) )
| ~ r1(X150,X151) ) )
| ~ r1(X0,X150) )
| ~ ! [X147] :
( ~ ( ~ p1(X147)
& ~ ! [X148] :
( ~ ! [X149] :
( p1(X149)
| ~ r1(X148,X149) )
| ~ r1(X147,X148) ) )
| ~ r1(X0,X147) )
| ! [X141] :
( ! [X142] :
( ! [X143] :
( ! [X144] :
( ! [X145] :
( ~ ! [X146] :
( p1(X146)
| ~ r1(X145,X146) )
| p1(X145)
| ~ r1(X144,X145) )
| ~ r1(X143,X144) )
| ~ r1(X142,X143) )
| ~ r1(X141,X142) )
| ~ r1(X0,X141) )
| ~ ! [X138] :
( ! [X139] :
( ~ ! [X140] : ~ r1(X139,X140)
| ~ r1(X138,X139) )
| ~ r1(X0,X138) )
| ~ ! [X133] :
( ! [X134] :
( ~ ( ! [X137] :
( p1(X137)
| ~ r1(X134,X137) )
& ~ ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) ) )
| ~ r1(X133,X134) )
| ~ r1(X0,X133) )
| ~ ! [X126] :
( ! [X127] :
( ~ ( ! [X131] :
( ~ ! [X132] :
( ~ p1(X132)
| ~ r1(X131,X132) )
| ~ r1(X127,X131) )
& ~ ! [X128] :
( ! [X129] :
( ~ ! [X130] :
( ~ p1(X130)
| ~ r1(X129,X130) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) ) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
| ~ ! [X122] :
( ! [X123] :
( ~ ( p1(X123)
& ~ ! [X124] :
( ~ ! [X125] :
( ~ p1(X125)
| ~ r1(X124,X125) )
| ~ r1(X123,X124) ) )
| ~ r1(X122,X123) )
| ~ r1(X0,X122) )
| ~ ! [X118] :
( ! [X119] :
( ~ ( ~ p1(X119)
& ~ ! [X120] :
( ~ ! [X121] :
( p1(X121)
| ~ r1(X120,X121) )
| ~ r1(X119,X120) ) )
| ~ r1(X118,X119) )
| ~ r1(X0,X118) )
| ! [X112] :
( ! [X113] :
( ! [X114] :
( ! [X115] :
( ! [X116] :
( ~ ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
| p1(X116)
| ~ r1(X115,X116) )
| ~ r1(X114,X115) )
| ~ r1(X113,X114) )
| ~ r1(X112,X113) )
| ~ r1(X0,X112) )
| ~ ! [X108] :
( ! [X109] :
( ! [X110] :
( ~ ! [X111] : ~ r1(X110,X111)
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X0,X108) )
| ~ ! [X102] :
( ! [X103] :
( ! [X104] :
( ~ ( ! [X107] :
( p1(X107)
| ~ r1(X104,X107) )
& ~ ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) ) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X0,X102) )
| ~ ! [X94] :
( ! [X95] :
( ! [X96] :
( ~ ( ! [X100] :
( ~ ! [X101] :
( ~ p1(X101)
| ~ r1(X100,X101) )
| ~ r1(X96,X100) )
& ~ ! [X97] :
( ! [X98] :
( ~ ! [X99] :
( ~ p1(X99)
| ~ r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) ) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X0,X94) )
| ~ ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ ( p1(X91)
& ~ ! [X92] :
( ~ ! [X93] :
( ~ p1(X93)
| ~ r1(X92,X93) )
| ~ r1(X91,X92) ) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
| ~ ! [X84] :
( ! [X85] :
( ! [X86] :
( ~ ( ~ p1(X86)
& ~ ! [X87] :
( ~ ! [X88] :
( p1(X88)
| ~ r1(X87,X88) )
| ~ r1(X86,X87) ) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) )
| ! [X78] :
( ! [X79] :
( ! [X80] :
( ! [X81] :
( ! [X82] :
( ~ ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
| p1(X82)
| ~ r1(X81,X82) )
| ~ r1(X80,X81) )
| ~ r1(X79,X80) )
| ~ r1(X78,X79) )
| ~ r1(X0,X78) )
| ~ ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( ~ ! [X77] : ~ r1(X76,X77)
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X0,X73) )
| ~ ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ~ ( ! [X72] :
( p1(X72)
| ~ r1(X69,X72) )
& ~ ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) ) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) )
| ~ ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ~ ( ! [X64] :
( ~ ! [X65] :
( ~ p1(X65)
| ~ r1(X64,X65) )
| ~ r1(X60,X64) )
& ~ ! [X61] :
( ! [X62] :
( ~ ! [X63] :
( ~ p1(X63)
| ~ r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) ) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X0,X57) )
| ~ ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ ( p1(X54)
& ~ ! [X55] :
( ~ ! [X56] :
( ~ p1(X56)
| ~ r1(X55,X56) )
| ~ r1(X54,X55) ) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X0,X51) )
| ~ ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( ~ ( ~ p1(X48)
& ~ ! [X49] :
( ~ ! [X50] :
( p1(X50)
| ~ r1(X49,X50) )
| ~ r1(X48,X49) ) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X0,X45) )
| ! [X39] :
( ! [X40] :
( ! [X41] :
( ! [X42] :
( ! [X43] :
( ~ ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
| p1(X43)
| ~ r1(X42,X43) )
| ~ r1(X41,X42) )
| ~ r1(X40,X41) )
| ~ r1(X39,X40) )
| ~ r1(X0,X39) )
| ~ ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ~ ! [X38] : ~ r1(X37,X38)
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
| ~ ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ~ ( ! [X32] :
( p1(X32)
| ~ r1(X29,X32) )
& ~ ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) ) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X0,X25) )
| ~ ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ~ ( ! [X23] :
( ~ ! [X24] :
( ~ p1(X24)
| ~ r1(X23,X24) )
| ~ r1(X19,X23) )
& ~ ! [X20] :
( ! [X21] :
( ~ ! [X22] :
( ~ p1(X22)
| ~ r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) ) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
| ~ ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ ( p1(X12)
& ~ ! [X13] :
( ~ ! [X14] :
( ~ p1(X14)
| ~ r1(X13,X14) )
| ~ r1(X12,X13) ) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
| ~ ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ~ ( ~ p1(X5)
& ~ ! [X6] :
( ~ ! [X7] :
( p1(X7)
| ~ r1(X6,X7) )
| ~ r1(X5,X6) ) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f4]) ).
fof(f6,plain,
? [X0] :
( ? [X165] :
( ? [X166] :
( ? [X167] :
( ? [X168] :
( ? [X169] :
( ! [X170] :
( p1(X170)
| ~ r1(X169,X170) )
& ~ p1(X169)
& r1(X168,X169) )
& r1(X167,X168) )
& r1(X166,X167) )
& r1(X165,X166) )
& r1(X0,X165) )
& ! [X163] :
( ? [X164] : r1(X163,X164)
| ~ r1(X0,X163) )
& ! [X159] :
( ? [X162] :
( ~ p1(X162)
& r1(X159,X162) )
| ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) )
| ~ r1(X0,X159) )
& ! [X153] :
( ? [X157] :
( ! [X158] :
( ~ p1(X158)
| ~ r1(X157,X158) )
& r1(X153,X157) )
| ! [X154] :
( ! [X155] :
( ? [X156] :
( p1(X156)
& r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X0,X153) )
& ! [X150] :
( ~ p1(X150)
| ! [X151] :
( ? [X152] :
( p1(X152)
& r1(X151,X152) )
| ~ r1(X150,X151) )
| ~ r1(X0,X150) )
& ! [X147] :
( p1(X147)
| ! [X148] :
( ? [X149] :
( ~ p1(X149)
& r1(X148,X149) )
| ~ r1(X147,X148) )
| ~ r1(X0,X147) )
& ? [X141] :
( ? [X142] :
( ? [X143] :
( ? [X144] :
( ? [X145] :
( ! [X146] :
( p1(X146)
| ~ r1(X145,X146) )
& ~ p1(X145)
& r1(X144,X145) )
& r1(X143,X144) )
& r1(X142,X143) )
& r1(X141,X142) )
& r1(X0,X141) )
& ! [X138] :
( ! [X139] :
( ? [X140] : r1(X139,X140)
| ~ r1(X138,X139) )
| ~ r1(X0,X138) )
& ! [X133] :
( ! [X134] :
( ? [X137] :
( ~ p1(X137)
& r1(X134,X137) )
| ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X0,X133) )
& ! [X126] :
( ! [X127] :
( ? [X131] :
( ! [X132] :
( ~ p1(X132)
| ~ r1(X131,X132) )
& r1(X127,X131) )
| ! [X128] :
( ! [X129] :
( ? [X130] :
( p1(X130)
& r1(X129,X130) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ! [X122] :
( ! [X123] :
( ~ p1(X123)
| ! [X124] :
( ? [X125] :
( p1(X125)
& r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X0,X122) )
& ! [X118] :
( ! [X119] :
( p1(X119)
| ! [X120] :
( ? [X121] :
( ~ p1(X121)
& r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X0,X118) )
& ? [X112] :
( ? [X113] :
( ? [X114] :
( ? [X115] :
( ? [X116] :
( ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
& ~ p1(X116)
& r1(X115,X116) )
& r1(X114,X115) )
& r1(X113,X114) )
& r1(X112,X113) )
& r1(X0,X112) )
& ! [X108] :
( ! [X109] :
( ! [X110] :
( ? [X111] : r1(X110,X111)
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X0,X108) )
& ! [X102] :
( ! [X103] :
( ! [X104] :
( ? [X107] :
( ~ p1(X107)
& r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X0,X102) )
& ! [X94] :
( ! [X95] :
( ! [X96] :
( ? [X100] :
( ! [X101] :
( ~ p1(X101)
| ~ r1(X100,X101) )
& r1(X96,X100) )
| ! [X97] :
( ! [X98] :
( ? [X99] :
( p1(X99)
& r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X0,X94) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ p1(X91)
| ! [X92] :
( ? [X93] :
( p1(X93)
& r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
& ! [X84] :
( ! [X85] :
( ! [X86] :
( p1(X86)
| ! [X87] :
( ? [X88] :
( ~ p1(X88)
& r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) )
& ? [X78] :
( ? [X79] :
( ? [X80] :
( ? [X81] :
( ? [X82] :
( ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
& ~ p1(X82)
& r1(X81,X82) )
& r1(X80,X81) )
& r1(X79,X80) )
& r1(X78,X79) )
& r1(X0,X78) )
& ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( ? [X77] : r1(X76,X77)
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X0,X73) )
& ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ? [X72] :
( ~ p1(X72)
& r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) )
& ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ? [X64] :
( ! [X65] :
( ~ p1(X65)
| ~ r1(X64,X65) )
& r1(X60,X64) )
| ! [X61] :
( ! [X62] :
( ? [X63] :
( p1(X63)
& r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X0,X57) )
& ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ p1(X54)
| ! [X55] :
( ? [X56] :
( p1(X56)
& r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X0,X51) )
& ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( p1(X48)
| ! [X49] :
( ? [X50] :
( ~ p1(X50)
& r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X0,X45) )
& ? [X39] :
( ? [X40] :
( ? [X41] :
( ? [X42] :
( ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
& r1(X40,X41) )
& r1(X39,X40) )
& r1(X0,X39) )
& ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ? [X38] : r1(X37,X38)
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
& ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ? [X32] :
( ~ p1(X32)
& r1(X29,X32) )
| ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X0,X25) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ? [X23] :
( ! [X24] :
( ~ p1(X24)
| ~ r1(X23,X24) )
& r1(X19,X23) )
| ! [X20] :
( ! [X21] :
( ? [X22] :
( p1(X22)
& r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ p1(X12)
| ! [X13] :
( ? [X14] :
( p1(X14)
& r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( p1(X5)
| ! [X6] :
( ? [X7] :
( ~ p1(X7)
& r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(ennf_transformation,[],[f5]) ).
fof(f7,plain,
? [X0] :
( ? [X165] :
( ? [X166] :
( ? [X167] :
( ? [X168] :
( ? [X169] :
( ! [X170] :
( p1(X170)
| ~ r1(X169,X170) )
& ~ p1(X169)
& r1(X168,X169) )
& r1(X167,X168) )
& r1(X166,X167) )
& r1(X165,X166) )
& r1(X0,X165) )
& ! [X163] :
( ? [X164] : r1(X163,X164)
| ~ r1(X0,X163) )
& ! [X159] :
( ? [X162] :
( ~ p1(X162)
& r1(X159,X162) )
| ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) )
| ~ r1(X0,X159) )
& ! [X153] :
( ? [X157] :
( ! [X158] :
( ~ p1(X158)
| ~ r1(X157,X158) )
& r1(X153,X157) )
| ! [X154] :
( ! [X155] :
( ? [X156] :
( p1(X156)
& r1(X155,X156) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(X0,X153) )
& ! [X150] :
( ~ p1(X150)
| ! [X151] :
( ? [X152] :
( p1(X152)
& r1(X151,X152) )
| ~ r1(X150,X151) )
| ~ r1(X0,X150) )
& ! [X147] :
( p1(X147)
| ! [X148] :
( ? [X149] :
( ~ p1(X149)
& r1(X148,X149) )
| ~ r1(X147,X148) )
| ~ r1(X0,X147) )
& ? [X141] :
( ? [X142] :
( ? [X143] :
( ? [X144] :
( ? [X145] :
( ! [X146] :
( p1(X146)
| ~ r1(X145,X146) )
& ~ p1(X145)
& r1(X144,X145) )
& r1(X143,X144) )
& r1(X142,X143) )
& r1(X141,X142) )
& r1(X0,X141) )
& ! [X138] :
( ! [X139] :
( ? [X140] : r1(X139,X140)
| ~ r1(X138,X139) )
| ~ r1(X0,X138) )
& ! [X133] :
( ! [X134] :
( ? [X137] :
( ~ p1(X137)
& r1(X134,X137) )
| ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(X0,X133) )
& ! [X126] :
( ! [X127] :
( ? [X131] :
( ! [X132] :
( ~ p1(X132)
| ~ r1(X131,X132) )
& r1(X127,X131) )
| ! [X128] :
( ! [X129] :
( ? [X130] :
( p1(X130)
& r1(X129,X130) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(X0,X126) )
& ! [X122] :
( ! [X123] :
( ~ p1(X123)
| ! [X124] :
( ? [X125] :
( p1(X125)
& r1(X124,X125) )
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(X0,X122) )
& ! [X118] :
( ! [X119] :
( p1(X119)
| ! [X120] :
( ? [X121] :
( ~ p1(X121)
& r1(X120,X121) )
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(X0,X118) )
& ? [X112] :
( ? [X113] :
( ? [X114] :
( ? [X115] :
( ? [X116] :
( ! [X117] :
( p1(X117)
| ~ r1(X116,X117) )
& ~ p1(X116)
& r1(X115,X116) )
& r1(X114,X115) )
& r1(X113,X114) )
& r1(X112,X113) )
& r1(X0,X112) )
& ! [X108] :
( ! [X109] :
( ! [X110] :
( ? [X111] : r1(X110,X111)
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(X0,X108) )
& ! [X102] :
( ! [X103] :
( ! [X104] :
( ? [X107] :
( ~ p1(X107)
& r1(X104,X107) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(X0,X102) )
& ! [X94] :
( ! [X95] :
( ! [X96] :
( ? [X100] :
( ! [X101] :
( ~ p1(X101)
| ~ r1(X100,X101) )
& r1(X96,X100) )
| ! [X97] :
( ! [X98] :
( ? [X99] :
( p1(X99)
& r1(X98,X99) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(X0,X94) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ p1(X91)
| ! [X92] :
( ? [X93] :
( p1(X93)
& r1(X92,X93) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(X0,X89) )
& ! [X84] :
( ! [X85] :
( ! [X86] :
( p1(X86)
| ! [X87] :
( ? [X88] :
( ~ p1(X88)
& r1(X87,X88) )
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(X0,X84) )
& ? [X78] :
( ? [X79] :
( ? [X80] :
( ? [X81] :
( ? [X82] :
( ! [X83] :
( p1(X83)
| ~ r1(X82,X83) )
& ~ p1(X82)
& r1(X81,X82) )
& r1(X80,X81) )
& r1(X79,X80) )
& r1(X78,X79) )
& r1(X0,X78) )
& ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( ? [X77] : r1(X76,X77)
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(X0,X73) )
& ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ? [X72] :
( ~ p1(X72)
& r1(X69,X72) )
| ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(X0,X66) )
& ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ? [X64] :
( ! [X65] :
( ~ p1(X65)
| ~ r1(X64,X65) )
& r1(X60,X64) )
| ! [X61] :
( ! [X62] :
( ? [X63] :
( p1(X63)
& r1(X62,X63) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(X0,X57) )
& ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ p1(X54)
| ! [X55] :
( ? [X56] :
( p1(X56)
& r1(X55,X56) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(X0,X51) )
& ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( p1(X48)
| ! [X49] :
( ? [X50] :
( ~ p1(X50)
& r1(X49,X50) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(X0,X45) )
& ? [X39] :
( ? [X40] :
( ? [X41] :
( ? [X42] :
( ? [X43] :
( ! [X44] :
( p1(X44)
| ~ r1(X43,X44) )
& ~ p1(X43)
& r1(X42,X43) )
& r1(X41,X42) )
& r1(X40,X41) )
& r1(X39,X40) )
& r1(X0,X39) )
& ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( ? [X38] : r1(X37,X38)
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(X0,X33) )
& ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ? [X32] :
( ~ p1(X32)
& r1(X29,X32) )
| ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(X0,X25) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ? [X23] :
( ! [X24] :
( ~ p1(X24)
| ~ r1(X23,X24) )
& r1(X19,X23) )
| ! [X20] :
( ! [X21] :
( ? [X22] :
( p1(X22)
& r1(X21,X22) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(X0,X15) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ p1(X12)
| ! [X13] :
( ? [X14] :
( p1(X14)
& r1(X13,X14) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(X0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( p1(X5)
| ! [X6] :
( ? [X7] :
( ~ p1(X7)
& r1(X6,X7) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(X0,X1) ) ),
inference(flattening,[],[f6]) ).
fof(f8,plain,
( ! [X170] :
( p1(X170)
| ~ r1(sK55,X170) )
& ~ p1(sK55)
& r1(sK54,sK55)
& r1(sK53,sK54)
& r1(sK52,sK53)
& r1(sK51,sK52)
& r1(sK0,sK51)
& ! [X163] :
( r1(X163,sK50(X163))
| ~ r1(sK0,X163) )
& ! [X159] :
( ( ~ p1(sK49(X159))
& r1(X159,sK49(X159)) )
| ! [X160] :
( ! [X161] :
( p1(X161)
| ~ r1(X160,X161) )
| ~ r1(X159,X160) )
| ~ r1(sK0,X159) )
& ! [X153] :
( ( ! [X158] :
( ~ p1(X158)
| ~ r1(sK48(X153),X158) )
& r1(X153,sK48(X153)) )
| ! [X154] :
( ! [X155] :
( ( p1(sK47(X155))
& r1(X155,sK47(X155)) )
| ~ r1(X154,X155) )
| ~ r1(X153,X154) )
| ~ r1(sK0,X153) )
& ! [X150] :
( ~ p1(X150)
| ! [X151] :
( ( p1(sK46(X151))
& r1(X151,sK46(X151)) )
| ~ r1(X150,X151) )
| ~ r1(sK0,X150) )
& ! [X147] :
( p1(X147)
| ! [X148] :
( ( ~ p1(sK45(X148))
& r1(X148,sK45(X148)) )
| ~ r1(X147,X148) )
| ~ r1(sK0,X147) )
& ! [X146] :
( p1(X146)
| ~ r1(sK44,X146) )
& ~ p1(sK44)
& r1(sK43,sK44)
& r1(sK42,sK43)
& r1(sK41,sK42)
& r1(sK40,sK41)
& r1(sK0,sK40)
& ! [X138] :
( ! [X139] :
( r1(X139,sK39(X139))
| ~ r1(X138,X139) )
| ~ r1(sK0,X138) )
& ! [X133] :
( ! [X134] :
( ( ~ p1(sK38(X134))
& r1(X134,sK38(X134)) )
| ! [X135] :
( ! [X136] :
( p1(X136)
| ~ r1(X135,X136) )
| ~ r1(X134,X135) )
| ~ r1(X133,X134) )
| ~ r1(sK0,X133) )
& ! [X126] :
( ! [X127] :
( ( ! [X132] :
( ~ p1(X132)
| ~ r1(sK37(X127),X132) )
& r1(X127,sK37(X127)) )
| ! [X128] :
( ! [X129] :
( ( p1(sK36(X129))
& r1(X129,sK36(X129)) )
| ~ r1(X128,X129) )
| ~ r1(X127,X128) )
| ~ r1(X126,X127) )
| ~ r1(sK0,X126) )
& ! [X122] :
( ! [X123] :
( ~ p1(X123)
| ! [X124] :
( ( p1(sK35(X124))
& r1(X124,sK35(X124)) )
| ~ r1(X123,X124) )
| ~ r1(X122,X123) )
| ~ r1(sK0,X122) )
& ! [X118] :
( ! [X119] :
( p1(X119)
| ! [X120] :
( ( ~ p1(sK34(X120))
& r1(X120,sK34(X120)) )
| ~ r1(X119,X120) )
| ~ r1(X118,X119) )
| ~ r1(sK0,X118) )
& ! [X117] :
( p1(X117)
| ~ r1(sK33,X117) )
& ~ p1(sK33)
& r1(sK32,sK33)
& r1(sK31,sK32)
& r1(sK30,sK31)
& r1(sK29,sK30)
& r1(sK0,sK29)
& ! [X108] :
( ! [X109] :
( ! [X110] :
( r1(X110,sK28(X110))
| ~ r1(X109,X110) )
| ~ r1(X108,X109) )
| ~ r1(sK0,X108) )
& ! [X102] :
( ! [X103] :
( ! [X104] :
( ( ~ p1(sK27(X104))
& r1(X104,sK27(X104)) )
| ! [X105] :
( ! [X106] :
( p1(X106)
| ~ r1(X105,X106) )
| ~ r1(X104,X105) )
| ~ r1(X103,X104) )
| ~ r1(X102,X103) )
| ~ r1(sK0,X102) )
& ! [X94] :
( ! [X95] :
( ! [X96] :
( ( ! [X101] :
( ~ p1(X101)
| ~ r1(sK26(X96),X101) )
& r1(X96,sK26(X96)) )
| ! [X97] :
( ! [X98] :
( ( p1(sK25(X98))
& r1(X98,sK25(X98)) )
| ~ r1(X97,X98) )
| ~ r1(X96,X97) )
| ~ r1(X95,X96) )
| ~ r1(X94,X95) )
| ~ r1(sK0,X94) )
& ! [X89] :
( ! [X90] :
( ! [X91] :
( ~ p1(X91)
| ! [X92] :
( ( p1(sK24(X92))
& r1(X92,sK24(X92)) )
| ~ r1(X91,X92) )
| ~ r1(X90,X91) )
| ~ r1(X89,X90) )
| ~ r1(sK0,X89) )
& ! [X84] :
( ! [X85] :
( ! [X86] :
( p1(X86)
| ! [X87] :
( ( ~ p1(sK23(X87))
& r1(X87,sK23(X87)) )
| ~ r1(X86,X87) )
| ~ r1(X85,X86) )
| ~ r1(X84,X85) )
| ~ r1(sK0,X84) )
& ! [X83] :
( p1(X83)
| ~ r1(sK22,X83) )
& ~ p1(sK22)
& r1(sK21,sK22)
& r1(sK20,sK21)
& r1(sK19,sK20)
& r1(sK18,sK19)
& r1(sK0,sK18)
& ! [X73] :
( ! [X74] :
( ! [X75] :
( ! [X76] :
( r1(X76,sK17(X76))
| ~ r1(X75,X76) )
| ~ r1(X74,X75) )
| ~ r1(X73,X74) )
| ~ r1(sK0,X73) )
& ! [X66] :
( ! [X67] :
( ! [X68] :
( ! [X69] :
( ( ~ p1(sK16(X69))
& r1(X69,sK16(X69)) )
| ! [X70] :
( ! [X71] :
( p1(X71)
| ~ r1(X70,X71) )
| ~ r1(X69,X70) )
| ~ r1(X68,X69) )
| ~ r1(X67,X68) )
| ~ r1(X66,X67) )
| ~ r1(sK0,X66) )
& ! [X57] :
( ! [X58] :
( ! [X59] :
( ! [X60] :
( ( ! [X65] :
( ~ p1(X65)
| ~ r1(sK15(X60),X65) )
& r1(X60,sK15(X60)) )
| ! [X61] :
( ! [X62] :
( ( p1(sK14(X62))
& r1(X62,sK14(X62)) )
| ~ r1(X61,X62) )
| ~ r1(X60,X61) )
| ~ r1(X59,X60) )
| ~ r1(X58,X59) )
| ~ r1(X57,X58) )
| ~ r1(sK0,X57) )
& ! [X51] :
( ! [X52] :
( ! [X53] :
( ! [X54] :
( ~ p1(X54)
| ! [X55] :
( ( p1(sK13(X55))
& r1(X55,sK13(X55)) )
| ~ r1(X54,X55) )
| ~ r1(X53,X54) )
| ~ r1(X52,X53) )
| ~ r1(X51,X52) )
| ~ r1(sK0,X51) )
& ! [X45] :
( ! [X46] :
( ! [X47] :
( ! [X48] :
( p1(X48)
| ! [X49] :
( ( ~ p1(sK12(X49))
& r1(X49,sK12(X49)) )
| ~ r1(X48,X49) )
| ~ r1(X47,X48) )
| ~ r1(X46,X47) )
| ~ r1(X45,X46) )
| ~ r1(sK0,X45) )
& ! [X44] :
( p1(X44)
| ~ r1(sK11,X44) )
& ~ p1(sK11)
& r1(sK10,sK11)
& r1(sK9,sK10)
& r1(sK8,sK9)
& r1(sK7,sK8)
& r1(sK0,sK7)
& ! [X33] :
( ! [X34] :
( ! [X35] :
( ! [X36] :
( ! [X37] :
( r1(X37,sK6(X37))
| ~ r1(X36,X37) )
| ~ r1(X35,X36) )
| ~ r1(X34,X35) )
| ~ r1(X33,X34) )
| ~ r1(sK0,X33) )
& ! [X25] :
( ! [X26] :
( ! [X27] :
( ! [X28] :
( ! [X29] :
( ( ~ p1(sK5(X29))
& r1(X29,sK5(X29)) )
| ! [X30] :
( ! [X31] :
( p1(X31)
| ~ r1(X30,X31) )
| ~ r1(X29,X30) )
| ~ r1(X28,X29) )
| ~ r1(X27,X28) )
| ~ r1(X26,X27) )
| ~ r1(X25,X26) )
| ~ r1(sK0,X25) )
& ! [X15] :
( ! [X16] :
( ! [X17] :
( ! [X18] :
( ! [X19] :
( ( ! [X24] :
( ~ p1(X24)
| ~ r1(sK4(X19),X24) )
& r1(X19,sK4(X19)) )
| ! [X20] :
( ! [X21] :
( ( p1(sK3(X21))
& r1(X21,sK3(X21)) )
| ~ r1(X20,X21) )
| ~ r1(X19,X20) )
| ~ r1(X18,X19) )
| ~ r1(X17,X18) )
| ~ r1(X16,X17) )
| ~ r1(X15,X16) )
| ~ r1(sK0,X15) )
& ! [X8] :
( ! [X9] :
( ! [X10] :
( ! [X11] :
( ! [X12] :
( ~ p1(X12)
| ! [X13] :
( ( p1(sK2(X13))
& r1(X13,sK2(X13)) )
| ~ r1(X12,X13) )
| ~ r1(X11,X12) )
| ~ r1(X10,X11) )
| ~ r1(X9,X10) )
| ~ r1(X8,X9) )
| ~ r1(sK0,X8) )
& ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( p1(X5)
| ! [X6] :
( ( ~ p1(sK1(X6))
& r1(X6,sK1(X6)) )
| ~ r1(X5,X6) )
| ~ r1(X4,X5) )
| ~ r1(X3,X4) )
| ~ r1(X2,X3) )
| ~ r1(X1,X2) )
| ~ r1(sK0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,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,sK50,sK51,sK52,sK53,sK54,sK55]),skolemize(X0,sK0),skolemize(X7,sK1(X6)),skolemize(X14,sK2(X13)),skolemize(X22,sK3(X21)),skolemize(X23,sK4(X19)),skolemize(X32,sK5(X29)),skolemize(X38,sK6(X37)),skolemize(X39,sK7),skolemize(X40,sK8),skolemize(X41,sK9),skolemize(X42,sK10),skolemize(X43,sK11),skolemize(X50,sK12(X49)),skolemize(X56,sK13(X55)),skolemize(X63,sK14(X62)),skolemize(X64,sK15(X60)),skolemize(X72,sK16(X69)),skolemize(X77,sK17(X76)),skolemize(X78,sK18),skolemize(X79,sK19),skolemize(X80,sK20),skolemize(X81,sK21),skolemize(X82,sK22),skolemize(X88,sK23(X87)),skolemize(X93,sK24(X92)),skolemize(X99,sK25(X98)),skolemize(X100,sK26(X96)),skolemize(X107,sK27(X104)),skolemize(X111,sK28(X110)),skolemize(X112,sK29),skolemize(X113,sK30),skolemize(X114,sK31),skolemize(X115,sK32),skolemize(X116,sK33),skolemize(X121,sK34(X120)),skolemize(X125,sK35(X124)),skolemize(X130,sK36(X129)),skolemize(X131,sK37(X127)),skolemize(X137,sK38(X134)),skolemize(X140,sK39(X139)),skolemize(X141,sK40),skolemize(X142,sK41),skolemize(X143,sK42),skolemize(X144,sK43),skolemize(X145,sK44),skolemize(X149,sK45(X148)),skolemize(X152,sK46(X151)),skolemize(X156,sK47(X155)),skolemize(X157,sK48(X153)),skolemize(X162,sK49(X159)),skolemize(X164,sK50(X163)),skolemize(X165,sK51),skolemize(X166,sK52),skolemize(X167,sK53),skolemize(X168,sK54),skolemize(X169,sK55)],[f7]) ).
fof(f27,plain,
! [X146] :
( p1(X146)
| ~ r1(sK44,X146) ),
inference(cnf_transformation,[],[f8]) ).
fof(f28,plain,
~ p1(sK44),
inference(cnf_transformation,[],[f8]) ).
fof(f29,plain,
r1(sK43,sK44),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
r1(sK42,sK43),
inference(cnf_transformation,[],[f8]) ).
fof(f31,plain,
r1(sK41,sK42),
inference(cnf_transformation,[],[f8]) ).
fof(f32,plain,
r1(sK40,sK41),
inference(cnf_transformation,[],[f8]) ).
fof(f33,plain,
r1(sK0,sK40),
inference(cnf_transformation,[],[f8]) ).
fof(f88,plain,
! [X36,X37,X34,X35,X33] :
( r1(X37,sK6(X37))
| ~ r1(X36,X37)
| ~ r1(X35,X36)
| ~ r1(X34,X35)
| ~ r1(X33,X34)
| ~ r1(sK0,X33) ),
inference(cnf_transformation,[],[f8]) ).
fof(f89,plain,
! [X31,X28,X29,X26,X27,X25,X30] :
( ~ p1(sK5(X29))
| p1(X31)
| ~ r1(X30,X31)
| ~ r1(X29,X30)
| ~ r1(X28,X29)
| ~ r1(X27,X28)
| ~ r1(X26,X27)
| ~ r1(X25,X26)
| ~ r1(sK0,X25) ),
inference(cnf_transformation,[],[f8]) ).
fof(f90,plain,
! [X31,X28,X29,X26,X27,X25,X30] :
( r1(X29,sK5(X29))
| p1(X31)
| ~ r1(X30,X31)
| ~ r1(X29,X30)
| ~ r1(X28,X29)
| ~ r1(X27,X28)
| ~ r1(X26,X27)
| ~ r1(X25,X26)
| ~ r1(sK0,X25) ),
inference(cnf_transformation,[],[f8]) ).
fof(f97,plain,
! [X2,X3,X1,X6,X4,X5] :
( p1(X5)
| ~ p1(sK1(X6))
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f8]) ).
fof(f98,plain,
! [X2,X3,X1,X6,X4,X5] :
( p1(X5)
| r1(X6,sK1(X6))
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(sK0,X1) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_49,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X4)
| r1(X5,sK1(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_50,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X4)
| ~ p1(sK1(X5))
| ~ r1(sK0,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_57,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| r1(X4,sK5(X4))
| ~ r1(sK0,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_58,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( p1(X6)
| ~ p1(sK5(X4))
| ~ r1(sK0,X0)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_59,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( r1(X4,sK6(X4))
| ~ r1(sK0,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_114,negated_conjecture,
r1(sK0,sK40),
inference(cnf_transformation,[],[f33]) ).
tcf(c_115,negated_conjecture,
r1(sK40,sK41),
inference(cnf_transformation,[],[f32]) ).
tcf(c_116,negated_conjecture,
r1(sK41,sK42),
inference(cnf_transformation,[],[f31]) ).
tcf(c_117,negated_conjecture,
r1(sK42,sK43),
inference(cnf_transformation,[],[f30]) ).
tcf(c_118,negated_conjecture,
r1(sK43,sK44),
inference(cnf_transformation,[],[f29]) ).
tcf(c_119,negated_conjecture,
~ p1(sK44),
inference(cnf_transformation,[],[f28]) ).
tcf(c_120,negated_conjecture,
! [X0: $i] :
( p1(X0)
| ~ r1(sK44,X0) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_516,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( r1(X3,sK6(X3))
| ~ r1(sK0,sK40)
| ~ r1(sK40,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_59]) ).
tcf(c_621,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X3)
| r1(X4,sK1(X4))
| ~ r1(sK0,sK40)
| ~ r1(sK40,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_49]) ).
tcf(c_1284,plain,
! [X0: $i,X1: $i,X2: $i] :
( r1(X2,sK6(X2))
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_516]) ).
tcf(c_1602,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X2)
| r1(X3,sK1(X3))
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_621]) ).
tcf(c_2734,plain,
! [X0: $i,X1: $i] :
( r1(X1,sK6(X1))
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK42,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_3074,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X1)
| r1(X2,sK1(X2))
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK42,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_1602]) ).
tcf(c_5785,plain,
! [X0: $i] :
( r1(X0,sK6(X0))
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK43,X0) ),
inference(instantiation,[status(thm)],[c_2734]) ).
tcf(c_6187,plain,
! [X0: $i,X1: $i] :
( p1(X0)
| r1(X1,sK1(X1))
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK43,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_3074]) ).
tcf(c_10627,plain,
( r1(sK44,sK6(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40) ),
inference(instantiation,[status(thm)],[c_5785]) ).
tcf(c_12192,plain,
! [X0: $i] :
( p1(sK44)
| r1(X0,sK1(X0))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,X0) ),
inference(instantiation,[status(thm)],[c_6187]) ).
tcf(c_14270,plain,
( p1(sK44)
| r1(sK6(sK44),sK1(sK6(sK44)))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_12192]) ).
tcf(c_32765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| r1(X3,sK5(X3))
| ~ r1(sK0,sK40)
| ~ r1(sK40,X0)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_57]) ).
tcf(c_33372,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| r1(X2,sK5(X2))
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_32765]) ).
tcf(c_34680,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| r1(X1,sK5(X1))
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK42,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_33372]) ).
tcf(c_36792,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X2)
| r1(X0,sK5(X0))
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK43,X0)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_34680]) ).
tcf(c_39920,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| r1(sK44,sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_36792]) ).
tcf(c_42933,plain,
! [X0: $i] :
( p1(X0)
| r1(sK44,sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,sK6(sK44))
| ~ r1(sK6(sK44),X0) ),
inference(instantiation,[status(thm)],[c_39920]) ).
tcf(c_49924,plain,
( p1(sK1(sK6(sK44)))
| r1(sK44,sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,sK6(sK44))
| ~ r1(sK6(sK44),sK1(sK6(sK44))) ),
inference(instantiation,[status(thm)],[c_42933]) ).
tcf(c_63929,plain,
( p1(sK5(sK44))
| ~ r1(sK44,sK5(sK44)) ),
inference(instantiation,[status(thm)],[c_120]) ).
tcf(c_95069,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( p1(X5)
| ~ p1(sK5(sK44))
| ~ r1(sK44,X4)
| ~ r1(sK0,X0)
| ~ r1(X3,sK44)
| ~ r1(X4,X5)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_58]) ).
tcf(c_99366,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X4)
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK44,X3)
| ~ r1(sK0,X0)
| ~ r1(X2,sK43)
| ~ r1(X3,X4)
| ~ r1(X1,X2)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_95069]) ).
tcf(c_100538,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( p1(X0)
| ~ r1(sK0,X1)
| ~ r1(X4,X0)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(X0,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_50]) ).
tcf(c_103539,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X3)
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK44,X2)
| ~ r1(sK0,X0)
| ~ r1(X1,sK42)
| ~ r1(X2,X3)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_99366]) ).
tcf(c_103561,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( p1(X0)
| ~ r1(sK0,sK40)
| ~ r1(sK40,X1)
| ~ r1(X3,X0)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(X0,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_100538]) ).
tcf(c_107251,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X1)
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK44,X0)
| ~ r1(sK0,X2)
| ~ r1(X2,sK41)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_103539]) ).
tcf(c_107311,plain,
! [X0: $i,X1: $i,X2: $i] :
( p1(X0)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X1)
| ~ r1(X2,X0)
| ~ r1(X1,X2)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(X0,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_103561]) ).
tcf(c_112015,plain,
! [X0: $i,X1: $i] :
( p1(X1)
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,X0)
| ~ r1(X0,X1) ),
inference(instantiation,[status(thm)],[c_107251]) ).
tcf(c_113477,plain,
! [X0: $i,X1: $i] :
( p1(sK44)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X0)
| ~ r1(X1,sK44)
| ~ r1(X0,X1)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(sK44,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_107311]) ).
tcf(c_116852,plain,
! [X0: $i] :
( p1(X0)
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,sK6(sK44))
| ~ r1(sK6(sK44),X0) ),
inference(instantiation,[status(thm)],[c_112015]) ).
tcf(c_117371,plain,
! [X0: $i] :
( p1(sK44)
| ~ r1(sK43,sK44)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK41,X0)
| ~ r1(X0,sK43)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(sK44,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_113477]) ).
tcf(c_122761,plain,
( p1(sK44)
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ p1(sK1(sK6(sK44)))
| ~ r1(sK44,sK6(sK44)) ),
inference(instantiation,[status(thm)],[c_117371]) ).
tcf(c_123171,plain,
( p1(sK1(sK6(sK44)))
| ~ p1(sK5(sK44))
| ~ r1(sK43,sK44)
| ~ r1(sK42,sK43)
| ~ r1(sK41,sK42)
| ~ r1(sK40,sK41)
| ~ r1(sK0,sK40)
| ~ r1(sK44,sK6(sK44))
| ~ r1(sK6(sK44),sK1(sK6(sK44))) ),
inference(instantiation,[status(thm)],[c_116852]) ).
tcf(c_123172,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_123171,c_122761,c_63929,c_49924,c_14270,c_10627,c_114,c_115,c_116,c_117,c_118,c_119]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL638+1.005 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 23:50:57 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.16/0.43 Running first-order theorem proving
% 0.16/0.43 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.45
% 0.16/0.45 % ======== iProver multi-core TPTP/SMT =========
% 0.16/0.45
% 0.16/0.45 % Detected problem language: tptp
% 0.16/0.47 % Proving...
% 112.85/16.64 % SZS status Started for theBenchmark.p
% 112.85/16.64 % SZS status Theorem for theBenchmark.p
% 112.85/16.64
% 112.85/16.64 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 112.85/16.64
% 112.85/16.64 % ------ iProver source info
% 112.85/16.64
% 112.85/16.64 % git: date: 2026-07-19 20:42:38 +0200
% 112.85/16.64 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 112.85/16.64 % git: non_committed_changes: false
% 112.85/16.64
% 112.85/16.64 % ------ Parsing...
% 112.85/16.64 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 112.85/16.64
% 112.85/16.64 % ------ Preprocessing... sf_s rm: 0 0s sf_e %
% 112.85/16.64
% 112.85/16.64 % ------ Preprocessing...
% 112.85/16.64 % ------ Proving...
% 112.85/16.64 % ------ Problem Properties
% 112.85/16.64
% 112.85/16.64 %
% 112.85/16.64 % clauses 90
% 112.85/16.64 % conjectures 90
% 112.85/16.64 % EPR 35
% 112.85/16.64 % Horn 70
% 112.85/16.64 % unary 30
% 112.85/16.64 % binary 6
% 112.85/16.64 % lits 400
% 112.85/16.64 % lits eq 0
% 112.85/16.64 % fd_pure 0
% 112.85/16.64 % fd_pseudo 0
% 112.85/16.64 % fd_cond 0
% 112.85/16.64 % fd_pseudo_cond 0
% 112.85/16.64 % AC symbols 0
% 112.85/16.64
% 112.85/16.64 % ------ Input Options Time Limit: Unbounded
% 112.85/16.64
% 112.85/16.64
% 112.85/16.64 % ------
% 112.85/16.64 % Current options:
% 112.85/16.64 % ------
% 112.85/16.64
% 112.85/16.64
% 112.85/16.64 %
% 112.85/16.64
% 112.85/16.64 % ------ Proving...
% 112.85/16.64 %
% 112.85/16.64
% 112.85/16.64 % SZS status Theorem for theBenchmark.p
% 112.85/16.64
% 112.85/16.64 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 112.85/16.64
% 112.85/16.64
%------------------------------------------------------------------------------