%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : KRS155+1 : TPTP v5.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Sat Dec 25 13:07:46 EST 2010
% Result : Theorem 0.34s
% Output : CNFRefutation 0.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 28
% Syntax : Number of formulae : 203 ( 43 unt; 0 def)
% Number of atoms : 1048 ( 0 equ)
% Maximal formula atoms : 38 ( 5 avg)
% Number of connectives : 1470 ( 625 ~; 648 |; 180 &)
% ( 17 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 24 ( 23 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 9 con; 0-1 aty)
% Number of variables : 183 ( 2 sgn 124 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(2,axiom,
! [X1] :
( cC8(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC6xcomp(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_79) ).
fof(11,axiom,
! [X1] :
( cC60(X1)
<=> ( cC2xcomp(X1)
& cC58(X1) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_61) ).
fof(14,axiom,
! [X1] :
( cC62(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC60(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_62) ).
fof(29,axiom,
! [X1] :
( cC20(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_13) ).
fof(32,axiom,
! [X1] :
( cC10(X1)
<=> ( cC4(X1)
& cC8(X1) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_2) ).
fof(34,axiom,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_0) ).
fof(35,axiom,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_1) ).
fof(39,axiom,
! [X1] :
( cC14(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cTOP(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_5) ).
fof(40,axiom,
rR1(iV8467,iV8469),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_105) ).
fof(41,axiom,
rR1(iV8467,iV8470),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_104) ).
fof(46,axiom,
rR1(iV8467,iV8471),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_103) ).
fof(48,axiom,
cC78xcomp(iV8471),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_118) ).
fof(49,axiom,
cC2xcomp(iV8471),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_119) ).
fof(50,axiom,
cTOP(iV8470),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_116) ).
fof(55,axiom,
cC6xcomp(iV8469),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_113) ).
fof(56,axiom,
rR1(iV8467,iV8472),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_110) ).
fof(70,axiom,
cC2xcomp(iV8472),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_122) ).
fof(73,axiom,
cC32xcomp(iV8474),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_127) ).
fof(76,axiom,
rR1(iV8472,iV8476),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_124) ).
fof(86,axiom,
! [X1] :
( cC82(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC80(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_82) ).
fof(88,axiom,
! [X1] :
( cC80(X1)
<=> ( cC78xcomp(X1)
& cC2xcomp(X1) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_80) ).
fof(89,conjecture,
( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',the_axiom) ).
fof(92,axiom,
cC2(iV8476),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_132) ).
fof(103,axiom,
! [X1] :
( cC4(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_35) ).
fof(113,axiom,
! [X1] :
( cC58(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC2(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_57) ).
fof(115,axiom,
rR1(iV8467,iV8474),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_106) ).
fof(116,axiom,
! [X1] :
( cC34(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC32xcomp(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_29) ).
fof(135,axiom,
! [X1] :
( cC48(X1)
<=> ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) ),
file('/tmp/tmpgdu6Ji/sel_KRS155+1.p_1',axiom_44) ).
fof(136,negated_conjecture,
~ ( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
inference(assume_negation,[status(cth)],[89]) ).
fof(137,plain,
! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) ),
inference(fof_simplification,[status(thm)],[34,theory(equality)]) ).
fof(138,plain,
! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) ),
inference(fof_simplification,[status(thm)],[35,theory(equality)]) ).
fof(139,negated_conjecture,
~ ( ! [X1] :
( cowlThing(X1)
& ~ cowlNothing(X1) )
& ! [X1] :
( xsd_string(X1)
<=> ~ xsd_integer(X1) )
& cC20(iV8467)
& cC4(iV8467)
& cC8(iV8467)
& cC82(iV8467)
& cC62(iV8467)
& cC14(iV8467)
& cC34(iV8467)
& cC10(iV8467)
& cowlThing(iV8467)
& cC48(iV8467)
& cowlThing(iV8471)
& cC80(iV8471)
& cC58(iV8472)
& cC60(iV8472)
& cowlThing(iV8472) ),
inference(fof_simplification,[status(thm)],[136,theory(equality)]) ).
fof(146,plain,
! [X1] :
( ( ~ cC8(X1)
| ? [X2] :
( rR1(X1,X2)
& cC6xcomp(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC6xcomp(X2) )
| cC8(X1) ) ),
inference(fof_nnf,[status(thm)],[2]) ).
fof(147,plain,
! [X3] :
( ( ~ cC8(X3)
| ? [X4] :
( rR1(X3,X4)
& cC6xcomp(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC6xcomp(X5) )
| cC8(X3) ) ),
inference(variable_rename,[status(thm)],[146]) ).
fof(148,plain,
! [X3] :
( ( ~ cC8(X3)
| ( rR1(X3,esk2_1(X3))
& cC6xcomp(esk2_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC6xcomp(X5) )
| cC8(X3) ) ),
inference(skolemize,[status(esa)],[147]) ).
fof(149,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC6xcomp(X5)
| cC8(X3) )
& ( ~ cC8(X3)
| ( rR1(X3,esk2_1(X3))
& cC6xcomp(esk2_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[148]) ).
fof(150,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC6xcomp(X5)
| cC8(X3) )
& ( rR1(X3,esk2_1(X3))
| ~ cC8(X3) )
& ( cC6xcomp(esk2_1(X3))
| ~ cC8(X3) ) ),
inference(distribute,[status(thm)],[149]) ).
cnf(153,plain,
( cC8(X1)
| ~ cC6xcomp(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[150]) ).
fof(206,plain,
! [X1] :
( ( ~ cC60(X1)
| ( cC2xcomp(X1)
& cC58(X1) ) )
& ( ~ cC2xcomp(X1)
| ~ cC58(X1)
| cC60(X1) ) ),
inference(fof_nnf,[status(thm)],[11]) ).
fof(207,plain,
! [X2] :
( ( ~ cC60(X2)
| ( cC2xcomp(X2)
& cC58(X2) ) )
& ( ~ cC2xcomp(X2)
| ~ cC58(X2)
| cC60(X2) ) ),
inference(variable_rename,[status(thm)],[206]) ).
fof(208,plain,
! [X2] :
( ( cC2xcomp(X2)
| ~ cC60(X2) )
& ( cC58(X2)
| ~ cC60(X2) )
& ( ~ cC2xcomp(X2)
| ~ cC58(X2)
| cC60(X2) ) ),
inference(distribute,[status(thm)],[207]) ).
cnf(209,plain,
( cC60(X1)
| ~ cC58(X1)
| ~ cC2xcomp(X1) ),
inference(split_conjunct,[status(thm)],[208]) ).
cnf(210,plain,
( cC58(X1)
| ~ cC60(X1) ),
inference(split_conjunct,[status(thm)],[208]) ).
fof(224,plain,
! [X1] :
( ( ~ cC62(X1)
| ? [X2] :
( rR1(X1,X2)
& cC60(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC60(X2) )
| cC62(X1) ) ),
inference(fof_nnf,[status(thm)],[14]) ).
fof(225,plain,
! [X3] :
( ( ~ cC62(X3)
| ? [X4] :
( rR1(X3,X4)
& cC60(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC60(X5) )
| cC62(X3) ) ),
inference(variable_rename,[status(thm)],[224]) ).
fof(226,plain,
! [X3] :
( ( ~ cC62(X3)
| ( rR1(X3,esk12_1(X3))
& cC60(esk12_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC60(X5) )
| cC62(X3) ) ),
inference(skolemize,[status(esa)],[225]) ).
fof(227,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC60(X5)
| cC62(X3) )
& ( ~ cC62(X3)
| ( rR1(X3,esk12_1(X3))
& cC60(esk12_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[226]) ).
fof(228,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC60(X5)
| cC62(X3) )
& ( rR1(X3,esk12_1(X3))
| ~ cC62(X3) )
& ( cC60(esk12_1(X3))
| ~ cC62(X3) ) ),
inference(distribute,[status(thm)],[227]) ).
cnf(231,plain,
( cC62(X1)
| ~ cC60(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[228]) ).
fof(321,plain,
! [X1] :
( ( ~ cC20(X1)
| ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC2xcomp(X2) )
| cC20(X1) ) ),
inference(fof_nnf,[status(thm)],[29]) ).
fof(322,plain,
! [X3] :
( ( ~ cC20(X3)
| ? [X4] :
( rR1(X3,X4)
& cC2xcomp(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC20(X3) ) ),
inference(variable_rename,[status(thm)],[321]) ).
fof(323,plain,
! [X3] :
( ( ~ cC20(X3)
| ( rR1(X3,esk23_1(X3))
& cC2xcomp(esk23_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC20(X3) ) ),
inference(skolemize,[status(esa)],[322]) ).
fof(324,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC20(X3) )
& ( ~ cC20(X3)
| ( rR1(X3,esk23_1(X3))
& cC2xcomp(esk23_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[323]) ).
fof(325,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC20(X3) )
& ( rR1(X3,esk23_1(X3))
| ~ cC20(X3) )
& ( cC2xcomp(esk23_1(X3))
| ~ cC20(X3) ) ),
inference(distribute,[status(thm)],[324]) ).
cnf(328,plain,
( cC20(X1)
| ~ cC2xcomp(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[325]) ).
fof(341,plain,
! [X1] :
( ( ~ cC10(X1)
| ( cC4(X1)
& cC8(X1) ) )
& ( ~ cC4(X1)
| ~ cC8(X1)
| cC10(X1) ) ),
inference(fof_nnf,[status(thm)],[32]) ).
fof(342,plain,
! [X2] :
( ( ~ cC10(X2)
| ( cC4(X2)
& cC8(X2) ) )
& ( ~ cC4(X2)
| ~ cC8(X2)
| cC10(X2) ) ),
inference(variable_rename,[status(thm)],[341]) ).
fof(343,plain,
! [X2] :
( ( cC4(X2)
| ~ cC10(X2) )
& ( cC8(X2)
| ~ cC10(X2) )
& ( ~ cC4(X2)
| ~ cC8(X2)
| cC10(X2) ) ),
inference(distribute,[status(thm)],[342]) ).
cnf(344,plain,
( cC10(X1)
| ~ cC8(X1)
| ~ cC4(X1) ),
inference(split_conjunct,[status(thm)],[343]) ).
cnf(345,plain,
( cC8(X1)
| ~ cC10(X1) ),
inference(split_conjunct,[status(thm)],[343]) ).
cnf(346,plain,
( cC4(X1)
| ~ cC10(X1) ),
inference(split_conjunct,[status(thm)],[343]) ).
fof(355,plain,
! [X2] :
( cowlThing(X2)
& ~ cowlNothing(X2) ),
inference(variable_rename,[status(thm)],[137]) ).
cnf(356,plain,
~ cowlNothing(X1),
inference(split_conjunct,[status(thm)],[355]) ).
cnf(357,plain,
cowlThing(X1),
inference(split_conjunct,[status(thm)],[355]) ).
fof(358,plain,
! [X1] :
( ( ~ xsd_string(X1)
| ~ xsd_integer(X1) )
& ( xsd_integer(X1)
| xsd_string(X1) ) ),
inference(fof_nnf,[status(thm)],[138]) ).
fof(359,plain,
! [X2] :
( ( ~ xsd_string(X2)
| ~ xsd_integer(X2) )
& ( xsd_integer(X2)
| xsd_string(X2) ) ),
inference(variable_rename,[status(thm)],[358]) ).
cnf(360,plain,
( xsd_string(X1)
| xsd_integer(X1) ),
inference(split_conjunct,[status(thm)],[359]) ).
cnf(361,plain,
( ~ xsd_integer(X1)
| ~ xsd_string(X1) ),
inference(split_conjunct,[status(thm)],[359]) ).
fof(380,plain,
! [X1] :
( ( ~ cC14(X1)
| ? [X2] :
( rR1(X1,X2)
& cTOP(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cTOP(X2) )
| cC14(X1) ) ),
inference(fof_nnf,[status(thm)],[39]) ).
fof(381,plain,
! [X3] :
( ( ~ cC14(X3)
| ? [X4] :
( rR1(X3,X4)
& cTOP(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cTOP(X5) )
| cC14(X3) ) ),
inference(variable_rename,[status(thm)],[380]) ).
fof(382,plain,
! [X3] :
( ( ~ cC14(X3)
| ( rR1(X3,esk29_1(X3))
& cTOP(esk29_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cTOP(X5) )
| cC14(X3) ) ),
inference(skolemize,[status(esa)],[381]) ).
fof(383,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cTOP(X5)
| cC14(X3) )
& ( ~ cC14(X3)
| ( rR1(X3,esk29_1(X3))
& cTOP(esk29_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[382]) ).
fof(384,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cTOP(X5)
| cC14(X3) )
& ( rR1(X3,esk29_1(X3))
| ~ cC14(X3) )
& ( cTOP(esk29_1(X3))
| ~ cC14(X3) ) ),
inference(distribute,[status(thm)],[383]) ).
cnf(387,plain,
( cC14(X1)
| ~ cTOP(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[384]) ).
cnf(388,plain,
rR1(iV8467,iV8469),
inference(split_conjunct,[status(thm)],[40]) ).
cnf(389,plain,
rR1(iV8467,iV8470),
inference(split_conjunct,[status(thm)],[41]) ).
cnf(406,plain,
rR1(iV8467,iV8471),
inference(split_conjunct,[status(thm)],[46]) ).
cnf(408,plain,
cC78xcomp(iV8471),
inference(split_conjunct,[status(thm)],[48]) ).
cnf(409,plain,
cC2xcomp(iV8471),
inference(split_conjunct,[status(thm)],[49]) ).
cnf(410,plain,
cTOP(iV8470),
inference(split_conjunct,[status(thm)],[50]) ).
cnf(417,plain,
cC6xcomp(iV8469),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(418,plain,
rR1(iV8467,iV8472),
inference(split_conjunct,[status(thm)],[56]) ).
cnf(469,plain,
cC2xcomp(iV8472),
inference(split_conjunct,[status(thm)],[70]) ).
cnf(474,plain,
cC32xcomp(iV8474),
inference(split_conjunct,[status(thm)],[73]) ).
cnf(477,plain,
rR1(iV8472,iV8476),
inference(split_conjunct,[status(thm)],[76]) ).
fof(530,plain,
! [X1] :
( ( ~ cC82(X1)
| ? [X2] :
( rR1(X1,X2)
& cC80(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC80(X2) )
| cC82(X1) ) ),
inference(fof_nnf,[status(thm)],[86]) ).
fof(531,plain,
! [X3] :
( ( ~ cC82(X3)
| ? [X4] :
( rR1(X3,X4)
& cC80(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC80(X5) )
| cC82(X3) ) ),
inference(variable_rename,[status(thm)],[530]) ).
fof(532,plain,
! [X3] :
( ( ~ cC82(X3)
| ( rR1(X3,esk43_1(X3))
& cC80(esk43_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC80(X5) )
| cC82(X3) ) ),
inference(skolemize,[status(esa)],[531]) ).
fof(533,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC80(X5)
| cC82(X3) )
& ( ~ cC82(X3)
| ( rR1(X3,esk43_1(X3))
& cC80(esk43_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[532]) ).
fof(534,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC80(X5)
| cC82(X3) )
& ( rR1(X3,esk43_1(X3))
| ~ cC82(X3) )
& ( cC80(esk43_1(X3))
| ~ cC82(X3) ) ),
inference(distribute,[status(thm)],[533]) ).
cnf(537,plain,
( cC82(X1)
| ~ cC80(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[534]) ).
fof(544,plain,
! [X1] :
( ( ~ cC80(X1)
| ( cC78xcomp(X1)
& cC2xcomp(X1) ) )
& ( ~ cC78xcomp(X1)
| ~ cC2xcomp(X1)
| cC80(X1) ) ),
inference(fof_nnf,[status(thm)],[88]) ).
fof(545,plain,
! [X2] :
( ( ~ cC80(X2)
| ( cC78xcomp(X2)
& cC2xcomp(X2) ) )
& ( ~ cC78xcomp(X2)
| ~ cC2xcomp(X2)
| cC80(X2) ) ),
inference(variable_rename,[status(thm)],[544]) ).
fof(546,plain,
! [X2] :
( ( cC78xcomp(X2)
| ~ cC80(X2) )
& ( cC2xcomp(X2)
| ~ cC80(X2) )
& ( ~ cC78xcomp(X2)
| ~ cC2xcomp(X2)
| cC80(X2) ) ),
inference(distribute,[status(thm)],[545]) ).
cnf(547,plain,
( cC80(X1)
| ~ cC2xcomp(X1)
| ~ cC78xcomp(X1) ),
inference(split_conjunct,[status(thm)],[546]) ).
fof(550,negated_conjecture,
( ? [X1] :
( ~ cowlThing(X1)
| cowlNothing(X1) )
| ? [X1] :
( ( ~ xsd_string(X1)
| xsd_integer(X1) )
& ( xsd_string(X1)
| ~ xsd_integer(X1) ) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(fof_nnf,[status(thm)],[139]) ).
fof(551,negated_conjecture,
( ? [X2] :
( ~ cowlThing(X2)
| cowlNothing(X2) )
| ? [X3] :
( ( ~ xsd_string(X3)
| xsd_integer(X3) )
& ( xsd_string(X3)
| ~ xsd_integer(X3) ) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(variable_rename,[status(thm)],[550]) ).
fof(552,negated_conjecture,
( ~ cowlThing(esk45_0)
| cowlNothing(esk45_0)
| ( ( ~ xsd_string(esk46_0)
| xsd_integer(esk46_0) )
& ( xsd_string(esk46_0)
| ~ xsd_integer(esk46_0) ) )
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ),
inference(skolemize,[status(esa)],[551]) ).
fof(553,negated_conjecture,
( ( ~ xsd_string(esk46_0)
| xsd_integer(esk46_0)
| ~ cowlThing(esk45_0)
| cowlNothing(esk45_0)
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) )
& ( xsd_string(esk46_0)
| ~ xsd_integer(esk46_0)
| ~ cowlThing(esk45_0)
| cowlNothing(esk45_0)
| ~ cC20(iV8467)
| ~ cC4(iV8467)
| ~ cC8(iV8467)
| ~ cC82(iV8467)
| ~ cC62(iV8467)
| ~ cC14(iV8467)
| ~ cC34(iV8467)
| ~ cC10(iV8467)
| ~ cowlThing(iV8467)
| ~ cC48(iV8467)
| ~ cowlThing(iV8471)
| ~ cC80(iV8471)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cowlThing(iV8472) ) ),
inference(distribute,[status(thm)],[552]) ).
cnf(554,negated_conjecture,
( cowlNothing(esk45_0)
| xsd_string(esk46_0)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing(esk45_0)
| ~ xsd_integer(esk46_0) ),
inference(split_conjunct,[status(thm)],[553]) ).
cnf(555,negated_conjecture,
( cowlNothing(esk45_0)
| xsd_integer(esk46_0)
| ~ cowlThing(iV8472)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC80(iV8471)
| ~ cowlThing(iV8471)
| ~ cC48(iV8467)
| ~ cowlThing(iV8467)
| ~ cC10(iV8467)
| ~ cC34(iV8467)
| ~ cC14(iV8467)
| ~ cC62(iV8467)
| ~ cC82(iV8467)
| ~ cC8(iV8467)
| ~ cC4(iV8467)
| ~ cC20(iV8467)
| ~ cowlThing(esk45_0)
| ~ xsd_string(esk46_0) ),
inference(split_conjunct,[status(thm)],[553]) ).
cnf(558,plain,
cC2(iV8476),
inference(split_conjunct,[status(thm)],[92]) ).
fof(620,plain,
! [X1] :
( ( ~ cC4(X1)
| ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC2xcomp(X2) )
| cC4(X1) ) ),
inference(fof_nnf,[status(thm)],[103]) ).
fof(621,plain,
! [X3] :
( ( ~ cC4(X3)
| ? [X4] :
( rR1(X3,X4)
& cC2xcomp(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC4(X3) ) ),
inference(variable_rename,[status(thm)],[620]) ).
fof(622,plain,
! [X3] :
( ( ~ cC4(X3)
| ( rR1(X3,esk55_1(X3))
& cC2xcomp(esk55_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC4(X3) ) ),
inference(skolemize,[status(esa)],[621]) ).
fof(623,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC4(X3) )
& ( ~ cC4(X3)
| ( rR1(X3,esk55_1(X3))
& cC2xcomp(esk55_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[622]) ).
fof(624,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC4(X3) )
& ( rR1(X3,esk55_1(X3))
| ~ cC4(X3) )
& ( cC2xcomp(esk55_1(X3))
| ~ cC4(X3) ) ),
inference(distribute,[status(thm)],[623]) ).
cnf(627,plain,
( cC4(X1)
| ~ cC2xcomp(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[624]) ).
fof(686,plain,
! [X1] :
( ( ~ cC58(X1)
| ? [X2] :
( rR1(X1,X2)
& cC2(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC2(X2) )
| cC58(X1) ) ),
inference(fof_nnf,[status(thm)],[113]) ).
fof(687,plain,
! [X3] :
( ( ~ cC58(X3)
| ? [X4] :
( rR1(X3,X4)
& cC2(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2(X5) )
| cC58(X3) ) ),
inference(variable_rename,[status(thm)],[686]) ).
fof(688,plain,
! [X3] :
( ( ~ cC58(X3)
| ( rR1(X3,esk63_1(X3))
& cC2(esk63_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2(X5) )
| cC58(X3) ) ),
inference(skolemize,[status(esa)],[687]) ).
fof(689,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2(X5)
| cC58(X3) )
& ( ~ cC58(X3)
| ( rR1(X3,esk63_1(X3))
& cC2(esk63_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[688]) ).
fof(690,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2(X5)
| cC58(X3) )
& ( rR1(X3,esk63_1(X3))
| ~ cC58(X3) )
& ( cC2(esk63_1(X3))
| ~ cC58(X3) ) ),
inference(distribute,[status(thm)],[689]) ).
cnf(693,plain,
( cC58(X1)
| ~ cC2(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[690]) ).
cnf(695,plain,
rR1(iV8467,iV8474),
inference(split_conjunct,[status(thm)],[115]) ).
fof(696,plain,
! [X1] :
( ( ~ cC34(X1)
| ? [X2] :
( rR1(X1,X2)
& cC32xcomp(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC32xcomp(X2) )
| cC34(X1) ) ),
inference(fof_nnf,[status(thm)],[116]) ).
fof(697,plain,
! [X3] :
( ( ~ cC34(X3)
| ? [X4] :
( rR1(X3,X4)
& cC32xcomp(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC32xcomp(X5) )
| cC34(X3) ) ),
inference(variable_rename,[status(thm)],[696]) ).
fof(698,plain,
! [X3] :
( ( ~ cC34(X3)
| ( rR1(X3,esk64_1(X3))
& cC32xcomp(esk64_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC32xcomp(X5) )
| cC34(X3) ) ),
inference(skolemize,[status(esa)],[697]) ).
fof(699,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC32xcomp(X5)
| cC34(X3) )
& ( ~ cC34(X3)
| ( rR1(X3,esk64_1(X3))
& cC32xcomp(esk64_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[698]) ).
fof(700,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC32xcomp(X5)
| cC34(X3) )
& ( rR1(X3,esk64_1(X3))
| ~ cC34(X3) )
& ( cC32xcomp(esk64_1(X3))
| ~ cC34(X3) ) ),
inference(distribute,[status(thm)],[699]) ).
cnf(703,plain,
( cC34(X1)
| ~ cC32xcomp(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[700]) ).
fof(820,plain,
! [X1] :
( ( ~ cC48(X1)
| ? [X2] :
( rR1(X1,X2)
& cC2xcomp(X2) ) )
& ( ! [X2] :
( ~ rR1(X1,X2)
| ~ cC2xcomp(X2) )
| cC48(X1) ) ),
inference(fof_nnf,[status(thm)],[135]) ).
fof(821,plain,
! [X3] :
( ( ~ cC48(X3)
| ? [X4] :
( rR1(X3,X4)
& cC2xcomp(X4) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC48(X3) ) ),
inference(variable_rename,[status(thm)],[820]) ).
fof(822,plain,
! [X3] :
( ( ~ cC48(X3)
| ( rR1(X3,esk81_1(X3))
& cC2xcomp(esk81_1(X3)) ) )
& ( ! [X5] :
( ~ rR1(X3,X5)
| ~ cC2xcomp(X5) )
| cC48(X3) ) ),
inference(skolemize,[status(esa)],[821]) ).
fof(823,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC48(X3) )
& ( ~ cC48(X3)
| ( rR1(X3,esk81_1(X3))
& cC2xcomp(esk81_1(X3)) ) ) ),
inference(shift_quantors,[status(thm)],[822]) ).
fof(824,plain,
! [X3,X5] :
( ( ~ rR1(X3,X5)
| ~ cC2xcomp(X5)
| cC48(X3) )
& ( rR1(X3,esk81_1(X3))
| ~ cC48(X3) )
& ( cC2xcomp(esk81_1(X3))
| ~ cC48(X3) ) ),
inference(distribute,[status(thm)],[823]) ).
cnf(827,plain,
( cC48(X1)
| ~ cC2xcomp(X2)
| ~ rR1(X1,X2) ),
inference(split_conjunct,[status(thm)],[824]) ).
cnf(838,negated_conjecture,
( cowlNothing(esk45_0)
| xsd_string(esk46_0)
| ~ cC8(iV8467)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC62(iV8467)
| $false
| $false
| $false
| $false
| ~ cC20(iV8467)
| ~ cC10(iV8467)
| ~ cC4(iV8467)
| ~ xsd_integer(esk46_0)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC48(iV8467) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[554,357,theory(equality)]),357,theory(equality)]),357,theory(equality)]),357,theory(equality)]),
[unfolding] ).
cnf(839,negated_conjecture,
( cowlNothing(esk45_0)
| xsd_integer(esk46_0)
| ~ cC8(iV8467)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC62(iV8467)
| $false
| $false
| $false
| $false
| ~ cC20(iV8467)
| ~ cC10(iV8467)
| ~ cC4(iV8467)
| ~ xsd_string(esk46_0)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC48(iV8467) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[555,357,theory(equality)]),357,theory(equality)]),357,theory(equality)]),357,theory(equality)]),
[unfolding] ).
cnf(847,plain,
( cC62(iV8467)
| ~ cC60(iV8472) ),
inference(spm,[status(thm)],[231,418,theory(equality)]) ).
cnf(857,plain,
( cC82(iV8467)
| ~ cC80(iV8471) ),
inference(spm,[status(thm)],[537,406,theory(equality)]) ).
cnf(897,plain,
( cC80(iV8471)
| ~ cC2xcomp(iV8471) ),
inference(spm,[status(thm)],[547,408,theory(equality)]) ).
cnf(899,plain,
( cC80(iV8471)
| $false ),
inference(rw,[status(thm)],[897,409,theory(equality)]) ).
cnf(900,plain,
cC80(iV8471),
inference(cn,[status(thm)],[899,theory(equality)]) ).
cnf(901,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC8(iV8467)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC10(iV8467)
| ~ cC4(iV8467)
| ~ xsd_integer(esk46_0)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC48(iV8467) ),
inference(sr,[status(thm)],[838,356,theory(equality)]) ).
cnf(902,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC4(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[901,360]) ).
cnf(903,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[902,346]) ).
cnf(904,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[903,210]) ).
cnf(905,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(csr,[status(thm)],[904,345]) ).
cnf(906,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC8(iV8467)
| ~ cC60(iV8472)
| ~ cC58(iV8472)
| ~ cC62(iV8467)
| ~ cC20(iV8467)
| ~ cC10(iV8467)
| ~ cC4(iV8467)
| ~ xsd_string(esk46_0)
| ~ cC14(iV8467)
| ~ cC82(iV8467)
| ~ cC80(iV8471)
| ~ cC34(iV8467)
| ~ cC48(iV8467) ),
inference(sr,[status(thm)],[839,356,theory(equality)]) ).
cnf(907,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC4(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[906,360]) ).
cnf(908,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC58(iV8472)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[907,346]) ).
cnf(909,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472)
| ~ cC8(iV8467) ),
inference(csr,[status(thm)],[908,210]) ).
cnf(910,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC80(iV8471)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(csr,[status(thm)],[909,345]) ).
cnf(916,plain,
( cC8(iV8467)
| ~ cC6xcomp(iV8469) ),
inference(spm,[status(thm)],[153,388,theory(equality)]) ).
cnf(931,plain,
( cC8(iV8467)
| $false ),
inference(rw,[status(thm)],[916,417,theory(equality)]) ).
cnf(932,plain,
cC8(iV8467),
inference(cn,[status(thm)],[931,theory(equality)]) ).
cnf(935,plain,
( cC58(iV8472)
| ~ cC2(iV8476) ),
inference(spm,[status(thm)],[693,477,theory(equality)]) ).
cnf(951,plain,
( cC58(iV8472)
| $false ),
inference(rw,[status(thm)],[935,558,theory(equality)]) ).
cnf(952,plain,
cC58(iV8472),
inference(cn,[status(thm)],[951,theory(equality)]) ).
cnf(953,plain,
( cC20(iV8467)
| ~ cC2xcomp(iV8472) ),
inference(spm,[status(thm)],[328,418,theory(equality)]) ).
cnf(971,plain,
( cC20(iV8467)
| $false ),
inference(rw,[status(thm)],[953,469,theory(equality)]) ).
cnf(972,plain,
cC20(iV8467),
inference(cn,[status(thm)],[971,theory(equality)]) ).
cnf(999,plain,
( cC4(iV8467)
| ~ cC2xcomp(iV8472) ),
inference(spm,[status(thm)],[627,418,theory(equality)]) ).
cnf(1017,plain,
( cC4(iV8467)
| $false ),
inference(rw,[status(thm)],[999,469,theory(equality)]) ).
cnf(1018,plain,
cC4(iV8467),
inference(cn,[status(thm)],[1017,theory(equality)]) ).
cnf(1033,plain,
( cC14(iV8467)
| ~ cTOP(iV8470) ),
inference(spm,[status(thm)],[387,389,theory(equality)]) ).
cnf(1047,plain,
( cC14(iV8467)
| $false ),
inference(rw,[status(thm)],[1033,410,theory(equality)]) ).
cnf(1048,plain,
cC14(iV8467),
inference(cn,[status(thm)],[1047,theory(equality)]) ).
cnf(1057,plain,
( cC34(iV8467)
| ~ cC32xcomp(iV8474) ),
inference(spm,[status(thm)],[703,695,theory(equality)]) ).
cnf(1067,plain,
( cC34(iV8467)
| $false ),
inference(rw,[status(thm)],[1057,474,theory(equality)]) ).
cnf(1068,plain,
cC34(iV8467),
inference(cn,[status(thm)],[1067,theory(equality)]) ).
cnf(1069,plain,
( cC48(iV8467)
| ~ cC2xcomp(iV8472) ),
inference(spm,[status(thm)],[827,418,theory(equality)]) ).
cnf(1087,plain,
( cC48(iV8467)
| $false ),
inference(rw,[status(thm)],[1069,469,theory(equality)]) ).
cnf(1088,plain,
cC48(iV8467),
inference(cn,[status(thm)],[1087,theory(equality)]) ).
cnf(2303,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| $false
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[910,900,theory(equality)]) ).
cnf(2304,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2303,theory(equality)]) ).
cnf(2305,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| $false
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[905,900,theory(equality)]) ).
cnf(2306,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC20(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2305,theory(equality)]) ).
cnf(2308,plain,
( cC60(iV8472)
| ~ cC2xcomp(iV8472) ),
inference(spm,[status(thm)],[209,952,theory(equality)]) ).
cnf(2309,plain,
( cC60(iV8472)
| $false ),
inference(rw,[status(thm)],[2308,469,theory(equality)]) ).
cnf(2310,plain,
cC60(iV8472),
inference(cn,[status(thm)],[2309,theory(equality)]) ).
cnf(2315,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| $false
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2306,972,theory(equality)]) ).
cnf(2316,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2315,theory(equality)]) ).
cnf(2317,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| $false
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2304,972,theory(equality)]) ).
cnf(2318,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC14(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2317,theory(equality)]) ).
cnf(2326,plain,
( cC10(iV8467)
| ~ cC8(iV8467) ),
inference(spm,[status(thm)],[344,1018,theory(equality)]) ).
cnf(2327,plain,
( cC10(iV8467)
| $false ),
inference(rw,[status(thm)],[2326,932,theory(equality)]) ).
cnf(2328,plain,
cC10(iV8467),
inference(cn,[status(thm)],[2327,theory(equality)]) ).
cnf(2335,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| $false
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2318,1048,theory(equality)]) ).
cnf(2336,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2335,theory(equality)]) ).
cnf(2337,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| $false
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2316,1048,theory(equality)]) ).
cnf(2338,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC48(iV8467)
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2337,theory(equality)]) ).
cnf(2351,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| $false
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2336,1068,theory(equality)]) ).
cnf(2352,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC48(iV8467)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2351,theory(equality)]) ).
cnf(2355,negated_conjecture,
( xsd_integer(esk46_0)
| $false
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2352,1088,theory(equality)]) ).
cnf(2356,negated_conjecture,
( xsd_integer(esk46_0)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2355,theory(equality)]) ).
cnf(2357,negated_conjecture,
( ~ xsd_string(esk46_0)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(spm,[status(thm)],[361,2356,theory(equality)]) ).
cnf(2358,negated_conjecture,
( xsd_string(esk46_0)
| $false
| ~ cC34(iV8467)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2338,1088,theory(equality)]) ).
cnf(2359,negated_conjecture,
( xsd_string(esk46_0)
| $false
| $false
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(rw,[status(thm)],[2358,1068,theory(equality)]) ).
cnf(2360,negated_conjecture,
( xsd_string(esk46_0)
| ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(cn,[status(thm)],[2359,theory(equality)]) ).
cnf(2361,negated_conjecture,
( ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| ~ cC60(iV8472) ),
inference(csr,[status(thm)],[2357,2360]) ).
cnf(2370,negated_conjecture,
( ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467)
| $false ),
inference(rw,[status(thm)],[2361,2310,theory(equality)]) ).
cnf(2371,negated_conjecture,
( ~ cC82(iV8467)
| ~ cC10(iV8467)
| ~ cC62(iV8467) ),
inference(cn,[status(thm)],[2370,theory(equality)]) ).
cnf(2375,plain,
( cC62(iV8467)
| $false ),
inference(rw,[status(thm)],[847,2310,theory(equality)]) ).
cnf(2376,plain,
cC62(iV8467),
inference(cn,[status(thm)],[2375,theory(equality)]) ).
cnf(2378,negated_conjecture,
( ~ cC82(iV8467)
| $false
| ~ cC62(iV8467) ),
inference(rw,[status(thm)],[2371,2328,theory(equality)]) ).
cnf(2379,negated_conjecture,
( ~ cC82(iV8467)
| $false
| $false ),
inference(rw,[status(thm)],[2378,2376,theory(equality)]) ).
cnf(2380,negated_conjecture,
~ cC82(iV8467),
inference(cn,[status(thm)],[2379,theory(equality)]) ).
cnf(2385,plain,
( cC82(iV8467)
| $false ),
inference(rw,[status(thm)],[857,900,theory(equality)]) ).
cnf(2386,plain,
cC82(iV8467),
inference(cn,[status(thm)],[2385,theory(equality)]) ).
cnf(2387,plain,
$false,
inference(sr,[status(thm)],[2386,2380,theory(equality)]) ).
cnf(2388,plain,
$false,
2387,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% /home/graph/tptp/Systems/SInE---0.4/Source/sine.py:10: DeprecationWarning: the sets module is deprecated
% from sets import Set
% % SZS status Started for /home/graph/tptp/TPTP/Problems/KRS/KRS155+1.p
% --creating new selector for []
% -running prover on /tmp/tmpgdu6Ji/sel_KRS155+1.p_1 with time limit 29
% -prover status Theorem
% Problem KRS155+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/KRS/KRS155+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/KRS/KRS155+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
%
%------------------------------------------------------------------------------