%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : LCL686+1.005 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art06.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Sat Dec 25 20:48:00 EST 2010
% Result : Theorem 0.19s
% Output : CNFRefutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 3
% Syntax : Number of formulae : 37 ( 9 unt; 0 def)
% Number of atoms : 1392 ( 0 equ)
% Maximal formula atoms : 216 ( 37 avg)
% Number of connectives : 2272 ( 917 ~; 786 |; 568 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 86 ( 17 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 2 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 4 con; 0-1 aty)
% Number of variables : 262 ( 0 sgn 205 !; 42 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,conjecture,
~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p15(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)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ $true )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ) ) ),
file('/tmp/tmpaNgS7-/sel_LCL686+1.005.p_1',main) ).
fof(3,axiom,
! [X1] : r1(X1,X1),
file('/tmp/tmpaNgS7-/sel_LCL686+1.005.p_1',reflexivity) ).
fof(4,negated_conjecture,
~ ~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p15(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)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ $true )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ) ) ),
inference(assume_negation,[status(cth)],[1]) ).
fof(5,negated_conjecture,
~ ~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p15(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)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ $true )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ) ) ),
inference(fof_simplification,[status(thm)],[4,theory(equality)]) ).
fof(6,plain,
! [X1] :
( epred1_1(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)
| ! [X1] :
( ~ r1(X2,X1)
| ! [X2] :
( ~ r1(X1,X2)
| ~ $true )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p14(X2)
& ~ p13(X2) )
| ( ~ p14(X2)
& p13(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p13(X1)
& ~ p12(X1) )
| ( ~ p13(X1)
& p12(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p12(X2)
& ~ p11(X2) )
| ( ~ p12(X2)
& p11(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p11(X1)
& ~ p10(X1) )
| ( ~ p11(X1)
& p10(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p10(X2)
& ~ p9(X2) )
| ( ~ p10(X2)
& p9(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p9(X1)
& ~ p8(X1) )
| ( ~ p9(X1)
& p8(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p8(X2)
& ~ p7(X2) )
| ( ~ p8(X2)
& p7(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p7(X1)
& ~ p6(X1) )
| ( ~ p7(X1)
& p6(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p6(X2)
& ~ p5(X2) )
| ( ~ p6(X2)
& p5(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p5(X1)
& ~ p4(X1) )
| ( ~ p5(X1)
& p4(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p4(X2)
& ~ p3(X2) )
| ( ~ p4(X2)
& p3(X2) ) ) ) )
| ~ ! [X1] :
( ~ r1(X2,X1)
| ~ ( ( p3(X1)
& ~ p2(X1) )
| ( ~ p3(X1)
& p2(X1) ) ) ) )
| ~ ! [X2] :
( ~ r1(X1,X2)
| ~ ( ( p2(X2)
& ~ p1(X2) )
| ( ~ p2(X2)
& p1(X2) ) ) )
| ! [X2] :
( ~ r1(X1,X2)
| p15(X2) )
| ! [X2] :
( ~ r1(X1,X2)
| ( ~ p13(X2)
& ~ p14(X2) )
| ( p14(X2)
& p13(X2) )
| ( ~ p12(X2)
& ~ p13(X2) )
| ( p13(X2)
& p12(X2) )
| ( ~ p11(X2)
& ~ p12(X2) )
| ( p12(X2)
& p11(X2) )
| ( ~ p10(X2)
& ~ p11(X2) )
| ( p11(X2)
& p10(X2) )
| ( ~ p9(X2)
& ~ p10(X2) )
| ( p10(X2)
& p9(X2) )
| ( ~ p8(X2)
& ~ p9(X2) )
| ( p9(X2)
& p8(X2) )
| ( ~ p7(X2)
& ~ p8(X2) )
| ( p8(X2)
& p7(X2) )
| ( ~ p6(X2)
& ~ p7(X2) )
| ( p7(X2)
& p6(X2) )
| ( ~ p5(X2)
& ~ p6(X2) )
| ( p6(X2)
& p5(X2) )
| ( ~ p4(X2)
& ~ p5(X2) )
| ( p5(X2)
& p4(X2) )
| ( ~ p3(X2)
& ~ p4(X2) )
| ( p4(X2)
& p3(X2) )
| ( ~ p2(X2)
& ~ p3(X2) )
| ( p3(X2)
& p2(X2) )
| ( ~ p1(X2)
& ~ p2(X2) )
| ( p2(X2)
& p1(X2) ) ) ) ),
introduced(definition) ).
fof(7,negated_conjecture,
~ ~ ? [X1] :
~ ( ! [X2] :
( ~ r1(X1,X2)
| ~ p15(X2)
| ! [X1] :
( ~ r1(X2,X1)
| ~ p1(X1) ) )
| ! [X2] :
( ~ r1(X1,X2)
| ~ ! [X1] :
( ~ r1(X2,X1)
| epred1_1(X1) ) ) ),
inference(apply_def,[status(esa)],[5,6,theory(equality)]) ).
fof(8,negated_conjecture,
? [X1] :
( ? [X2] :
( r1(X1,X2)
& p15(X2)
& ? [X1] :
( r1(X2,X1)
& p1(X1) ) )
& ? [X2] :
( r1(X1,X2)
& ! [X1] :
( ~ r1(X2,X1)
| epred1_1(X1) ) ) ),
inference(fof_nnf,[status(thm)],[7]) ).
fof(9,negated_conjecture,
? [X3] :
( ? [X4] :
( r1(X3,X4)
& p15(X4)
& ? [X5] :
( r1(X4,X5)
& p1(X5) ) )
& ? [X6] :
( r1(X3,X6)
& ! [X7] :
( ~ r1(X6,X7)
| epred1_1(X7) ) ) ),
inference(variable_rename,[status(thm)],[8]) ).
fof(10,negated_conjecture,
( r1(esk1_0,esk2_0)
& p15(esk2_0)
& r1(esk2_0,esk3_0)
& p1(esk3_0)
& r1(esk1_0,esk4_0)
& ! [X7] :
( ~ r1(esk4_0,X7)
| epred1_1(X7) ) ),
inference(skolemize,[status(esa)],[9]) ).
fof(11,negated_conjecture,
! [X7] :
( ( ~ r1(esk4_0,X7)
| epred1_1(X7) )
& r1(esk1_0,esk4_0)
& r1(esk1_0,esk2_0)
& p15(esk2_0)
& r1(esk2_0,esk3_0)
& p1(esk3_0) ),
inference(shift_quantors,[status(thm)],[10]) ).
cnf(17,negated_conjecture,
( epred1_1(X1)
| ~ r1(esk4_0,X1) ),
inference(split_conjunct,[status(thm)],[11]) ).
fof(21,plain,
! [X2] : r1(X2,X2),
inference(variable_rename,[status(thm)],[3]) ).
cnf(22,plain,
r1(X1,X1),
inference(split_conjunct,[status(thm)],[21]) ).
fof(23,plain,
! [X1] :
( ~ epred1_1(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)
& ? [X1] :
( r1(X2,X1)
& ? [X2] :
( r1(X1,X2)
& $true )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p14(X2)
| p13(X2) )
& ( p14(X2)
| ~ p13(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p13(X1)
| p12(X1) )
& ( p13(X1)
| ~ p12(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p12(X2)
| p11(X2) )
& ( p12(X2)
| ~ p11(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p11(X1)
| p10(X1) )
& ( p11(X1)
| ~ p10(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p10(X2)
| p9(X2) )
& ( p10(X2)
| ~ p9(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p9(X1)
| p8(X1) )
& ( p9(X1)
| ~ p8(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p8(X2)
| p7(X2) )
& ( p8(X2)
| ~ p7(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p7(X1)
| p6(X1) )
& ( p7(X1)
| ~ p6(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p6(X2)
| p5(X2) )
& ( p6(X2)
| ~ p5(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p5(X1)
| p4(X1) )
& ( p5(X1)
| ~ p4(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p4(X2)
| p3(X2) )
& ( p4(X2)
| ~ p3(X2) ) ) ) )
& ! [X1] :
( ~ r1(X2,X1)
| ( ( ~ p3(X1)
| p2(X1) )
& ( p3(X1)
| ~ p2(X1) ) ) ) )
& ! [X2] :
( ~ r1(X1,X2)
| ( ( ~ p2(X2)
| p1(X2) )
& ( p2(X2)
| ~ p1(X2) ) ) )
& ? [X2] :
( r1(X1,X2)
& ~ p15(X2) )
& ? [X2] :
( r1(X1,X2)
& ( p13(X2)
| p14(X2) )
& ( ~ p14(X2)
| ~ p13(X2) )
& ( p12(X2)
| p13(X2) )
& ( ~ p13(X2)
| ~ p12(X2) )
& ( p11(X2)
| p12(X2) )
& ( ~ p12(X2)
| ~ p11(X2) )
& ( p10(X2)
| p11(X2) )
& ( ~ p11(X2)
| ~ p10(X2) )
& ( p9(X2)
| p10(X2) )
& ( ~ p10(X2)
| ~ p9(X2) )
& ( p8(X2)
| p9(X2) )
& ( ~ p9(X2)
| ~ p8(X2) )
& ( p7(X2)
| p8(X2) )
& ( ~ p8(X2)
| ~ p7(X2) )
& ( p6(X2)
| p7(X2) )
& ( ~ p7(X2)
| ~ p6(X2) )
& ( p5(X2)
| p6(X2) )
& ( ~ p6(X2)
| ~ p5(X2) )
& ( p4(X2)
| p5(X2) )
& ( ~ p5(X2)
| ~ p4(X2) )
& ( p3(X2)
| p4(X2) )
& ( ~ p4(X2)
| ~ p3(X2) )
& ( p2(X2)
| p3(X2) )
& ( ~ p3(X2)
| ~ p2(X2) )
& ( p1(X2)
| p2(X2) )
& ( ~ p2(X2)
| ~ p1(X2) ) ) ) ),
inference(fof_nnf,[status(thm)],[6]) ).
fof(24,plain,
! [X3] :
( ~ epred1_1(X3)
| ( ? [X4] :
( r1(X3,X4)
& ? [X5] :
( r1(X4,X5)
& ? [X6] :
( r1(X5,X6)
& ? [X7] :
( r1(X6,X7)
& ? [X8] :
( r1(X7,X8)
& ? [X9] :
( r1(X8,X9)
& ? [X10] :
( r1(X9,X10)
& ? [X11] :
( r1(X10,X11)
& ? [X12] :
( r1(X11,X12)
& ? [X13] :
( r1(X12,X13)
& ? [X14] :
( r1(X13,X14)
& ? [X15] :
( r1(X14,X15)
& ? [X16] :
( r1(X15,X16)
& $true )
& ! [X17] :
( ~ r1(X15,X17)
| ( ( ~ p14(X17)
| p13(X17) )
& ( p14(X17)
| ~ p13(X17) ) ) ) )
& ! [X18] :
( ~ r1(X14,X18)
| ( ( ~ p13(X18)
| p12(X18) )
& ( p13(X18)
| ~ p12(X18) ) ) ) )
& ! [X19] :
( ~ r1(X13,X19)
| ( ( ~ p12(X19)
| p11(X19) )
& ( p12(X19)
| ~ p11(X19) ) ) ) )
& ! [X20] :
( ~ r1(X12,X20)
| ( ( ~ p11(X20)
| p10(X20) )
& ( p11(X20)
| ~ p10(X20) ) ) ) )
& ! [X21] :
( ~ r1(X11,X21)
| ( ( ~ p10(X21)
| p9(X21) )
& ( p10(X21)
| ~ p9(X21) ) ) ) )
& ! [X22] :
( ~ r1(X10,X22)
| ( ( ~ p9(X22)
| p8(X22) )
& ( p9(X22)
| ~ p8(X22) ) ) ) )
& ! [X23] :
( ~ r1(X9,X23)
| ( ( ~ p8(X23)
| p7(X23) )
& ( p8(X23)
| ~ p7(X23) ) ) ) )
& ! [X24] :
( ~ r1(X8,X24)
| ( ( ~ p7(X24)
| p6(X24) )
& ( p7(X24)
| ~ p6(X24) ) ) ) )
& ! [X25] :
( ~ r1(X7,X25)
| ( ( ~ p6(X25)
| p5(X25) )
& ( p6(X25)
| ~ p5(X25) ) ) ) )
& ! [X26] :
( ~ r1(X6,X26)
| ( ( ~ p5(X26)
| p4(X26) )
& ( p5(X26)
| ~ p4(X26) ) ) ) )
& ! [X27] :
( ~ r1(X5,X27)
| ( ( ~ p4(X27)
| p3(X27) )
& ( p4(X27)
| ~ p3(X27) ) ) ) )
& ! [X28] :
( ~ r1(X4,X28)
| ( ( ~ p3(X28)
| p2(X28) )
& ( p3(X28)
| ~ p2(X28) ) ) ) )
& ! [X29] :
( ~ r1(X3,X29)
| ( ( ~ p2(X29)
| p1(X29) )
& ( p2(X29)
| ~ p1(X29) ) ) )
& ? [X30] :
( r1(X3,X30)
& ~ p15(X30) )
& ? [X31] :
( r1(X3,X31)
& ( p13(X31)
| p14(X31) )
& ( ~ p14(X31)
| ~ p13(X31) )
& ( p12(X31)
| p13(X31) )
& ( ~ p13(X31)
| ~ p12(X31) )
& ( p11(X31)
| p12(X31) )
& ( ~ p12(X31)
| ~ p11(X31) )
& ( p10(X31)
| p11(X31) )
& ( ~ p11(X31)
| ~ p10(X31) )
& ( p9(X31)
| p10(X31) )
& ( ~ p10(X31)
| ~ p9(X31) )
& ( p8(X31)
| p9(X31) )
& ( ~ p9(X31)
| ~ p8(X31) )
& ( p7(X31)
| p8(X31) )
& ( ~ p8(X31)
| ~ p7(X31) )
& ( p6(X31)
| p7(X31) )
& ( ~ p7(X31)
| ~ p6(X31) )
& ( p5(X31)
| p6(X31) )
& ( ~ p6(X31)
| ~ p5(X31) )
& ( p4(X31)
| p5(X31) )
& ( ~ p5(X31)
| ~ p4(X31) )
& ( p3(X31)
| p4(X31) )
& ( ~ p4(X31)
| ~ p3(X31) )
& ( p2(X31)
| p3(X31) )
& ( ~ p3(X31)
| ~ p2(X31) )
& ( p1(X31)
| p2(X31) )
& ( ~ p2(X31)
| ~ p1(X31) ) ) ) ),
inference(variable_rename,[status(thm)],[23]) ).
fof(25,plain,
! [X3] :
( ~ epred1_1(X3)
| ( r1(X3,esk5_1(X3))
& r1(esk5_1(X3),esk6_1(X3))
& r1(esk6_1(X3),esk7_1(X3))
& r1(esk7_1(X3),esk8_1(X3))
& r1(esk8_1(X3),esk9_1(X3))
& r1(esk9_1(X3),esk10_1(X3))
& r1(esk10_1(X3),esk11_1(X3))
& r1(esk11_1(X3),esk12_1(X3))
& r1(esk12_1(X3),esk13_1(X3))
& r1(esk13_1(X3),esk14_1(X3))
& r1(esk14_1(X3),esk15_1(X3))
& r1(esk15_1(X3),esk16_1(X3))
& r1(esk16_1(X3),esk17_1(X3))
& $true
& ! [X17] :
( ~ r1(esk16_1(X3),X17)
| ( ( ~ p14(X17)
| p13(X17) )
& ( p14(X17)
| ~ p13(X17) ) ) )
& ! [X18] :
( ~ r1(esk15_1(X3),X18)
| ( ( ~ p13(X18)
| p12(X18) )
& ( p13(X18)
| ~ p12(X18) ) ) )
& ! [X19] :
( ~ r1(esk14_1(X3),X19)
| ( ( ~ p12(X19)
| p11(X19) )
& ( p12(X19)
| ~ p11(X19) ) ) )
& ! [X20] :
( ~ r1(esk13_1(X3),X20)
| ( ( ~ p11(X20)
| p10(X20) )
& ( p11(X20)
| ~ p10(X20) ) ) )
& ! [X21] :
( ~ r1(esk12_1(X3),X21)
| ( ( ~ p10(X21)
| p9(X21) )
& ( p10(X21)
| ~ p9(X21) ) ) )
& ! [X22] :
( ~ r1(esk11_1(X3),X22)
| ( ( ~ p9(X22)
| p8(X22) )
& ( p9(X22)
| ~ p8(X22) ) ) )
& ! [X23] :
( ~ r1(esk10_1(X3),X23)
| ( ( ~ p8(X23)
| p7(X23) )
& ( p8(X23)
| ~ p7(X23) ) ) )
& ! [X24] :
( ~ r1(esk9_1(X3),X24)
| ( ( ~ p7(X24)
| p6(X24) )
& ( p7(X24)
| ~ p6(X24) ) ) )
& ! [X25] :
( ~ r1(esk8_1(X3),X25)
| ( ( ~ p6(X25)
| p5(X25) )
& ( p6(X25)
| ~ p5(X25) ) ) )
& ! [X26] :
( ~ r1(esk7_1(X3),X26)
| ( ( ~ p5(X26)
| p4(X26) )
& ( p5(X26)
| ~ p4(X26) ) ) )
& ! [X27] :
( ~ r1(esk6_1(X3),X27)
| ( ( ~ p4(X27)
| p3(X27) )
& ( p4(X27)
| ~ p3(X27) ) ) )
& ! [X28] :
( ~ r1(esk5_1(X3),X28)
| ( ( ~ p3(X28)
| p2(X28) )
& ( p3(X28)
| ~ p2(X28) ) ) )
& ! [X29] :
( ~ r1(X3,X29)
| ( ( ~ p2(X29)
| p1(X29) )
& ( p2(X29)
| ~ p1(X29) ) ) )
& r1(X3,esk18_1(X3))
& ~ p15(esk18_1(X3))
& r1(X3,esk19_1(X3))
& ( p13(esk19_1(X3))
| p14(esk19_1(X3)) )
& ( ~ p14(esk19_1(X3))
| ~ p13(esk19_1(X3)) )
& ( p12(esk19_1(X3))
| p13(esk19_1(X3)) )
& ( ~ p13(esk19_1(X3))
| ~ p12(esk19_1(X3)) )
& ( p11(esk19_1(X3))
| p12(esk19_1(X3)) )
& ( ~ p12(esk19_1(X3))
| ~ p11(esk19_1(X3)) )
& ( p10(esk19_1(X3))
| p11(esk19_1(X3)) )
& ( ~ p11(esk19_1(X3))
| ~ p10(esk19_1(X3)) )
& ( p9(esk19_1(X3))
| p10(esk19_1(X3)) )
& ( ~ p10(esk19_1(X3))
| ~ p9(esk19_1(X3)) )
& ( p8(esk19_1(X3))
| p9(esk19_1(X3)) )
& ( ~ p9(esk19_1(X3))
| ~ p8(esk19_1(X3)) )
& ( p7(esk19_1(X3))
| p8(esk19_1(X3)) )
& ( ~ p8(esk19_1(X3))
| ~ p7(esk19_1(X3)) )
& ( p6(esk19_1(X3))
| p7(esk19_1(X3)) )
& ( ~ p7(esk19_1(X3))
| ~ p6(esk19_1(X3)) )
& ( p5(esk19_1(X3))
| p6(esk19_1(X3)) )
& ( ~ p6(esk19_1(X3))
| ~ p5(esk19_1(X3)) )
& ( p4(esk19_1(X3))
| p5(esk19_1(X3)) )
& ( ~ p5(esk19_1(X3))
| ~ p4(esk19_1(X3)) )
& ( p3(esk19_1(X3))
| p4(esk19_1(X3)) )
& ( ~ p4(esk19_1(X3))
| ~ p3(esk19_1(X3)) )
& ( p2(esk19_1(X3))
| p3(esk19_1(X3)) )
& ( ~ p3(esk19_1(X3))
| ~ p2(esk19_1(X3)) )
& ( p1(esk19_1(X3))
| p2(esk19_1(X3)) )
& ( ~ p2(esk19_1(X3))
| ~ p1(esk19_1(X3)) ) ) ),
inference(skolemize,[status(esa)],[24]) ).
fof(26,plain,
! [X3,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( ( ( ~ r1(X3,X29)
| ( ( ~ p2(X29)
| p1(X29) )
& ( p2(X29)
| ~ p1(X29) ) ) )
& ( ~ r1(esk5_1(X3),X28)
| ( ( ~ p3(X28)
| p2(X28) )
& ( p3(X28)
| ~ p2(X28) ) ) )
& ( ~ r1(esk6_1(X3),X27)
| ( ( ~ p4(X27)
| p3(X27) )
& ( p4(X27)
| ~ p3(X27) ) ) )
& ( ~ r1(esk7_1(X3),X26)
| ( ( ~ p5(X26)
| p4(X26) )
& ( p5(X26)
| ~ p4(X26) ) ) )
& ( ~ r1(esk8_1(X3),X25)
| ( ( ~ p6(X25)
| p5(X25) )
& ( p6(X25)
| ~ p5(X25) ) ) )
& ( ~ r1(esk9_1(X3),X24)
| ( ( ~ p7(X24)
| p6(X24) )
& ( p7(X24)
| ~ p6(X24) ) ) )
& ( ~ r1(esk10_1(X3),X23)
| ( ( ~ p8(X23)
| p7(X23) )
& ( p8(X23)
| ~ p7(X23) ) ) )
& ( ~ r1(esk11_1(X3),X22)
| ( ( ~ p9(X22)
| p8(X22) )
& ( p9(X22)
| ~ p8(X22) ) ) )
& ( ~ r1(esk12_1(X3),X21)
| ( ( ~ p10(X21)
| p9(X21) )
& ( p10(X21)
| ~ p9(X21) ) ) )
& ( ~ r1(esk13_1(X3),X20)
| ( ( ~ p11(X20)
| p10(X20) )
& ( p11(X20)
| ~ p10(X20) ) ) )
& ( ~ r1(esk14_1(X3),X19)
| ( ( ~ p12(X19)
| p11(X19) )
& ( p12(X19)
| ~ p11(X19) ) ) )
& ( ~ r1(esk15_1(X3),X18)
| ( ( ~ p13(X18)
| p12(X18) )
& ( p13(X18)
| ~ p12(X18) ) ) )
& ( ~ r1(esk16_1(X3),X17)
| ( ( ~ p14(X17)
| p13(X17) )
& ( p14(X17)
| ~ p13(X17) ) ) )
& r1(esk15_1(X3),esk16_1(X3))
& r1(esk16_1(X3),esk17_1(X3))
& $true
& r1(esk14_1(X3),esk15_1(X3))
& r1(esk13_1(X3),esk14_1(X3))
& r1(esk12_1(X3),esk13_1(X3))
& r1(esk11_1(X3),esk12_1(X3))
& r1(esk10_1(X3),esk11_1(X3))
& r1(esk9_1(X3),esk10_1(X3))
& r1(esk8_1(X3),esk9_1(X3))
& r1(esk7_1(X3),esk8_1(X3))
& r1(esk6_1(X3),esk7_1(X3))
& r1(esk5_1(X3),esk6_1(X3))
& r1(X3,esk5_1(X3))
& r1(X3,esk18_1(X3))
& ~ p15(esk18_1(X3))
& r1(X3,esk19_1(X3))
& ( p13(esk19_1(X3))
| p14(esk19_1(X3)) )
& ( ~ p14(esk19_1(X3))
| ~ p13(esk19_1(X3)) )
& ( p12(esk19_1(X3))
| p13(esk19_1(X3)) )
& ( ~ p13(esk19_1(X3))
| ~ p12(esk19_1(X3)) )
& ( p11(esk19_1(X3))
| p12(esk19_1(X3)) )
& ( ~ p12(esk19_1(X3))
| ~ p11(esk19_1(X3)) )
& ( p10(esk19_1(X3))
| p11(esk19_1(X3)) )
& ( ~ p11(esk19_1(X3))
| ~ p10(esk19_1(X3)) )
& ( p9(esk19_1(X3))
| p10(esk19_1(X3)) )
& ( ~ p10(esk19_1(X3))
| ~ p9(esk19_1(X3)) )
& ( p8(esk19_1(X3))
| p9(esk19_1(X3)) )
& ( ~ p9(esk19_1(X3))
| ~ p8(esk19_1(X3)) )
& ( p7(esk19_1(X3))
| p8(esk19_1(X3)) )
& ( ~ p8(esk19_1(X3))
| ~ p7(esk19_1(X3)) )
& ( p6(esk19_1(X3))
| p7(esk19_1(X3)) )
& ( ~ p7(esk19_1(X3))
| ~ p6(esk19_1(X3)) )
& ( p5(esk19_1(X3))
| p6(esk19_1(X3)) )
& ( ~ p6(esk19_1(X3))
| ~ p5(esk19_1(X3)) )
& ( p4(esk19_1(X3))
| p5(esk19_1(X3)) )
& ( ~ p5(esk19_1(X3))
| ~ p4(esk19_1(X3)) )
& ( p3(esk19_1(X3))
| p4(esk19_1(X3)) )
& ( ~ p4(esk19_1(X3))
| ~ p3(esk19_1(X3)) )
& ( p2(esk19_1(X3))
| p3(esk19_1(X3)) )
& ( ~ p3(esk19_1(X3))
| ~ p2(esk19_1(X3)) )
& ( p1(esk19_1(X3))
| p2(esk19_1(X3)) )
& ( ~ p2(esk19_1(X3))
| ~ p1(esk19_1(X3)) ) )
| ~ epred1_1(X3) ),
inference(shift_quantors,[status(thm)],[25]) ).
fof(27,plain,
! [X3,X17,X18,X19,X20,X21,X22,X23,X24,X25,X26,X27,X28,X29] :
( ( ~ p2(X29)
| p1(X29)
| ~ r1(X3,X29)
| ~ epred1_1(X3) )
& ( p2(X29)
| ~ p1(X29)
| ~ r1(X3,X29)
| ~ epred1_1(X3) )
& ( ~ p3(X28)
| p2(X28)
| ~ r1(esk5_1(X3),X28)
| ~ epred1_1(X3) )
& ( p3(X28)
| ~ p2(X28)
| ~ r1(esk5_1(X3),X28)
| ~ epred1_1(X3) )
& ( ~ p4(X27)
| p3(X27)
| ~ r1(esk6_1(X3),X27)
| ~ epred1_1(X3) )
& ( p4(X27)
| ~ p3(X27)
| ~ r1(esk6_1(X3),X27)
| ~ epred1_1(X3) )
& ( ~ p5(X26)
| p4(X26)
| ~ r1(esk7_1(X3),X26)
| ~ epred1_1(X3) )
& ( p5(X26)
| ~ p4(X26)
| ~ r1(esk7_1(X3),X26)
| ~ epred1_1(X3) )
& ( ~ p6(X25)
| p5(X25)
| ~ r1(esk8_1(X3),X25)
| ~ epred1_1(X3) )
& ( p6(X25)
| ~ p5(X25)
| ~ r1(esk8_1(X3),X25)
| ~ epred1_1(X3) )
& ( ~ p7(X24)
| p6(X24)
| ~ r1(esk9_1(X3),X24)
| ~ epred1_1(X3) )
& ( p7(X24)
| ~ p6(X24)
| ~ r1(esk9_1(X3),X24)
| ~ epred1_1(X3) )
& ( ~ p8(X23)
| p7(X23)
| ~ r1(esk10_1(X3),X23)
| ~ epred1_1(X3) )
& ( p8(X23)
| ~ p7(X23)
| ~ r1(esk10_1(X3),X23)
| ~ epred1_1(X3) )
& ( ~ p9(X22)
| p8(X22)
| ~ r1(esk11_1(X3),X22)
| ~ epred1_1(X3) )
& ( p9(X22)
| ~ p8(X22)
| ~ r1(esk11_1(X3),X22)
| ~ epred1_1(X3) )
& ( ~ p10(X21)
| p9(X21)
| ~ r1(esk12_1(X3),X21)
| ~ epred1_1(X3) )
& ( p10(X21)
| ~ p9(X21)
| ~ r1(esk12_1(X3),X21)
| ~ epred1_1(X3) )
& ( ~ p11(X20)
| p10(X20)
| ~ r1(esk13_1(X3),X20)
| ~ epred1_1(X3) )
& ( p11(X20)
| ~ p10(X20)
| ~ r1(esk13_1(X3),X20)
| ~ epred1_1(X3) )
& ( ~ p12(X19)
| p11(X19)
| ~ r1(esk14_1(X3),X19)
| ~ epred1_1(X3) )
& ( p12(X19)
| ~ p11(X19)
| ~ r1(esk14_1(X3),X19)
| ~ epred1_1(X3) )
& ( ~ p13(X18)
| p12(X18)
| ~ r1(esk15_1(X3),X18)
| ~ epred1_1(X3) )
& ( p13(X18)
| ~ p12(X18)
| ~ r1(esk15_1(X3),X18)
| ~ epred1_1(X3) )
& ( ~ p14(X17)
| p13(X17)
| ~ r1(esk16_1(X3),X17)
| ~ epred1_1(X3) )
& ( p14(X17)
| ~ p13(X17)
| ~ r1(esk16_1(X3),X17)
| ~ epred1_1(X3) )
& ( r1(esk15_1(X3),esk16_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk16_1(X3),esk17_1(X3))
| ~ epred1_1(X3) )
& ( $true
| ~ epred1_1(X3) )
& ( r1(esk14_1(X3),esk15_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk13_1(X3),esk14_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk12_1(X3),esk13_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk11_1(X3),esk12_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk10_1(X3),esk11_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk9_1(X3),esk10_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk8_1(X3),esk9_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk7_1(X3),esk8_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk6_1(X3),esk7_1(X3))
| ~ epred1_1(X3) )
& ( r1(esk5_1(X3),esk6_1(X3))
| ~ epred1_1(X3) )
& ( r1(X3,esk5_1(X3))
| ~ epred1_1(X3) )
& ( r1(X3,esk18_1(X3))
| ~ epred1_1(X3) )
& ( ~ p15(esk18_1(X3))
| ~ epred1_1(X3) )
& ( r1(X3,esk19_1(X3))
| ~ epred1_1(X3) )
& ( p13(esk19_1(X3))
| p14(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p14(esk19_1(X3))
| ~ p13(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p12(esk19_1(X3))
| p13(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p13(esk19_1(X3))
| ~ p12(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p11(esk19_1(X3))
| p12(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p12(esk19_1(X3))
| ~ p11(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p10(esk19_1(X3))
| p11(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p11(esk19_1(X3))
| ~ p10(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p9(esk19_1(X3))
| p10(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p10(esk19_1(X3))
| ~ p9(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p8(esk19_1(X3))
| p9(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p9(esk19_1(X3))
| ~ p8(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p7(esk19_1(X3))
| p8(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p8(esk19_1(X3))
| ~ p7(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p6(esk19_1(X3))
| p7(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p7(esk19_1(X3))
| ~ p6(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p5(esk19_1(X3))
| p6(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p6(esk19_1(X3))
| ~ p5(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p4(esk19_1(X3))
| p5(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p5(esk19_1(X3))
| ~ p4(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p3(esk19_1(X3))
| p4(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p4(esk19_1(X3))
| ~ p3(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p2(esk19_1(X3))
| p3(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p3(esk19_1(X3))
| ~ p2(esk19_1(X3))
| ~ epred1_1(X3) )
& ( p1(esk19_1(X3))
| p2(esk19_1(X3))
| ~ epred1_1(X3) )
& ( ~ p2(esk19_1(X3))
| ~ p1(esk19_1(X3))
| ~ epred1_1(X3) ) ),
inference(distribute,[status(thm)],[26]) ).
cnf(28,plain,
( ~ epred1_1(X1)
| ~ p1(esk19_1(X1))
| ~ p2(esk19_1(X1)) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(29,plain,
( p2(esk19_1(X1))
| p1(esk19_1(X1))
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(54,plain,
( r1(X1,esk19_1(X1))
| ~ epred1_1(X1) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(95,plain,
( p2(X2)
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ p1(X2) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(96,plain,
( p1(X2)
| ~ epred1_1(X1)
| ~ r1(X1,X2)
| ~ p2(X2) ),
inference(split_conjunct,[status(thm)],[27]) ).
cnf(97,negated_conjecture,
epred1_1(esk4_0),
inference(spm,[status(thm)],[17,22,theory(equality)]) ).
cnf(123,plain,
( epred1_1(esk19_1(esk4_0))
| ~ epred1_1(esk4_0) ),
inference(spm,[status(thm)],[17,54,theory(equality)]) ).
cnf(124,plain,
( p2(esk19_1(X1))
| ~ epred1_1(X1)
| ~ p1(esk19_1(X1)) ),
inference(spm,[status(thm)],[95,54,theory(equality)]) ).
cnf(244,plain,
( p1(X1)
| ~ epred1_1(X1)
| ~ p2(X1) ),
inference(spm,[status(thm)],[96,22,theory(equality)]) ).
cnf(298,plain,
( epred1_1(esk19_1(esk4_0))
| $false ),
inference(rw,[status(thm)],[123,97,theory(equality)]) ).
cnf(299,plain,
epred1_1(esk19_1(esk4_0)),
inference(cn,[status(thm)],[298,theory(equality)]) ).
cnf(318,plain,
( p2(esk19_1(X1))
| ~ epred1_1(X1) ),
inference(csr,[status(thm)],[124,29]) ).
cnf(319,plain,
( ~ epred1_1(X1)
| ~ p1(esk19_1(X1)) ),
inference(spm,[status(thm)],[28,318,theory(equality)]) ).
cnf(321,plain,
( ~ epred1_1(X1)
| ~ epred1_1(esk19_1(X1))
| ~ p2(esk19_1(X1)) ),
inference(spm,[status(thm)],[319,244,theory(equality)]) ).
cnf(323,plain,
( ~ epred1_1(esk19_1(X1))
| ~ epred1_1(X1) ),
inference(csr,[status(thm)],[321,318]) ).
cnf(324,plain,
~ epred1_1(esk4_0),
inference(spm,[status(thm)],[323,299,theory(equality)]) ).
cnf(325,plain,
$false,
inference(rw,[status(thm)],[324,97,theory(equality)]) ).
cnf(326,plain,
$false,
inference(cn,[status(thm)],[325,theory(equality)]) ).
cnf(327,plain,
$false,
326,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/LCL/LCL686+1.005.p
% --creating new selector for []
% -running prover on /tmp/tmpaNgS7-/sel_LCL686+1.005.p_1 with time limit 29
% -prover status Theorem
% Problem LCL686+1.005.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/LCL/LCL686+1.005.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/LCL/LCL686+1.005.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------