%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL638+1.005 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n023.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:40:40 PM UTC 2026
% Result : Theorem 12.28s 7.43s
% Output : CNFRefutation 12.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 1
% Syntax : Number of formulae : 62 ( 13 unt; 0 def)
% Number of atoms : 1091 ( 0 equ)
% Maximal formula atoms : 400 ( 17 avg)
% Number of connectives : 2076 (1047 ~; 900 |; 129 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 207 ( 10 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-2 aty)
% Number of functors : 56 ( 56 usr; 26 con; 0-7 aty)
% Number of variables : 604 ( 0 sgn 455 !; 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)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ~ p1(X2) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
& p1(X2) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [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)
| ~ ( ~ ! [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)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ $true ) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,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)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
& p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [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) ) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,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) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ $true ) ) ) ) )
| ! [X2] :
( ~ r1(X1,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)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(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) ) )
& p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [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) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ $true ) ) ) )
| ! [X2] :
( ~ r1(X1,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) ) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
& p1(X1) ) ) )
| ~ ! [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) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [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)
| ~ $true ) ) )
| ! [X2] :
( ~ r1(X1,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)
| p1(X2) ) )
& ~ p1(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
& p1(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)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ $true ) )
| ! [X2] :
( ~ r1(X1,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) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/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)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(X2) ) )
& ~ p1(X2) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
& p1(X2) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [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)
| ~ ( ~ ! [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)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] : ~ r1(X2,X1) ) ) ) ) )
| ! [X2] :
( ~ r1(X1,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)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) )
& ~ p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
& p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [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) ) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,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) ) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] : ~ r1(X1,X2) ) ) ) )
| ! [X2] :
( ~ r1(X1,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)
| ~ ! [X2] :
( ~ r1(X1,X2)
| p1(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) ) )
& p1(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [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) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] : ~ r1(X2,X1) ) ) )
| ! [X2] :
( ~ r1(X1,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) ) )
& ~ p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
& p1(X1) ) ) )
| ~ ! [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) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [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) ) )
| ! [X2] :
( ~ r1(X1,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)
| p1(X2) ) )
& ~ p1(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ p1(X2) ) )
& p1(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)
| p1(X2) ) )
& ! [X1] :
( ~ r1(X2,X1)
| p1(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] : ~ r1(X2,X1) )
| ! [X2] :
( ~ r1(X1,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) ) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]) ).
fof(c_0_2,negated_conjecture,
! [X175,X176,X177,X178,X179,X180,X182,X183,X184,X185,X186,X187,X189,X190,X191,X192,X193,X194,X195,X198,X199,X200,X201,X202,X203,X204,X205,X207,X208,X209,X210,X211,X218,X219,X220,X221,X222,X223,X225,X226,X227,X228,X229,X231,X232,X233,X234,X235,X236,X239,X240,X241,X242,X243,X244,X245,X247,X248,X249,X250,X257,X258,X259,X260,X261,X263,X264,X265,X266,X268,X269,X270,X271,X272,X275,X276,X277,X278,X279,X280,X282,X283,X284,X291,X292,X293,X294,X296,X297,X298,X300,X301,X302,X303,X306,X307,X308,X309,X310,X312,X313,X320,X321,X322,X324,X325,X327,X328,X329,X332,X333,X334,X335,X337,X344] :
( ( r1(X180,esk2_6(X175,X176,X177,X178,X179,X180))
| ~ r1(X179,X180)
| p1(X179)
| ~ r1(X178,X179)
| ~ r1(X177,X178)
| ~ r1(X176,X177)
| ~ r1(X175,X176)
| ~ r1(esk1_0,X175) )
& ( ~ p1(esk2_6(X175,X176,X177,X178,X179,X180))
| ~ r1(X179,X180)
| p1(X179)
| ~ r1(X178,X179)
| ~ r1(X177,X178)
| ~ r1(X176,X177)
| ~ r1(X175,X176)
| ~ r1(esk1_0,X175) )
& ( r1(X187,esk3_6(X182,X183,X184,X185,X186,X187))
| ~ r1(X186,X187)
| ~ p1(X186)
| ~ r1(X185,X186)
| ~ r1(X184,X185)
| ~ r1(X183,X184)
| ~ r1(X182,X183)
| ~ r1(esk1_0,X182) )
& ( p1(esk3_6(X182,X183,X184,X185,X186,X187))
| ~ r1(X186,X187)
| ~ p1(X186)
| ~ r1(X185,X186)
| ~ r1(X184,X185)
| ~ r1(X183,X184)
| ~ r1(X182,X183)
| ~ r1(esk1_0,X182) )
& ( r1(X193,esk5_5(X189,X190,X191,X192,X193))
| r1(X195,esk4_7(X189,X190,X191,X192,X193,X194,X195))
| ~ r1(X194,X195)
| ~ r1(X193,X194)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(X190,X191)
| ~ r1(X189,X190)
| ~ r1(esk1_0,X189) )
& ( ~ r1(esk5_5(X189,X190,X191,X192,X193),X198)
| ~ p1(X198)
| r1(X195,esk4_7(X189,X190,X191,X192,X193,X194,X195))
| ~ r1(X194,X195)
| ~ r1(X193,X194)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(X190,X191)
| ~ r1(X189,X190)
| ~ r1(esk1_0,X189) )
& ( r1(X193,esk5_5(X189,X190,X191,X192,X193))
| p1(esk4_7(X189,X190,X191,X192,X193,X194,X195))
| ~ r1(X194,X195)
| ~ r1(X193,X194)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(X190,X191)
| ~ r1(X189,X190)
| ~ r1(esk1_0,X189) )
& ( ~ r1(esk5_5(X189,X190,X191,X192,X193),X198)
| ~ p1(X198)
| p1(esk4_7(X189,X190,X191,X192,X193,X194,X195))
| ~ r1(X194,X195)
| ~ r1(X193,X194)
| ~ r1(X192,X193)
| ~ r1(X191,X192)
| ~ r1(X190,X191)
| ~ r1(X189,X190)
| ~ r1(esk1_0,X189) )
& ( r1(X203,esk6_5(X199,X200,X201,X202,X203))
| ~ r1(X203,X204)
| ~ r1(X204,X205)
| p1(X205)
| ~ r1(X202,X203)
| ~ r1(X201,X202)
| ~ r1(X200,X201)
| ~ r1(X199,X200)
| ~ r1(esk1_0,X199) )
& ( ~ p1(esk6_5(X199,X200,X201,X202,X203))
| ~ r1(X203,X204)
| ~ r1(X204,X205)
| p1(X205)
| ~ r1(X202,X203)
| ~ r1(X201,X202)
| ~ r1(X200,X201)
| ~ r1(X199,X200)
| ~ r1(esk1_0,X199) )
& ( ~ r1(esk1_0,X207)
| ~ r1(X207,X208)
| ~ r1(X208,X209)
| ~ r1(X209,X210)
| ~ r1(X210,X211)
| r1(X211,esk7_5(X207,X208,X209,X210,X211)) )
& r1(esk1_0,esk8_0)
& r1(esk8_0,esk9_0)
& r1(esk9_0,esk10_0)
& r1(esk10_0,esk11_0)
& r1(esk11_0,esk12_0)
& ~ p1(esk12_0)
& ( ~ r1(esk12_0,X218)
| p1(X218) )
& ( r1(X223,esk13_5(X219,X220,X221,X222,X223))
| ~ r1(X222,X223)
| p1(X222)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ r1(X219,X220)
| ~ r1(esk1_0,X219) )
& ( ~ p1(esk13_5(X219,X220,X221,X222,X223))
| ~ r1(X222,X223)
| p1(X222)
| ~ r1(X221,X222)
| ~ r1(X220,X221)
| ~ r1(X219,X220)
| ~ r1(esk1_0,X219) )
& ( r1(X229,esk14_5(X225,X226,X227,X228,X229))
| ~ r1(X228,X229)
| ~ p1(X228)
| ~ r1(X227,X228)
| ~ r1(X226,X227)
| ~ r1(X225,X226)
| ~ r1(esk1_0,X225) )
& ( p1(esk14_5(X225,X226,X227,X228,X229))
| ~ r1(X228,X229)
| ~ p1(X228)
| ~ r1(X227,X228)
| ~ r1(X226,X227)
| ~ r1(X225,X226)
| ~ r1(esk1_0,X225) )
& ( r1(X234,esk16_4(X231,X232,X233,X234))
| r1(X236,esk15_6(X231,X232,X233,X234,X235,X236))
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X233,X234)
| ~ r1(X232,X233)
| ~ r1(X231,X232)
| ~ r1(esk1_0,X231) )
& ( ~ r1(esk16_4(X231,X232,X233,X234),X239)
| ~ p1(X239)
| r1(X236,esk15_6(X231,X232,X233,X234,X235,X236))
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X233,X234)
| ~ r1(X232,X233)
| ~ r1(X231,X232)
| ~ r1(esk1_0,X231) )
& ( r1(X234,esk16_4(X231,X232,X233,X234))
| p1(esk15_6(X231,X232,X233,X234,X235,X236))
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X233,X234)
| ~ r1(X232,X233)
| ~ r1(X231,X232)
| ~ r1(esk1_0,X231) )
& ( ~ r1(esk16_4(X231,X232,X233,X234),X239)
| ~ p1(X239)
| p1(esk15_6(X231,X232,X233,X234,X235,X236))
| ~ r1(X235,X236)
| ~ r1(X234,X235)
| ~ r1(X233,X234)
| ~ r1(X232,X233)
| ~ r1(X231,X232)
| ~ r1(esk1_0,X231) )
& ( r1(X243,esk17_4(X240,X241,X242,X243))
| ~ r1(X243,X244)
| ~ r1(X244,X245)
| p1(X245)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X240,X241)
| ~ r1(esk1_0,X240) )
& ( ~ p1(esk17_4(X240,X241,X242,X243))
| ~ r1(X243,X244)
| ~ r1(X244,X245)
| p1(X245)
| ~ r1(X242,X243)
| ~ r1(X241,X242)
| ~ r1(X240,X241)
| ~ r1(esk1_0,X240) )
& ( ~ r1(esk1_0,X247)
| ~ r1(X247,X248)
| ~ r1(X248,X249)
| ~ r1(X249,X250)
| r1(X250,esk18_4(X247,X248,X249,X250)) )
& r1(esk1_0,esk19_0)
& r1(esk19_0,esk20_0)
& r1(esk20_0,esk21_0)
& r1(esk21_0,esk22_0)
& r1(esk22_0,esk23_0)
& ~ p1(esk23_0)
& ( ~ r1(esk23_0,X257)
| p1(X257) )
& ( r1(X261,esk24_4(X258,X259,X260,X261))
| ~ r1(X260,X261)
| p1(X260)
| ~ r1(X259,X260)
| ~ r1(X258,X259)
| ~ r1(esk1_0,X258) )
& ( ~ p1(esk24_4(X258,X259,X260,X261))
| ~ r1(X260,X261)
| p1(X260)
| ~ r1(X259,X260)
| ~ r1(X258,X259)
| ~ r1(esk1_0,X258) )
& ( r1(X266,esk25_4(X263,X264,X265,X266))
| ~ r1(X265,X266)
| ~ p1(X265)
| ~ r1(X264,X265)
| ~ r1(X263,X264)
| ~ r1(esk1_0,X263) )
& ( p1(esk25_4(X263,X264,X265,X266))
| ~ r1(X265,X266)
| ~ p1(X265)
| ~ r1(X264,X265)
| ~ r1(X263,X264)
| ~ r1(esk1_0,X263) )
& ( r1(X270,esk27_3(X268,X269,X270))
| r1(X272,esk26_5(X268,X269,X270,X271,X272))
| ~ r1(X271,X272)
| ~ r1(X270,X271)
| ~ r1(X269,X270)
| ~ r1(X268,X269)
| ~ r1(esk1_0,X268) )
& ( ~ r1(esk27_3(X268,X269,X270),X275)
| ~ p1(X275)
| r1(X272,esk26_5(X268,X269,X270,X271,X272))
| ~ r1(X271,X272)
| ~ r1(X270,X271)
| ~ r1(X269,X270)
| ~ r1(X268,X269)
| ~ r1(esk1_0,X268) )
& ( r1(X270,esk27_3(X268,X269,X270))
| p1(esk26_5(X268,X269,X270,X271,X272))
| ~ r1(X271,X272)
| ~ r1(X270,X271)
| ~ r1(X269,X270)
| ~ r1(X268,X269)
| ~ r1(esk1_0,X268) )
& ( ~ r1(esk27_3(X268,X269,X270),X275)
| ~ p1(X275)
| p1(esk26_5(X268,X269,X270,X271,X272))
| ~ r1(X271,X272)
| ~ r1(X270,X271)
| ~ r1(X269,X270)
| ~ r1(X268,X269)
| ~ r1(esk1_0,X268) )
& ( r1(X278,esk28_3(X276,X277,X278))
| ~ r1(X278,X279)
| ~ r1(X279,X280)
| p1(X280)
| ~ r1(X277,X278)
| ~ r1(X276,X277)
| ~ r1(esk1_0,X276) )
& ( ~ p1(esk28_3(X276,X277,X278))
| ~ r1(X278,X279)
| ~ r1(X279,X280)
| p1(X280)
| ~ r1(X277,X278)
| ~ r1(X276,X277)
| ~ r1(esk1_0,X276) )
& ( ~ r1(esk1_0,X282)
| ~ r1(X282,X283)
| ~ r1(X283,X284)
| r1(X284,esk29_3(X282,X283,X284)) )
& r1(esk1_0,esk30_0)
& r1(esk30_0,esk31_0)
& r1(esk31_0,esk32_0)
& r1(esk32_0,esk33_0)
& r1(esk33_0,esk34_0)
& ~ p1(esk34_0)
& ( ~ r1(esk34_0,X291)
| p1(X291) )
& ( r1(X294,esk35_3(X292,X293,X294))
| ~ r1(X293,X294)
| p1(X293)
| ~ r1(X292,X293)
| ~ r1(esk1_0,X292) )
& ( ~ p1(esk35_3(X292,X293,X294))
| ~ r1(X293,X294)
| p1(X293)
| ~ r1(X292,X293)
| ~ r1(esk1_0,X292) )
& ( r1(X298,esk36_3(X296,X297,X298))
| ~ r1(X297,X298)
| ~ p1(X297)
| ~ r1(X296,X297)
| ~ r1(esk1_0,X296) )
& ( p1(esk36_3(X296,X297,X298))
| ~ r1(X297,X298)
| ~ p1(X297)
| ~ r1(X296,X297)
| ~ r1(esk1_0,X296) )
& ( r1(X301,esk38_2(X300,X301))
| r1(X303,esk37_4(X300,X301,X302,X303))
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(esk1_0,X300) )
& ( ~ r1(esk38_2(X300,X301),X306)
| ~ p1(X306)
| r1(X303,esk37_4(X300,X301,X302,X303))
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(esk1_0,X300) )
& ( r1(X301,esk38_2(X300,X301))
| p1(esk37_4(X300,X301,X302,X303))
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(esk1_0,X300) )
& ( ~ r1(esk38_2(X300,X301),X306)
| ~ p1(X306)
| p1(esk37_4(X300,X301,X302,X303))
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(X300,X301)
| ~ r1(esk1_0,X300) )
& ( r1(X308,esk39_2(X307,X308))
| ~ r1(X308,X309)
| ~ r1(X309,X310)
| p1(X310)
| ~ r1(X307,X308)
| ~ r1(esk1_0,X307) )
& ( ~ p1(esk39_2(X307,X308))
| ~ r1(X308,X309)
| ~ r1(X309,X310)
| p1(X310)
| ~ r1(X307,X308)
| ~ r1(esk1_0,X307) )
& ( ~ r1(esk1_0,X312)
| ~ r1(X312,X313)
| r1(X313,esk40_2(X312,X313)) )
& r1(esk1_0,esk41_0)
& r1(esk41_0,esk42_0)
& r1(esk42_0,esk43_0)
& r1(esk43_0,esk44_0)
& r1(esk44_0,esk45_0)
& ~ p1(esk45_0)
& ( ~ r1(esk45_0,X320)
| p1(X320) )
& ( r1(X322,esk46_2(X321,X322))
| ~ r1(X321,X322)
| p1(X321)
| ~ r1(esk1_0,X321) )
& ( ~ p1(esk46_2(X321,X322))
| ~ r1(X321,X322)
| p1(X321)
| ~ r1(esk1_0,X321) )
& ( r1(X325,esk47_2(X324,X325))
| ~ r1(X324,X325)
| ~ p1(X324)
| ~ r1(esk1_0,X324) )
& ( p1(esk47_2(X324,X325))
| ~ r1(X324,X325)
| ~ p1(X324)
| ~ r1(esk1_0,X324) )
& ( r1(X327,esk49_1(X327))
| r1(X329,esk48_3(X327,X328,X329))
| ~ r1(X328,X329)
| ~ r1(X327,X328)
| ~ r1(esk1_0,X327) )
& ( ~ r1(esk49_1(X327),X332)
| ~ p1(X332)
| r1(X329,esk48_3(X327,X328,X329))
| ~ r1(X328,X329)
| ~ r1(X327,X328)
| ~ r1(esk1_0,X327) )
& ( r1(X327,esk49_1(X327))
| p1(esk48_3(X327,X328,X329))
| ~ r1(X328,X329)
| ~ r1(X327,X328)
| ~ r1(esk1_0,X327) )
& ( ~ r1(esk49_1(X327),X332)
| ~ p1(X332)
| p1(esk48_3(X327,X328,X329))
| ~ r1(X328,X329)
| ~ r1(X327,X328)
| ~ r1(esk1_0,X327) )
& ( r1(X333,esk50_1(X333))
| ~ r1(X333,X334)
| ~ r1(X334,X335)
| p1(X335)
| ~ r1(esk1_0,X333) )
& ( ~ p1(esk50_1(X333))
| ~ r1(X333,X334)
| ~ r1(X334,X335)
| p1(X335)
| ~ r1(esk1_0,X333) )
& ( ~ r1(esk1_0,X337)
| r1(X337,esk51_1(X337)) )
& r1(esk1_0,esk52_0)
& r1(esk52_0,esk53_0)
& r1(esk53_0,esk54_0)
& r1(esk54_0,esk55_0)
& r1(esk55_0,esk56_0)
& ~ p1(esk56_0)
& ( ~ r1(esk56_0,X344)
| p1(X344) ) ),
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,esk13_5(X2,X3,X4,X5,X1))
| p1(X5)
| ~ r1(X5,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_4,negated_conjecture,
r1(esk1_0,esk52_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_5,negated_conjecture,
( p1(X4)
| ~ p1(esk13_5(X1,X2,X3,X4,X5))
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_6,negated_conjecture,
( p1(X1)
| r1(X2,esk13_5(esk52_0,X3,X4,X1,X2))
| ~ r1(esk52_0,X3)
| ~ r1(X1,X2)
| ~ r1(X4,X1)
| ~ r1(X3,X4) ),
inference(spm,[status(thm)],[c_0_3,c_0_4]) ).
cnf(c_0_7,negated_conjecture,
r1(esk52_0,esk53_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_8,negated_conjecture,
( p1(X1)
| ~ p1(esk13_5(esk52_0,X2,X3,X1,X4))
| ~ r1(esk52_0,X2)
| ~ r1(X1,X4)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_5,c_0_4]) ).
cnf(c_0_9,negated_conjecture,
( r1(X1,esk14_5(X2,X3,X4,X5,X1))
| ~ r1(X5,X1)
| ~ p1(X5)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_10,negated_conjecture,
( p1(X1)
| r1(X2,esk13_5(esk52_0,esk53_0,X3,X1,X2))
| ~ r1(esk53_0,X3)
| ~ r1(X1,X2)
| ~ r1(X3,X1) ),
inference(spm,[status(thm)],[c_0_6,c_0_7]) ).
cnf(c_0_11,negated_conjecture,
r1(esk53_0,esk54_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_12,negated_conjecture,
( p1(X1)
| ~ p1(esk13_5(esk52_0,esk53_0,X2,X1,X3))
| ~ r1(esk53_0,X2)
| ~ r1(X1,X3)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_8,c_0_7]) ).
cnf(c_0_13,negated_conjecture,
( r1(X1,esk6_5(X2,X3,X4,X5,X1))
| p1(X7)
| ~ r1(X1,X6)
| ~ r1(X6,X7)
| ~ r1(X5,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_14,negated_conjecture,
( r1(X1,esk14_5(esk52_0,X2,X3,X4,X1))
| ~ p1(X4)
| ~ r1(esk52_0,X2)
| ~ r1(X4,X1)
| ~ r1(X3,X4)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_9,c_0_4]) ).
cnf(c_0_15,negated_conjecture,
( p1(X1)
| r1(X2,esk13_5(esk52_0,esk53_0,esk54_0,X1,X2))
| ~ r1(esk54_0,X1)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_10,c_0_11]) ).
cnf(c_0_16,negated_conjecture,
r1(esk54_0,esk55_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_17,negated_conjecture,
( p1(X1)
| ~ p1(esk13_5(esk52_0,esk53_0,esk54_0,X1,X2))
| ~ r1(esk54_0,X1)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_12,c_0_11]) ).
cnf(c_0_18,negated_conjecture,
( r1(X1,esk2_6(X2,X3,X4,X5,X6,X1))
| p1(X6)
| ~ r1(X6,X1)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(esk1_0,X2) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_19,negated_conjecture,
( p1(X5)
| ~ p1(esk2_6(X1,X2,X3,X4,X5,X6))
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_20,negated_conjecture,
( p1(X1)
| r1(X2,esk6_5(esk52_0,X3,X4,X5,X2))
| ~ r1(esk52_0,X3)
| ~ r1(X6,X1)
| ~ r1(X5,X2)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X6) ),
inference(spm,[status(thm)],[c_0_13,c_0_4]) ).
cnf(c_0_21,negated_conjecture,
( r1(X1,esk14_5(esk52_0,esk53_0,X2,X3,X1))
| ~ p1(X3)
| ~ r1(esk53_0,X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_14,c_0_7]) ).
cnf(c_0_22,negated_conjecture,
( p1(esk55_0)
| r1(X1,esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))
| ~ r1(esk55_0,X1) ),
inference(spm,[status(thm)],[c_0_15,c_0_16]) ).
cnf(c_0_23,negated_conjecture,
r1(esk55_0,esk56_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_24,negated_conjecture,
( p1(esk55_0)
| ~ p1(esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))
| ~ r1(esk55_0,X1) ),
inference(spm,[status(thm)],[c_0_17,c_0_16]) ).
cnf(c_0_25,negated_conjecture,
( p1(X1)
| r1(X2,esk2_6(esk52_0,X3,X4,X5,X1,X2))
| ~ r1(esk52_0,X3)
| ~ r1(X1,X2)
| ~ r1(X5,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4) ),
inference(spm,[status(thm)],[c_0_18,c_0_4]) ).
cnf(c_0_26,negated_conjecture,
( p1(X1)
| ~ p1(esk2_6(esk52_0,X2,X3,X4,X1,X5))
| ~ r1(esk52_0,X2)
| ~ r1(X1,X5)
| ~ r1(X4,X1)
| ~ r1(X3,X4)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_19,c_0_4]) ).
cnf(c_0_27,negated_conjecture,
( p1(X1)
| r1(X2,esk6_5(esk52_0,esk53_0,X3,X4,X2))
| ~ r1(esk53_0,X3)
| ~ r1(X5,X1)
| ~ r1(X4,X2)
| ~ r1(X3,X4)
| ~ r1(X2,X5) ),
inference(spm,[status(thm)],[c_0_20,c_0_7]) ).
cnf(c_0_28,negated_conjecture,
( r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,X2,X1))
| ~ p1(X2)
| ~ r1(esk54_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_21,c_0_11]) ).
cnf(c_0_29,negated_conjecture,
( p1(X1)
| ~ r1(esk56_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_30,negated_conjecture,
( p1(esk55_0)
| r1(esk56_0,esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)) ),
inference(spm,[status(thm)],[c_0_22,c_0_23]) ).
cnf(c_0_31,negated_conjecture,
( p1(esk55_0)
| ~ p1(esk13_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)) ),
inference(spm,[status(thm)],[c_0_24,c_0_23]) ).
cnf(c_0_32,negated_conjecture,
( p1(X1)
| r1(X2,esk2_6(esk52_0,esk53_0,X3,X4,X1,X2))
| ~ r1(esk53_0,X3)
| ~ r1(X1,X2)
| ~ r1(X4,X1)
| ~ r1(X3,X4) ),
inference(spm,[status(thm)],[c_0_25,c_0_7]) ).
cnf(c_0_33,negated_conjecture,
( p1(X1)
| ~ p1(esk2_6(esk52_0,esk53_0,X2,X3,X1,X4))
| ~ r1(esk53_0,X2)
| ~ r1(X1,X4)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_26,c_0_7]) ).
cnf(c_0_34,negated_conjecture,
( p1(X7)
| ~ p1(esk6_5(X1,X2,X3,X4,X5))
| ~ r1(X5,X6)
| ~ r1(X6,X7)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3)
| ~ r1(X1,X2)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_35,negated_conjecture,
( p1(X1)
| r1(X2,esk6_5(esk52_0,esk53_0,esk54_0,X3,X2))
| ~ r1(esk54_0,X3)
| ~ r1(X4,X1)
| ~ r1(X3,X2)
| ~ r1(X2,X4) ),
inference(spm,[status(thm)],[c_0_27,c_0_11]) ).
cnf(c_0_36,negated_conjecture,
( r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))
| ~ p1(esk55_0)
| ~ r1(esk55_0,X1) ),
inference(spm,[status(thm)],[c_0_28,c_0_16]) ).
cnf(c_0_37,negated_conjecture,
p1(esk55_0),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_29,c_0_30]),c_0_31]) ).
cnf(c_0_38,negated_conjecture,
( p1(X1)
| r1(X2,esk2_6(esk52_0,esk53_0,esk54_0,X3,X1,X2))
| ~ r1(esk54_0,X3)
| ~ r1(X1,X2)
| ~ r1(X3,X1) ),
inference(spm,[status(thm)],[c_0_32,c_0_11]) ).
cnf(c_0_39,negated_conjecture,
( p1(X1)
| ~ p1(esk2_6(esk52_0,esk53_0,esk54_0,X2,X1,X3))
| ~ r1(esk54_0,X2)
| ~ r1(X1,X3)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_33,c_0_11]) ).
cnf(c_0_40,negated_conjecture,
( p1(X1)
| ~ p1(esk6_5(esk52_0,X2,X3,X4,X5))
| ~ r1(esk52_0,X2)
| ~ r1(X6,X1)
| ~ r1(X5,X6)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_34,c_0_4]) ).
cnf(c_0_41,negated_conjecture,
( p1(X1)
| r1(X2,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,X2))
| ~ r1(esk55_0,X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_35,c_0_16]) ).
cnf(c_0_42,negated_conjecture,
( r1(X1,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,X1))
| ~ r1(esk55_0,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36,c_0_37])]) ).
cnf(c_0_43,negated_conjecture,
( p1(X1)
| r1(X2,esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,X1,X2))
| ~ r1(esk55_0,X1)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_38,c_0_16]) ).
cnf(c_0_44,negated_conjecture,
~ p1(esk56_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_45,negated_conjecture,
( p1(X1)
| ~ p1(esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,X1,X2))
| ~ r1(esk55_0,X1)
| ~ r1(X1,X2) ),
inference(spm,[status(thm)],[c_0_39,c_0_16]) ).
cnf(c_0_46,negated_conjecture,
( p1(X1)
| ~ p1(esk6_5(esk52_0,esk53_0,X2,X3,X4))
| ~ r1(esk53_0,X2)
| ~ r1(X5,X1)
| ~ r1(X4,X5)
| ~ r1(X3,X4)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_40,c_0_7]) ).
cnf(c_0_47,negated_conjecture,
( p1(X1)
| r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))
| ~ r1(esk56_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_41,c_0_23]) ).
cnf(c_0_48,negated_conjecture,
r1(esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)),
inference(spm,[status(thm)],[c_0_42,c_0_23]) ).
cnf(c_0_49,negated_conjecture,
( r1(X1,esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,X1))
| ~ r1(esk56_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_23]),c_0_44]) ).
cnf(c_0_50,negated_conjecture,
( ~ p1(esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,X1))
| ~ r1(esk56_0,X1) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_45,c_0_23]),c_0_44]) ).
cnf(c_0_51,negated_conjecture,
( p1(X1)
| ~ p1(esk6_5(esk52_0,esk53_0,esk54_0,X2,X3))
| ~ r1(esk54_0,X2)
| ~ r1(X4,X1)
| ~ r1(X3,X4)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_46,c_0_11]) ).
cnf(c_0_52,negated_conjecture,
( p1(X1)
| r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))
| ~ r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),X1) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_53,negated_conjecture,
r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))),
inference(spm,[status(thm)],[c_0_49,c_0_48]) ).
cnf(c_0_54,negated_conjecture,
~ p1(esk2_6(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0,esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))),
inference(spm,[status(thm)],[c_0_50,c_0_48]) ).
cnf(c_0_55,negated_conjecture,
( p1(X1)
| ~ p1(esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,X2))
| ~ r1(esk55_0,X2)
| ~ r1(X3,X1)
| ~ r1(X2,X3) ),
inference(spm,[status(thm)],[c_0_51,c_0_16]) ).
cnf(c_0_56,negated_conjecture,
r1(esk56_0,esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_54]) ).
cnf(c_0_57,negated_conjecture,
( p1(X1)
| ~ p1(esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0))
| ~ r1(esk56_0,X2)
| ~ r1(X2,X1) ),
inference(spm,[status(thm)],[c_0_55,c_0_23]) ).
cnf(c_0_58,negated_conjecture,
p1(esk6_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0)),
inference(spm,[status(thm)],[c_0_29,c_0_56]) ).
cnf(c_0_59,negated_conjecture,
( p1(X1)
| ~ r1(esk56_0,X2)
| ~ r1(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_57,c_0_58])]) ).
cnf(c_0_60,negated_conjecture,
( p1(X1)
| ~ r1(esk14_5(esk52_0,esk53_0,esk54_0,esk55_0,esk56_0),X1) ),
inference(spm,[status(thm)],[c_0_59,c_0_48]) ).
cnf(c_0_61,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_53]),c_0_54]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : LCL638+1.005 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.33 % Computer : n023.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:53 EDT 2026
% 0.14/0.33 % CPUTime :
% 0.14/0.34 % start to proof: theBenchmark
% 12.28/7.43 % Version : CSE_E---1.7
% 12.28/7.43 % Problem : theBenchmark.p
% 12.28/7.43 % SZS status Theorem for theBenchmark.p
% 12.28/7.43 % SZS output start CNFRefutation
% See solution above
% 12.28/7.45 % Total time : 6.384s
%------------------------------------------------------------------------------