%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : KRS154+1 : TPTP v5.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art03.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 13:03:22 EST 2010
% Result : Theorem 0.35s
% Output : CNFRefutation 0.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 23
% Syntax : Number of formulae : 138 ( 35 unt; 0 def)
% Number of atoms : 599 ( 0 equ)
% Maximal formula atoms : 26 ( 4 avg)
% Number of connectives : 804 ( 343 ~; 350 |; 98 &)
% ( 13 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 25 ( 24 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 65 ( 2 sgn 45 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(11,axiom,
cC10xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_167) ).
fof(16,axiom,
cC34(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_162) ).
fof(17,axiom,
cC86xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_161) ).
fof(18,axiom,
cC134xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_160) ).
fof(19,axiom,
cC92xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_168) ).
fof(32,axiom,
! [X1] :
( cC110(X1)
<=> ( cC102xcomp(X1)
& cC108xcomp(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_15) ).
fof(43,axiom,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_0) ).
fof(44,axiom,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_1) ).
fof(60,axiom,
! [X1] :
( cC80(X1)
<=> ( cC78xcomp(X1)
& cC76xcomp(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_117) ).
fof(69,axiom,
! [X1] :
( cC58(X1)
<=> ( cC34(X1)
& cC56(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_94) ).
fof(76,axiom,
! [X1] :
( cC56(X1)
<=> ( cC4(X1)
& cC10xcomp(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_93) ).
fof(98,conjecture,
( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC58(iV822576)
& cC116(iV822576)
& cC114(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& cC80(iV822576)
& cC110(iV822576)
& cC136(iV822576)
& cC56(iV822576) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',the_axiom) ).
fof(101,axiom,
! [X1] :
( cC94(X1)
<=> ( cC86xcomp(X1)
& cC92xcomp(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_136) ).
fof(136,axiom,
cC102xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_147) ).
fof(138,axiom,
cC4(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_149) ).
fof(139,axiom,
cC108xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_148) ).
fof(146,axiom,
! [X1] :
( cC114(X1)
<=> ( cC112xcomp(X1)
& cC96xcomp(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_21) ).
fof(149,axiom,
! [X1] :
( cC116(X1)
<=> ( cC114(X1)
& cC80(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_22) ).
fof(153,axiom,
! [X1] :
( cC136(X1)
<=> ( cC134xcomp(X1)
& cC116(X1) ) ),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_42) ).
fof(161,axiom,
cC76xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_152) ).
fof(162,axiom,
cC96xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_153) ).
fof(164,axiom,
cC112xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_151) ).
fof(169,axiom,
cC78xcomp(iV822576),
file('/tmp/tmp1TDx_p/sel_KRS154+1.p_1',axiom_158) ).
fof(171,negated_conjecture,
~ ( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC58(iV822576)
& cC116(iV822576)
& cC114(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& cC80(iV822576)
& cC110(iV822576)
& cC136(iV822576)
& cC56(iV822576) ),
inference(assume_negation,[status(cth)],[98]) ).
fof(172,plain,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
inference(fof_simplification,[status(thm)],[43,theory(equality)]) ).
fof(173,plain,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
inference(fof_simplification,[status(thm)],[44,theory(equality)]) ).
fof(174,negated_conjecture,
~ ( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC58(iV822576)
& cC116(iV822576)
& cC114(iV822576)
& cowlThing(iV822576)
& cC94(iV822576)
& cC80(iV822576)
& cC110(iV822576)
& cC136(iV822576)
& cC56(iV822576) ),
inference(fof_simplification,[status(thm)],[171,theory(equality)]) ).
cnf(237,plain,
cC10xcomp(iV822576),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(244,plain,
cC34(iV822576),
inference(split_conjunct,[status(thm)],[16]) ).
cnf(245,plain,
cC86xcomp(iV822576),
inference(split_conjunct,[status(thm)],[17]) ).
cnf(246,plain,
cC134xcomp(iV822576),
inference(split_conjunct,[status(thm)],[18]) ).
cnf(247,plain,
cC92xcomp(iV822576),
inference(split_conjunct,[status(thm)],[19]) ).
fof(322,plain,
! [X1] :
( ( ~ cC110(X1)
| ( cC102xcomp(X1)
& cC108xcomp(X1) ) )
& ( ~ cC102xcomp(X1)
| ~ cC108xcomp(X1)
| cC110(X1) ) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(323,plain,
! [X2] :
( ( ~ cC110(X2)
| ( cC102xcomp(X2)
& cC108xcomp(X2) ) )
& ( ~ cC102xcomp(X2)
| ~ cC108xcomp(X2)
| cC110(X2) ) ),
inference(variable_rename,[status(thm)],[322]) ).
fof(324,plain,
! [X2] :
( ( cC102xcomp(X2)
| ~ cC110(X2) )
& ( cC108xcomp(X2)
| ~ cC110(X2) )
& ( ~ cC102xcomp(X2)
| ~ cC108xcomp(X2)
| cC110(X2) ) ),
inference(distribute,[status(thm)],[323]) ).
cnf(325,plain,
( cC110(X1)
| ~ cC108xcomp(X1)
| ~ cC102xcomp(X1) ),
inference(split_conjunct,[status(thm)],[324]) ).
fof(390,plain,
! [X2] :
( cowlThing(X2)
& ~ cowlNothing(X2) ),
inference(variable_rename,[status(thm)],[172]) ).
cnf(391,plain,
~ cowlNothing(X1),
inference(split_conjunct,[status(thm)],[390]) ).
cnf(392,plain,
cowlThing(X1),
inference(split_conjunct,[status(thm)],[390]) ).
fof(393,plain,
! [X1] :
( ( ~ xsd_string(X1)
| ~ xsd_integer(X1) )
& ( xsd_integer(X1)
| xsd_string(X1) ) ),
inference(fof_nnf,[status(thm)],[173]) ).
fof(394,plain,
! [X2] :
( ( ~ xsd_string(X2)
| ~ xsd_integer(X2) )
& ( xsd_integer(X2)
| xsd_string(X2) ) ),
inference(variable_rename,[status(thm)],[393]) ).
cnf(395,plain,
( xsd_string(X1)
| xsd_integer(X1) ),
inference(split_conjunct,[status(thm)],[394]) ).
cnf(396,plain,
( ~ xsd_integer(X1)
| ~ xsd_string(X1) ),
inference(split_conjunct,[status(thm)],[394]) ).
fof(489,plain,
! [X1] :
( ( ~ cC80(X1)
| ( cC78xcomp(X1)
& cC76xcomp(X1) ) )
& ( ~ cC78xcomp(X1)
| ~ cC76xcomp(X1)
| cC80(X1) ) ),
inference(fof_nnf,[status(thm)],[60]) ).
fof(490,plain,
! [X2] :
( ( ~ cC80(X2)
| ( cC78xcomp(X2)
& cC76xcomp(X2) ) )
& ( ~ cC78xcomp(X2)
| ~ cC76xcomp(X2)
| cC80(X2) ) ),
inference(variable_rename,[status(thm)],[489]) ).
fof(491,plain,
! [X2] :
( ( cC78xcomp(X2)
| ~ cC80(X2) )
& ( cC76xcomp(X2)
| ~ cC80(X2) )
& ( ~ cC78xcomp(X2)
| ~ cC76xcomp(X2)
| cC80(X2) ) ),
inference(distribute,[status(thm)],[490]) ).
cnf(492,plain,
( cC80(X1)
| ~ cC76xcomp(X1)
| ~ cC78xcomp(X1) ),
inference(split_conjunct,[status(thm)],[491]) ).
fof(545,plain,
! [X1] :
( ( ~ cC58(X1)
| ( cC34(X1)
& cC56(X1) ) )
& ( ~ cC34(X1)
| ~ cC56(X1)
| cC58(X1) ) ),
inference(fof_nnf,[status(thm)],[69]) ).
fof(546,plain,
! [X2] :
( ( ~ cC58(X2)
| ( cC34(X2)
& cC56(X2) ) )
& ( ~ cC34(X2)
| ~ cC56(X2)
| cC58(X2) ) ),
inference(variable_rename,[status(thm)],[545]) ).
fof(547,plain,
! [X2] :
( ( cC34(X2)
| ~ cC58(X2) )
& ( cC56(X2)
| ~ cC58(X2) )
& ( ~ cC34(X2)
| ~ cC56(X2)
| cC58(X2) ) ),
inference(distribute,[status(thm)],[546]) ).
cnf(548,plain,
( cC58(X1)
| ~ cC56(X1)
| ~ cC34(X1) ),
inference(split_conjunct,[status(thm)],[547]) ).
cnf(549,plain,
( cC56(X1)
| ~ cC58(X1) ),
inference(split_conjunct,[status(thm)],[547]) ).
fof(589,plain,
! [X1] :
( ( ~ cC56(X1)
| ( cC4(X1)
& cC10xcomp(X1) ) )
& ( ~ cC4(X1)
| ~ cC10xcomp(X1)
| cC56(X1) ) ),
inference(fof_nnf,[status(thm)],[76]) ).
fof(590,plain,
! [X2] :
( ( ~ cC56(X2)
| ( cC4(X2)
& cC10xcomp(X2) ) )
& ( ~ cC4(X2)
| ~ cC10xcomp(X2)
| cC56(X2) ) ),
inference(variable_rename,[status(thm)],[589]) ).
fof(591,plain,
! [X2] :
( ( cC4(X2)
| ~ cC56(X2) )
& ( cC10xcomp(X2)
| ~ cC56(X2) )
& ( ~ cC4(X2)
| ~ cC10xcomp(X2)
| cC56(X2) ) ),
inference(distribute,[status(thm)],[590]) ).
cnf(592,plain,
( cC56(X1)
| ~ cC10xcomp(X1)
| ~ cC4(X1) ),
inference(split_conjunct,[status(thm)],[591]) ).
fof(725,negated_conjecture,
( ? [X1] :
( ~ cowlThing(X1)
| cowlNothing(X1) )
| ? [X1] :
( ( ~ xsd_string(X1)
| xsd_integer(X1) )
& ( xsd_string(X1)
| ~ xsd_integer(X1) ) )
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
inference(fof_nnf,[status(thm)],[174]) ).
fof(726,negated_conjecture,
( ? [X2] :
( ~ cowlThing(X2)
| cowlNothing(X2) )
| ? [X3] :
( ( ~ xsd_string(X3)
| xsd_integer(X3) )
& ( xsd_string(X3)
| ~ xsd_integer(X3) ) )
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
inference(variable_rename,[status(thm)],[725]) ).
fof(727,negated_conjecture,
( ~ cowlThing(esk55_0)
| cowlNothing(esk55_0)
| ( ( ~ xsd_string(esk56_0)
| xsd_integer(esk56_0) )
& ( xsd_string(esk56_0)
| ~ xsd_integer(esk56_0) ) )
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ),
inference(skolemize,[status(esa)],[726]) ).
fof(728,negated_conjecture,
( ( ~ xsd_string(esk56_0)
| xsd_integer(esk56_0)
| ~ cowlThing(esk55_0)
| cowlNothing(esk55_0)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) )
& ( xsd_string(esk56_0)
| ~ xsd_integer(esk56_0)
| ~ cowlThing(esk55_0)
| cowlNothing(esk55_0)
| ~ cC58(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cowlThing(iV822576)
| ~ cC94(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576)
| ~ cC136(iV822576)
| ~ cC56(iV822576) ) ),
inference(distribute,[status(thm)],[727]) ).
cnf(729,negated_conjecture,
( cowlNothing(esk55_0)
| xsd_string(esk56_0)
| ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(esk55_0)
| ~ xsd_integer(esk56_0) ),
inference(split_conjunct,[status(thm)],[728]) ).
cnf(730,negated_conjecture,
( cowlNothing(esk55_0)
| xsd_integer(esk56_0)
| ~ cC56(iV822576)
| ~ cC136(iV822576)
| ~ cC110(iV822576)
| ~ cC80(iV822576)
| ~ cC94(iV822576)
| ~ cowlThing(iV822576)
| ~ cC114(iV822576)
| ~ cC116(iV822576)
| ~ cC58(iV822576)
| ~ cowlThing(esk55_0)
| ~ xsd_string(esk56_0) ),
inference(split_conjunct,[status(thm)],[728]) ).
fof(743,plain,
! [X1] :
( ( ~ cC94(X1)
| ( cC86xcomp(X1)
& cC92xcomp(X1) ) )
& ( ~ cC86xcomp(X1)
| ~ cC92xcomp(X1)
| cC94(X1) ) ),
inference(fof_nnf,[status(thm)],[101]) ).
fof(744,plain,
! [X2] :
( ( ~ cC94(X2)
| ( cC86xcomp(X2)
& cC92xcomp(X2) ) )
& ( ~ cC86xcomp(X2)
| ~ cC92xcomp(X2)
| cC94(X2) ) ),
inference(variable_rename,[status(thm)],[743]) ).
fof(745,plain,
! [X2] :
( ( cC86xcomp(X2)
| ~ cC94(X2) )
& ( cC92xcomp(X2)
| ~ cC94(X2) )
& ( ~ cC86xcomp(X2)
| ~ cC92xcomp(X2)
| cC94(X2) ) ),
inference(distribute,[status(thm)],[744]) ).
cnf(746,plain,
( cC94(X1)
| ~ cC92xcomp(X1)
| ~ cC86xcomp(X1) ),
inference(split_conjunct,[status(thm)],[745]) ).
cnf(959,plain,
cC102xcomp(iV822576),
inference(split_conjunct,[status(thm)],[136]) ).
cnf(961,plain,
cC4(iV822576),
inference(split_conjunct,[status(thm)],[138]) ).
cnf(962,plain,
cC108xcomp(iV822576),
inference(split_conjunct,[status(thm)],[139]) ).
fof(1001,plain,
! [X1] :
( ( ~ cC114(X1)
| ( cC112xcomp(X1)
& cC96xcomp(X1) ) )
& ( ~ cC112xcomp(X1)
| ~ cC96xcomp(X1)
| cC114(X1) ) ),
inference(fof_nnf,[status(thm)],[146]) ).
fof(1002,plain,
! [X2] :
( ( ~ cC114(X2)
| ( cC112xcomp(X2)
& cC96xcomp(X2) ) )
& ( ~ cC112xcomp(X2)
| ~ cC96xcomp(X2)
| cC114(X2) ) ),
inference(variable_rename,[status(thm)],[1001]) ).
fof(1003,plain,
! [X2] :
( ( cC112xcomp(X2)
| ~ cC114(X2) )
& ( cC96xcomp(X2)
| ~ cC114(X2) )
& ( ~ cC112xcomp(X2)
| ~ cC96xcomp(X2)
| cC114(X2) ) ),
inference(distribute,[status(thm)],[1002]) ).
cnf(1004,plain,
( cC114(X1)
| ~ cC96xcomp(X1)
| ~ cC112xcomp(X1) ),
inference(split_conjunct,[status(thm)],[1003]) ).
fof(1019,plain,
! [X1] :
( ( ~ cC116(X1)
| ( cC114(X1)
& cC80(X1) ) )
& ( ~ cC114(X1)
| ~ cC80(X1)
| cC116(X1) ) ),
inference(fof_nnf,[status(thm)],[149]) ).
fof(1020,plain,
! [X2] :
( ( ~ cC116(X2)
| ( cC114(X2)
& cC80(X2) ) )
& ( ~ cC114(X2)
| ~ cC80(X2)
| cC116(X2) ) ),
inference(variable_rename,[status(thm)],[1019]) ).
fof(1021,plain,
! [X2] :
( ( cC114(X2)
| ~ cC116(X2) )
& ( cC80(X2)
| ~ cC116(X2) )
& ( ~ cC114(X2)
| ~ cC80(X2)
| cC116(X2) ) ),
inference(distribute,[status(thm)],[1020]) ).
cnf(1022,plain,
( cC116(X1)
| ~ cC80(X1)
| ~ cC114(X1) ),
inference(split_conjunct,[status(thm)],[1021]) ).
cnf(1024,plain,
( cC114(X1)
| ~ cC116(X1) ),
inference(split_conjunct,[status(thm)],[1021]) ).
fof(1043,plain,
! [X1] :
( ( ~ cC136(X1)
| ( cC134xcomp(X1)
& cC116(X1) ) )
& ( ~ cC134xcomp(X1)
| ~ cC116(X1)
| cC136(X1) ) ),
inference(fof_nnf,[status(thm)],[153]) ).
fof(1044,plain,
! [X2] :
( ( ~ cC136(X2)
| ( cC134xcomp(X2)
& cC116(X2) ) )
& ( ~ cC134xcomp(X2)
| ~ cC116(X2)
| cC136(X2) ) ),
inference(variable_rename,[status(thm)],[1043]) ).
fof(1045,plain,
! [X2] :
( ( cC134xcomp(X2)
| ~ cC136(X2) )
& ( cC116(X2)
| ~ cC136(X2) )
& ( ~ cC134xcomp(X2)
| ~ cC116(X2)
| cC136(X2) ) ),
inference(distribute,[status(thm)],[1044]) ).
cnf(1046,plain,
( cC136(X1)
| ~ cC116(X1)
| ~ cC134xcomp(X1) ),
inference(split_conjunct,[status(thm)],[1045]) ).
cnf(1047,plain,
( cC116(X1)
| ~ cC136(X1) ),
inference(split_conjunct,[status(thm)],[1045]) ).
cnf(1093,plain,
cC76xcomp(iV822576),
inference(split_conjunct,[status(thm)],[161]) ).
cnf(1094,plain,
cC96xcomp(iV822576),
inference(split_conjunct,[status(thm)],[162]) ).
cnf(1096,plain,
cC112xcomp(iV822576),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(1103,plain,
cC78xcomp(iV822576),
inference(split_conjunct,[status(thm)],[169]) ).
cnf(1108,negated_conjecture,
( cowlNothing(esk55_0)
| xsd_string(esk56_0)
| $false
| $false
| ~ cC110(iV822576)
| ~ xsd_integer(esk56_0)
| ~ cC80(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC94(iV822576)
| ~ cC136(iV822576) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[729,392,theory(equality)]),392,theory(equality)]),
[unfolding] ).
cnf(1109,negated_conjecture,
( cowlNothing(esk55_0)
| xsd_integer(esk56_0)
| $false
| $false
| ~ cC110(iV822576)
| ~ xsd_string(esk56_0)
| ~ cC80(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC94(iV822576)
| ~ cC136(iV822576) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[730,392,theory(equality)]),392,theory(equality)]),
[unfolding] ).
cnf(1116,plain,
( cC136(iV822576)
| ~ cC116(iV822576) ),
inference(spm,[status(thm)],[1046,246,theory(equality)]) ).
cnf(1118,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC110(iV822576)
| ~ xsd_integer(esk56_0)
| ~ cC80(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC94(iV822576)
| ~ cC136(iV822576) ),
inference(sr,[status(thm)],[1108,391,theory(equality)]) ).
cnf(1119,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1118,1024]) ).
cnf(1120,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1119,1047]) ).
cnf(1121,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_integer(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1120,549]) ).
cnf(1122,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1121,395]) ).
cnf(1123,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC110(iV822576)
| ~ xsd_string(esk56_0)
| ~ cC80(iV822576)
| ~ cC58(iV822576)
| ~ cC56(iV822576)
| ~ cC116(iV822576)
| ~ cC114(iV822576)
| ~ cC94(iV822576)
| ~ cC136(iV822576) ),
inference(sr,[status(thm)],[1109,391,theory(equality)]) ).
cnf(1124,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC116(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1123,1024]) ).
cnf(1125,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC56(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1124,1047]) ).
cnf(1126,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ xsd_string(esk56_0)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1125,549]) ).
cnf(1127,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| ~ cC110(iV822576) ),
inference(csr,[status(thm)],[1126,1122]) ).
cnf(1159,plain,
( cC110(iV822576)
| ~ cC108xcomp(iV822576) ),
inference(spm,[status(thm)],[325,959,theory(equality)]) ).
cnf(1161,plain,
( cC110(iV822576)
| $false ),
inference(rw,[status(thm)],[1159,962,theory(equality)]) ).
cnf(1162,plain,
cC110(iV822576),
inference(cn,[status(thm)],[1161,theory(equality)]) ).
cnf(1163,plain,
( cC80(iV822576)
| ~ cC78xcomp(iV822576) ),
inference(spm,[status(thm)],[492,1093,theory(equality)]) ).
cnf(1165,plain,
( cC80(iV822576)
| $false ),
inference(rw,[status(thm)],[1163,1103,theory(equality)]) ).
cnf(1166,plain,
cC80(iV822576),
inference(cn,[status(thm)],[1165,theory(equality)]) ).
cnf(1169,plain,
( cC58(X1)
| ~ cC34(X1)
| ~ cC10xcomp(X1)
| ~ cC4(X1) ),
inference(spm,[status(thm)],[548,592,theory(equality)]) ).
cnf(1172,plain,
( cC114(iV822576)
| ~ cC96xcomp(iV822576) ),
inference(spm,[status(thm)],[1004,1096,theory(equality)]) ).
cnf(1174,plain,
( cC114(iV822576)
| $false ),
inference(rw,[status(thm)],[1172,1094,theory(equality)]) ).
cnf(1175,plain,
cC114(iV822576),
inference(cn,[status(thm)],[1174,theory(equality)]) ).
cnf(1176,plain,
( cC94(iV822576)
| ~ cC86xcomp(iV822576) ),
inference(spm,[status(thm)],[746,247,theory(equality)]) ).
cnf(1178,plain,
( cC94(iV822576)
| $false ),
inference(rw,[status(thm)],[1176,245,theory(equality)]) ).
cnf(1179,plain,
cC94(iV822576),
inference(cn,[status(thm)],[1178,theory(equality)]) ).
cnf(1569,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| $false ),
inference(rw,[status(thm)],[1127,1162,theory(equality)]) ).
cnf(1570,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576) ),
inference(cn,[status(thm)],[1569,theory(equality)]) ).
cnf(1571,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576)
| $false ),
inference(rw,[status(thm)],[1122,1162,theory(equality)]) ).
cnf(1572,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| ~ cC80(iV822576) ),
inference(cn,[status(thm)],[1571,theory(equality)]) ).
cnf(1573,plain,
( cC116(iV822576)
| ~ cC80(iV822576) ),
inference(spm,[status(thm)],[1022,1175,theory(equality)]) ).
cnf(1574,plain,
( cC116(iV822576)
| $false ),
inference(rw,[status(thm)],[1573,1166,theory(equality)]) ).
cnf(1575,plain,
cC116(iV822576),
inference(cn,[status(thm)],[1574,theory(equality)]) ).
cnf(1576,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| $false ),
inference(rw,[status(thm)],[1570,1166,theory(equality)]) ).
cnf(1577,negated_conjecture,
( xsd_integer(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576) ),
inference(cn,[status(thm)],[1576,theory(equality)]) ).
cnf(1578,negated_conjecture,
( ~ xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576) ),
inference(spm,[status(thm)],[396,1577,theory(equality)]) ).
cnf(1579,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576)
| $false ),
inference(rw,[status(thm)],[1572,1166,theory(equality)]) ).
cnf(1580,negated_conjecture,
( xsd_string(esk56_0)
| ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576) ),
inference(cn,[status(thm)],[1579,theory(equality)]) ).
cnf(1581,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC94(iV822576)
| ~ cC58(iV822576) ),
inference(csr,[status(thm)],[1578,1580]) ).
cnf(1584,negated_conjecture,
( ~ cC136(iV822576)
| $false
| ~ cC58(iV822576) ),
inference(rw,[status(thm)],[1581,1179,theory(equality)]) ).
cnf(1585,negated_conjecture,
( ~ cC136(iV822576)
| ~ cC58(iV822576) ),
inference(cn,[status(thm)],[1584,theory(equality)]) ).
cnf(1588,plain,
( cC136(iV822576)
| $false ),
inference(rw,[status(thm)],[1116,1575,theory(equality)]) ).
cnf(1589,plain,
cC136(iV822576),
inference(cn,[status(thm)],[1588,theory(equality)]) ).
cnf(1590,negated_conjecture,
( $false
| ~ cC58(iV822576) ),
inference(rw,[status(thm)],[1585,1589,theory(equality)]) ).
cnf(1591,negated_conjecture,
~ cC58(iV822576),
inference(cn,[status(thm)],[1590,theory(equality)]) ).
cnf(1861,negated_conjecture,
( ~ cC10xcomp(iV822576)
| ~ cC4(iV822576)
| ~ cC34(iV822576) ),
inference(spm,[status(thm)],[1591,1169,theory(equality)]) ).
cnf(1865,negated_conjecture,
( $false
| ~ cC4(iV822576)
| ~ cC34(iV822576) ),
inference(rw,[status(thm)],[1861,237,theory(equality)]) ).
cnf(1866,negated_conjecture,
( $false
| $false
| ~ cC34(iV822576) ),
inference(rw,[status(thm)],[1865,961,theory(equality)]) ).
cnf(1867,negated_conjecture,
( $false
| $false
| $false ),
inference(rw,[status(thm)],[1866,244,theory(equality)]) ).
cnf(1868,negated_conjecture,
$false,
inference(cn,[status(thm)],[1867,theory(equality)]) ).
cnf(1869,negated_conjecture,
$false,
1868,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/KRS/KRS154+1.p
% --creating new selector for []
% -running prover on /tmp/tmp1TDx_p/sel_KRS154+1.p_1 with time limit 29
% -prover status Theorem
% Problem KRS154+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/KRS/KRS154+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/KRS/KRS154+1.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
%
%------------------------------------------------------------------------------