%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : KRS103+1 : TPTP v5.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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 12:59:45 EST 2010
% Result : Unsatisfiable 0.20s
% Output : CNFRefutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 29
% Syntax : Number of formulae : 163 ( 5 unt; 0 def)
% Number of atoms : 543 ( 0 equ)
% Maximal formula atoms : 4 ( 3 avg)
% Number of connectives : 582 ( 202 ~; 352 |; 8 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-1 aty)
% Number of functors : 1 ( 1 usr; 1 con; 0-0 aty)
% Number of variables : 159 ( 1 sgn 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus5(X1)
| cminus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_15) ).
fof(5,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cminus4(X1)
| cplus6(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_10) ).
fof(9,axiom,
! [X1] :
~ ( cplus4(X1)
& cminus4(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_50) ).
fof(10,axiom,
! [X1] :
~ ( cminus7(X1)
& cplus7(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_51) ).
fof(11,axiom,
! [X1] :
~ ( cplus3(X1)
& cminus3(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_52) ).
fof(12,axiom,
! [X1] :
~ ( cplus5(X1)
& cminus5(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_53) ).
fof(13,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cplus6(X1)
| cplus9(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_18) ).
fof(15,axiom,
! [X1] :
~ ( cplus6(X1)
& cminus6(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_56) ).
fof(17,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cminus5(X1)
| cminus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_3) ).
fof(22,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus7(X1)
| cplus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_4) ).
fof(24,axiom,
! [X1] :
( cTest(X1)
=> ( cminus7(X1)
| cplus9(X1)
| cminus6(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_8) ).
fof(25,axiom,
! [X1] :
( cTest(X1)
=> ( cminus9(X1)
| cminus4(X1)
| cminus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_9) ).
fof(26,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cminus3(X1)
| cminus7(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_29) ).
fof(27,axiom,
! [X1] :
( cTest(X1)
=> ( cminus9(X1)
| cplus3(X1)
| cplus4(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_28) ).
fof(28,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus4(X1)
| cplus9(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_25) ).
fof(32,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cplus4(X1)
| cminus6(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_21) ).
fof(33,axiom,
! [X1] :
( cTest(X1)
=> ( cminus3(X1)
| cplus2(X1)
| cplus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_20) ).
fof(35,axiom,
! [X1] :
( cTest(X1)
=> ( cminus2(X1)
| cplus6(X1)
| cminus7(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_22) ).
fof(36,axiom,
! [X1] :
~ ( cminus9(X1)
& cplus9(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_49) ).
fof(37,axiom,
! [X1] :
~ ( cminus8(X1)
& cplus8(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_48) ).
fof(39,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cminus3(X1)
| cplus6(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_42) ).
fof(42,axiom,
cTest(i2003_11_14_17_20_46476),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_47) ).
fof(44,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cplus2(X1)
| cplus8(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_45) ).
fof(47,axiom,
! [X1] :
~ ( cminus2(X1)
& cplus2(X1) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_54) ).
fof(48,axiom,
! [X1] :
( cTest(X1)
=> ( cplus3(X1)
| cplus4(X1)
| cplus6(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_38) ).
fof(51,axiom,
! [X1] :
( cTest(X1)
=> ( cminus9(X1)
| cminus2(X1)
| cplus7(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_33) ).
fof(53,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cminus8(X1)
| cplus9(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_31) ).
fof(56,axiom,
! [X1] :
( cTest(X1)
=> ( cminus4(X1)
| cplus9(X1)
| cplus7(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_34) ).
fof(57,axiom,
! [X1] :
( cTest(X1)
=> ( cminus9(X1)
| cminus2(X1)
| cplus3(X1) ) ),
file('/tmp/tmpKsiKFD/sel_KRS103+1.p_1',axiom_35) ).
fof(63,plain,
! [X1] :
( ~ cTest(X1)
| cminus3(X1)
| cplus5(X1)
| cminus8(X1) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(64,plain,
! [X2] :
( ~ cTest(X2)
| cminus3(X2)
| cplus5(X2)
| cminus8(X2) ),
inference(variable_rename,[status(thm)],[63]) ).
cnf(65,plain,
( cminus8(X1)
| cplus5(X1)
| cminus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[64]) ).
fof(72,plain,
! [X1] :
( ~ cTest(X1)
| cplus3(X1)
| cminus4(X1)
| cplus6(X1) ),
inference(fof_nnf,[status(thm)],[5]) ).
fof(73,plain,
! [X2] :
( ~ cTest(X2)
| cplus3(X2)
| cminus4(X2)
| cplus6(X2) ),
inference(variable_rename,[status(thm)],[72]) ).
cnf(74,plain,
( cplus6(X1)
| cminus4(X1)
| cplus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[73]) ).
fof(84,plain,
! [X1] :
( ~ cplus4(X1)
| ~ cminus4(X1) ),
inference(fof_nnf,[status(thm)],[9]) ).
fof(85,plain,
! [X2] :
( ~ cplus4(X2)
| ~ cminus4(X2) ),
inference(variable_rename,[status(thm)],[84]) ).
cnf(86,plain,
( ~ cminus4(X1)
| ~ cplus4(X1) ),
inference(split_conjunct,[status(thm)],[85]) ).
fof(87,plain,
! [X1] :
( ~ cminus7(X1)
| ~ cplus7(X1) ),
inference(fof_nnf,[status(thm)],[10]) ).
fof(88,plain,
! [X2] :
( ~ cminus7(X2)
| ~ cplus7(X2) ),
inference(variable_rename,[status(thm)],[87]) ).
cnf(89,plain,
( ~ cplus7(X1)
| ~ cminus7(X1) ),
inference(split_conjunct,[status(thm)],[88]) ).
fof(90,plain,
! [X1] :
( ~ cplus3(X1)
| ~ cminus3(X1) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(91,plain,
! [X2] :
( ~ cplus3(X2)
| ~ cminus3(X2) ),
inference(variable_rename,[status(thm)],[90]) ).
cnf(92,plain,
( ~ cminus3(X1)
| ~ cplus3(X1) ),
inference(split_conjunct,[status(thm)],[91]) ).
fof(93,plain,
! [X1] :
( ~ cplus5(X1)
| ~ cminus5(X1) ),
inference(fof_nnf,[status(thm)],[12]) ).
fof(94,plain,
! [X2] :
( ~ cplus5(X2)
| ~ cminus5(X2) ),
inference(variable_rename,[status(thm)],[93]) ).
cnf(95,plain,
( ~ cminus5(X1)
| ~ cplus5(X1) ),
inference(split_conjunct,[status(thm)],[94]) ).
fof(96,plain,
! [X1] :
( ~ cTest(X1)
| cminus2(X1)
| cplus6(X1)
| cplus9(X1) ),
inference(fof_nnf,[status(thm)],[13]) ).
fof(97,plain,
! [X2] :
( ~ cTest(X2)
| cminus2(X2)
| cplus6(X2)
| cplus9(X2) ),
inference(variable_rename,[status(thm)],[96]) ).
cnf(98,plain,
( cplus9(X1)
| cplus6(X1)
| cminus2(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[97]) ).
fof(102,plain,
! [X1] :
( ~ cplus6(X1)
| ~ cminus6(X1) ),
inference(fof_nnf,[status(thm)],[15]) ).
fof(103,plain,
! [X2] :
( ~ cplus6(X2)
| ~ cminus6(X2) ),
inference(variable_rename,[status(thm)],[102]) ).
cnf(104,plain,
( ~ cminus6(X1)
| ~ cplus6(X1) ),
inference(split_conjunct,[status(thm)],[103]) ).
fof(108,plain,
! [X1] :
( ~ cTest(X1)
| cminus3(X1)
| cminus5(X1)
| cminus8(X1) ),
inference(fof_nnf,[status(thm)],[17]) ).
fof(109,plain,
! [X2] :
( ~ cTest(X2)
| cminus3(X2)
| cminus5(X2)
| cminus8(X2) ),
inference(variable_rename,[status(thm)],[108]) ).
cnf(110,plain,
( cminus8(X1)
| cminus5(X1)
| cminus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[109]) ).
fof(124,plain,
! [X1] :
( ~ cTest(X1)
| cminus3(X1)
| cplus7(X1)
| cplus8(X1) ),
inference(fof_nnf,[status(thm)],[22]) ).
fof(125,plain,
! [X2] :
( ~ cTest(X2)
| cminus3(X2)
| cplus7(X2)
| cplus8(X2) ),
inference(variable_rename,[status(thm)],[124]) ).
cnf(126,plain,
( cplus8(X1)
| cplus7(X1)
| cminus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[125]) ).
fof(130,plain,
! [X1] :
( ~ cTest(X1)
| cminus7(X1)
| cplus9(X1)
| cminus6(X1) ),
inference(fof_nnf,[status(thm)],[24]) ).
fof(131,plain,
! [X2] :
( ~ cTest(X2)
| cminus7(X2)
| cplus9(X2)
| cminus6(X2) ),
inference(variable_rename,[status(thm)],[130]) ).
cnf(132,plain,
( cminus6(X1)
| cplus9(X1)
| cminus7(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[131]) ).
fof(133,plain,
! [X1] :
( ~ cTest(X1)
| cminus9(X1)
| cminus4(X1)
| cminus8(X1) ),
inference(fof_nnf,[status(thm)],[25]) ).
fof(134,plain,
! [X2] :
( ~ cTest(X2)
| cminus9(X2)
| cminus4(X2)
| cminus8(X2) ),
inference(variable_rename,[status(thm)],[133]) ).
cnf(135,plain,
( cminus8(X1)
| cminus4(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[134]) ).
fof(136,plain,
! [X1] :
( ~ cTest(X1)
| cminus4(X1)
| cminus3(X1)
| cminus7(X1) ),
inference(fof_nnf,[status(thm)],[26]) ).
fof(137,plain,
! [X2] :
( ~ cTest(X2)
| cminus4(X2)
| cminus3(X2)
| cminus7(X2) ),
inference(variable_rename,[status(thm)],[136]) ).
cnf(138,plain,
( cminus7(X1)
| cminus3(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[137]) ).
fof(139,plain,
! [X1] :
( ~ cTest(X1)
| cminus9(X1)
| cplus3(X1)
| cplus4(X1) ),
inference(fof_nnf,[status(thm)],[27]) ).
fof(140,plain,
! [X2] :
( ~ cTest(X2)
| cminus9(X2)
| cplus3(X2)
| cplus4(X2) ),
inference(variable_rename,[status(thm)],[139]) ).
cnf(141,plain,
( cplus4(X1)
| cplus3(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[140]) ).
fof(142,plain,
! [X1] :
( ~ cTest(X1)
| cplus3(X1)
| cplus4(X1)
| cplus9(X1) ),
inference(fof_nnf,[status(thm)],[28]) ).
fof(143,plain,
! [X2] :
( ~ cTest(X2)
| cplus3(X2)
| cplus4(X2)
| cplus9(X2) ),
inference(variable_rename,[status(thm)],[142]) ).
cnf(144,plain,
( cplus9(X1)
| cplus4(X1)
| cplus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[143]) ).
fof(154,plain,
! [X1] :
( ~ cTest(X1)
| cminus2(X1)
| cplus4(X1)
| cminus6(X1) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(155,plain,
! [X2] :
( ~ cTest(X2)
| cminus2(X2)
| cplus4(X2)
| cminus6(X2) ),
inference(variable_rename,[status(thm)],[154]) ).
cnf(156,plain,
( cminus6(X1)
| cplus4(X1)
| cminus2(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[155]) ).
fof(157,plain,
! [X1] :
( ~ cTest(X1)
| cminus3(X1)
| cplus2(X1)
| cplus8(X1) ),
inference(fof_nnf,[status(thm)],[33]) ).
fof(158,plain,
! [X2] :
( ~ cTest(X2)
| cminus3(X2)
| cplus2(X2)
| cplus8(X2) ),
inference(variable_rename,[status(thm)],[157]) ).
cnf(159,plain,
( cplus8(X1)
| cplus2(X1)
| cminus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[158]) ).
fof(163,plain,
! [X1] :
( ~ cTest(X1)
| cminus2(X1)
| cplus6(X1)
| cminus7(X1) ),
inference(fof_nnf,[status(thm)],[35]) ).
fof(164,plain,
! [X2] :
( ~ cTest(X2)
| cminus2(X2)
| cplus6(X2)
| cminus7(X2) ),
inference(variable_rename,[status(thm)],[163]) ).
cnf(165,plain,
( cminus7(X1)
| cplus6(X1)
| cminus2(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[164]) ).
fof(166,plain,
! [X1] :
( ~ cminus9(X1)
| ~ cplus9(X1) ),
inference(fof_nnf,[status(thm)],[36]) ).
fof(167,plain,
! [X2] :
( ~ cminus9(X2)
| ~ cplus9(X2) ),
inference(variable_rename,[status(thm)],[166]) ).
cnf(168,plain,
( ~ cplus9(X1)
| ~ cminus9(X1) ),
inference(split_conjunct,[status(thm)],[167]) ).
fof(169,plain,
! [X1] :
( ~ cminus8(X1)
| ~ cplus8(X1) ),
inference(fof_nnf,[status(thm)],[37]) ).
fof(170,plain,
! [X2] :
( ~ cminus8(X2)
| ~ cplus8(X2) ),
inference(variable_rename,[status(thm)],[169]) ).
cnf(171,plain,
( ~ cplus8(X1)
| ~ cminus8(X1) ),
inference(split_conjunct,[status(thm)],[170]) ).
fof(175,plain,
! [X1] :
( ~ cTest(X1)
| cminus4(X1)
| cminus3(X1)
| cplus6(X1) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(176,plain,
! [X2] :
( ~ cTest(X2)
| cminus4(X2)
| cminus3(X2)
| cplus6(X2) ),
inference(variable_rename,[status(thm)],[175]) ).
cnf(177,plain,
( cplus6(X1)
| cminus3(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[176]) ).
cnf(184,plain,
cTest(i2003_11_14_17_20_46476),
inference(split_conjunct,[status(thm)],[42]) ).
fof(188,plain,
! [X1] :
( ~ cTest(X1)
| cminus4(X1)
| cplus2(X1)
| cplus8(X1) ),
inference(fof_nnf,[status(thm)],[44]) ).
fof(189,plain,
! [X2] :
( ~ cTest(X2)
| cminus4(X2)
| cplus2(X2)
| cplus8(X2) ),
inference(variable_rename,[status(thm)],[188]) ).
cnf(190,plain,
( cplus8(X1)
| cplus2(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[189]) ).
fof(197,plain,
! [X1] :
( ~ cminus2(X1)
| ~ cplus2(X1) ),
inference(fof_nnf,[status(thm)],[47]) ).
fof(198,plain,
! [X2] :
( ~ cminus2(X2)
| ~ cplus2(X2) ),
inference(variable_rename,[status(thm)],[197]) ).
cnf(199,plain,
( ~ cplus2(X1)
| ~ cminus2(X1) ),
inference(split_conjunct,[status(thm)],[198]) ).
fof(200,plain,
! [X1] :
( ~ cTest(X1)
| cplus3(X1)
| cplus4(X1)
| cplus6(X1) ),
inference(fof_nnf,[status(thm)],[48]) ).
fof(201,plain,
! [X2] :
( ~ cTest(X2)
| cplus3(X2)
| cplus4(X2)
| cplus6(X2) ),
inference(variable_rename,[status(thm)],[200]) ).
cnf(202,plain,
( cplus6(X1)
| cplus4(X1)
| cplus3(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[201]) ).
fof(209,plain,
! [X1] :
( ~ cTest(X1)
| cminus9(X1)
| cminus2(X1)
| cplus7(X1) ),
inference(fof_nnf,[status(thm)],[51]) ).
fof(210,plain,
! [X2] :
( ~ cTest(X2)
| cminus9(X2)
| cminus2(X2)
| cplus7(X2) ),
inference(variable_rename,[status(thm)],[209]) ).
cnf(211,plain,
( cplus7(X1)
| cminus2(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[210]) ).
fof(215,plain,
! [X1] :
( ~ cTest(X1)
| cminus4(X1)
| cminus8(X1)
| cplus9(X1) ),
inference(fof_nnf,[status(thm)],[53]) ).
fof(216,plain,
! [X2] :
( ~ cTest(X2)
| cminus4(X2)
| cminus8(X2)
| cplus9(X2) ),
inference(variable_rename,[status(thm)],[215]) ).
cnf(217,plain,
( cplus9(X1)
| cminus8(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[216]) ).
fof(224,plain,
! [X1] :
( ~ cTest(X1)
| cminus4(X1)
| cplus9(X1)
| cplus7(X1) ),
inference(fof_nnf,[status(thm)],[56]) ).
fof(225,plain,
! [X2] :
( ~ cTest(X2)
| cminus4(X2)
| cplus9(X2)
| cplus7(X2) ),
inference(variable_rename,[status(thm)],[224]) ).
cnf(226,plain,
( cplus7(X1)
| cplus9(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[225]) ).
fof(227,plain,
! [X1] :
( ~ cTest(X1)
| cminus9(X1)
| cminus2(X1)
| cplus3(X1) ),
inference(fof_nnf,[status(thm)],[57]) ).
fof(228,plain,
! [X2] :
( ~ cTest(X2)
| cminus9(X2)
| cminus2(X2)
| cplus3(X2) ),
inference(variable_rename,[status(thm)],[227]) ).
cnf(229,plain,
( cplus3(X1)
| cminus2(X1)
| cminus9(X1)
| ~ cTest(X1) ),
inference(split_conjunct,[status(thm)],[228]) ).
cnf(231,plain,
( cplus2(X1)
| cminus4(X1)
| ~ cminus8(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[171,190,theory(equality)]) ).
cnf(233,plain,
( cplus6(X1)
| cminus4(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[92,177,theory(equality)]) ).
cnf(236,plain,
( cminus8(X1)
| cminus4(X1)
| ~ cplus9(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[168,135,theory(equality)]) ).
cnf(239,plain,
( cplus9(X1)
| cminus4(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[89,226,theory(equality)]) ).
cnf(241,plain,
( cminus3(X1)
| cplus2(X1)
| ~ cminus8(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[171,159,theory(equality)]) ).
cnf(249,plain,
( cminus8(X1)
| cminus3(X1)
| ~ cminus5(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[95,65,theory(equality)]) ).
cnf(250,plain,
( cplus8(X1)
| cminus3(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[89,126,theory(equality)]) ).
cnf(252,plain,
( cplus3(X1)
| cplus6(X1)
| ~ cminus4(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[86,202,theory(equality)]) ).
cnf(254,plain,
( cplus9(X1)
| cminus7(X1)
| ~ cplus6(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[104,132,theory(equality)]) ).
cnf(256,plain,
( cplus4(X1)
| cplus3(X1)
| ~ cplus9(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[168,141,theory(equality)]) ).
cnf(257,plain,
( cminus2(X1)
| cplus3(X1)
| ~ cplus9(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[168,229,theory(equality)]) ).
cnf(258,plain,
( cminus2(X1)
| cplus4(X1)
| ~ cplus6(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[104,156,theory(equality)]) ).
cnf(260,plain,
( cminus9(X1)
| cminus2(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[89,211,theory(equality)]) ).
cnf(263,plain,
( cminus4(X1)
| ~ cminus2(X1)
| ~ cminus8(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[199,231,theory(equality)]) ).
cnf(264,plain,
( cplus6(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[233,74]) ).
cnf(270,plain,
( cminus8(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[236,217]) ).
cnf(275,plain,
( cplus2(X1)
| ~ cplus3(X1)
| ~ cminus8(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[92,241,theory(equality)]) ).
cnf(287,plain,
( cminus8(X1)
| cminus3(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[249,110]) ).
cnf(288,plain,
( cminus8(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[92,287,theory(equality)]) ).
cnf(289,plain,
( cminus3(X1)
| ~ cminus8(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[171,250,theory(equality)]) ).
cnf(294,plain,
( cplus3(X1)
| cplus6(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[252,264]) ).
cnf(297,plain,
( cplus9(X1)
| cminus4(X1)
| ~ cTest(X1)
| ~ cplus6(X1) ),
inference(spm,[status(thm)],[239,254,theory(equality)]) ).
cnf(299,plain,
( cplus4(X1)
| cplus3(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[256,144]) ).
cnf(306,plain,
( cminus2(X1)
| ~ cplus9(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[168,260,theory(equality)]) ).
cnf(307,plain,
( cminus4(X1)
| ~ cminus2(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[263,270]) ).
cnf(311,plain,
( cminus4(X1)
| cplus3(X1)
| ~ cTest(X1)
| ~ cplus9(X1) ),
inference(spm,[status(thm)],[307,257,theory(equality)]) ).
cnf(321,plain,
( cplus2(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[275,288]) ).
cnf(322,plain,
( ~ cminus2(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[199,321,theory(equality)]) ).
cnf(324,plain,
( cplus9(X1)
| cplus6(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[322,98,theory(equality)]) ).
cnf(327,plain,
( cplus4(X1)
| ~ cplus3(X1)
| ~ cTest(X1)
| ~ cplus6(X1) ),
inference(spm,[status(thm)],[322,258,theory(equality)]) ).
cnf(337,plain,
( cminus3(X1)
| ~ cminus7(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[289,287]) ).
cnf(338,plain,
( cminus3(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[337,138,theory(equality)]) ).
cnf(344,plain,
( cminus4(X1)
| ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[92,338,theory(equality)]) ).
cnf(347,plain,
( cplus9(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[297,264]) ).
cnf(349,plain,
( cminus2(X1)
| cplus6(X1)
| ~ cplus9(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[306,165,theory(equality)]) ).
cnf(356,plain,
( cplus3(X1)
| cminus4(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[311,347]) ).
cnf(357,plain,
( cminus4(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[356,344]) ).
cnf(358,plain,
( cplus9(X1)
| cplus6(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[324,294]) ).
cnf(359,plain,
( cplus4(X1)
| ~ cplus6(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[327,299]) ).
cnf(360,plain,
( ~ cminus4(X1)
| ~ cplus6(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[86,359,theory(equality)]) ).
cnf(365,plain,
( ~ cplus6(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[360,357]) ).
cnf(366,plain,
( cplus9(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[365,358,theory(equality)]) ).
cnf(369,plain,
( cminus2(X1)
| cplus6(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[349,366]) ).
cnf(370,plain,
( cminus2(X1)
| ~ cTest(X1) ),
inference(csr,[status(thm)],[369,365]) ).
cnf(371,plain,
( ~ cplus3(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[322,370,theory(equality)]) ).
cnf(373,plain,
( cplus6(X1)
| ~ cTest(X1) ),
inference(spm,[status(thm)],[371,294,theory(equality)]) ).
cnf(375,plain,
~ cTest(X1),
inference(csr,[status(thm)],[373,365]) ).
cnf(376,plain,
$false,
inference(sr,[status(thm)],[184,375,theory(equality)]) ).
cnf(377,plain,
$false,
376,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/KRS/KRS103+1.p
% --creating new selector for []
% -running prover on /tmp/tmpKsiKFD/sel_KRS103+1.p_1 with time limit 29
% -prover status Unsatisfiable
% Problem KRS103+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/KRS/KRS103+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/KRS/KRS103+1.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Unsatisfiable
% # SZS output start CNFRefutation.
% See solution above
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------