%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : LCL664+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 : n013.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:44:10 PM UTC 2026
% Result : Theorem 5.66s 3.97s
% Output : CNFRefutation 5.66s
% 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 : 32 ( 31 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)
| p56(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p54(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p54(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p52(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p46(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p46(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p44(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p44(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p42(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p42(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p35(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p35(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p41(X1) )
& ~ p34(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p33(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p33(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p31(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p31(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p26(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p26(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p24(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p24(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p22(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p22(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p15(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p15(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p13(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p13(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p21(X1) )
& ~ p12(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p11(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p11(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p13(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p12(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p11(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)
| p56(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p54(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p54(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| p52(X2) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p56(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p46(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p44(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p52(X2) )
& ~ p42(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p46(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p46(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p45(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p44(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p44(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p43(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p42(X1) )
& ~ p36(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p42(X1) )
& ~ p32(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p55(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p54(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p53(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p51(X2) )
& ~ p41(X1) ) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p36(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p35(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p35(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p41(X1) )
& ~ p34(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p33(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p33(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p26(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p24(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p32(X2) )
& ~ p22(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p45(X1) )
& ~ p31(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p43(X1) )
& ~ p31(X2) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p26(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p26(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p25(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p24(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p24(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p23(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p22(X1) )
& ~ p16(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p22(X1) )
& ~ p14(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p35(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p34(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p33(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ ( ! [X2] :
( ~ r1(X1,X2)
| p31(X2) )
& ~ p21(X1) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p15(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p15(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p13(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p13(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p21(X1) )
& ~ p12(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p25(X1) )
& ~ p11(X2) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ! [X1] :
( ~ r1(X2,X1)
| p23(X1) )
& ~ p11(X2) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p13(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p12(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| p11(X2) ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[main])]) ).
fof(c_0_2,negated_conjecture,
! [X261,X262,X263,X264,X265,X266,X267,X268,X269,X270,X271,X272,X273,X274,X275,X276,X277,X278,X279,X280,X281,X282,X283,X284,X286,X287,X288,X289,X291,X292,X293,X294,X296,X297,X298,X299,X301,X302,X303,X304,X306,X307,X308,X309,X311,X312,X313,X314,X316,X317,X318,X319,X321,X322,X323,X324,X326,X327,X328,X330,X331,X332,X334,X335,X336,X337,X339,X340,X341,X342,X344,X345,X346,X347,X349,X350,X351,X353,X354,X355,X357,X358,X359,X360,X362,X363,X364,X365,X367,X368,X369,X370,X372,X373,X374,X376,X377,X378,X380,X381,X382,X383,X385,X386,X387,X388,X390,X391,X392,X393,X395,X396,X397,X398,X400,X401,X403,X404,X406,X407,X409,X410,X411,X413,X414,X415,X417,X418,X420,X421,X423,X424,X426,X427,X428,X430,X431,X432,X434,X435,X436,X438,X439,X441,X442,X444,X445,X447,X448,X449,X451,X452,X453,X455,X457,X459,X460,X462,X463,X465,X466,X468,X470,X472,X473,X475,X476,X478,X479,X481,X483,X485,X486,X488,X489,X491,X492,X494,X495,X497,X499,X501,X503,X505,X507,X509] :
( ( ~ r1(esk1_0,X261)
| ~ r1(X261,X262)
| ~ r1(X262,X263)
| ~ r1(X263,X264)
| ~ r1(X264,X265)
| p56(X265) )
& ( ~ r1(esk1_0,X266)
| ~ r1(X266,X267)
| ~ r1(X267,X268)
| ~ r1(X268,X269)
| ~ r1(X269,X270)
| p54(X270) )
& ( ~ r1(esk1_0,X271)
| ~ r1(X271,X272)
| ~ r1(X272,X273)
| ~ r1(X273,X274)
| ~ r1(X274,X275)
| p54(X275) )
& ( ~ r1(esk1_0,X276)
| ~ r1(X276,X277)
| ~ r1(X277,X278)
| ~ r1(X278,X279)
| ~ r1(X279,X280)
| p52(X280) )
& ( r1(X284,esk2_4(X281,X282,X283,X284))
| p46(X284)
| ~ r1(X283,X284)
| ~ r1(X282,X283)
| ~ r1(X281,X282)
| ~ r1(esk1_0,X281) )
& ( ~ p56(esk2_4(X281,X282,X283,X284))
| p46(X284)
| ~ r1(X283,X284)
| ~ r1(X282,X283)
| ~ r1(X281,X282)
| ~ r1(esk1_0,X281) )
& ( r1(X289,esk3_4(X286,X287,X288,X289))
| p44(X289)
| ~ r1(X288,X289)
| ~ r1(X287,X288)
| ~ r1(X286,X287)
| ~ r1(esk1_0,X286) )
& ( ~ p56(esk3_4(X286,X287,X288,X289))
| p44(X289)
| ~ r1(X288,X289)
| ~ r1(X287,X288)
| ~ r1(X286,X287)
| ~ r1(esk1_0,X286) )
& ( r1(X294,esk4_4(X291,X292,X293,X294))
| p42(X294)
| ~ r1(X293,X294)
| ~ r1(X292,X293)
| ~ r1(X291,X292)
| ~ r1(esk1_0,X291) )
& ( ~ p56(esk4_4(X291,X292,X293,X294))
| p42(X294)
| ~ r1(X293,X294)
| ~ r1(X292,X293)
| ~ r1(X291,X292)
| ~ r1(esk1_0,X291) )
& ( r1(X299,esk5_4(X296,X297,X298,X299))
| p46(X299)
| ~ r1(X298,X299)
| ~ r1(X297,X298)
| ~ r1(X296,X297)
| ~ r1(esk1_0,X296) )
& ( ~ p54(esk5_4(X296,X297,X298,X299))
| p46(X299)
| ~ r1(X298,X299)
| ~ r1(X297,X298)
| ~ r1(X296,X297)
| ~ r1(esk1_0,X296) )
& ( r1(X304,esk6_4(X301,X302,X303,X304))
| p44(X304)
| ~ r1(X303,X304)
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(esk1_0,X301) )
& ( ~ p54(esk6_4(X301,X302,X303,X304))
| p44(X304)
| ~ r1(X303,X304)
| ~ r1(X302,X303)
| ~ r1(X301,X302)
| ~ r1(esk1_0,X301) )
& ( r1(X309,esk7_4(X306,X307,X308,X309))
| p42(X309)
| ~ r1(X308,X309)
| ~ r1(X307,X308)
| ~ r1(X306,X307)
| ~ r1(esk1_0,X306) )
& ( ~ p54(esk7_4(X306,X307,X308,X309))
| p42(X309)
| ~ r1(X308,X309)
| ~ r1(X307,X308)
| ~ r1(X306,X307)
| ~ r1(esk1_0,X306) )
& ( r1(X314,esk8_4(X311,X312,X313,X314))
| p46(X314)
| ~ r1(X313,X314)
| ~ r1(X312,X313)
| ~ r1(X311,X312)
| ~ r1(esk1_0,X311) )
& ( ~ p52(esk8_4(X311,X312,X313,X314))
| p46(X314)
| ~ r1(X313,X314)
| ~ r1(X312,X313)
| ~ r1(X311,X312)
| ~ r1(esk1_0,X311) )
& ( r1(X319,esk9_4(X316,X317,X318,X319))
| p44(X319)
| ~ r1(X318,X319)
| ~ r1(X317,X318)
| ~ r1(X316,X317)
| ~ r1(esk1_0,X316) )
& ( ~ p52(esk9_4(X316,X317,X318,X319))
| p44(X319)
| ~ r1(X318,X319)
| ~ r1(X317,X318)
| ~ r1(X316,X317)
| ~ r1(esk1_0,X316) )
& ( r1(X324,esk10_4(X321,X322,X323,X324))
| p42(X324)
| ~ r1(X323,X324)
| ~ r1(X322,X323)
| ~ r1(X321,X322)
| ~ r1(esk1_0,X321) )
& ( ~ p52(esk10_4(X321,X322,X323,X324))
| p42(X324)
| ~ r1(X323,X324)
| ~ r1(X322,X323)
| ~ r1(X321,X322)
| ~ r1(esk1_0,X321) )
& ( r1(X328,esk11_3(X326,X327,X328))
| p36(X328)
| ~ r1(X327,X328)
| ~ r1(X326,X327)
| ~ r1(esk1_0,X326) )
& ( ~ p46(esk11_3(X326,X327,X328))
| p36(X328)
| ~ r1(X327,X328)
| ~ r1(X326,X327)
| ~ r1(esk1_0,X326) )
& ( r1(X332,esk12_3(X330,X331,X332))
| p32(X332)
| ~ r1(X331,X332)
| ~ r1(X330,X331)
| ~ r1(esk1_0,X330) )
& ( ~ p46(esk12_3(X330,X331,X332))
| p32(X332)
| ~ r1(X331,X332)
| ~ r1(X330,X331)
| ~ r1(esk1_0,X330) )
& ( r1(X337,esk13_4(X334,X335,X336,X337))
| p45(X337)
| ~ r1(X336,X337)
| ~ r1(X335,X336)
| ~ r1(X334,X335)
| ~ r1(esk1_0,X334) )
& ( ~ p55(esk13_4(X334,X335,X336,X337))
| p45(X337)
| ~ r1(X336,X337)
| ~ r1(X335,X336)
| ~ r1(X334,X335)
| ~ r1(esk1_0,X334) )
& ( r1(X342,esk14_4(X339,X340,X341,X342))
| p45(X342)
| ~ r1(X341,X342)
| ~ r1(X340,X341)
| ~ r1(X339,X340)
| ~ r1(esk1_0,X339) )
& ( ~ p53(esk14_4(X339,X340,X341,X342))
| p45(X342)
| ~ r1(X341,X342)
| ~ r1(X340,X341)
| ~ r1(X339,X340)
| ~ r1(esk1_0,X339) )
& ( r1(X347,esk15_4(X344,X345,X346,X347))
| p45(X347)
| ~ r1(X346,X347)
| ~ r1(X345,X346)
| ~ r1(X344,X345)
| ~ r1(esk1_0,X344) )
& ( ~ p51(esk15_4(X344,X345,X346,X347))
| p45(X347)
| ~ r1(X346,X347)
| ~ r1(X345,X346)
| ~ r1(X344,X345)
| ~ r1(esk1_0,X344) )
& ( r1(X351,esk16_3(X349,X350,X351))
| p36(X351)
| ~ r1(X350,X351)
| ~ r1(X349,X350)
| ~ r1(esk1_0,X349) )
& ( ~ p44(esk16_3(X349,X350,X351))
| p36(X351)
| ~ r1(X350,X351)
| ~ r1(X349,X350)
| ~ r1(esk1_0,X349) )
& ( r1(X355,esk17_3(X353,X354,X355))
| p32(X355)
| ~ r1(X354,X355)
| ~ r1(X353,X354)
| ~ r1(esk1_0,X353) )
& ( ~ p44(esk17_3(X353,X354,X355))
| p32(X355)
| ~ r1(X354,X355)
| ~ r1(X353,X354)
| ~ r1(esk1_0,X353) )
& ( r1(X360,esk18_4(X357,X358,X359,X360))
| p43(X360)
| ~ r1(X359,X360)
| ~ r1(X358,X359)
| ~ r1(X357,X358)
| ~ r1(esk1_0,X357) )
& ( ~ p55(esk18_4(X357,X358,X359,X360))
| p43(X360)
| ~ r1(X359,X360)
| ~ r1(X358,X359)
| ~ r1(X357,X358)
| ~ r1(esk1_0,X357) )
& ( r1(X365,esk19_4(X362,X363,X364,X365))
| p43(X365)
| ~ r1(X364,X365)
| ~ r1(X363,X364)
| ~ r1(X362,X363)
| ~ r1(esk1_0,X362) )
& ( ~ p53(esk19_4(X362,X363,X364,X365))
| p43(X365)
| ~ r1(X364,X365)
| ~ r1(X363,X364)
| ~ r1(X362,X363)
| ~ r1(esk1_0,X362) )
& ( r1(X370,esk20_4(X367,X368,X369,X370))
| p43(X370)
| ~ r1(X369,X370)
| ~ r1(X368,X369)
| ~ r1(X367,X368)
| ~ r1(esk1_0,X367) )
& ( ~ p51(esk20_4(X367,X368,X369,X370))
| p43(X370)
| ~ r1(X369,X370)
| ~ r1(X368,X369)
| ~ r1(X367,X368)
| ~ r1(esk1_0,X367) )
& ( r1(X374,esk21_3(X372,X373,X374))
| p36(X374)
| ~ r1(X373,X374)
| ~ r1(X372,X373)
| ~ r1(esk1_0,X372) )
& ( ~ p42(esk21_3(X372,X373,X374))
| p36(X374)
| ~ r1(X373,X374)
| ~ r1(X372,X373)
| ~ r1(esk1_0,X372) )
& ( r1(X378,esk22_3(X376,X377,X378))
| p32(X378)
| ~ r1(X377,X378)
| ~ r1(X376,X377)
| ~ r1(esk1_0,X376) )
& ( ~ p42(esk22_3(X376,X377,X378))
| p32(X378)
| ~ r1(X377,X378)
| ~ r1(X376,X377)
| ~ r1(esk1_0,X376) )
& ( r1(X383,esk23_4(X380,X381,X382,X383))
| p41(X383)
| ~ r1(X382,X383)
| ~ r1(X381,X382)
| ~ r1(X380,X381)
| ~ r1(esk1_0,X380) )
& ( ~ p55(esk23_4(X380,X381,X382,X383))
| p41(X383)
| ~ r1(X382,X383)
| ~ r1(X381,X382)
| ~ r1(X380,X381)
| ~ r1(esk1_0,X380) )
& ( r1(X388,esk24_4(X385,X386,X387,X388))
| p41(X388)
| ~ r1(X387,X388)
| ~ r1(X386,X387)
| ~ r1(X385,X386)
| ~ r1(esk1_0,X385) )
& ( ~ p54(esk24_4(X385,X386,X387,X388))
| p41(X388)
| ~ r1(X387,X388)
| ~ r1(X386,X387)
| ~ r1(X385,X386)
| ~ r1(esk1_0,X385) )
& ( r1(X393,esk25_4(X390,X391,X392,X393))
| p41(X393)
| ~ r1(X392,X393)
| ~ r1(X391,X392)
| ~ r1(X390,X391)
| ~ r1(esk1_0,X390) )
& ( ~ p53(esk25_4(X390,X391,X392,X393))
| p41(X393)
| ~ r1(X392,X393)
| ~ r1(X391,X392)
| ~ r1(X390,X391)
| ~ r1(esk1_0,X390) )
& ( r1(X398,esk26_4(X395,X396,X397,X398))
| p41(X398)
| ~ r1(X397,X398)
| ~ r1(X396,X397)
| ~ r1(X395,X396)
| ~ r1(esk1_0,X395) )
& ( ~ p51(esk26_4(X395,X396,X397,X398))
| p41(X398)
| ~ r1(X397,X398)
| ~ r1(X396,X397)
| ~ r1(X395,X396)
| ~ r1(esk1_0,X395) )
& ( r1(X401,esk27_2(X400,X401))
| p26(X401)
| ~ r1(X400,X401)
| ~ r1(esk1_0,X400) )
& ( ~ p36(esk27_2(X400,X401))
| p26(X401)
| ~ r1(X400,X401)
| ~ r1(esk1_0,X400) )
& ( r1(X404,esk28_2(X403,X404))
| p24(X404)
| ~ r1(X403,X404)
| ~ r1(esk1_0,X403) )
& ( ~ p36(esk28_2(X403,X404))
| p24(X404)
| ~ r1(X403,X404)
| ~ r1(esk1_0,X403) )
& ( r1(X407,esk29_2(X406,X407))
| p22(X407)
| ~ r1(X406,X407)
| ~ r1(esk1_0,X406) )
& ( ~ p36(esk29_2(X406,X407))
| p22(X407)
| ~ r1(X406,X407)
| ~ r1(esk1_0,X406) )
& ( r1(X411,esk30_3(X409,X410,X411))
| p35(X411)
| ~ r1(X410,X411)
| ~ r1(X409,X410)
| ~ r1(esk1_0,X409) )
& ( ~ p45(esk30_3(X409,X410,X411))
| p35(X411)
| ~ r1(X410,X411)
| ~ r1(X409,X410)
| ~ r1(esk1_0,X409) )
& ( r1(X415,esk31_3(X413,X414,X415))
| p35(X415)
| ~ r1(X414,X415)
| ~ r1(X413,X414)
| ~ r1(esk1_0,X413) )
& ( ~ p43(esk31_3(X413,X414,X415))
| p35(X415)
| ~ r1(X414,X415)
| ~ r1(X413,X414)
| ~ r1(esk1_0,X413) )
& ( r1(X418,esk32_2(X417,X418))
| p26(X418)
| ~ r1(X417,X418)
| ~ r1(esk1_0,X417) )
& ( ~ p34(esk32_2(X417,X418))
| p26(X418)
| ~ r1(X417,X418)
| ~ r1(esk1_0,X417) )
& ( r1(X421,esk33_2(X420,X421))
| p24(X421)
| ~ r1(X420,X421)
| ~ r1(esk1_0,X420) )
& ( ~ p34(esk33_2(X420,X421))
| p24(X421)
| ~ r1(X420,X421)
| ~ r1(esk1_0,X420) )
& ( r1(X424,esk34_2(X423,X424))
| p22(X424)
| ~ r1(X423,X424)
| ~ r1(esk1_0,X423) )
& ( ~ p34(esk34_2(X423,X424))
| p22(X424)
| ~ r1(X423,X424)
| ~ r1(esk1_0,X423) )
& ( r1(X428,esk35_3(X426,X427,X428))
| p34(X428)
| ~ r1(X427,X428)
| ~ r1(X426,X427)
| ~ r1(esk1_0,X426) )
& ( ~ p41(esk35_3(X426,X427,X428))
| p34(X428)
| ~ r1(X427,X428)
| ~ r1(X426,X427)
| ~ r1(esk1_0,X426) )
& ( r1(X432,esk36_3(X430,X431,X432))
| p33(X432)
| ~ r1(X431,X432)
| ~ r1(X430,X431)
| ~ r1(esk1_0,X430) )
& ( ~ p45(esk36_3(X430,X431,X432))
| p33(X432)
| ~ r1(X431,X432)
| ~ r1(X430,X431)
| ~ r1(esk1_0,X430) )
& ( r1(X436,esk37_3(X434,X435,X436))
| p33(X436)
| ~ r1(X435,X436)
| ~ r1(X434,X435)
| ~ r1(esk1_0,X434) )
& ( ~ p43(esk37_3(X434,X435,X436))
| p33(X436)
| ~ r1(X435,X436)
| ~ r1(X434,X435)
| ~ r1(esk1_0,X434) )
& ( r1(X439,esk38_2(X438,X439))
| p26(X439)
| ~ r1(X438,X439)
| ~ r1(esk1_0,X438) )
& ( ~ p32(esk38_2(X438,X439))
| p26(X439)
| ~ r1(X438,X439)
| ~ r1(esk1_0,X438) )
& ( r1(X442,esk39_2(X441,X442))
| p24(X442)
| ~ r1(X441,X442)
| ~ r1(esk1_0,X441) )
& ( ~ p32(esk39_2(X441,X442))
| p24(X442)
| ~ r1(X441,X442)
| ~ r1(esk1_0,X441) )
& ( r1(X445,esk40_2(X444,X445))
| p22(X445)
| ~ r1(X444,X445)
| ~ r1(esk1_0,X444) )
& ( ~ p32(esk40_2(X444,X445))
| p22(X445)
| ~ r1(X444,X445)
| ~ r1(esk1_0,X444) )
& ( r1(X449,esk41_3(X447,X448,X449))
| p31(X449)
| ~ r1(X448,X449)
| ~ r1(X447,X448)
| ~ r1(esk1_0,X447) )
& ( ~ p45(esk41_3(X447,X448,X449))
| p31(X449)
| ~ r1(X448,X449)
| ~ r1(X447,X448)
| ~ r1(esk1_0,X447) )
& ( r1(X453,esk42_3(X451,X452,X453))
| p31(X453)
| ~ r1(X452,X453)
| ~ r1(X451,X452)
| ~ r1(esk1_0,X451) )
& ( ~ p43(esk42_3(X451,X452,X453))
| p31(X453)
| ~ r1(X452,X453)
| ~ r1(X451,X452)
| ~ r1(esk1_0,X451) )
& ( r1(X455,esk43_1(X455))
| p16(X455)
| ~ r1(esk1_0,X455) )
& ( ~ p26(esk43_1(X455))
| p16(X455)
| ~ r1(esk1_0,X455) )
& ( r1(X457,esk44_1(X457))
| p14(X457)
| ~ r1(esk1_0,X457) )
& ( ~ p26(esk44_1(X457))
| p14(X457)
| ~ r1(esk1_0,X457) )
& ( r1(X460,esk45_2(X459,X460))
| p25(X460)
| ~ r1(X459,X460)
| ~ r1(esk1_0,X459) )
& ( ~ p35(esk45_2(X459,X460))
| p25(X460)
| ~ r1(X459,X460)
| ~ r1(esk1_0,X459) )
& ( r1(X463,esk46_2(X462,X463))
| p25(X463)
| ~ r1(X462,X463)
| ~ r1(esk1_0,X462) )
& ( ~ p33(esk46_2(X462,X463))
| p25(X463)
| ~ r1(X462,X463)
| ~ r1(esk1_0,X462) )
& ( r1(X466,esk47_2(X465,X466))
| p25(X466)
| ~ r1(X465,X466)
| ~ r1(esk1_0,X465) )
& ( ~ p31(esk47_2(X465,X466))
| p25(X466)
| ~ r1(X465,X466)
| ~ r1(esk1_0,X465) )
& ( r1(X468,esk48_1(X468))
| p16(X468)
| ~ r1(esk1_0,X468) )
& ( ~ p24(esk48_1(X468))
| p16(X468)
| ~ r1(esk1_0,X468) )
& ( r1(X470,esk49_1(X470))
| p14(X470)
| ~ r1(esk1_0,X470) )
& ( ~ p24(esk49_1(X470))
| p14(X470)
| ~ r1(esk1_0,X470) )
& ( r1(X473,esk50_2(X472,X473))
| p23(X473)
| ~ r1(X472,X473)
| ~ r1(esk1_0,X472) )
& ( ~ p35(esk50_2(X472,X473))
| p23(X473)
| ~ r1(X472,X473)
| ~ r1(esk1_0,X472) )
& ( r1(X476,esk51_2(X475,X476))
| p23(X476)
| ~ r1(X475,X476)
| ~ r1(esk1_0,X475) )
& ( ~ p33(esk51_2(X475,X476))
| p23(X476)
| ~ r1(X475,X476)
| ~ r1(esk1_0,X475) )
& ( r1(X479,esk52_2(X478,X479))
| p23(X479)
| ~ r1(X478,X479)
| ~ r1(esk1_0,X478) )
& ( ~ p31(esk52_2(X478,X479))
| p23(X479)
| ~ r1(X478,X479)
| ~ r1(esk1_0,X478) )
& ( r1(X481,esk53_1(X481))
| p16(X481)
| ~ r1(esk1_0,X481) )
& ( ~ p22(esk53_1(X481))
| p16(X481)
| ~ r1(esk1_0,X481) )
& ( r1(X483,esk54_1(X483))
| p14(X483)
| ~ r1(esk1_0,X483) )
& ( ~ p22(esk54_1(X483))
| p14(X483)
| ~ r1(esk1_0,X483) )
& ( r1(X486,esk55_2(X485,X486))
| p21(X486)
| ~ r1(X485,X486)
| ~ r1(esk1_0,X485) )
& ( ~ p35(esk55_2(X485,X486))
| p21(X486)
| ~ r1(X485,X486)
| ~ r1(esk1_0,X485) )
& ( r1(X489,esk56_2(X488,X489))
| p21(X489)
| ~ r1(X488,X489)
| ~ r1(esk1_0,X488) )
& ( ~ p34(esk56_2(X488,X489))
| p21(X489)
| ~ r1(X488,X489)
| ~ r1(esk1_0,X488) )
& ( r1(X492,esk57_2(X491,X492))
| p21(X492)
| ~ r1(X491,X492)
| ~ r1(esk1_0,X491) )
& ( ~ p33(esk57_2(X491,X492))
| p21(X492)
| ~ r1(X491,X492)
| ~ r1(esk1_0,X491) )
& ( r1(X495,esk58_2(X494,X495))
| p21(X495)
| ~ r1(X494,X495)
| ~ r1(esk1_0,X494) )
& ( ~ p31(esk58_2(X494,X495))
| p21(X495)
| ~ r1(X494,X495)
| ~ r1(esk1_0,X494) )
& ( r1(X497,esk59_1(X497))
| p15(X497)
| ~ r1(esk1_0,X497) )
& ( ~ p25(esk59_1(X497))
| p15(X497)
| ~ r1(esk1_0,X497) )
& ( r1(X499,esk60_1(X499))
| p15(X499)
| ~ r1(esk1_0,X499) )
& ( ~ p23(esk60_1(X499))
| p15(X499)
| ~ r1(esk1_0,X499) )
& ( r1(X501,esk61_1(X501))
| p13(X501)
| ~ r1(esk1_0,X501) )
& ( ~ p25(esk61_1(X501))
| p13(X501)
| ~ r1(esk1_0,X501) )
& ( r1(X503,esk62_1(X503))
| p13(X503)
| ~ r1(esk1_0,X503) )
& ( ~ p23(esk62_1(X503))
| p13(X503)
| ~ r1(esk1_0,X503) )
& ( r1(X505,esk63_1(X505))
| p12(X505)
| ~ r1(esk1_0,X505) )
& ( ~ p21(esk63_1(X505))
| p12(X505)
| ~ r1(esk1_0,X505) )
& ( r1(X507,esk64_1(X507))
| p11(X507)
| ~ r1(esk1_0,X507) )
& ( ~ p25(esk64_1(X507))
| p11(X507)
| ~ r1(esk1_0,X507) )
& ( r1(X509,esk65_1(X509))
| p11(X509)
| ~ r1(esk1_0,X509) )
& ( ~ p23(esk65_1(X509))
| p11(X509)
| ~ r1(esk1_0,X509) )
& r1(esk1_0,esk66_0)
& ~ p15(esk66_0)
& r1(esk1_0,esk67_0)
& ~ p13(esk67_0)
& r1(esk1_0,esk68_0)
& ~ p12(esk68_0)
& r1(esk1_0,esk69_0)
& ~ p11(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))
| p21(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))
| p12(X1)
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_6,negated_conjecture,
~ p12(esk68_0),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_7,negated_conjecture,
( r1(X1,esk35_3(X2,X3,X1))
| p34(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,
( p21(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,
( p21(X2)
| ~ p34(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,
( p34(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,
( p12(X1)
| ~ p21(esk63_1(X1))
| ~ r1(esk1_0,X1) ),
inference(split_conjunct,[status(thm)],[c_0_2]) ).
cnf(c_0_13,negated_conjecture,
( p21(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))
| p41(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,
( p21(X1)
| ~ p34(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,
( p34(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,
( p34(X3)
| ~ p41(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,
( p41(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,
( p21(esk63_1(esk68_0))
| ~ p34(esk56_2(esk68_0,esk63_1(esk68_0))) ),
inference(spm,[status(thm)],[c_0_15,c_0_9]) ).
cnf(c_0_21,negated_conjecture,
( p34(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,
( p34(X1)
| ~ p41(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,
( p41(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,
( p21(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,
( p54(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,
( p34(X1)
| ~ p41(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,
( p41(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,
( p41(X4)
| ~ p54(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,
( p54(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,
( p34(esk56_2(esk68_0,esk63_1(esk68_0)))
| ~ p41(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,
( p41(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,
( p41(X1)
| ~ p54(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,
( p54(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,
( p34(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,
( p41(X1)
| ~ p54(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,
( p54(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,
( p21(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,
( p41(X1)
| ~ p54(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,
( p54(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,
( p41(esk35_3(esk68_0,esk63_1(esk68_0),esk56_2(esk68_0,esk63_1(esk68_0))))
| ~ p54(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,
p54(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,
p41(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,
p34(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,
p21(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 : LCL664+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.16/0.33 % Computer : n013.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Mon May 4 22:53:11 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 5.66/3.97 % Version : CSE_E---1.7
% 5.66/3.97 % Problem : theBenchmark.p
% 5.66/3.97 % SZS status Theorem for theBenchmark.p
% 5.66/3.97 % SZS output start CNFRefutation
% See solution above
% 5.66/3.97 % Total time : 3.374s
%------------------------------------------------------------------------------