%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : LCL652+1.020 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n006.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 : Thu Sep 24 01:15:13 PM UTC 2026
% Result : Theorem 185.13s 27.77s
% Output : CNFRefutation 185.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 6
% Syntax : Number of formulae : 137 ( 37 unt; 0 def)
% Number of atoms : 4436 ( 0 equ)
% Maximal formula atoms : 606 ( 32 avg)
% Number of connectives : 9166 (4867 ~;3731 |; 558 &)
% ( 5 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 307 ( 14 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 11 ( 10 usr; 1 prp; 0-2 aty)
% Number of functors : 176 ( 176 usr; 81 con; 0-7 aty)
% Number of variables : 2268 ( 0 sgn2126 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ p4(X2)
| ~ r1(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(c_0_1,negated_conjecture,
~ ~ ? [X1] :
~ ( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ p4(X2)
| ~ r1(X1,X2) ) ),
inference(assume_negation,[status(cth)],[main]) ).
fof(c_0_2,plain,
! [X1] :
( epred5_1(X1)
<=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
introduced(definition) ).
fof(c_0_3,negated_conjecture,
~ ~ ? [X1] :
~ ( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ! [X2] :
( ~ ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ! [X1] :
( ~ ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( epred5_1(X1)
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ p4(X2)
| ~ r1(X1,X2) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_1]),c_0_2]) ).
fof(c_0_4,negated_conjecture,
! [X4,X5,X6,X7,X10,X11,X12,X13,X14,X17,X18,X19,X20,X21,X24,X25,X26,X27,X28,X31,X32,X33,X34,X35,X37,X38,X39,X41,X42,X43,X45,X46,X47,X51,X56,X61,X66,X71,X76,X81,X86,X91,X96,X101,X106,X111,X116,X121,X126,X131,X136,X141,X146,X149,X151,X152,X153,X155,X156,X157,X159,X160,X161,X163,X164,X165,X167,X168,X169,X171,X172,X173,X175,X176,X177,X179,X180,X181,X183,X184,X185,X187,X188,X189,X191,X192,X193,X195,X196,X197,X199,X200,X201,X203,X204,X205,X207,X208,X209,X211,X212,X213,X215,X216,X217,X219,X220,X221,X223,X224,X225,X227,X228,X229] :
( ( ~ p1(X229)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(esk1_0,X227)
| p1(esk114_1(X227)) )
& ( ~ p1(X229)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(esk1_0,X227)
| r1(X227,esk114_1(X227)) )
& ( ~ p1(X225)
| ~ r1(X224,X225)
| ~ r1(X223,X224)
| ~ r1(esk17_0,X223)
| p1(esk113_1(X223)) )
& ( ~ p1(X225)
| ~ r1(X224,X225)
| ~ r1(X223,X224)
| ~ r1(esk17_0,X223)
| r1(X223,esk113_1(X223)) )
& ( ~ p1(X221)
| ~ r1(X220,X221)
| ~ r1(X219,X220)
| ~ r1(esk21_0,X219)
| p1(esk112_1(X219)) )
& ( ~ p1(X221)
| ~ r1(X220,X221)
| ~ r1(X219,X220)
| ~ r1(esk21_0,X219)
| r1(X219,esk112_1(X219)) )
& ( ~ p1(X217)
| ~ r1(X216,X217)
| ~ r1(X215,X216)
| ~ r1(esk25_0,X215)
| p1(esk111_1(X215)) )
& ( ~ p1(X217)
| ~ r1(X216,X217)
| ~ r1(X215,X216)
| ~ r1(esk25_0,X215)
| r1(X215,esk111_1(X215)) )
& ( ~ p1(X213)
| ~ r1(X212,X213)
| ~ r1(X211,X212)
| ~ r1(esk29_0,X211)
| p1(esk110_1(X211)) )
& ( ~ p1(X213)
| ~ r1(X212,X213)
| ~ r1(X211,X212)
| ~ r1(esk29_0,X211)
| r1(X211,esk110_1(X211)) )
& ( ~ p1(X209)
| ~ r1(X208,X209)
| ~ r1(X207,X208)
| ~ r1(esk33_0,X207)
| p1(esk109_1(X207)) )
& ( ~ p1(X209)
| ~ r1(X208,X209)
| ~ r1(X207,X208)
| ~ r1(esk33_0,X207)
| r1(X207,esk109_1(X207)) )
& ( ~ p1(X205)
| ~ r1(X204,X205)
| ~ r1(X203,X204)
| ~ r1(esk37_0,X203)
| p1(esk108_1(X203)) )
& ( ~ p1(X205)
| ~ r1(X204,X205)
| ~ r1(X203,X204)
| ~ r1(esk37_0,X203)
| r1(X203,esk108_1(X203)) )
& ( ~ p1(X201)
| ~ r1(X200,X201)
| ~ r1(X199,X200)
| ~ r1(esk41_0,X199)
| p1(esk107_1(X199)) )
& ( ~ p1(X201)
| ~ r1(X200,X201)
| ~ r1(X199,X200)
| ~ r1(esk41_0,X199)
| r1(X199,esk107_1(X199)) )
& ( ~ p1(X197)
| ~ r1(X196,X197)
| ~ r1(X195,X196)
| ~ r1(esk45_0,X195)
| p1(esk106_1(X195)) )
& ( ~ p1(X197)
| ~ r1(X196,X197)
| ~ r1(X195,X196)
| ~ r1(esk45_0,X195)
| r1(X195,esk106_1(X195)) )
& ( ~ p1(X193)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(esk49_0,X191)
| p1(esk105_1(X191)) )
& ( ~ p1(X193)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(esk49_0,X191)
| r1(X191,esk105_1(X191)) )
& ( ~ p1(X189)
| ~ r1(X188,X189)
| ~ r1(X187,X188)
| ~ r1(esk53_0,X187)
| p1(esk104_1(X187)) )
& ( ~ p1(X189)
| ~ r1(X188,X189)
| ~ r1(X187,X188)
| ~ r1(esk53_0,X187)
| r1(X187,esk104_1(X187)) )
& ( ~ p1(X185)
| ~ r1(X184,X185)
| ~ r1(X183,X184)
| ~ r1(esk57_0,X183)
| p1(esk103_1(X183)) )
& ( ~ p1(X185)
| ~ r1(X184,X185)
| ~ r1(X183,X184)
| ~ r1(esk57_0,X183)
| r1(X183,esk103_1(X183)) )
& ( ~ p1(X181)
| ~ r1(X180,X181)
| ~ r1(X179,X180)
| ~ r1(esk61_0,X179)
| p1(esk102_1(X179)) )
& ( ~ p1(X181)
| ~ r1(X180,X181)
| ~ r1(X179,X180)
| ~ r1(esk61_0,X179)
| r1(X179,esk102_1(X179)) )
& ( ~ p1(X177)
| ~ r1(X176,X177)
| ~ r1(X175,X176)
| ~ r1(esk65_0,X175)
| p1(esk101_1(X175)) )
& ( ~ p1(X177)
| ~ r1(X176,X177)
| ~ r1(X175,X176)
| ~ r1(esk65_0,X175)
| r1(X175,esk101_1(X175)) )
& ( ~ p1(X173)
| ~ r1(X172,X173)
| ~ r1(X171,X172)
| ~ r1(esk69_0,X171)
| p1(esk100_1(X171)) )
& ( ~ p1(X173)
| ~ r1(X172,X173)
| ~ r1(X171,X172)
| ~ r1(esk69_0,X171)
| r1(X171,esk100_1(X171)) )
& ( ~ p1(X169)
| ~ r1(X168,X169)
| ~ r1(X167,X168)
| ~ r1(esk73_0,X167)
| p1(esk99_1(X167)) )
& ( ~ p1(X169)
| ~ r1(X168,X169)
| ~ r1(X167,X168)
| ~ r1(esk73_0,X167)
| r1(X167,esk99_1(X167)) )
& ( ~ p1(X165)
| ~ r1(X164,X165)
| ~ r1(X163,X164)
| ~ r1(esk77_0,X163)
| p1(esk98_1(X163)) )
& ( ~ p1(X165)
| ~ r1(X164,X165)
| ~ r1(X163,X164)
| ~ r1(esk77_0,X163)
| r1(X163,esk98_1(X163)) )
& ( ~ p1(X161)
| ~ r1(X160,X161)
| ~ r1(X159,X160)
| ~ r1(esk81_0,X159)
| p1(esk97_1(X159)) )
& ( ~ p1(X161)
| ~ r1(X160,X161)
| ~ r1(X159,X160)
| ~ r1(esk81_0,X159)
| r1(X159,esk97_1(X159)) )
& ( ~ p1(X157)
| ~ r1(X156,X157)
| ~ r1(X155,X156)
| ~ r1(esk85_0,X155)
| p1(esk96_1(X155)) )
& ( ~ p1(X157)
| ~ r1(X156,X157)
| ~ r1(X155,X156)
| ~ r1(esk85_0,X155)
| r1(X155,esk96_1(X155)) )
& ( ~ p1(X153)
| ~ r1(X152,X153)
| ~ r1(X151,X152)
| ~ r1(esk89_0,X151)
| p1(esk95_1(X151)) )
& ( ~ p1(X153)
| ~ r1(X152,X153)
| ~ r1(X151,X152)
| ~ r1(esk89_0,X151)
| r1(X151,esk95_1(X151)) )
& ( ~ r1(esk93_0,X149)
| ~ p2(esk94_1(X149)) )
& ( ~ r1(esk93_0,X149)
| r1(X149,esk94_1(X149)) )
& r1(esk89_0,esk93_0)
& ~ p1(esk92_0)
& r1(esk90_0,esk92_0)
& ( p1(X146)
| ~ r1(esk91_0,X146) )
& r1(esk90_0,esk91_0)
& r1(esk89_0,esk90_0)
& r1(esk85_0,esk89_0)
& ~ p1(esk88_0)
& r1(esk86_0,esk88_0)
& ( p1(X141)
| ~ r1(esk87_0,X141) )
& r1(esk86_0,esk87_0)
& r1(esk85_0,esk86_0)
& r1(esk81_0,esk85_0)
& ~ p1(esk84_0)
& r1(esk82_0,esk84_0)
& ( p1(X136)
| ~ r1(esk83_0,X136) )
& r1(esk82_0,esk83_0)
& r1(esk81_0,esk82_0)
& r1(esk77_0,esk81_0)
& ~ p1(esk80_0)
& r1(esk78_0,esk80_0)
& ( p1(X131)
| ~ r1(esk79_0,X131) )
& r1(esk78_0,esk79_0)
& r1(esk77_0,esk78_0)
& r1(esk73_0,esk77_0)
& ~ p1(esk76_0)
& r1(esk74_0,esk76_0)
& ( p1(X126)
| ~ r1(esk75_0,X126) )
& r1(esk74_0,esk75_0)
& r1(esk73_0,esk74_0)
& r1(esk69_0,esk73_0)
& ~ p1(esk72_0)
& r1(esk70_0,esk72_0)
& ( p1(X121)
| ~ r1(esk71_0,X121) )
& r1(esk70_0,esk71_0)
& r1(esk69_0,esk70_0)
& r1(esk65_0,esk69_0)
& ~ p1(esk68_0)
& r1(esk66_0,esk68_0)
& ( p1(X116)
| ~ r1(esk67_0,X116) )
& r1(esk66_0,esk67_0)
& r1(esk65_0,esk66_0)
& r1(esk61_0,esk65_0)
& ~ p1(esk64_0)
& r1(esk62_0,esk64_0)
& ( p1(X111)
| ~ r1(esk63_0,X111) )
& r1(esk62_0,esk63_0)
& r1(esk61_0,esk62_0)
& r1(esk57_0,esk61_0)
& ~ p1(esk60_0)
& r1(esk58_0,esk60_0)
& ( p1(X106)
| ~ r1(esk59_0,X106) )
& r1(esk58_0,esk59_0)
& r1(esk57_0,esk58_0)
& r1(esk53_0,esk57_0)
& ~ p1(esk56_0)
& r1(esk54_0,esk56_0)
& ( p1(X101)
| ~ r1(esk55_0,X101) )
& r1(esk54_0,esk55_0)
& r1(esk53_0,esk54_0)
& r1(esk49_0,esk53_0)
& ~ p1(esk52_0)
& r1(esk50_0,esk52_0)
& ( p1(X96)
| ~ r1(esk51_0,X96) )
& r1(esk50_0,esk51_0)
& r1(esk49_0,esk50_0)
& r1(esk45_0,esk49_0)
& ~ p1(esk48_0)
& r1(esk46_0,esk48_0)
& ( p1(X91)
| ~ r1(esk47_0,X91) )
& r1(esk46_0,esk47_0)
& r1(esk45_0,esk46_0)
& r1(esk41_0,esk45_0)
& ~ p1(esk44_0)
& r1(esk42_0,esk44_0)
& ( p1(X86)
| ~ r1(esk43_0,X86) )
& r1(esk42_0,esk43_0)
& r1(esk41_0,esk42_0)
& r1(esk37_0,esk41_0)
& ~ p1(esk40_0)
& r1(esk38_0,esk40_0)
& ( p1(X81)
| ~ r1(esk39_0,X81) )
& r1(esk38_0,esk39_0)
& r1(esk37_0,esk38_0)
& r1(esk33_0,esk37_0)
& ~ p1(esk36_0)
& r1(esk34_0,esk36_0)
& ( p1(X76)
| ~ r1(esk35_0,X76) )
& r1(esk34_0,esk35_0)
& r1(esk33_0,esk34_0)
& r1(esk29_0,esk33_0)
& ~ p1(esk32_0)
& r1(esk30_0,esk32_0)
& ( p1(X71)
| ~ r1(esk31_0,X71) )
& r1(esk30_0,esk31_0)
& r1(esk29_0,esk30_0)
& r1(esk25_0,esk29_0)
& ~ p1(esk28_0)
& r1(esk26_0,esk28_0)
& ( p1(X66)
| ~ r1(esk27_0,X66) )
& r1(esk26_0,esk27_0)
& r1(esk25_0,esk26_0)
& r1(esk21_0,esk25_0)
& ~ p1(esk24_0)
& r1(esk22_0,esk24_0)
& ( p1(X61)
| ~ r1(esk23_0,X61) )
& r1(esk22_0,esk23_0)
& r1(esk21_0,esk22_0)
& r1(esk17_0,esk21_0)
& ~ p1(esk20_0)
& r1(esk18_0,esk20_0)
& ( p1(X56)
| ~ r1(esk19_0,X56) )
& r1(esk18_0,esk19_0)
& r1(esk17_0,esk18_0)
& r1(esk1_0,esk17_0)
& ~ p1(esk16_0)
& r1(esk14_0,esk16_0)
& ( p1(X51)
| ~ r1(esk15_0,X51) )
& r1(esk14_0,esk15_0)
& r1(esk1_0,esk14_0)
& ( ~ r1(esk1_0,X45)
| p1(X47)
| ~ r1(X46,X47)
| ~ r1(X45,X46)
| ~ p1(esk13_1(X45)) )
& ( ~ r1(esk1_0,X45)
| p1(X47)
| ~ r1(X46,X47)
| ~ r1(X45,X46)
| r1(X45,esk13_1(X45)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X41)
| p1(X43)
| ~ r1(X42,X43)
| ~ r1(X41,X42)
| ~ p1(esk12_2(X11,X41)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X41)
| p1(X43)
| ~ r1(X42,X43)
| ~ r1(X41,X42)
| r1(X41,esk12_2(X11,X41)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X37)
| p1(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| ~ p1(esk11_3(X11,X18,X37)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X37)
| p1(X39)
| ~ r1(X38,X39)
| ~ r1(X37,X38)
| r1(X37,esk11_3(X11,X18,X37)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X33)
| p1(X35)
| ~ r1(X34,X35)
| ~ r1(X33,X34)
| ~ p1(esk10_4(X11,X18,X25,X33)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X33)
| p1(X35)
| ~ r1(X34,X35)
| ~ r1(X33,X34)
| r1(X33,esk10_4(X11,X18,X25,X33)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| epred5_1(X32)
| ~ r1(X25,X32) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(esk8_6(X11,X18,X25,X26,X27,X28))
| ~ p1(X31)
| ~ r1(esk9_4(X11,X18,X25,X26),X31) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| p1(esk8_6(X11,X18,X25,X26,X27,X28))
| r1(X26,esk9_4(X11,X18,X25,X26)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| r1(X28,esk8_6(X11,X18,X25,X26,X27,X28))
| ~ p1(X31)
| ~ r1(esk9_4(X11,X18,X25,X26),X31) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X25)
| ~ r1(X25,X26)
| ~ r1(X26,X27)
| ~ r1(X27,X28)
| r1(X28,esk8_6(X11,X18,X25,X26,X27,X28))
| r1(X26,esk9_4(X11,X18,X25,X26)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| p1(esk6_5(X11,X18,X19,X20,X21))
| ~ p1(X24)
| ~ r1(esk7_3(X11,X18,X19),X24) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| p1(esk6_5(X11,X18,X19,X20,X21))
| r1(X19,esk7_3(X11,X18,X19)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| r1(X21,esk6_5(X11,X18,X19,X20,X21))
| ~ p1(X24)
| ~ r1(esk7_3(X11,X18,X19),X24) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X18)
| ~ r1(X18,X19)
| ~ r1(X19,X20)
| ~ r1(X20,X21)
| r1(X21,esk6_5(X11,X18,X19,X20,X21))
| r1(X19,esk7_3(X11,X18,X19)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p1(esk4_4(X11,X12,X13,X14))
| ~ p1(X17)
| ~ r1(esk5_2(X11,X12),X17) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| p1(esk4_4(X11,X12,X13,X14))
| r1(X12,esk5_2(X11,X12)) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| r1(X14,esk4_4(X11,X12,X13,X14))
| ~ p1(X17)
| ~ r1(esk5_2(X11,X12),X17) )
& ( ~ r1(esk1_0,X11)
| ~ r1(X11,X12)
| ~ r1(X12,X13)
| ~ r1(X13,X14)
| r1(X14,esk4_4(X11,X12,X13,X14))
| r1(X12,esk5_2(X11,X12)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(esk2_3(X5,X6,X7))
| ~ p1(X10)
| ~ r1(esk3_1(X5),X10) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| p1(esk2_3(X5,X6,X7))
| r1(X5,esk3_1(X5)) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| r1(X7,esk2_3(X5,X6,X7))
| ~ p1(X10)
| ~ r1(esk3_1(X5),X10) )
& ( ~ r1(esk1_0,X5)
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| r1(X7,esk2_3(X5,X6,X7))
| r1(X5,esk3_1(X5)) )
& ( ~ p4(X4)
| ~ r1(esk1_0,X4) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])])]) ).
cnf(c_0_5,negated_conjecture,
( ~ r1(esk1_0,X4)
| ~ r1(X4,X3)
| ~ r1(X3,X1)
| ~ r1(X1,X2)
| epred5_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_6,negated_conjecture,
r1(esk1_0,esk17_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_7,plain,
! [X1] :
( epred4_1(X1)
<=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
introduced(definition) ).
cnf(c_0_8,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk17_0,X2)
| epred5_1(X1) ),
inference(spm,[status(thm)],[c_0_5,c_0_6]) ).
cnf(c_0_9,negated_conjecture,
r1(esk17_0,esk21_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_10,plain,
! [X1] :
( epred5_1(X1)
=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( epred4_1(X1)
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_2]),c_0_7]) ).
cnf(c_0_11,negated_conjecture,
( ~ r1(X2,X1)
| ~ r1(esk21_0,X2)
| epred5_1(X1) ),
inference(spm,[status(thm)],[c_0_8,c_0_9]) ).
cnf(c_0_12,negated_conjecture,
r1(esk21_0,esk25_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_13,plain,
! [X393,X394,X395,X396,X399,X400,X401,X402,X403,X406,X407,X408,X409,X410,X413,X414,X415,X416,X417,X420,X421,X422,X423,X424,X426,X427,X428,X430,X431,X432,X434,X435,X436] :
( ( ~ epred5_1(X393)
| ~ r1(X393,X434)
| p1(X436)
| ~ r1(X435,X436)
| ~ r1(X434,X435)
| ~ p1(esk176_2(X393,X434)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X434)
| p1(X436)
| ~ r1(X435,X436)
| ~ r1(X434,X435)
| r1(X434,esk176_2(X393,X434)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X430)
| p1(X432)
| ~ r1(X431,X432)
| ~ r1(X430,X431)
| ~ p1(esk175_3(X393,X400,X430)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X430)
| p1(X432)
| ~ r1(X431,X432)
| ~ r1(X430,X431)
| r1(X430,esk175_3(X393,X400,X430)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X426)
| p1(X428)
| ~ r1(X427,X428)
| ~ r1(X426,X427)
| ~ p1(esk174_4(X393,X400,X407,X426)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X426)
| p1(X428)
| ~ r1(X427,X428)
| ~ r1(X426,X427)
| r1(X426,esk174_4(X393,X400,X407,X426)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X422)
| p1(X424)
| ~ r1(X423,X424)
| ~ r1(X422,X423)
| ~ p1(esk173_5(X393,X400,X407,X414,X422)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X422)
| p1(X424)
| ~ r1(X423,X424)
| ~ r1(X422,X423)
| r1(X422,esk173_5(X393,X400,X407,X414,X422)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| epred4_1(X421)
| ~ r1(X414,X421) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X415)
| ~ r1(X415,X416)
| ~ r1(X416,X417)
| p1(esk171_7(X393,X400,X407,X414,X415,X416,X417))
| ~ p1(X420)
| ~ r1(esk172_5(X393,X400,X407,X414,X415),X420) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X415)
| ~ r1(X415,X416)
| ~ r1(X416,X417)
| p1(esk171_7(X393,X400,X407,X414,X415,X416,X417))
| r1(X415,esk172_5(X393,X400,X407,X414,X415)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X415)
| ~ r1(X415,X416)
| ~ r1(X416,X417)
| r1(X417,esk171_7(X393,X400,X407,X414,X415,X416,X417))
| ~ p1(X420)
| ~ r1(esk172_5(X393,X400,X407,X414,X415),X420) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X414)
| ~ r1(X414,X415)
| ~ r1(X415,X416)
| ~ r1(X416,X417)
| r1(X417,esk171_7(X393,X400,X407,X414,X415,X416,X417))
| r1(X415,esk172_5(X393,X400,X407,X414,X415)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X408)
| ~ r1(X408,X409)
| ~ r1(X409,X410)
| p1(esk169_6(X393,X400,X407,X408,X409,X410))
| ~ p1(X413)
| ~ r1(esk170_4(X393,X400,X407,X408),X413) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X408)
| ~ r1(X408,X409)
| ~ r1(X409,X410)
| p1(esk169_6(X393,X400,X407,X408,X409,X410))
| r1(X408,esk170_4(X393,X400,X407,X408)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X408)
| ~ r1(X408,X409)
| ~ r1(X409,X410)
| r1(X410,esk169_6(X393,X400,X407,X408,X409,X410))
| ~ p1(X413)
| ~ r1(esk170_4(X393,X400,X407,X408),X413) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X407)
| ~ r1(X407,X408)
| ~ r1(X408,X409)
| ~ r1(X409,X410)
| r1(X410,esk169_6(X393,X400,X407,X408,X409,X410))
| r1(X408,esk170_4(X393,X400,X407,X408)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X401)
| ~ r1(X401,X402)
| ~ r1(X402,X403)
| p1(esk167_5(X393,X400,X401,X402,X403))
| ~ p1(X406)
| ~ r1(esk168_3(X393,X400,X401),X406) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X401)
| ~ r1(X401,X402)
| ~ r1(X402,X403)
| p1(esk167_5(X393,X400,X401,X402,X403))
| r1(X401,esk168_3(X393,X400,X401)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X401)
| ~ r1(X401,X402)
| ~ r1(X402,X403)
| r1(X403,esk167_5(X393,X400,X401,X402,X403))
| ~ p1(X406)
| ~ r1(esk168_3(X393,X400,X401),X406) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X400)
| ~ r1(X400,X401)
| ~ r1(X401,X402)
| ~ r1(X402,X403)
| r1(X403,esk167_5(X393,X400,X401,X402,X403))
| r1(X401,esk168_3(X393,X400,X401)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X394)
| ~ r1(X394,X395)
| ~ r1(X395,X396)
| p1(esk165_4(X393,X394,X395,X396))
| ~ p1(X399)
| ~ r1(esk166_2(X393,X394),X399) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X394)
| ~ r1(X394,X395)
| ~ r1(X395,X396)
| p1(esk165_4(X393,X394,X395,X396))
| r1(X394,esk166_2(X393,X394)) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X394)
| ~ r1(X394,X395)
| ~ r1(X395,X396)
| r1(X396,esk165_4(X393,X394,X395,X396))
| ~ p1(X399)
| ~ r1(esk166_2(X393,X394),X399) )
& ( ~ epred5_1(X393)
| ~ r1(X393,X394)
| ~ r1(X394,X395)
| ~ r1(X395,X396)
| r1(X396,esk165_4(X393,X394,X395,X396))
| r1(X394,esk166_2(X393,X394)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_10])])])])])]) ).
cnf(c_0_14,negated_conjecture,
( ~ r1(esk25_0,X1)
| epred5_1(X1) ),
inference(spm,[status(thm)],[c_0_11,c_0_12]) ).
cnf(c_0_15,negated_conjecture,
r1(esk25_0,esk29_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_16,plain,
! [X1] :
( epred3_1(X1)
<=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
introduced(definition) ).
cnf(c_0_17,plain,
( ~ epred5_1(X5)
| ~ r1(X5,X4)
| ~ r1(X4,X3)
| ~ r1(X3,X1)
| ~ r1(X1,X2)
| epred4_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_13]) ).
cnf(c_0_18,negated_conjecture,
r1(esk29_0,esk33_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_19,negated_conjecture,
epred5_1(esk29_0),
inference(spm,[status(thm)],[c_0_14,c_0_15]) ).
fof(c_0_20,plain,
! [X1] :
( epred4_1(X1)
=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( epred3_1(X1)
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_7]),c_0_16]) ).
cnf(c_0_21,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk33_0,X2)
| epred4_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_17,c_0_18]),c_0_19])]) ).
cnf(c_0_22,negated_conjecture,
r1(esk33_0,esk37_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_23,plain,
! [X348,X349,X350,X351,X354,X355,X356,X357,X358,X361,X362,X363,X364,X365,X368,X369,X370,X371,X372,X375,X376,X377,X378,X379,X381,X382,X383,X385,X386,X387,X389,X390,X391] :
( ( ~ epred4_1(X348)
| ~ r1(X348,X389)
| p1(X391)
| ~ r1(X390,X391)
| ~ r1(X389,X390)
| ~ p1(esk164_2(X348,X389)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X389)
| p1(X391)
| ~ r1(X390,X391)
| ~ r1(X389,X390)
| r1(X389,esk164_2(X348,X389)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X385)
| p1(X387)
| ~ r1(X386,X387)
| ~ r1(X385,X386)
| ~ p1(esk163_3(X348,X355,X385)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X385)
| p1(X387)
| ~ r1(X386,X387)
| ~ r1(X385,X386)
| r1(X385,esk163_3(X348,X355,X385)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X381)
| p1(X383)
| ~ r1(X382,X383)
| ~ r1(X381,X382)
| ~ p1(esk162_4(X348,X355,X362,X381)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X381)
| p1(X383)
| ~ r1(X382,X383)
| ~ r1(X381,X382)
| r1(X381,esk162_4(X348,X355,X362,X381)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X377)
| p1(X379)
| ~ r1(X378,X379)
| ~ r1(X377,X378)
| ~ p1(esk161_5(X348,X355,X362,X369,X377)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X377)
| p1(X379)
| ~ r1(X378,X379)
| ~ r1(X377,X378)
| r1(X377,esk161_5(X348,X355,X362,X369,X377)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| epred3_1(X376)
| ~ r1(X369,X376) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X370)
| ~ r1(X370,X371)
| ~ r1(X371,X372)
| p1(esk159_7(X348,X355,X362,X369,X370,X371,X372))
| ~ p1(X375)
| ~ r1(esk160_5(X348,X355,X362,X369,X370),X375) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X370)
| ~ r1(X370,X371)
| ~ r1(X371,X372)
| p1(esk159_7(X348,X355,X362,X369,X370,X371,X372))
| r1(X370,esk160_5(X348,X355,X362,X369,X370)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X370)
| ~ r1(X370,X371)
| ~ r1(X371,X372)
| r1(X372,esk159_7(X348,X355,X362,X369,X370,X371,X372))
| ~ p1(X375)
| ~ r1(esk160_5(X348,X355,X362,X369,X370),X375) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X369)
| ~ r1(X369,X370)
| ~ r1(X370,X371)
| ~ r1(X371,X372)
| r1(X372,esk159_7(X348,X355,X362,X369,X370,X371,X372))
| r1(X370,esk160_5(X348,X355,X362,X369,X370)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X363)
| ~ r1(X363,X364)
| ~ r1(X364,X365)
| p1(esk157_6(X348,X355,X362,X363,X364,X365))
| ~ p1(X368)
| ~ r1(esk158_4(X348,X355,X362,X363),X368) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X363)
| ~ r1(X363,X364)
| ~ r1(X364,X365)
| p1(esk157_6(X348,X355,X362,X363,X364,X365))
| r1(X363,esk158_4(X348,X355,X362,X363)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X363)
| ~ r1(X363,X364)
| ~ r1(X364,X365)
| r1(X365,esk157_6(X348,X355,X362,X363,X364,X365))
| ~ p1(X368)
| ~ r1(esk158_4(X348,X355,X362,X363),X368) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X362)
| ~ r1(X362,X363)
| ~ r1(X363,X364)
| ~ r1(X364,X365)
| r1(X365,esk157_6(X348,X355,X362,X363,X364,X365))
| r1(X363,esk158_4(X348,X355,X362,X363)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X356)
| ~ r1(X356,X357)
| ~ r1(X357,X358)
| p1(esk155_5(X348,X355,X356,X357,X358))
| ~ p1(X361)
| ~ r1(esk156_3(X348,X355,X356),X361) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X356)
| ~ r1(X356,X357)
| ~ r1(X357,X358)
| p1(esk155_5(X348,X355,X356,X357,X358))
| r1(X356,esk156_3(X348,X355,X356)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X356)
| ~ r1(X356,X357)
| ~ r1(X357,X358)
| r1(X358,esk155_5(X348,X355,X356,X357,X358))
| ~ p1(X361)
| ~ r1(esk156_3(X348,X355,X356),X361) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X355)
| ~ r1(X355,X356)
| ~ r1(X356,X357)
| ~ r1(X357,X358)
| r1(X358,esk155_5(X348,X355,X356,X357,X358))
| r1(X356,esk156_3(X348,X355,X356)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X349)
| ~ r1(X349,X350)
| ~ r1(X350,X351)
| p1(esk153_4(X348,X349,X350,X351))
| ~ p1(X354)
| ~ r1(esk154_2(X348,X349),X354) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X349)
| ~ r1(X349,X350)
| ~ r1(X350,X351)
| p1(esk153_4(X348,X349,X350,X351))
| r1(X349,esk154_2(X348,X349)) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X349)
| ~ r1(X349,X350)
| ~ r1(X350,X351)
| r1(X351,esk153_4(X348,X349,X350,X351))
| ~ p1(X354)
| ~ r1(esk154_2(X348,X349),X354) )
& ( ~ epred4_1(X348)
| ~ r1(X348,X349)
| ~ r1(X349,X350)
| ~ r1(X350,X351)
| r1(X351,esk153_4(X348,X349,X350,X351))
| r1(X349,esk154_2(X348,X349)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])])])])]) ).
cnf(c_0_24,negated_conjecture,
( ~ r1(X2,X1)
| ~ r1(esk37_0,X2)
| epred4_1(X1) ),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
cnf(c_0_25,negated_conjecture,
r1(esk37_0,esk41_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_26,plain,
( ~ epred4_1(X5)
| ~ r1(X5,X4)
| ~ r1(X4,X3)
| ~ r1(X3,X1)
| ~ r1(X1,X2)
| epred3_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_23]) ).
cnf(c_0_27,negated_conjecture,
r1(esk45_0,esk49_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_28,negated_conjecture,
( ~ r1(esk41_0,X1)
| epred4_1(X1) ),
inference(spm,[status(thm)],[c_0_24,c_0_25]) ).
cnf(c_0_29,negated_conjecture,
r1(esk41_0,esk45_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_30,plain,
! [X1] :
( epred2_1(X1)
<=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
introduced(definition) ).
cnf(c_0_31,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk49_0,X2)
| ~ epred4_1(esk45_0)
| epred3_1(X1) ),
inference(spm,[status(thm)],[c_0_26,c_0_27]) ).
cnf(c_0_32,negated_conjecture,
epred4_1(esk45_0),
inference(spm,[status(thm)],[c_0_28,c_0_29]) ).
fof(c_0_33,plain,
! [X1] :
( epred3_1(X1)
=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( epred2_1(X1)
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_16]),c_0_30]) ).
cnf(c_0_34,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk49_0,X2)
| epred3_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_32])]) ).
cnf(c_0_35,negated_conjecture,
r1(esk49_0,esk53_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_36,plain,
! [X303,X304,X305,X306,X309,X310,X311,X312,X313,X316,X317,X318,X319,X320,X323,X324,X325,X326,X327,X330,X331,X332,X333,X334,X336,X337,X338,X340,X341,X342,X344,X345,X346] :
( ( ~ epred3_1(X303)
| ~ r1(X303,X344)
| p1(X346)
| ~ r1(X345,X346)
| ~ r1(X344,X345)
| ~ p1(esk152_2(X303,X344)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X344)
| p1(X346)
| ~ r1(X345,X346)
| ~ r1(X344,X345)
| r1(X344,esk152_2(X303,X344)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X340)
| p1(X342)
| ~ r1(X341,X342)
| ~ r1(X340,X341)
| ~ p1(esk151_3(X303,X310,X340)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X340)
| p1(X342)
| ~ r1(X341,X342)
| ~ r1(X340,X341)
| r1(X340,esk151_3(X303,X310,X340)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X336)
| p1(X338)
| ~ r1(X337,X338)
| ~ r1(X336,X337)
| ~ p1(esk150_4(X303,X310,X317,X336)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X336)
| p1(X338)
| ~ r1(X337,X338)
| ~ r1(X336,X337)
| r1(X336,esk150_4(X303,X310,X317,X336)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X332)
| p1(X334)
| ~ r1(X333,X334)
| ~ r1(X332,X333)
| ~ p1(esk149_5(X303,X310,X317,X324,X332)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X332)
| p1(X334)
| ~ r1(X333,X334)
| ~ r1(X332,X333)
| r1(X332,esk149_5(X303,X310,X317,X324,X332)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| epred2_1(X331)
| ~ r1(X324,X331) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X325)
| ~ r1(X325,X326)
| ~ r1(X326,X327)
| p1(esk147_7(X303,X310,X317,X324,X325,X326,X327))
| ~ p1(X330)
| ~ r1(esk148_5(X303,X310,X317,X324,X325),X330) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X325)
| ~ r1(X325,X326)
| ~ r1(X326,X327)
| p1(esk147_7(X303,X310,X317,X324,X325,X326,X327))
| r1(X325,esk148_5(X303,X310,X317,X324,X325)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X325)
| ~ r1(X325,X326)
| ~ r1(X326,X327)
| r1(X327,esk147_7(X303,X310,X317,X324,X325,X326,X327))
| ~ p1(X330)
| ~ r1(esk148_5(X303,X310,X317,X324,X325),X330) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X324)
| ~ r1(X324,X325)
| ~ r1(X325,X326)
| ~ r1(X326,X327)
| r1(X327,esk147_7(X303,X310,X317,X324,X325,X326,X327))
| r1(X325,esk148_5(X303,X310,X317,X324,X325)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X318)
| ~ r1(X318,X319)
| ~ r1(X319,X320)
| p1(esk145_6(X303,X310,X317,X318,X319,X320))
| ~ p1(X323)
| ~ r1(esk146_4(X303,X310,X317,X318),X323) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X318)
| ~ r1(X318,X319)
| ~ r1(X319,X320)
| p1(esk145_6(X303,X310,X317,X318,X319,X320))
| r1(X318,esk146_4(X303,X310,X317,X318)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X318)
| ~ r1(X318,X319)
| ~ r1(X319,X320)
| r1(X320,esk145_6(X303,X310,X317,X318,X319,X320))
| ~ p1(X323)
| ~ r1(esk146_4(X303,X310,X317,X318),X323) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X317)
| ~ r1(X317,X318)
| ~ r1(X318,X319)
| ~ r1(X319,X320)
| r1(X320,esk145_6(X303,X310,X317,X318,X319,X320))
| r1(X318,esk146_4(X303,X310,X317,X318)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X311)
| ~ r1(X311,X312)
| ~ r1(X312,X313)
| p1(esk143_5(X303,X310,X311,X312,X313))
| ~ p1(X316)
| ~ r1(esk144_3(X303,X310,X311),X316) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X311)
| ~ r1(X311,X312)
| ~ r1(X312,X313)
| p1(esk143_5(X303,X310,X311,X312,X313))
| r1(X311,esk144_3(X303,X310,X311)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X311)
| ~ r1(X311,X312)
| ~ r1(X312,X313)
| r1(X313,esk143_5(X303,X310,X311,X312,X313))
| ~ p1(X316)
| ~ r1(esk144_3(X303,X310,X311),X316) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X310)
| ~ r1(X310,X311)
| ~ r1(X311,X312)
| ~ r1(X312,X313)
| r1(X313,esk143_5(X303,X310,X311,X312,X313))
| r1(X311,esk144_3(X303,X310,X311)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X304)
| ~ r1(X304,X305)
| ~ r1(X305,X306)
| p1(esk141_4(X303,X304,X305,X306))
| ~ p1(X309)
| ~ r1(esk142_2(X303,X304),X309) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X304)
| ~ r1(X304,X305)
| ~ r1(X305,X306)
| p1(esk141_4(X303,X304,X305,X306))
| r1(X304,esk142_2(X303,X304)) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X304)
| ~ r1(X304,X305)
| ~ r1(X305,X306)
| r1(X306,esk141_4(X303,X304,X305,X306))
| ~ p1(X309)
| ~ r1(esk142_2(X303,X304),X309) )
& ( ~ epred3_1(X303)
| ~ r1(X303,X304)
| ~ r1(X304,X305)
| ~ r1(X305,X306)
| r1(X306,esk141_4(X303,X304,X305,X306))
| r1(X304,esk142_2(X303,X304)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])])])]) ).
cnf(c_0_37,negated_conjecture,
( ~ r1(X2,X1)
| ~ r1(esk53_0,X2)
| epred3_1(X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_35]) ).
cnf(c_0_38,negated_conjecture,
r1(esk53_0,esk57_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_39,plain,
( ~ epred3_1(X5)
| ~ r1(X5,X4)
| ~ r1(X4,X3)
| ~ r1(X3,X1)
| ~ r1(X1,X2)
| epred2_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_36]) ).
cnf(c_0_40,negated_conjecture,
r1(esk61_0,esk65_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_41,negated_conjecture,
( ~ r1(esk57_0,X1)
| epred3_1(X1) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_42,negated_conjecture,
r1(esk57_0,esk61_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_43,plain,
! [X1] :
( epred1_1(X1)
<=> ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) ) ),
introduced(definition) ).
cnf(c_0_44,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk65_0,X2)
| ~ epred3_1(esk61_0)
| epred2_1(X1) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_45,negated_conjecture,
epred3_1(esk61_0),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
fof(c_0_46,plain,
! [X1] :
( epred2_1(X1)
=> ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ~ ! [X2] :
( ~ ( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ( ! [X2] :
( p1(X2)
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( epred1_1(X1)
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) )
| ~ ! [X1] :
( ~ ( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ p1(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ~ ! [X1] :
( ! [X2] :
( ~ ! [X1] :
( ~ p1(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) ) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_30]),c_0_43]) ).
cnf(c_0_47,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk65_0,X2)
| epred2_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_44,c_0_45])]) ).
cnf(c_0_48,negated_conjecture,
r1(esk65_0,esk69_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_49,plain,
! [X258,X259,X260,X261,X264,X265,X266,X267,X268,X271,X272,X273,X274,X275,X278,X279,X280,X281,X282,X285,X286,X287,X288,X289,X291,X292,X293,X295,X296,X297,X299,X300,X301] :
( ( ~ epred2_1(X258)
| ~ r1(X258,X299)
| p1(X301)
| ~ r1(X300,X301)
| ~ r1(X299,X300)
| ~ p1(esk140_2(X258,X299)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X299)
| p1(X301)
| ~ r1(X300,X301)
| ~ r1(X299,X300)
| r1(X299,esk140_2(X258,X299)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X295)
| p1(X297)
| ~ r1(X296,X297)
| ~ r1(X295,X296)
| ~ p1(esk139_3(X258,X265,X295)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X295)
| p1(X297)
| ~ r1(X296,X297)
| ~ r1(X295,X296)
| r1(X295,esk139_3(X258,X265,X295)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X291)
| p1(X293)
| ~ r1(X292,X293)
| ~ r1(X291,X292)
| ~ p1(esk138_4(X258,X265,X272,X291)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X291)
| p1(X293)
| ~ r1(X292,X293)
| ~ r1(X291,X292)
| r1(X291,esk138_4(X258,X265,X272,X291)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X287)
| p1(X289)
| ~ r1(X288,X289)
| ~ r1(X287,X288)
| ~ p1(esk137_5(X258,X265,X272,X279,X287)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X287)
| p1(X289)
| ~ r1(X288,X289)
| ~ r1(X287,X288)
| r1(X287,esk137_5(X258,X265,X272,X279,X287)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| epred1_1(X286)
| ~ r1(X279,X286) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X280)
| ~ r1(X280,X281)
| ~ r1(X281,X282)
| p1(esk135_7(X258,X265,X272,X279,X280,X281,X282))
| ~ p1(X285)
| ~ r1(esk136_5(X258,X265,X272,X279,X280),X285) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X280)
| ~ r1(X280,X281)
| ~ r1(X281,X282)
| p1(esk135_7(X258,X265,X272,X279,X280,X281,X282))
| r1(X280,esk136_5(X258,X265,X272,X279,X280)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X280)
| ~ r1(X280,X281)
| ~ r1(X281,X282)
| r1(X282,esk135_7(X258,X265,X272,X279,X280,X281,X282))
| ~ p1(X285)
| ~ r1(esk136_5(X258,X265,X272,X279,X280),X285) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X279)
| ~ r1(X279,X280)
| ~ r1(X280,X281)
| ~ r1(X281,X282)
| r1(X282,esk135_7(X258,X265,X272,X279,X280,X281,X282))
| r1(X280,esk136_5(X258,X265,X272,X279,X280)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X273)
| ~ r1(X273,X274)
| ~ r1(X274,X275)
| p1(esk133_6(X258,X265,X272,X273,X274,X275))
| ~ p1(X278)
| ~ r1(esk134_4(X258,X265,X272,X273),X278) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X273)
| ~ r1(X273,X274)
| ~ r1(X274,X275)
| p1(esk133_6(X258,X265,X272,X273,X274,X275))
| r1(X273,esk134_4(X258,X265,X272,X273)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X273)
| ~ r1(X273,X274)
| ~ r1(X274,X275)
| r1(X275,esk133_6(X258,X265,X272,X273,X274,X275))
| ~ p1(X278)
| ~ r1(esk134_4(X258,X265,X272,X273),X278) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X272)
| ~ r1(X272,X273)
| ~ r1(X273,X274)
| ~ r1(X274,X275)
| r1(X275,esk133_6(X258,X265,X272,X273,X274,X275))
| r1(X273,esk134_4(X258,X265,X272,X273)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| p1(esk131_5(X258,X265,X266,X267,X268))
| ~ p1(X271)
| ~ r1(esk132_3(X258,X265,X266),X271) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| p1(esk131_5(X258,X265,X266,X267,X268))
| r1(X266,esk132_3(X258,X265,X266)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| r1(X268,esk131_5(X258,X265,X266,X267,X268))
| ~ p1(X271)
| ~ r1(esk132_3(X258,X265,X266),X271) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| r1(X268,esk131_5(X258,X265,X266,X267,X268))
| r1(X266,esk132_3(X258,X265,X266)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| p1(esk129_4(X258,X259,X260,X261))
| ~ p1(X264)
| ~ r1(esk130_2(X258,X259),X264) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| p1(esk129_4(X258,X259,X260,X261))
| r1(X259,esk130_2(X258,X259)) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| r1(X261,esk129_4(X258,X259,X260,X261))
| ~ p1(X264)
| ~ r1(esk130_2(X258,X259),X264) )
& ( ~ epred2_1(X258)
| ~ r1(X258,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| r1(X261,esk129_4(X258,X259,X260,X261))
| r1(X259,esk130_2(X258,X259)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_46])])])])])]) ).
cnf(c_0_50,negated_conjecture,
( ~ r1(X2,X1)
| ~ r1(esk69_0,X2)
| epred2_1(X1) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_51,negated_conjecture,
r1(esk69_0,esk73_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_52,plain,
( ~ epred2_1(X5)
| ~ r1(X5,X4)
| ~ r1(X4,X3)
| ~ r1(X3,X1)
| ~ r1(X1,X2)
| epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_49]) ).
cnf(c_0_53,negated_conjecture,
r1(esk77_0,esk81_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_54,negated_conjecture,
( ~ r1(esk73_0,X1)
| epred2_1(X1) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_55,negated_conjecture,
r1(esk73_0,esk77_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_56,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk81_0,X2)
| ~ epred2_1(esk77_0)
| epred1_1(X1) ),
inference(spm,[status(thm)],[c_0_52,c_0_53]) ).
cnf(c_0_57,negated_conjecture,
epred2_1(esk77_0),
inference(spm,[status(thm)],[c_0_54,c_0_55]) ).
cnf(c_0_58,negated_conjecture,
( ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk81_0,X2)
| epred1_1(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_56,c_0_57])]) ).
cnf(c_0_59,negated_conjecture,
r1(esk81_0,esk85_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_60,plain,
! [X1] :
( epred1_1(X1)
=> ~ ( ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ( ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
& ~ ! [X2] :
( ! [X1] :
( ~ ! [X2] :
( ~ p2(X2)
| ! [X1] :
( p3(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) )
| ~ ! [X2] :
( ~ ( ~ ! [X1] :
( ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ~ r1(X2,X1) )
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
& p2(X2)
& ~ ! [X1] :
( ~ ( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) ) )
| ~ r1(X2,X1) ) )
| ~ r1(X1,X2) )
| ~ ! [X2] :
( ~ ! [X1] :
( ~ p2(X1)
| ! [X2] :
( p3(X2)
| ~ r1(X1,X2) )
| ~ r1(X2,X1) )
| ~ r1(X1,X2) ) ) ),
inference(split_equiv,[status(thm)],[c_0_43]) ).
cnf(c_0_61,negated_conjecture,
( ~ r1(X2,X1)
| ~ r1(esk85_0,X2)
| epred1_1(X1) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_62,negated_conjecture,
r1(esk85_0,esk89_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
fof(c_0_63,plain,
! [X231,X232,X235,X236,X238,X240,X241,X242,X246,X247,X249,X251,X257] :
( ( ~ epred1_1(X231)
| p2(esk126_1(X231))
| ~ p2(X257)
| ~ r1(esk128_1(X231),X257) )
& ( ~ epred1_1(X231)
| p2(esk126_1(X231))
| r1(X231,esk128_1(X231)) )
& ( ~ epred1_1(X231)
| ~ p3(esk127_1(X231))
| ~ p2(X257)
| ~ r1(esk128_1(X231),X257) )
& ( ~ epred1_1(X231)
| ~ p3(esk127_1(X231))
| r1(X231,esk128_1(X231)) )
& ( ~ epred1_1(X231)
| r1(esk126_1(X231),esk127_1(X231))
| ~ p2(X257)
| ~ r1(esk128_1(X231),X257) )
& ( ~ epred1_1(X231)
| r1(esk126_1(X231),esk127_1(X231))
| r1(X231,esk128_1(X231)) )
& ( ~ epred1_1(X231)
| r1(X231,esk126_1(X231))
| ~ p2(X257)
| ~ r1(esk128_1(X231),X257) )
& ( ~ epred1_1(X231)
| r1(X231,esk126_1(X231))
| r1(X231,esk128_1(X231)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| ~ p2(X249)
| ~ r1(esk122_2(X231,X247),X249)
| ~ r1(esk123_2(X231,X247),X251)
| p2(esk124_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| ~ p2(X249)
| ~ r1(esk122_2(X231,X247),X249)
| ~ r1(esk123_2(X231,X247),X251)
| ~ p3(esk125_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| ~ p2(X249)
| ~ r1(esk122_2(X231,X247),X249)
| ~ r1(esk123_2(X231,X247),X251)
| r1(esk124_3(X231,X247,X251),esk125_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| ~ p2(X249)
| ~ r1(esk122_2(X231,X247),X249)
| ~ r1(esk123_2(X231,X247),X251)
| r1(X251,esk124_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| ~ p2(X249)
| ~ r1(esk122_2(X231,X247),X249)
| r1(X247,esk123_2(X231,X247)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| r1(X247,esk122_2(X231,X247))
| ~ r1(esk123_2(X231,X247),X251)
| p2(esk124_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| r1(X247,esk122_2(X231,X247))
| ~ r1(esk123_2(X231,X247),X251)
| ~ p3(esk125_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| r1(X247,esk122_2(X231,X247))
| ~ r1(esk123_2(X231,X247),X251)
| r1(esk124_3(X231,X247,X251),esk125_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| r1(X247,esk122_2(X231,X247))
| ~ r1(esk123_2(X231,X247),X251)
| r1(X251,esk124_3(X231,X247,X251)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X247)
| r1(X247,esk122_2(X231,X247))
| r1(X247,esk123_2(X231,X247)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| p2(esk119_3(X231,X241,X242))
| ~ p2(X246)
| ~ r1(esk121_1(X231),X246) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| p2(esk119_3(X231,X241,X242))
| r1(X231,esk121_1(X231)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| ~ p3(esk120_3(X231,X241,X242))
| ~ p2(X246)
| ~ r1(esk121_1(X231),X246) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| ~ p3(esk120_3(X231,X241,X242))
| r1(X231,esk121_1(X231)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| r1(esk119_3(X231,X241,X242),esk120_3(X231,X241,X242))
| ~ p2(X246)
| ~ r1(esk121_1(X231),X246) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| r1(esk119_3(X231,X241,X242),esk120_3(X231,X241,X242))
| r1(X231,esk121_1(X231)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| r1(X242,esk119_3(X231,X241,X242))
| ~ p2(X246)
| ~ r1(esk121_1(X231),X246) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X241)
| ~ r1(X241,X242)
| r1(X242,esk119_3(X231,X241,X242))
| r1(X231,esk121_1(X231)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| p2(X236)
| ~ r1(X235,X238)
| ~ p2(X240)
| ~ r1(esk118_3(X231,X235,X238),X240) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| p2(X236)
| ~ r1(X235,X238)
| r1(X238,esk118_3(X231,X235,X238)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| ~ p3(esk117_3(X231,X235,X236))
| ~ r1(X235,X238)
| ~ p2(X240)
| ~ r1(esk118_3(X231,X235,X238),X240) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| ~ p3(esk117_3(X231,X235,X236))
| ~ r1(X235,X238)
| r1(X238,esk118_3(X231,X235,X238)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| r1(X236,esk117_3(X231,X235,X236))
| ~ r1(X235,X238)
| ~ p2(X240)
| ~ r1(esk118_3(X231,X235,X238),X240) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X235)
| ~ p2(X235)
| ~ r1(X235,X236)
| r1(X236,esk117_3(X231,X235,X236))
| ~ r1(X235,X238)
| r1(X238,esk118_3(X231,X235,X238)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X232)
| p2(esk115_2(X231,X232)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X232)
| ~ p3(esk116_2(X231,X232)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X232)
| r1(esk115_2(X231,X232),esk116_2(X231,X232)) )
& ( ~ epred1_1(X231)
| ~ r1(X231,X232)
| r1(X232,esk115_2(X231,X232)) ) ),
inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])])])]) ).
cnf(c_0_64,negated_conjecture,
( ~ r1(esk89_0,X1)
| epred1_1(X1) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
cnf(c_0_65,negated_conjecture,
r1(esk89_0,esk93_0),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_66,plain,
( ~ epred1_1(X1)
| r1(X1,esk126_1(X1))
| r1(X1,esk128_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_67,negated_conjecture,
epred1_1(esk93_0),
inference(spm,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_68,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X1)
| r1(X1,esk115_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_69,plain,
( r1(esk93_0,esk128_1(esk93_0))
| r1(esk93_0,esk126_1(esk93_0)) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
cnf(c_0_70,plain,
( ~ epred1_1(X1)
| p2(esk126_1(X1))
| r1(X1,esk128_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_71,plain,
( ~ epred1_1(X1)
| ~ p2(X2)
| ~ r1(esk128_1(X1),X2)
| r1(X1,esk126_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_72,plain,
( r1(esk93_0,esk126_1(esk93_0))
| r1(esk128_1(esk93_0),esk115_2(esk93_0,esk128_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_69]),c_0_67])]) ).
cnf(c_0_73,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X2)
| p2(esk115_2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_74,plain,
( r1(esk93_0,esk128_1(esk93_0))
| p2(esk126_1(esk93_0)) ),
inference(spm,[status(thm)],[c_0_70,c_0_67]) ).
cnf(c_0_75,plain,
( ~ p2(esk115_2(esk93_0,esk128_1(esk93_0)))
| r1(esk93_0,esk126_1(esk93_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_67])]) ).
cnf(c_0_76,plain,
( r1(esk93_0,esk126_1(esk93_0))
| p2(esk115_2(esk93_0,esk128_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_69]),c_0_67])]) ).
cnf(c_0_77,plain,
( ~ epred1_1(X1)
| ~ p2(X2)
| ~ r1(esk128_1(X1),X2)
| p2(esk126_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_78,plain,
( r1(esk128_1(esk93_0),esk115_2(esk93_0,esk128_1(esk93_0)))
| p2(esk126_1(esk93_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_74]),c_0_67])]) ).
cnf(c_0_79,negated_conjecture,
( ~ r1(esk93_0,X1)
| r1(X1,esk94_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_80,plain,
r1(esk93_0,esk126_1(esk93_0)),
inference(spm,[status(thm)],[c_0_75,c_0_76]) ).
cnf(c_0_81,plain,
( ~ p2(esk115_2(esk93_0,esk128_1(esk93_0)))
| p2(esk126_1(esk93_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_78]),c_0_67])]) ).
cnf(c_0_82,plain,
( p2(esk126_1(esk93_0))
| p2(esk115_2(esk93_0,esk128_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_74]),c_0_67])]) ).
cnf(c_0_83,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X3)
| ~ p2(X3)
| ~ r1(X3,X4)
| ~ r1(X3,X1)
| p2(X4)
| r1(X1,esk118_3(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_84,negated_conjecture,
r1(esk126_1(esk93_0),esk94_1(esk126_1(esk93_0))),
inference(spm,[status(thm)],[c_0_79,c_0_80]) ).
cnf(c_0_85,plain,
p2(esk126_1(esk93_0)),
inference(spm,[status(thm)],[c_0_81,c_0_82]) ).
cnf(c_0_86,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X1)
| r1(X1,esk122_2(X2,X1))
| r1(X1,esk123_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_87,negated_conjecture,
( ~ r1(X2,esk126_1(esk93_0))
| ~ r1(esk126_1(esk93_0),X1)
| ~ epred1_1(X2)
| r1(X1,esk118_3(X2,esk126_1(esk93_0),X1))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_83,c_0_84]),c_0_85])]) ).
cnf(c_0_88,plain,
( r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))
| r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_80]),c_0_67])]) ).
cnf(c_0_89,plain,
( ~ r1(X1,esk126_1(esk93_0))
| ~ epred1_1(X1)
| r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(X1,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(spm,[status(thm)],[c_0_87,c_0_88]) ).
cnf(c_0_90,negated_conjecture,
( ~ r1(esk93_0,X1)
| ~ p2(esk94_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_4]) ).
cnf(c_0_91,plain,
( r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_80]),c_0_67])]) ).
cnf(c_0_92,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X3)
| ~ r1(esk123_2(X2,X3),X1)
| r1(X3,esk122_2(X2,X3))
| r1(X1,esk124_3(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_93,negated_conjecture,
( r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_91]),c_0_80])]) ).
cnf(c_0_94,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ p2(X2)
| ~ r1(X2,X5)
| ~ r1(X2,X3)
| ~ p2(X4)
| ~ r1(esk118_3(X1,X2,X3),X4)
| p2(X5) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_95,plain,
( r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| r1(esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))),esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_67]),c_0_80])]) ).
cnf(c_0_96,plain,
( ~ r1(esk126_1(esk93_0),X1)
| ~ r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))
| ~ p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))
| r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| p2(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_95]),c_0_67]),c_0_85]),c_0_80])]) ).
cnf(c_0_97,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(esk123_2(X1,X2),X3)
| r1(X2,esk122_2(X1,X2))
| p2(esk124_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_98,plain,
( ~ r1(esk126_1(esk93_0),X1)
| ~ p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))))
| r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| p2(X1) ),
inference(spm,[status(thm)],[c_0_96,c_0_88]) ).
cnf(c_0_99,plain,
( r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_93]),c_0_67]),c_0_80])]) ).
cnf(c_0_100,plain,
( ~ r1(esk126_1(esk93_0),X1)
| r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| p2(X1) ),
inference(spm,[status(thm)],[c_0_98,c_0_99]) ).
cnf(c_0_101,negated_conjecture,
( r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(spm,[status(thm)],[c_0_100,c_0_84]) ).
cnf(c_0_102,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X3)
| ~ r1(X3,X2)
| r1(X2,esk119_3(X1,X3,X2))
| r1(X1,esk121_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_103,negated_conjecture,
r1(esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_101]),c_0_80])]) ).
cnf(c_0_104,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| p2(esk119_3(X1,X2,X3))
| r1(X1,esk121_1(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_105,plain,
( ~ r1(X1,esk126_1(esk93_0))
| ~ epred1_1(X1)
| r1(X1,esk121_1(X1))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(X1,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_102,c_0_103]) ).
cnf(c_0_106,plain,
( ~ r1(X1,esk126_1(esk93_0))
| ~ epred1_1(X1)
| r1(X1,esk121_1(X1))
| p2(esk119_3(X1,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_104,c_0_103]) ).
cnf(c_0_107,plain,
( r1(esk93_0,esk121_1(esk93_0))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105,c_0_80]),c_0_67])]) ).
cnf(c_0_108,plain,
( r1(esk93_0,esk121_1(esk93_0))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_80]),c_0_67])]) ).
cnf(c_0_109,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X4)
| ~ r1(X4,X3)
| ~ p2(X2)
| ~ r1(esk121_1(X1),X2)
| r1(X3,esk119_3(X1,X4,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_110,plain,
( r1(esk121_1(esk93_0),esk115_2(esk93_0,esk121_1(esk93_0)))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_107]),c_0_67])]) ).
cnf(c_0_111,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X3)
| ~ r1(X3,X4)
| ~ p2(X2)
| ~ r1(esk121_1(X1),X2)
| p2(esk119_3(X1,X3,X4)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_112,plain,
( r1(esk121_1(esk93_0),esk115_2(esk93_0,esk121_1(esk93_0)))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_108]),c_0_67])]) ).
cnf(c_0_113,plain,
( ~ r1(X2,X1)
| ~ r1(esk93_0,X2)
| ~ p2(esk115_2(esk93_0,esk121_1(esk93_0)))
| r1(X1,esk119_3(esk93_0,X2,X1))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_110]),c_0_67])]) ).
cnf(c_0_114,plain,
( r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0))))
| p2(esk115_2(esk93_0,esk121_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_107]),c_0_67])]) ).
cnf(c_0_115,plain,
( ~ r1(X1,X2)
| ~ r1(esk93_0,X1)
| ~ p2(esk115_2(esk93_0,esk121_1(esk93_0)))
| p2(esk119_3(esk93_0,X1,X2))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_111,c_0_112]),c_0_67])]) ).
cnf(c_0_116,plain,
( p2(esk115_2(esk93_0,esk121_1(esk93_0)))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_108]),c_0_67])]) ).
cnf(c_0_117,plain,
( ~ r1(X2,X1)
| ~ r1(esk93_0,X2)
| r1(X1,esk119_3(esk93_0,X2,X1))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_113,c_0_114]) ).
cnf(c_0_118,plain,
( ~ r1(X1,X2)
| ~ r1(esk93_0,X1)
| p2(esk119_3(esk93_0,X1,X2))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_119,plain,
( ~ r1(esk126_1(esk93_0),X1)
| r1(X1,esk119_3(esk93_0,esk126_1(esk93_0),X1))
| r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_117,c_0_80]) ).
cnf(c_0_120,plain,
( ~ r1(esk126_1(esk93_0),X1)
| p2(esk119_3(esk93_0,esk126_1(esk93_0),X1))
| p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))) ),
inference(spm,[status(thm)],[c_0_118,c_0_80]) ).
cnf(c_0_121,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X1)
| ~ p2(X3)
| ~ r1(esk122_2(X2,X1),X3)
| r1(X1,esk123_2(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_122,negated_conjecture,
r1(esk122_2(esk93_0,esk126_1(esk93_0)),esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))),
inference(spm,[status(thm)],[c_0_119,c_0_103]) ).
cnf(c_0_123,negated_conjecture,
p2(esk119_3(esk93_0,esk126_1(esk93_0),esk122_2(esk93_0,esk126_1(esk93_0)))),
inference(spm,[status(thm)],[c_0_120,c_0_103]) ).
cnf(c_0_124,plain,
r1(esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_122]),c_0_67]),c_0_123]),c_0_80])]) ).
cnf(c_0_125,negated_conjecture,
( ~ r1(X1,esk126_1(esk93_0))
| ~ epred1_1(X1)
| r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(X1,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(spm,[status(thm)],[c_0_87,c_0_124]) ).
cnf(c_0_126,plain,
( ~ epred1_1(X2)
| ~ r1(X2,X3)
| ~ p2(X4)
| ~ r1(esk122_2(X2,X3),X4)
| ~ r1(esk123_2(X2,X3),X1)
| r1(X1,esk124_3(X2,X3,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_127,plain,
( r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))
| p2(esk94_1(esk126_1(esk93_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_125,c_0_80]),c_0_67])]) ).
cnf(c_0_128,plain,
( ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ p2(X4)
| ~ r1(esk122_2(X1,X2),X4)
| ~ r1(esk123_2(X1,X2),X3)
| p2(esk124_3(X1,X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_129,plain,
( ~ r1(esk123_2(esk93_0,esk126_1(esk93_0)),X1)
| r1(X1,esk124_3(esk93_0,esk126_1(esk93_0),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_126,c_0_122]),c_0_67]),c_0_123]),c_0_80])]) ).
cnf(c_0_130,negated_conjecture,
r1(esk123_2(esk93_0,esk126_1(esk93_0)),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_127]),c_0_80])]) ).
cnf(c_0_131,plain,
( ~ r1(esk123_2(esk93_0,esk126_1(esk93_0)),X1)
| p2(esk124_3(esk93_0,esk126_1(esk93_0),X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128,c_0_122]),c_0_67]),c_0_123]),c_0_80])]) ).
cnf(c_0_132,plain,
r1(esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))),esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))),
inference(spm,[status(thm)],[c_0_129,c_0_130]) ).
cnf(c_0_133,plain,
p2(esk124_3(esk93_0,esk126_1(esk93_0),esk118_3(esk93_0,esk126_1(esk93_0),esk123_2(esk93_0,esk126_1(esk93_0))))),
inference(spm,[status(thm)],[c_0_131,c_0_130]) ).
cnf(c_0_134,plain,
( ~ r1(esk126_1(esk93_0),X1)
| p2(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_132]),c_0_67]),c_0_133]),c_0_85]),c_0_124]),c_0_80])]) ).
cnf(c_0_135,negated_conjecture,
p2(esk94_1(esk126_1(esk93_0))),
inference(spm,[status(thm)],[c_0_134,c_0_84]) ).
cnf(c_0_136,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_135]),c_0_80])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL652+1.020 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.18/0.44 % Computer : n006.cluster.edu
% 0.18/0.44 % Model : x86_64 x86_64
% 0.18/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.44 % Memory : 8046.5625MB
% 0.18/0.44 % OS : Linux 6.8.0-71-generic
% 0.18/0.44 % CPULimit : 300
% 0.18/0.44 % WCLimit : 300
% 0.18/0.44 % DateTime : Mon Sep 21 00:46:12 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.52 Running first-order theorem proving
% 0.26/0.52 Running: /export/starexec/sandbox2/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 185.13/27.77 % Version: 3.5.1
% 185.13/27.77 % Preprocessing class: FSLSSMSSSSSNFFN.
% 185.13/27.77 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 185.13/27.77 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 185.13/27.77 % Starting new_bool_3 with 300s (1) cores
% 185.13/27.77 % Starting new_bool_1 with 300s (1) cores
% 185.13/27.77 % Starting sh5l with 300s (1) cores
% 185.13/27.77 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with pid 1653895 completed with status 0
% 185.13/27.77 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S
% 185.13/27.77 % Preprocessing class: FSLSSMSSSSSNFFN.
% 185.13/27.77 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 185.13/27.77 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 185.13/27.77 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 185.13/27.77 % No SInE strategy applied
% 185.13/27.77 % Search class: FGHNF-FSLM33-SFFFFFNN
% 185.13/27.77 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 185.13/27.77 % Starting SubtermCWHack with 136s (1) cores
% 185.13/27.77 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 185.13/27.77 % Starting G-E--_107_C41_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 185.13/27.77 % Starting new_bool_3 with 136s (1) cores
% 185.13/27.77 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 136s (1) cores
% 185.13/27.77 % H----_042_B03_F1_AE_Q4_SP_S2S with pid 1653904 completed with status 0
% 185.13/27.77 % Result found by H----_042_B03_F1_AE_Q4_SP_S2S
% 185.13/27.77 % Preprocessing class: FSLSSMSSSSSNFFN.
% 185.13/27.77 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 185.13/27.77 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 1500s (5) cores
% 185.13/27.77 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 185.13/27.77 % No SInE strategy applied
% 185.13/27.77 % Search class: FGHNF-FSLM33-SFFFFFNN
% 185.13/27.77 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 185.13/27.77 % Starting SubtermCWHack with 136s (1) cores
% 185.13/27.77 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S5PRR_S2S with 151s (1) cores
% 185.13/27.77 % Starting G-E--_107_C41_F1_PI_AE_Q4_CS_SP_PS_S4S with 136s (1) cores
% 185.13/27.77 % Starting new_bool_3 with 136s (1) cores
% 185.13/27.77 % Starting H----_042_B03_F1_AE_Q4_SP_S2S with 136s (1) cores
% 185.13/27.77 % Preprocessing time : 0.010 s
% 185.13/27.77
% 185.13/27.77 % Proof found!
% 185.13/27.77 % SZS status Theorem
% 185.13/27.77 % SZS output start CNFRefutation
% See solution above
% 185.13/27.77 % Parsed axioms : 1
% 185.13/27.77 % Removed by relevancy pruning/SinE : 0
% 185.13/27.77 % Initial clauses : 324
% 185.13/27.77 % Removed in clause preprocessing : 0
% 185.13/27.77 % Initial clauses in saturation : 324
% 185.13/27.77 % Processed clauses : 42099
% 185.13/27.77 % ...of these trivial : 8
% 185.13/27.77 % ...subsumed : 4704
% 185.13/27.77 % ...remaining for further processing : 37387
% 185.13/27.77 % Other redundant clauses eliminated : 0
% 185.13/27.77 % Clauses deleted for lack of memory : 0
% 185.13/27.77 % Backward-subsumed : 661
% 185.13/27.77 % Backward-rewritten : 1475
% 185.13/27.77 % Generated clauses : 76598
% 185.13/27.77 % ...of the previous two non-redundant : 76169
% 185.13/27.77 % ...aggressively subsumed : 0
% 185.13/27.77 % Contextual simplify-reflections : 0
% 185.13/27.77 % Paramodulations : 76598
% 185.13/27.77 % Factorizations : 0
% 185.13/27.77 % NegExts : 0
% 185.13/27.77 % Equation resolutions : 0
% 185.13/27.77 % Disequality decompositions : 0
% 185.13/27.77 % Total rewrite steps : 4845
% 185.13/27.77 % ...of those cached : 4720
% 185.13/27.77 % Propositional unsat checks : 0
% 185.13/27.77 % Propositional check models : 0
% 185.13/27.77 % Propositional check unsatisfiable : 0
% 185.13/27.77 % Propositional clauses : 0
% 185.13/27.77 % Propositional clauses after purity: 0
% 185.13/27.77 % Propositional unsat core size : 0
% 185.13/27.77 % Propositional preprocessing time : 0.000
% 185.13/27.77 % Propositional encoding time : 0.000
% 185.13/27.77 % Propositional solver time : 0.000
% 185.13/27.77 % Success case prop preproc time : 0.000
% 185.13/27.77 % Success case prop encoding time : 0.000
% 185.13/27.77 % Success case prop solver time : 0.000
% 185.13/27.77 % Current number of processed clauses : 35251
% 185.13/27.77 % Positive orientable unit clauses : 240
% 185.13/27.77 % Positive unorientable unit clauses: 0
% 185.13/27.77 % Negative unit clauses : 22
% 185.13/27.77 % Non-unit-clauses : 34989
% 185.13/27.77 % Current number of unprocessed clauses: 32417
% 185.13/27.77 % ...number of literals in the above : 252074
% 185.13/27.77 % Current number of archived formulas : 0
% 185.13/27.77 % Current number of archived clauses : 2136
% 185.13/27.77 % Clause-clause subsumption calls (NU) : 16912282
% 185.13/27.77 % Rec. Clause-clause subsumption calls : 2086345
% 185.13/27.77 % Non-unit clause-clause subsumptions : 5325
% 185.13/27.77 % Unit Clause-clause subsumption calls : 223257
% 185.13/27.77 % Rewrite failures with RHS unbound : 0
% 185.13/27.77 % BW rewrite match attempts : 114
% 185.13/27.77 % BW rewrite match successes : 86
% 185.13/27.77 % Condensation attempts : 0
% 185.13/27.77 % Condensation successes : 0
% 185.13/27.77 % Termbank termtop insertions : 2777240
% 185.13/27.77 % Search garbage collected termcells : 6405
% 185.13/27.77
% 185.13/27.77 % -------------------------------------------------
% 185.13/27.77 % User time : 25.920 s
% 185.13/27.77 % System time : 0.211 s
% 185.13/27.77 % Total time : 26.131 s
% 185.13/27.77 % Maximum resident set size: 4692 pages
% 185.13/27.77
% 185.13/27.77 % -------------------------------------------------
% 185.13/27.77 % User time : 130.779 s
% 185.13/27.77 % System time : 1.876 s
% 185.13/27.77 % Total time : 132.655 s
% 185.13/27.77 % Maximum resident set size: 4608 pages
% 185.13/27.77 % E exiting
%------------------------------------------------------------------------------