%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL646+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 : n009.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:33 PM UTC 2026
% Result : Theorem 2.07s 1.85s
% Output : CNFRefutation 2.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 1
% Syntax : Number of formulae : 48 ( 11 unt; 0 def)
% Number of atoms : 1529 ( 0 equ)
% Maximal formula atoms : 620 ( 31 avg)
% Number of connectives : 2875 (1394 ~;1214 |; 267 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 327 ( 13 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-2 aty)
% Number of functors : 69 ( 69 usr; 5 con; 0-4 aty)
% Number of variables : 751 ( 0 sgn 694 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(main,conjecture,
~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,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)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p5(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p5(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& ~ p4(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p3(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p3(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p5(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p5(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p3(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p3(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& ~ p2(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p1(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p1(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',main) ).
fof(c_0_1,negated_conjecture,
~ ~ ? [X1] :
~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p6(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p4(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,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)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p6(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p4(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p2(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p5(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p3(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p6(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p2(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p6(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p5(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p5(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& ~ p4(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p3(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p3(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p6(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p4(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
& ~ p2(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p6(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p5(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p4(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p3(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p6(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p2(X1) )
& ~ p4(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p4(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p1(X2) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p5(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p5(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p3(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p3(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p1(X1) )
& ~ p2(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p5(X1) )
& ~ p1(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p3(X1) )
& ~ p1(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p5(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p3(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p2(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]) ).
fof(c_0_2,negated_conjecture,
! [X259,X260,X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275,X276,X277,X278,X279,X280,X281,X282,X284,X285,X286,X287,X289,X290,X291,X292,X294,X295,X296,X297,X299,X300,X301,X302,X304,X305,X306,X307,X309,X310,X311,X312,X314,X315,X316,X317,X319,X320,X321,X322,X324,X325,X326,X328,X329,X330,X332,X333,X334,X335,X337,X338,X339,X340,X342,X343,X344,X345,X347,X348,X349,X351,X352,X353,X355,X356,X357,X358,X360,X361,X362,X363,X365,X366,X367,X368,X370,X371,X372,X374,X375,X376,X378,X379,X380,X381,X383,X384,X385,X386,X388,X389,X390,X391,X393,X394,X395,X396,X398,X399,X401,X402,X404,X405,X407,X408,X409,X411,X412,X413,X415,X416,X418,X419,X421,X422,X424,X425,X426,X428,X429,X430,X432,X433,X434,X436,X437,X439,X440,X442,X443,X445,X446,X447,X449,X450,X451,X453,X455,X457,X458,X460,X461,X463,X464,X466,X468,X470,X471,X473,X474,X476,X477,X479,X481,X483,X484,X486,X487,X489,X490,X492,X493,X495,X497,X499,X501,X503,X505,X507] :
( ( ~ r1(esk1_0,X259)
| ~ r1(X259,X260)
| ~ r1(X260,X261)
| ~ r1(X261,X262)
| ~ r1(X262,X263)
| p6(X263) )
& ( ~ r1(esk1_0,X264)
| ~ r1(X264,X265)
| ~ r1(X265,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| p4(X268) )
& ( ~ r1(esk1_0,X269)
| ~ r1(X269,X270)
| ~ r1(X270,X271)
| ~ r1(X271,X272)
| ~ r1(X272,X273)
| p4(X273) )
& ( ~ r1(esk1_0,X274)
| ~ r1(X274,X275)
| ~ r1(X275,X276)
| ~ r1(X276,X277)
| ~ r1(X277,X278)
| p2(X278) )
& ( r1(X282,esk2_4(X279,X280,X281,X282))
| p6(X282)
| ~ r1(X281,X282)
| ~ r1(X280,X281)
| ~ r1(X279,X280)
| ~ r1(esk1_0,X279) )
& ( ~ p6(esk2_4(X279,X280,X281,X282))
| p6(X282)
| ~ r1(X281,X282)
| ~ r1(X280,X281)
| ~ r1(X279,X280)
| ~ r1(esk1_0,X279) )
& ( r1(X287,esk3_4(X284,X285,X286,X287))
| p4(X287)
| ~ r1(X286,X287)
| ~ r1(X285,X286)
| ~ r1(X284,X285)
| ~ r1(esk1_0,X284) )
& ( ~ p6(esk3_4(X284,X285,X286,X287))
| p4(X287)
| ~ r1(X286,X287)
| ~ r1(X285,X286)
| ~ r1(X284,X285)
| ~ r1(esk1_0,X284) )
& ( r1(X292,esk4_4(X289,X290,X291,X292))
| p2(X292)
| ~ r1(X291,X292)
| ~ r1(X290,X291)
| ~ r1(X289,X290)
| ~ r1(esk1_0,X289) )
& ( ~ p6(esk4_4(X289,X290,X291,X292))
| p2(X292)
| ~ r1(X291,X292)
| ~ r1(X290,X291)
| ~ r1(X289,X290)
| ~ r1(esk1_0,X289) )
& ( r1(X297,esk5_4(X294,X295,X296,X297))
| p6(X297)
| ~ r1(X296,X297)
| ~ r1(X295,X296)
| ~ r1(X294,X295)
| ~ r1(esk1_0,X294) )
& ( ~ p4(esk5_4(X294,X295,X296,X297))
| p6(X297)
| ~ r1(X296,X297)
| ~ r1(X295,X296)
| ~ r1(X294,X295)
| ~ r1(esk1_0,X294) )
& ( r1(X302,esk6_4(X299,X300,X301,X302))
| p4(X302)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(X299,X300)
| ~ r1(esk1_0,X299) )
& ( ~ p4(esk6_4(X299,X300,X301,X302))
| p4(X302)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(X299,X300)
| ~ r1(esk1_0,X299) )
& ( r1(X307,esk7_4(X304,X305,X306,X307))
| p2(X307)
| ~ r1(X306,X307)
| ~ r1(X305,X306)
| ~ r1(X304,X305)
| ~ r1(esk1_0,X304) )
& ( ~ p4(esk7_4(X304,X305,X306,X307))
| p2(X307)
| ~ r1(X306,X307)
| ~ r1(X305,X306)
| ~ r1(X304,X305)
| ~ r1(esk1_0,X304) )
& ( r1(X312,esk8_4(X309,X310,X311,X312))
| p6(X312)
| ~ r1(X311,X312)
| ~ r1(X310,X311)
| ~ r1(X309,X310)
| ~ r1(esk1_0,X309) )
& ( ~ p2(esk8_4(X309,X310,X311,X312))
| p6(X312)
| ~ r1(X311,X312)
| ~ r1(X310,X311)
| ~ r1(X309,X310)
| ~ r1(esk1_0,X309) )
& ( r1(X317,esk9_4(X314,X315,X316,X317))
| p4(X317)
| ~ r1(X316,X317)
| ~ r1(X315,X316)
| ~ r1(X314,X315)
| ~ r1(esk1_0,X314) )
& ( ~ p2(esk9_4(X314,X315,X316,X317))
| p4(X317)
| ~ r1(X316,X317)
| ~ r1(X315,X316)
| ~ r1(X314,X315)
| ~ r1(esk1_0,X314) )
& ( r1(X322,esk10_4(X319,X320,X321,X322))
| p2(X322)
| ~ r1(X321,X322)
| ~ r1(X320,X321)
| ~ r1(X319,X320)
| ~ r1(esk1_0,X319) )
& ( ~ p2(esk10_4(X319,X320,X321,X322))
| p2(X322)
| ~ r1(X321,X322)
| ~ r1(X320,X321)
| ~ r1(X319,X320)
| ~ r1(esk1_0,X319) )
& ( r1(X326,esk11_3(X324,X325,X326))
| p6(X326)
| ~ r1(X325,X326)
| ~ r1(X324,X325)
| ~ r1(esk1_0,X324) )
& ( ~ p6(esk11_3(X324,X325,X326))
| p6(X326)
| ~ r1(X325,X326)
| ~ r1(X324,X325)
| ~ r1(esk1_0,X324) )
& ( r1(X330,esk12_3(X328,X329,X330))
| p2(X330)
| ~ r1(X329,X330)
| ~ r1(X328,X329)
| ~ r1(esk1_0,X328) )
& ( ~ p6(esk12_3(X328,X329,X330))
| p2(X330)
| ~ r1(X329,X330)
| ~ r1(X328,X329)
| ~ r1(esk1_0,X328) )
& ( r1(X335,esk13_4(X332,X333,X334,X335))
| p5(X335)
| ~ r1(X334,X335)
| ~ r1(X333,X334)
| ~ r1(X332,X333)
| ~ r1(esk1_0,X332) )
& ( ~ p5(esk13_4(X332,X333,X334,X335))
| p5(X335)
| ~ r1(X334,X335)
| ~ r1(X333,X334)
| ~ r1(X332,X333)
| ~ r1(esk1_0,X332) )
& ( r1(X340,esk14_4(X337,X338,X339,X340))
| p5(X340)
| ~ r1(X339,X340)
| ~ r1(X338,X339)
| ~ r1(X337,X338)
| ~ r1(esk1_0,X337) )
& ( ~ p3(esk14_4(X337,X338,X339,X340))
| p5(X340)
| ~ r1(X339,X340)
| ~ r1(X338,X339)
| ~ r1(X337,X338)
| ~ r1(esk1_0,X337) )
& ( r1(X345,esk15_4(X342,X343,X344,X345))
| p5(X345)
| ~ r1(X344,X345)
| ~ r1(X343,X344)
| ~ r1(X342,X343)
| ~ r1(esk1_0,X342) )
& ( ~ p1(esk15_4(X342,X343,X344,X345))
| p5(X345)
| ~ r1(X344,X345)
| ~ r1(X343,X344)
| ~ r1(X342,X343)
| ~ r1(esk1_0,X342) )
& ( r1(X349,esk16_3(X347,X348,X349))
| p6(X349)
| ~ r1(X348,X349)
| ~ r1(X347,X348)
| ~ r1(esk1_0,X347) )
& ( ~ p4(esk16_3(X347,X348,X349))
| p6(X349)
| ~ r1(X348,X349)
| ~ r1(X347,X348)
| ~ r1(esk1_0,X347) )
& ( r1(X353,esk17_3(X351,X352,X353))
| p2(X353)
| ~ r1(X352,X353)
| ~ r1(X351,X352)
| ~ r1(esk1_0,X351) )
& ( ~ p4(esk17_3(X351,X352,X353))
| p2(X353)
| ~ r1(X352,X353)
| ~ r1(X351,X352)
| ~ r1(esk1_0,X351) )
& ( r1(X358,esk18_4(X355,X356,X357,X358))
| p3(X358)
| ~ r1(X357,X358)
| ~ r1(X356,X357)
| ~ r1(X355,X356)
| ~ r1(esk1_0,X355) )
& ( ~ p5(esk18_4(X355,X356,X357,X358))
| p3(X358)
| ~ r1(X357,X358)
| ~ r1(X356,X357)
| ~ r1(X355,X356)
| ~ r1(esk1_0,X355) )
& ( r1(X363,esk19_4(X360,X361,X362,X363))
| p3(X363)
| ~ r1(X362,X363)
| ~ r1(X361,X362)
| ~ r1(X360,X361)
| ~ r1(esk1_0,X360) )
& ( ~ p3(esk19_4(X360,X361,X362,X363))
| p3(X363)
| ~ r1(X362,X363)
| ~ r1(X361,X362)
| ~ r1(X360,X361)
| ~ r1(esk1_0,X360) )
& ( r1(X368,esk20_4(X365,X366,X367,X368))
| p3(X368)
| ~ r1(X367,X368)
| ~ r1(X366,X367)
| ~ r1(X365,X366)
| ~ r1(esk1_0,X365) )
& ( ~ p1(esk20_4(X365,X366,X367,X368))
| p3(X368)
| ~ r1(X367,X368)
| ~ r1(X366,X367)
| ~ r1(X365,X366)
| ~ r1(esk1_0,X365) )
& ( r1(X372,esk21_3(X370,X371,X372))
| p6(X372)
| ~ r1(X371,X372)
| ~ r1(X370,X371)
| ~ r1(esk1_0,X370) )
& ( ~ p2(esk21_3(X370,X371,X372))
| p6(X372)
| ~ r1(X371,X372)
| ~ r1(X370,X371)
| ~ r1(esk1_0,X370) )
& ( r1(X376,esk22_3(X374,X375,X376))
| p2(X376)
| ~ r1(X375,X376)
| ~ r1(X374,X375)
| ~ r1(esk1_0,X374) )
& ( ~ p2(esk22_3(X374,X375,X376))
| p2(X376)
| ~ r1(X375,X376)
| ~ r1(X374,X375)
| ~ r1(esk1_0,X374) )
& ( r1(X381,esk23_4(X378,X379,X380,X381))
| p1(X381)
| ~ r1(X380,X381)
| ~ r1(X379,X380)
| ~ r1(X378,X379)
| ~ r1(esk1_0,X378) )
& ( ~ p5(esk23_4(X378,X379,X380,X381))
| p1(X381)
| ~ r1(X380,X381)
| ~ r1(X379,X380)
| ~ r1(X378,X379)
| ~ r1(esk1_0,X378) )
& ( r1(X386,esk24_4(X383,X384,X385,X386))
| p1(X386)
| ~ r1(X385,X386)
| ~ r1(X384,X385)
| ~ r1(X383,X384)
| ~ r1(esk1_0,X383) )
& ( ~ p4(esk24_4(X383,X384,X385,X386))
| p1(X386)
| ~ r1(X385,X386)
| ~ r1(X384,X385)
| ~ r1(X383,X384)
| ~ r1(esk1_0,X383) )
& ( r1(X391,esk25_4(X388,X389,X390,X391))
| p1(X391)
| ~ r1(X390,X391)
| ~ r1(X389,X390)
| ~ r1(X388,X389)
| ~ r1(esk1_0,X388) )
& ( ~ p3(esk25_4(X388,X389,X390,X391))
| p1(X391)
| ~ r1(X390,X391)
| ~ r1(X389,X390)
| ~ r1(X388,X389)
| ~ r1(esk1_0,X388) )
& ( r1(X396,esk26_4(X393,X394,X395,X396))
| p1(X396)
| ~ r1(X395,X396)
| ~ r1(X394,X395)
| ~ r1(X393,X394)
| ~ r1(esk1_0,X393) )
& ( ~ p1(esk26_4(X393,X394,X395,X396))
| p1(X396)
| ~ r1(X395,X396)
| ~ r1(X394,X395)
| ~ r1(X393,X394)
| ~ r1(esk1_0,X393) )
& ( r1(X399,esk27_2(X398,X399))
| p6(X399)
| ~ r1(X398,X399)
| ~ r1(esk1_0,X398) )
& ( ~ p6(esk27_2(X398,X399))
| p6(X399)
| ~ r1(X398,X399)
| ~ r1(esk1_0,X398) )
& ( r1(X402,esk28_2(X401,X402))
| p4(X402)
| ~ r1(X401,X402)
| ~ r1(esk1_0,X401) )
& ( ~ p6(esk28_2(X401,X402))
| p4(X402)
| ~ r1(X401,X402)
| ~ r1(esk1_0,X401) )
& ( r1(X405,esk29_2(X404,X405))
| p2(X405)
| ~ r1(X404,X405)
| ~ r1(esk1_0,X404) )
& ( ~ p6(esk29_2(X404,X405))
| p2(X405)
| ~ r1(X404,X405)
| ~ r1(esk1_0,X404) )
& ( r1(X409,esk30_3(X407,X408,X409))
| p5(X409)
| ~ r1(X408,X409)
| ~ r1(X407,X408)
| ~ r1(esk1_0,X407) )
& ( ~ p5(esk30_3(X407,X408,X409))
| p5(X409)
| ~ r1(X408,X409)
| ~ r1(X407,X408)
| ~ r1(esk1_0,X407) )
& ( r1(X413,esk31_3(X411,X412,X413))
| p5(X413)
| ~ r1(X412,X413)
| ~ r1(X411,X412)
| ~ r1(esk1_0,X411) )
& ( ~ p3(esk31_3(X411,X412,X413))
| p5(X413)
| ~ r1(X412,X413)
| ~ r1(X411,X412)
| ~ r1(esk1_0,X411) )
& ( r1(X416,esk32_2(X415,X416))
| p6(X416)
| ~ r1(X415,X416)
| ~ r1(esk1_0,X415) )
& ( ~ p4(esk32_2(X415,X416))
| p6(X416)
| ~ r1(X415,X416)
| ~ r1(esk1_0,X415) )
& ( r1(X419,esk33_2(X418,X419))
| p4(X419)
| ~ r1(X418,X419)
| ~ r1(esk1_0,X418) )
& ( ~ p4(esk33_2(X418,X419))
| p4(X419)
| ~ r1(X418,X419)
| ~ r1(esk1_0,X418) )
& ( r1(X422,esk34_2(X421,X422))
| p2(X422)
| ~ r1(X421,X422)
| ~ r1(esk1_0,X421) )
& ( ~ p4(esk34_2(X421,X422))
| p2(X422)
| ~ r1(X421,X422)
| ~ r1(esk1_0,X421) )
& ( r1(X426,esk35_3(X424,X425,X426))
| p4(X426)
| ~ r1(X425,X426)
| ~ r1(X424,X425)
| ~ r1(esk1_0,X424) )
& ( ~ p1(esk35_3(X424,X425,X426))
| p4(X426)
| ~ r1(X425,X426)
| ~ r1(X424,X425)
| ~ r1(esk1_0,X424) )
& ( r1(X430,esk36_3(X428,X429,X430))
| p3(X430)
| ~ r1(X429,X430)
| ~ r1(X428,X429)
| ~ r1(esk1_0,X428) )
& ( ~ p5(esk36_3(X428,X429,X430))
| p3(X430)
| ~ r1(X429,X430)
| ~ r1(X428,X429)
| ~ r1(esk1_0,X428) )
& ( r1(X434,esk37_3(X432,X433,X434))
| p3(X434)
| ~ r1(X433,X434)
| ~ r1(X432,X433)
| ~ r1(esk1_0,X432) )
& ( ~ p3(esk37_3(X432,X433,X434))
| p3(X434)
| ~ r1(X433,X434)
| ~ r1(X432,X433)
| ~ r1(esk1_0,X432) )
& ( r1(X437,esk38_2(X436,X437))
| p6(X437)
| ~ r1(X436,X437)
| ~ r1(esk1_0,X436) )
& ( ~ p2(esk38_2(X436,X437))
| p6(X437)
| ~ r1(X436,X437)
| ~ r1(esk1_0,X436) )
& ( r1(X440,esk39_2(X439,X440))
| p4(X440)
| ~ r1(X439,X440)
| ~ r1(esk1_0,X439) )
& ( ~ p2(esk39_2(X439,X440))
| p4(X440)
| ~ r1(X439,X440)
| ~ r1(esk1_0,X439) )
& ( r1(X443,esk40_2(X442,X443))
| p2(X443)
| ~ r1(X442,X443)
| ~ r1(esk1_0,X442) )
& ( ~ p2(esk40_2(X442,X443))
| p2(X443)
| ~ r1(X442,X443)
| ~ r1(esk1_0,X442) )
& ( r1(X447,esk41_3(X445,X446,X447))
| p1(X447)
| ~ r1(X446,X447)
| ~ r1(X445,X446)
| ~ r1(esk1_0,X445) )
& ( ~ p5(esk41_3(X445,X446,X447))
| p1(X447)
| ~ r1(X446,X447)
| ~ r1(X445,X446)
| ~ r1(esk1_0,X445) )
& ( r1(X451,esk42_3(X449,X450,X451))
| p1(X451)
| ~ r1(X450,X451)
| ~ r1(X449,X450)
| ~ r1(esk1_0,X449) )
& ( ~ p3(esk42_3(X449,X450,X451))
| p1(X451)
| ~ r1(X450,X451)
| ~ r1(X449,X450)
| ~ r1(esk1_0,X449) )
& ( r1(X453,esk43_1(X453))
| p6(X453)
| ~ r1(esk1_0,X453) )
& ( ~ p6(esk43_1(X453))
| p6(X453)
| ~ r1(esk1_0,X453) )
& ( r1(X455,esk44_1(X455))
| p4(X455)
| ~ r1(esk1_0,X455) )
& ( ~ p6(esk44_1(X455))
| p4(X455)
| ~ r1(esk1_0,X455) )
& ( r1(X458,esk45_2(X457,X458))
| p5(X458)
| ~ r1(X457,X458)
| ~ r1(esk1_0,X457) )
& ( ~ p5(esk45_2(X457,X458))
| p5(X458)
| ~ r1(X457,X458)
| ~ r1(esk1_0,X457) )
& ( r1(X461,esk46_2(X460,X461))
| p5(X461)
| ~ r1(X460,X461)
| ~ r1(esk1_0,X460) )
& ( ~ p3(esk46_2(X460,X461))
| p5(X461)
| ~ r1(X460,X461)
| ~ r1(esk1_0,X460) )
& ( r1(X464,esk47_2(X463,X464))
| p5(X464)
| ~ r1(X463,X464)
| ~ r1(esk1_0,X463) )
& ( ~ p1(esk47_2(X463,X464))
| p5(X464)
| ~ r1(X463,X464)
| ~ r1(esk1_0,X463) )
& ( r1(X466,esk48_1(X466))
| p6(X466)
| ~ r1(esk1_0,X466) )
& ( ~ p4(esk48_1(X466))
| p6(X466)
| ~ r1(esk1_0,X466) )
& ( r1(X468,esk49_1(X468))
| p4(X468)
| ~ r1(esk1_0,X468) )
& ( ~ p4(esk49_1(X468))
| p4(X468)
| ~ r1(esk1_0,X468) )
& ( r1(X471,esk50_2(X470,X471))
| p3(X471)
| ~ r1(X470,X471)
| ~ r1(esk1_0,X470) )
& ( ~ p5(esk50_2(X470,X471))
| p3(X471)
| ~ r1(X470,X471)
| ~ r1(esk1_0,X470) )
& ( r1(X474,esk51_2(X473,X474))
| p3(X474)
| ~ r1(X473,X474)
| ~ r1(esk1_0,X473) )
& ( ~ p3(esk51_2(X473,X474))
| p3(X474)
| ~ r1(X473,X474)
| ~ r1(esk1_0,X473) )
& ( r1(X477,esk52_2(X476,X477))
| p3(X477)
| ~ r1(X476,X477)
| ~ r1(esk1_0,X476) )
& ( ~ p1(esk52_2(X476,X477))
| p3(X477)
| ~ r1(X476,X477)
| ~ r1(esk1_0,X476) )
& ( r1(X479,esk53_1(X479))
| p6(X479)
| ~ r1(esk1_0,X479) )
& ( ~ p2(esk53_1(X479))
| p6(X479)
| ~ r1(esk1_0,X479) )
& ( r1(X481,esk54_1(X481))
| p4(X481)
| ~ r1(esk1_0,X481) )
& ( ~ p2(esk54_1(X481))
| p4(X481)
| ~ r1(esk1_0,X481) )
& ( r1(X484,esk55_2(X483,X484))
| p1(X484)
| ~ r1(X483,X484)
| ~ r1(esk1_0,X483) )
& ( ~ p5(esk55_2(X483,X484))
| p1(X484)
| ~ r1(X483,X484)
| ~ r1(esk1_0,X483) )
& ( r1(X487,esk56_2(X486,X487))
| p1(X487)
| ~ r1(X486,X487)
| ~ r1(esk1_0,X486) )
& ( ~ p4(esk56_2(X486,X487))
| p1(X487)
| ~ r1(X486,X487)
| ~ r1(esk1_0,X486) )
& ( r1(X490,esk57_2(X489,X490))
| p1(X490)
| ~ r1(X489,X490)
| ~ r1(esk1_0,X489) )
& ( ~ p3(esk57_2(X489,X490))
| p1(X490)
| ~ r1(X489,X490)
| ~ r1(esk1_0,X489) )
& ( r1(X493,esk58_2(X492,X493))
| p1(X493)
| ~ r1(X492,X493)
| ~ r1(esk1_0,X492) )
& ( ~ p1(esk58_2(X492,X493))
| p1(X493)
| ~ r1(X492,X493)
| ~ r1(esk1_0,X492) )
& ( r1(X495,esk59_1(X495))
| p5(X495)
| ~ r1(esk1_0,X495) )
& ( ~ p5(esk59_1(X495))
| p5(X495)
| ~ r1(esk1_0,X495) )
& ( r1(X497,esk60_1(X497))
| p5(X497)
| ~ r1(esk1_0,X497) )
& ( ~ p3(esk60_1(X497))
| p5(X497)
| ~ r1(esk1_0,X497) )
& ( r1(X499,esk61_1(X499))
| p3(X499)
| ~ r1(esk1_0,X499) )
& ( ~ p5(esk61_1(X499))
| p3(X499)
| ~ r1(esk1_0,X499) )
& ( r1(X501,esk62_1(X501))
| p3(X501)
| ~ r1(esk1_0,X501) )
& ( ~ p3(esk62_1(X501))
| p3(X501)
| ~ r1(esk1_0,X501) )
& ( r1(X503,esk63_1(X503))
| p2(X503)
| ~ r1(esk1_0,X503) )
& ( ~ p1(esk63_1(X503))
| p2(X503)
| ~ r1(esk1_0,X503) )
& ( r1(X505,esk64_1(X505))
| p1(X505)
| ~ r1(esk1_0,X505) )
& ( ~ p5(esk64_1(X505))
| p1(X505)
| ~ r1(esk1_0,X505) )
& ( r1(X507,esk65_1(X507))
| p1(X507)
| ~ r1(esk1_0,X507) )
& ( ~ p3(esk65_1(X507))
| p1(X507)
| ~ r1(esk1_0,X507) )
& r1(esk1_0,esk66_0)
& ~ p5(esk66_0)
& r1(esk1_0,esk67_0)
& ~ p3(esk67_0)
& r1(esk1_0,esk68_0)
& ~ p2(esk68_0)
& r1(esk1_0,esk69_0)
& ~ p1(esk69_0) ),
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_1])])])])]) ).
cnf(c_0_3,negated_conjecture,
( r1(X1,esk56_2(X2,X1))
| p1(X1)
| ~ r1(X2,X1)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_4,negated_conjecture,
r1(esk1_0,esk68_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_5,negated_conjecture,
( r1(X1,esk63_1(X1))
| p2(X1)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_6,negated_conjecture,
~ p2(esk68_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_7,negated_conjecture,
( r1(X1,esk35_3(X2,X3,X1))
| p4(X1)
| ~ r1(X3,X1)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_8,negated_conjecture,
( p1(X1)
| r1(X1,esk56_2(esk68_0,X1))
| ~ r1(esk68_0,X1) ),
inference(spm,[status(thm)],[c_0_3,c_0_4]) ).
cnf(c_0_9,negated_conjecture,
r1(esk68_0,esk63_1(esk68_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_5,c_0_4]),c_0_6]) ).
cnf(c_0_10,negated_conjecture,
( p1(X2)
| ~ p4(esk56_2(X1,X2))
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_11,negated_conjecture,
( p4(X1)
| r1(X1,esk35_3(esk68_0,X2,X1))
| ~ r1(esk68_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_7,c_0_4]) ).
cnf(c_0_12,negated_conjecture,
( p2(X1)
| ~ p1(esk63_1(X1))
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_13,negated_conjecture,
( p1(esk63_1(esk68_0))
| r1(esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))) ),
inference(spm,[status(thm)],[c_0_8,c_0_9]) ).
cnf(c_0_14,negated_conjecture,
( r1(X1,esk24_4(X2,X3,X4,X1))
| p1(X1)
| ~ r1(X4,X1)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_15,negated_conjecture,
( p1(X1)
| ~ p4(esk56_2(esk68_0,X1))
| ~ r1(esk68_0,X1) ),
inference(spm,[status(thm)],[c_0_10,c_0_4]) ).
cnf(c_0_16,negated_conjecture,
( p4(X1)
| r1(X1,esk35_3(esk68_0,esk63_1(esk68_0),X1))
| ~ r1(esk63_1(esk68_0),X1) ),
inference(spm,[status(thm)],[c_0_11,c_0_9]) ).
cnf(c_0_17,negated_conjecture,
r1(esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_13]),c_0_4])]),c_0_6]) ).
cnf(c_0_18,negated_conjecture,
( p4(X3)
| ~ p1(esk35_3(X1,X2,X3))
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_19,negated_conjecture,
( p1(X1)
| r1(X1,esk24_4(esk68_0,X2,X3,X1))
| ~ r1(esk68_0,X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_14,c_0_4]) ).
cnf(c_0_20,negated_conjecture,
( p1(esk63_1(esk68_0))
| ~ p4(esk56_2(esk68_0,esk63_1(esk68_0))) ),
inference(spm,[status(thm)],[c_0_15,c_0_9]) ).
cnf(c_0_21,negated_conjecture,
( p4(esk56_2(esk68_0,esk63_1(esk68_0)))
| r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))) ),
inference(spm,[status(thm)],[c_0_16,c_0_17]) ).
cnf(c_0_22,negated_conjecture,
( p4(X1)
| ~ p1(esk35_3(esk68_0,X2,X1))
| ~ r1(esk68_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_18,c_0_4]) ).
cnf(c_0_23,negated_conjecture,
( p1(X1)
| r1(X1,esk24_4(esk68_0,esk63_1(esk68_0),X2,X1))
| ~ r1(esk63_1(esk68_0),X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_19,c_0_9]) ).
cnf(c_0_24,negated_conjecture,
( p1(esk63_1(esk68_0))
| r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_25,negated_conjecture,
( p4(X5)
| ~ r1(esk1_0,X1)
| ~ r1(X1,X2)
| ~ r1(X2,X3)
| ~ r1(X3,X4)
| ~ r1(X4,X5) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_26,negated_conjecture,
( p4(X1)
| ~ p1(esk35_3(esk68_0,esk63_1(esk68_0),X1))
| ~ r1(esk63_1(esk68_0),X1) ),
inference(spm,[status(thm)],[c_0_22,c_0_9]) ).
cnf(c_0_27,negated_conjecture,
( p1(X1)
| r1(X1,esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),X1))
| ~ r1(esk56_2(esk68_0,esk63_1(esk68_0)),X1) ),
inference(spm,[status(thm)],[c_0_23,c_0_17]) ).
cnf(c_0_28,negated_conjecture,
r1(esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_24]),c_0_4])]),c_0_6]) ).
cnf(c_0_29,negated_conjecture,
( p1(X4)
| ~ p4(esk24_4(X1,X2,X3,X4))
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_30,negated_conjecture,
( p4(X1)
| ~ r1(esk68_0,X2)
| ~ r1(X3,X1)
| ~ r1(X4,X3)
| ~ r1(X2,X4) ),
inference(spm,[status(thm)],[c_0_25,c_0_4]) ).
cnf(c_0_31,negated_conjecture,
( p4(esk56_2(esk68_0,esk63_1(esk68_0)))
| ~ p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))) ),
inference(spm,[status(thm)],[c_0_26,c_0_17]) ).
cnf(c_0_32,negated_conjecture,
( p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))
| r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_33,negated_conjecture,
( p1(X1)
| ~ p4(esk24_4(esk68_0,X2,X3,X1))
| ~ r1(esk68_0,X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_29,c_0_4]) ).
cnf(c_0_34,negated_conjecture,
( p4(X1)
| ~ r1(esk63_1(esk68_0),X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_30,c_0_9]) ).
cnf(c_0_35,negated_conjecture,
( p4(esk56_2(esk68_0,esk63_1(esk68_0)))
| r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))) ),
inference(spm,[status(thm)],[c_0_31,c_0_32]) ).
cnf(c_0_36,negated_conjecture,
( p1(X1)
| ~ p4(esk24_4(esk68_0,esk63_1(esk68_0),X2,X1))
| ~ r1(esk63_1(esk68_0),X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_33,c_0_9]) ).
cnf(c_0_37,negated_conjecture,
( p4(X1)
| ~ r1(esk56_2(esk68_0,esk63_1(esk68_0)),X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_34,c_0_17]) ).
cnf(c_0_38,negated_conjecture,
( p1(esk63_1(esk68_0))
| r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))) ),
inference(spm,[status(thm)],[c_0_20,c_0_35]) ).
cnf(c_0_39,negated_conjecture,
( p1(X1)
| ~ p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),X1))
| ~ r1(esk56_2(esk68_0,esk63_1(esk68_0)),X1) ),
inference(spm,[status(thm)],[c_0_36,c_0_17]) ).
cnf(c_0_40,negated_conjecture,
( p4(X1)
| ~ r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),X1) ),
inference(spm,[status(thm)],[c_0_37,c_0_28]) ).
cnf(c_0_41,negated_conjecture,
r1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))),esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_38]),c_0_4])]),c_0_6]) ).
cnf(c_0_42,negated_conjecture,
( p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))
| ~ p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))) ),
inference(spm,[status(thm)],[c_0_39,c_0_28]) ).
cnf(c_0_43,negated_conjecture,
p4(esk24_4(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)),esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_44,negated_conjecture,
p1(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0)))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42,c_0_43])]) ).
cnf(c_0_45,negated_conjecture,
p4(esk56_2(esk68_0,esk63_1(esk68_0))),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31,c_0_44])]) ).
cnf(c_0_46,negated_conjecture,
p1(esk63_1(esk68_0)),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20,c_0_45])]) ).
cnf(c_0_47,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_12,c_0_46]),c_0_4])]),c_0_6]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : LCL646+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.14/0.33 % Computer : n009.cluster.edu
% 0.14/0.33 % Model : x86_64 x86_64
% 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.33 % Memory : 8042.1875MB
% 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.33 % CPULimit : 300
% 0.14/0.33 % WCLimit : 300
% 0.14/0.33 % DateTime : Mon May 4 22:46:26 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 2.07/1.85 % Version : CSE_E---1.7
% 2.07/1.85 % Problem : theBenchmark.p
% 2.07/1.85 % SZS status Theorem for theBenchmark.p
% 2.07/1.85 % SZS output start CNFRefutation
% See solution above
% 2.07/1.86 % Total time : 1.374s
%------------------------------------------------------------------------------