%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL652+1.005 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 04:42:45 PM UTC 2026
% Result : Theorem 78.63s 47.63s
% Output : CNFRefutation 78.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 3
% Syntax : Number of formulae : 129 ( 18 unt; 0 def)
% Number of atoms : 1415 ( 0 equ)
% Maximal formula atoms : 194 ( 10 avg)
% Number of connectives : 2485 (1199 ~;1126 |; 156 &)
% ( 2 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 85 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 21 con; 0-7 aty)
% Number of variables : 542 ( 0 sgn 434 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p4(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
& p2(X1)
& ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) ) ) ) )
| ( ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(c_0_1,plain,
! [X2] :
( epred2_1(X2)
<=> ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
& p2(X1)
& ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) ) ) ) )
| ( ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) ),
introduced(definition) ).
fof(c_0_2,plain,
! [X2] :
( epred1_1(X2)
<=> ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
& p2(X1)
& ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) ) ) ) )
| ( ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) ),
introduced(definition) ).
fof(c_0_3,negated_conjecture,
~ ~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p4(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| epred2_1(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p2(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ),
inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]),c_0_1]) ).
fof(c_0_4,plain,
! [X2] :
( epred2_1(X2)
=> ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| epred1_1(X2) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ) ) ) ),
inference(apply_def,[status(thm)],[inference(split_equiv,[status(thm)],[c_0_1]),c_0_2]) ).
fof(c_0_5,negated_conjecture,
! [X134,X135,X136,X137,X140,X141,X142,X143,X144,X148,X153,X158,X163,X168,X171,X173,X174,X175,X177,X178,X179,X181,X182,X183,X185,X186,X187,X189,X190,X191] :
( ( ~ r1(esk1_0,X134)
| ~ p4(X134) )
& ( r1(X135,esk3_1(X135))
| r1(X137,esk2_3(X135,X136,X137))
| ~ r1(X136,X137)
| ~ r1(X135,X136)
| ~ r1(esk1_0,X135) )
& ( ~ r1(esk3_1(X135),X140)
| ~ p1(X140)
| r1(X137,esk2_3(X135,X136,X137))
| ~ r1(X136,X137)
| ~ r1(X135,X136)
| ~ r1(esk1_0,X135) )
& ( r1(X135,esk3_1(X135))
| p1(esk2_3(X135,X136,X137))
| ~ r1(X136,X137)
| ~ r1(X135,X136)
| ~ r1(esk1_0,X135) )
& ( ~ r1(esk3_1(X135),X140)
| ~ p1(X140)
| p1(esk2_3(X135,X136,X137))
| ~ r1(X136,X137)
| ~ r1(X135,X136)
| ~ r1(esk1_0,X135) )
& ( ~ r1(esk1_0,X141)
| epred2_1(X141) )
& ( r1(X142,esk4_1(X142))
| ~ r1(X142,X143)
| ~ r1(X143,X144)
| p1(X144)
| ~ r1(esk1_0,X142) )
& ( ~ p1(esk4_1(X142))
| ~ r1(X142,X143)
| ~ r1(X143,X144)
| p1(X144)
| ~ r1(esk1_0,X142) )
& r1(esk1_0,esk5_0)
& r1(esk5_0,esk6_0)
& ( ~ r1(esk6_0,X148)
| p1(X148) )
& r1(esk5_0,esk7_0)
& ~ p1(esk7_0)
& r1(esk1_0,esk8_0)
& r1(esk8_0,esk9_0)
& r1(esk9_0,esk10_0)
& ( ~ r1(esk10_0,X153)
| p1(X153) )
& r1(esk9_0,esk11_0)
& ~ p1(esk11_0)
& r1(esk8_0,esk12_0)
& r1(esk12_0,esk13_0)
& r1(esk13_0,esk14_0)
& ( ~ r1(esk14_0,X158)
| p1(X158) )
& r1(esk13_0,esk15_0)
& ~ p1(esk15_0)
& r1(esk12_0,esk16_0)
& r1(esk16_0,esk17_0)
& r1(esk17_0,esk18_0)
& ( ~ r1(esk18_0,X163)
| p1(X163) )
& r1(esk17_0,esk19_0)
& ~ p1(esk19_0)
& r1(esk16_0,esk20_0)
& r1(esk20_0,esk21_0)
& r1(esk21_0,esk22_0)
& ( ~ r1(esk22_0,X168)
| p1(X168) )
& r1(esk21_0,esk23_0)
& ~ p1(esk23_0)
& r1(esk20_0,esk24_0)
& ( r1(X171,esk25_1(X171))
| ~ r1(esk24_0,X171) )
& ( ~ p2(esk25_1(X171))
| ~ r1(esk24_0,X171) )
& ( r1(X173,esk26_1(X173))
| ~ r1(esk20_0,X173)
| ~ r1(X173,X174)
| ~ r1(X174,X175)
| ~ p1(X175) )
& ( p1(esk26_1(X173))
| ~ r1(esk20_0,X173)
| ~ r1(X173,X174)
| ~ r1(X174,X175)
| ~ p1(X175) )
& ( r1(X177,esk27_1(X177))
| ~ r1(esk16_0,X177)
| ~ r1(X177,X178)
| ~ r1(X178,X179)
| ~ p1(X179) )
& ( p1(esk27_1(X177))
| ~ r1(esk16_0,X177)
| ~ r1(X177,X178)
| ~ r1(X178,X179)
| ~ p1(X179) )
& ( r1(X181,esk28_1(X181))
| ~ r1(esk12_0,X181)
| ~ r1(X181,X182)
| ~ r1(X182,X183)
| ~ p1(X183) )
& ( p1(esk28_1(X181))
| ~ r1(esk12_0,X181)
| ~ r1(X181,X182)
| ~ r1(X182,X183)
| ~ p1(X183) )
& ( r1(X185,esk29_1(X185))
| ~ r1(esk8_0,X185)
| ~ r1(X185,X186)
| ~ r1(X186,X187)
| ~ p1(X187) )
& ( p1(esk29_1(X185))
| ~ r1(esk8_0,X185)
| ~ r1(X185,X186)
| ~ r1(X186,X187)
| ~ p1(X187) )
& ( r1(X189,esk30_1(X189))
| ~ r1(esk1_0,X189)
| ~ r1(X189,X190)
| ~ r1(X190,X191)
| ~ p1(X191) )
& ( p1(esk30_1(X189))
| ~ r1(esk1_0,X189)
| ~ r1(X189,X190)
| ~ r1(X190,X191)
| ~ p1(X191) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_3])])])])]) ).
fof(c_0_6,plain,
! [X220,X221,X222,X223,X226,X227,X228,X229,X230,X233,X234,X235,X236,X237,X240,X241,X242,X243,X244,X247,X248,X249,X250,X251,X253,X254,X255,X257,X258,X259,X261,X262,X263] :
( ( r1(X221,esk46_2(X220,X221))
| r1(X223,esk45_4(X220,X221,X222,X223))
| ~ r1(X222,X223)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ epred2_1(X220) )
& ( ~ r1(esk46_2(X220,X221),X226)
| ~ p1(X226)
| r1(X223,esk45_4(X220,X221,X222,X223))
| ~ r1(X222,X223)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ epred2_1(X220) )
& ( r1(X221,esk46_2(X220,X221))
| p1(esk45_4(X220,X221,X222,X223))
| ~ r1(X222,X223)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ epred2_1(X220) )
& ( ~ r1(esk46_2(X220,X221),X226)
| ~ p1(X226)
| p1(esk45_4(X220,X221,X222,X223))
| ~ r1(X222,X223)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ epred2_1(X220) )
& ( r1(X228,esk48_3(X220,X227,X228))
| r1(X230,esk47_5(X220,X227,X228,X229,X230))
| ~ r1(X229,X230)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk48_3(X220,X227,X228),X233)
| ~ p1(X233)
| r1(X230,esk47_5(X220,X227,X228,X229,X230))
| ~ r1(X229,X230)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X228,esk48_3(X220,X227,X228))
| p1(esk47_5(X220,X227,X228,X229,X230))
| ~ r1(X229,X230)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk48_3(X220,X227,X228),X233)
| ~ p1(X233)
| p1(esk47_5(X220,X227,X228,X229,X230))
| ~ r1(X229,X230)
| ~ r1(X228,X229)
| ~ r1(X227,X228)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X235,esk50_4(X220,X227,X234,X235))
| r1(X237,esk49_6(X220,X227,X234,X235,X236,X237))
| ~ r1(X236,X237)
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk50_4(X220,X227,X234,X235),X240)
| ~ p1(X240)
| r1(X237,esk49_6(X220,X227,X234,X235,X236,X237))
| ~ r1(X236,X237)
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X235,esk50_4(X220,X227,X234,X235))
| p1(esk49_6(X220,X227,X234,X235,X236,X237))
| ~ r1(X236,X237)
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk50_4(X220,X227,X234,X235),X240)
| ~ p1(X240)
| p1(esk49_6(X220,X227,X234,X235,X236,X237))
| ~ r1(X236,X237)
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X242,esk52_5(X220,X227,X234,X241,X242))
| r1(X244,esk51_7(X220,X227,X234,X241,X242,X243,X244))
| ~ r1(X243,X244)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk52_5(X220,X227,X234,X241,X242),X247)
| ~ p1(X247)
| r1(X244,esk51_7(X220,X227,X234,X241,X242,X243,X244))
| ~ r1(X243,X244)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X242,esk52_5(X220,X227,X234,X241,X242))
| p1(esk51_7(X220,X227,X234,X241,X242,X243,X244))
| ~ r1(X243,X244)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(esk52_5(X220,X227,X234,X241,X242),X247)
| ~ p1(X247)
| p1(esk51_7(X220,X227,X234,X241,X242,X243,X244))
| ~ r1(X243,X244)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ r1(X241,X248)
| epred1_1(X248)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X249,esk53_5(X220,X227,X234,X241,X249))
| ~ r1(X249,X250)
| ~ r1(X250,X251)
| p1(X251)
| ~ r1(X241,X249)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ p1(esk53_5(X220,X227,X234,X241,X249))
| ~ r1(X249,X250)
| ~ r1(X250,X251)
| p1(X251)
| ~ r1(X241,X249)
| ~ r1(X234,X241)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X253,esk54_4(X220,X227,X234,X253))
| ~ r1(X253,X254)
| ~ r1(X254,X255)
| p1(X255)
| ~ r1(X234,X253)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ p1(esk54_4(X220,X227,X234,X253))
| ~ r1(X253,X254)
| ~ r1(X254,X255)
| p1(X255)
| ~ r1(X234,X253)
| ~ r1(X227,X234)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X257,esk55_3(X220,X227,X257))
| ~ r1(X257,X258)
| ~ r1(X258,X259)
| p1(X259)
| ~ r1(X227,X257)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( ~ p1(esk55_3(X220,X227,X257))
| ~ r1(X257,X258)
| ~ r1(X258,X259)
| p1(X259)
| ~ r1(X227,X257)
| ~ r1(X220,X227)
| ~ epred2_1(X220) )
& ( r1(X261,esk56_2(X220,X261))
| ~ r1(X261,X262)
| ~ r1(X262,X263)
| p1(X263)
| ~ r1(X220,X261)
| ~ epred2_1(X220) )
& ( ~ p1(esk56_2(X220,X261))
| ~ r1(X261,X262)
| ~ r1(X262,X263)
| p1(X263)
| ~ r1(X220,X261)
| ~ epred2_1(X220) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_4])])])])]) ).
cnf(c_0_7,negated_conjecture,
( epred2_1(X1)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_8,negated_conjecture,
r1(esk1_0,esk8_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_9,plain,
( epred1_1(X2)
| ~ r1(X1,X2)
| ~ r1(X3,X1)
| ~ r1(X4,X3)
| ~ r1(X5,X4)
| ~ epred2_1(X5) ),
inference(split_conjunct,[status(thm)],[c_0_6]) ).
cnf(c_0_10,negated_conjecture,
r1(esk8_0,esk12_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_11,negated_conjecture,
epred2_1(esk8_0),
inference(spm,[status(thm)],[c_0_7,c_0_8]) ).
cnf(c_0_12,negated_conjecture,
( epred1_1(X1)
| ~ r1(esk12_0,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_9,c_0_10]),c_0_11])]) ).
cnf(c_0_13,negated_conjecture,
r1(esk12_0,esk16_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
fof(c_0_14,plain,
! [X2] :
( epred1_1(X2)
=> ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) )
& p2(X1)
& ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) )
| ( ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p2(X1) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
| ~ p2(X2) ) ) ) ) )
| ( ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ~ p2(X1) )
& ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p2(X2) ) ) ) ) ),
inference(split_equiv,[status(thm)],[c_0_2]) ).
cnf(c_0_15,negated_conjecture,
( epred1_1(X1)
| ~ r1(esk16_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_12,c_0_13]) ).
cnf(c_0_16,negated_conjecture,
r1(esk16_0,esk20_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
fof(c_0_17,plain,
! [X193,X194,X197,X198,X200,X202,X203,X204,X208,X209,X211,X213,X219] :
( ( r1(X194,esk31_2(X193,X194))
| ~ r1(X193,X194)
| ~ epred1_1(X193) )
& ( r1(esk31_2(X193,X194),esk32_2(X193,X194))
| ~ r1(X193,X194)
| ~ epred1_1(X193) )
& ( ~ p3(esk32_2(X193,X194))
| ~ r1(X193,X194)
| ~ epred1_1(X193) )
& ( p2(esk31_2(X193,X194))
| ~ r1(X193,X194)
| ~ epred1_1(X193) )
& ( r1(X200,esk34_3(X193,X197,X200))
| ~ r1(X197,X200)
| r1(X198,esk33_3(X193,X197,X198))
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( ~ r1(esk34_3(X193,X197,X200),X202)
| ~ p2(X202)
| ~ r1(X197,X200)
| r1(X198,esk33_3(X193,X197,X198))
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( r1(X200,esk34_3(X193,X197,X200))
| ~ r1(X197,X200)
| ~ p3(esk33_3(X193,X197,X198))
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( ~ r1(esk34_3(X193,X197,X200),X202)
| ~ p2(X202)
| ~ r1(X197,X200)
| ~ p3(esk33_3(X193,X197,X198))
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( r1(X200,esk34_3(X193,X197,X200))
| ~ r1(X197,X200)
| p2(X198)
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( ~ r1(esk34_3(X193,X197,X200),X202)
| ~ p2(X202)
| ~ r1(X197,X200)
| p2(X198)
| ~ r1(X197,X198)
| ~ p2(X197)
| ~ r1(X193,X197)
| ~ epred1_1(X193) )
& ( r1(X193,esk37_1(X193))
| r1(X204,esk35_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( ~ r1(esk37_1(X193),X208)
| ~ p2(X208)
| r1(X204,esk35_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( r1(X193,esk37_1(X193))
| r1(esk35_3(X193,X203,X204),esk36_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( ~ r1(esk37_1(X193),X208)
| ~ p2(X208)
| r1(esk35_3(X193,X203,X204),esk36_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( r1(X193,esk37_1(X193))
| ~ p3(esk36_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( ~ r1(esk37_1(X193),X208)
| ~ p2(X208)
| ~ p3(esk36_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( r1(X193,esk37_1(X193))
| p2(esk35_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( ~ r1(esk37_1(X193),X208)
| ~ p2(X208)
| p2(esk35_3(X193,X203,X204))
| ~ r1(X203,X204)
| ~ r1(X193,X203)
| ~ epred1_1(X193) )
& ( r1(X209,esk39_2(X193,X209))
| r1(X209,esk38_2(X193,X209))
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(X213,esk40_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| r1(X209,esk38_2(X193,X209))
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(esk40_3(X193,X209,X213),esk41_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| r1(X209,esk38_2(X193,X209))
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( ~ p3(esk41_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| r1(X209,esk38_2(X193,X209))
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( p2(esk40_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| r1(X209,esk38_2(X193,X209))
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(X209,esk39_2(X193,X209))
| ~ r1(esk38_2(X193,X209),X211)
| ~ p2(X211)
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(X213,esk40_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| ~ r1(esk38_2(X193,X209),X211)
| ~ p2(X211)
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(esk40_3(X193,X209,X213),esk41_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| ~ r1(esk38_2(X193,X209),X211)
| ~ p2(X211)
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( ~ p3(esk41_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| ~ r1(esk38_2(X193,X209),X211)
| ~ p2(X211)
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( p2(esk40_3(X193,X209,X213))
| ~ r1(esk39_2(X193,X209),X213)
| ~ r1(esk38_2(X193,X209),X211)
| ~ p2(X211)
| ~ r1(X193,X209)
| ~ epred1_1(X193) )
& ( r1(X193,esk44_1(X193))
| r1(X193,esk42_1(X193))
| ~ epred1_1(X193) )
& ( ~ r1(esk44_1(X193),X219)
| ~ p2(X219)
| r1(X193,esk42_1(X193))
| ~ epred1_1(X193) )
& ( r1(X193,esk44_1(X193))
| r1(esk42_1(X193),esk43_1(X193))
| ~ epred1_1(X193) )
& ( ~ r1(esk44_1(X193),X219)
| ~ p2(X219)
| r1(esk42_1(X193),esk43_1(X193))
| ~ epred1_1(X193) )
& ( r1(X193,esk44_1(X193))
| ~ p3(esk43_1(X193))
| ~ epred1_1(X193) )
& ( ~ r1(esk44_1(X193),X219)
| ~ p2(X219)
| ~ p3(esk43_1(X193))
| ~ epred1_1(X193) )
& ( r1(X193,esk44_1(X193))
| p2(esk42_1(X193))
| ~ epred1_1(X193) )
& ( ~ r1(esk44_1(X193),X219)
| ~ p2(X219)
| p2(esk42_1(X193))
| ~ epred1_1(X193) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_14])])])])]) ).
cnf(c_0_18,negated_conjecture,
( epred1_1(X1)
| ~ r1(esk20_0,X1) ),
inference(spm,[status(thm)],[c_0_15,c_0_16]) ).
cnf(c_0_19,negated_conjecture,
r1(esk20_0,esk24_0),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_20,plain,
( r1(X1,esk44_1(X1))
| r1(X1,esk42_1(X1))
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_21,negated_conjecture,
epred1_1(esk24_0),
inference(spm,[status(thm)],[c_0_18,c_0_19]) ).
cnf(c_0_22,negated_conjecture,
( r1(X1,esk25_1(X1))
| ~ r1(esk24_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_23,plain,
( r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_24,plain,
( r1(X1,esk44_1(X1))
| p2(esk42_1(X1))
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_25,plain,
( r1(X1,esk34_3(X2,X3,X1))
| p2(X4)
| ~ r1(X3,X1)
| ~ r1(X3,X4)
| ~ p2(X3)
| ~ r1(X2,X3)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_26,negated_conjecture,
( r1(esk42_1(esk24_0),esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_27,plain,
( p2(esk42_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_24,c_0_21]) ).
cnf(c_0_28,plain,
( r1(X1,esk39_2(X2,X1))
| r1(X1,esk38_2(X2,X1))
| ~ r1(X2,X1)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_29,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk34_3(X2,esk42_1(esk24_0),X1))
| r1(esk24_0,esk44_1(esk24_0))
| ~ epred1_1(X2)
| ~ r1(esk42_1(esk24_0),X1)
| ~ r1(X2,esk42_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_26]),c_0_27]) ).
cnf(c_0_30,plain,
( r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_23]),c_0_21])]) ).
cnf(c_0_31,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_29,c_0_30]) ).
cnf(c_0_32,plain,
( r1(X1,esk40_3(X2,X3,X1))
| r1(X3,esk38_2(X2,X3))
| ~ r1(esk39_2(X2,X3),X1)
| ~ r1(X2,X3)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_33,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_23]),c_0_21])]) ).
cnf(c_0_34,plain,
( p2(esk40_3(X1,X2,X3))
| r1(X2,esk38_2(X1,X2))
| ~ r1(esk39_2(X1,X2),X3)
| ~ r1(X1,X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_35,plain,
( p2(X5)
| ~ r1(esk34_3(X1,X2,X3),X4)
| ~ p2(X4)
| ~ r1(X2,X3)
| ~ r1(X2,X5)
| ~ p2(X2)
| ~ r1(X1,X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_36,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_21])]),c_0_23]) ).
cnf(c_0_37,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_33]),c_0_21])]),c_0_23]) ).
cnf(c_0_38,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_36]),c_0_21])]),c_0_23]),c_0_30]),c_0_27]),c_0_37]) ).
cnf(c_0_39,plain,
( r1(X1,esk37_1(X1))
| r1(X2,esk35_3(X1,X3,X2))
| ~ r1(X3,X2)
| ~ r1(X1,X3)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_40,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_38,c_0_26]) ).
cnf(c_0_41,plain,
( r1(X1,esk37_1(X1))
| p2(esk35_3(X1,X2,X3))
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_42,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk44_1(esk24_0))
| r1(X1,esk37_1(X1))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_39,c_0_40]) ).
cnf(c_0_43,plain,
( p2(esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| r1(X1,esk37_1(X1))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_41,c_0_40]) ).
cnf(c_0_44,plain,
( r1(X1,esk39_2(X2,X1))
| ~ r1(esk38_2(X2,X1),X3)
| ~ p2(X3)
| ~ r1(X2,X1)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_45,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_23]),c_0_21])]) ).
cnf(c_0_46,plain,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_23]),c_0_21])]) ).
cnf(c_0_47,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_45]),c_0_21])]),c_0_23]),c_0_46]) ).
cnf(c_0_48,plain,
( r1(X1,esk40_3(X2,X3,X1))
| ~ r1(esk39_2(X2,X3),X1)
| ~ r1(esk38_2(X2,X3),X4)
| ~ p2(X4)
| ~ r1(X2,X3)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_49,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_29,c_0_47]) ).
cnf(c_0_50,plain,
( p2(esk40_3(X1,X2,X3))
| ~ r1(esk39_2(X1,X2),X3)
| ~ r1(esk38_2(X1,X2),X4)
| ~ p2(X4)
| ~ r1(X1,X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_51,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))
| r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_45]),c_0_21])]),c_0_23]),c_0_46]) ).
cnf(c_0_52,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_23]),c_0_21])]) ).
cnf(c_0_53,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_45]),c_0_21])]),c_0_23]),c_0_46]) ).
cnf(c_0_54,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_51,c_0_52]) ).
cnf(c_0_55,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_53,c_0_52]) ).
cnf(c_0_56,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_54]),c_0_21])]),c_0_23]),c_0_47]),c_0_27]),c_0_55]) ).
cnf(c_0_57,negated_conjecture,
( ~ p2(esk25_1(X1))
| ~ r1(esk24_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_5]) ).
cnf(c_0_58,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_56,c_0_26]) ).
cnf(c_0_59,plain,
( r1(X1,esk31_2(X2,X1))
| ~ r1(X2,X1)
| ~ epred1_1(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_60,negated_conjecture,
( r1(esk24_0,esk44_1(esk24_0))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_23]) ).
cnf(c_0_61,plain,
( p2(esk31_2(X1,X2))
| ~ r1(X1,X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_62,plain,
( r1(X3,esk35_3(X1,X4,X3))
| ~ r1(esk37_1(X1),X2)
| ~ p2(X2)
| ~ r1(X4,X3)
| ~ r1(X1,X4)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_63,plain,
( r1(esk37_1(esk24_0),esk31_2(esk24_0,esk37_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_60]),c_0_21])]) ).
cnf(c_0_64,plain,
( p2(esk31_2(esk24_0,esk37_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_60]),c_0_21])]) ).
cnf(c_0_65,plain,
( p2(esk35_3(X1,X3,X4))
| ~ r1(esk37_1(X1),X2)
| ~ p2(X2)
| ~ r1(X3,X4)
| ~ r1(X1,X3)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_66,plain,
( r1(X1,esk35_3(esk24_0,X2,X1))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk24_0,X2)
| ~ r1(X2,X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_63]),c_0_21])]),c_0_64]) ).
cnf(c_0_67,plain,
( p2(esk35_3(esk24_0,X1,X2))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk24_0,X1)
| ~ r1(X1,X2) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_63]),c_0_21])]),c_0_64]) ).
cnf(c_0_68,plain,
( r1(X1,esk35_3(esk24_0,esk42_1(esk24_0),X1))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(spm,[status(thm)],[c_0_66,c_0_23]) ).
cnf(c_0_69,plain,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),X1))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(spm,[status(thm)],[c_0_67,c_0_23]) ).
cnf(c_0_70,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_68,c_0_40]) ).
cnf(c_0_71,negated_conjecture,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_69,c_0_40]) ).
cnf(c_0_72,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_70]),c_0_21])]),c_0_23]),c_0_71]) ).
cnf(c_0_73,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk44_1(esk24_0))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_29,c_0_72]) ).
cnf(c_0_74,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_70]),c_0_21])]),c_0_23]),c_0_71]) ).
cnf(c_0_75,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_23]),c_0_21])]) ).
cnf(c_0_76,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_70]),c_0_21])]),c_0_23]),c_0_71]) ).
cnf(c_0_77,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_78,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_76,c_0_75]) ).
cnf(c_0_79,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| r1(esk24_0,esk44_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_77]),c_0_21])]),c_0_23]),c_0_72]),c_0_27]),c_0_78]) ).
cnf(c_0_80,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk44_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_79,c_0_26]) ).
cnf(c_0_81,negated_conjecture,
r1(esk24_0,esk44_1(esk24_0)),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_80]),c_0_23]) ).
cnf(c_0_82,plain,
( r1(X1,esk42_1(X1))
| ~ r1(esk44_1(X1),X2)
| ~ p2(X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_83,plain,
r1(esk44_1(esk24_0),esk31_2(esk24_0,esk44_1(esk24_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_81]),c_0_21])]) ).
cnf(c_0_84,plain,
p2(esk31_2(esk24_0,esk44_1(esk24_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_81]),c_0_21])]) ).
cnf(c_0_85,plain,
r1(esk24_0,esk42_1(esk24_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_83]),c_0_21]),c_0_84])]) ).
cnf(c_0_86,plain,
( p2(esk42_1(X1))
| ~ r1(esk44_1(X1),X2)
| ~ p2(X2)
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_87,negated_conjecture,
r1(esk42_1(esk24_0),esk25_1(esk42_1(esk24_0))),
inference(spm,[status(thm)],[c_0_22,c_0_85]) ).
cnf(c_0_88,plain,
p2(esk42_1(esk24_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_83]),c_0_21]),c_0_84])]) ).
cnf(c_0_89,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk34_3(X2,esk42_1(esk24_0),X1))
| ~ epred1_1(X2)
| ~ r1(esk42_1(esk24_0),X1)
| ~ r1(X2,esk42_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_87]),c_0_88])]) ).
cnf(c_0_90,plain,
( r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_85]),c_0_21])]) ).
cnf(c_0_91,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_89,c_0_90]) ).
cnf(c_0_92,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_85]),c_0_21])]) ).
cnf(c_0_93,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_92]),c_0_21]),c_0_85])]) ).
cnf(c_0_94,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_92]),c_0_21]),c_0_85])]) ).
cnf(c_0_95,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_93]),c_0_21]),c_0_88]),c_0_85])]),c_0_90]),c_0_94]) ).
cnf(c_0_96,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))) ),
inference(spm,[status(thm)],[c_0_95,c_0_87]) ).
cnf(c_0_97,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| r1(X1,esk37_1(X1))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_39,c_0_96]) ).
cnf(c_0_98,plain,
( p2(esk35_3(X1,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk37_1(X1))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_41,c_0_96]) ).
cnf(c_0_99,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_85]),c_0_21])]) ).
cnf(c_0_100,plain,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_98,c_0_85]),c_0_21])]) ).
cnf(c_0_101,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_99]),c_0_21]),c_0_85])]),c_0_100]) ).
cnf(c_0_102,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk37_1(esk24_0))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_89,c_0_101]) ).
cnf(c_0_103,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_99]),c_0_21]),c_0_85])]),c_0_100]) ).
cnf(c_0_104,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_85]),c_0_21])]) ).
cnf(c_0_105,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_99]),c_0_21]),c_0_85])]),c_0_100]) ).
cnf(c_0_106,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_107,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_105,c_0_104]) ).
cnf(c_0_108,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| r1(esk24_0,esk37_1(esk24_0))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_106]),c_0_21]),c_0_88]),c_0_85])]),c_0_101]),c_0_107]) ).
cnf(c_0_109,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk24_0,esk37_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_108,c_0_87]) ).
cnf(c_0_110,negated_conjecture,
r1(esk24_0,esk37_1(esk24_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_109]),c_0_85])]) ).
cnf(c_0_111,plain,
r1(esk37_1(esk24_0),esk31_2(esk24_0,esk37_1(esk24_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_110]),c_0_21])]) ).
cnf(c_0_112,plain,
p2(esk31_2(esk24_0,esk37_1(esk24_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61,c_0_110]),c_0_21])]) ).
cnf(c_0_113,plain,
( r1(X1,esk35_3(esk24_0,X2,X1))
| ~ r1(esk24_0,X2)
| ~ r1(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62,c_0_111]),c_0_21]),c_0_112])]) ).
cnf(c_0_114,plain,
( p2(esk35_3(esk24_0,X1,X2))
| ~ r1(esk24_0,X1)
| ~ r1(X1,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_111]),c_0_21]),c_0_112])]) ).
cnf(c_0_115,plain,
( r1(X1,esk35_3(esk24_0,esk42_1(esk24_0),X1))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(spm,[status(thm)],[c_0_113,c_0_85]) ).
cnf(c_0_116,plain,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),X1))
| ~ r1(esk42_1(esk24_0),X1) ),
inference(spm,[status(thm)],[c_0_114,c_0_85]) ).
cnf(c_0_117,negated_conjecture,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk38_2(esk24_0,esk42_1(esk24_0)),esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0)))) ),
inference(spm,[status(thm)],[c_0_115,c_0_96]) ).
cnf(c_0_118,negated_conjecture,
( p2(esk35_3(esk24_0,esk42_1(esk24_0),esk38_2(esk24_0,esk42_1(esk24_0))))
| p2(esk25_1(esk42_1(esk24_0))) ),
inference(spm,[status(thm)],[c_0_116,c_0_96]) ).
cnf(c_0_119,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_44,c_0_117]),c_0_21]),c_0_85])]),c_0_118]) ).
cnf(c_0_120,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(X1,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))
| ~ epred1_1(X1)
| ~ r1(X1,esk42_1(esk24_0)) ),
inference(spm,[status(thm)],[c_0_89,c_0_119]) ).
cnf(c_0_121,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(X1,esk40_3(esk24_0,esk42_1(esk24_0),X1))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_117]),c_0_21]),c_0_85])]),c_0_118]) ).
cnf(c_0_122,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk39_2(esk24_0,esk42_1(esk24_0)),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_85]),c_0_21])]) ).
cnf(c_0_123,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),X1))
| p2(esk25_1(esk42_1(esk24_0)))
| ~ r1(esk39_2(esk24_0,esk42_1(esk24_0)),X1) ),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_117]),c_0_21]),c_0_85])]),c_0_118]) ).
cnf(c_0_124,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| r1(esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))),esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0))))) ),
inference(spm,[status(thm)],[c_0_121,c_0_122]) ).
cnf(c_0_125,plain,
( p2(esk40_3(esk24_0,esk42_1(esk24_0),esk34_3(esk24_0,esk42_1(esk24_0),esk39_2(esk24_0,esk42_1(esk24_0)))))
| p2(esk25_1(esk42_1(esk24_0))) ),
inference(spm,[status(thm)],[c_0_123,c_0_122]) ).
cnf(c_0_126,plain,
( p2(esk25_1(esk42_1(esk24_0)))
| p2(X1)
| ~ r1(esk42_1(esk24_0),X1) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_35,c_0_124]),c_0_21]),c_0_88]),c_0_85])]),c_0_119]),c_0_125]) ).
cnf(c_0_127,negated_conjecture,
p2(esk25_1(esk42_1(esk24_0))),
inference(spm,[status(thm)],[c_0_126,c_0_87]) ).
cnf(c_0_128,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_127]),c_0_85])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL652+1.005 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n022.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Mon May 4 22:49:51 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 78.63/47.63 % Version : CSE_E---1.7
% 78.63/47.63 % Problem : theBenchmark.p
% 78.63/47.63 % SZS status Theorem for theBenchmark.p
% 78.63/47.63 % SZS output start CNFRefutation
% See solution above
% 78.63/47.67 % Total time : 46.087s
%------------------------------------------------------------------------------