%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR040+1 : TPTP v5.0.0. Released v3.4.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 06:14:04 EST 2010
% Result : Theorem 0.24s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 21
% Syntax : Number of formulae : 105 ( 8 unt; 0 def)
% Number of atoms : 202 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 188 ( 91 ~; 74 |; 2 &)
% ( 0 <=>; 21 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 93 ( 0 sgn 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(1,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',query40) ).
fof(43,axiom,
! [X8] :
( tptpcol_12_109157(X8)
=> tptpcol_11_109125(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just41) ).
fof(45,axiom,
! [X8] :
( tptpcol_13_109173(X8)
=> tptpcol_12_109157(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just43) ).
fof(47,axiom,
! [X8] :
( tptpcol_14_109181(X8)
=> tptpcol_13_109173(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just45) ).
fof(49,axiom,
! [X8] :
( tptpcol_15_109185(X8)
=> tptpcol_14_109181(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just47) ).
fof(58,axiom,
! [X8] :
( firstordercollection(X8)
=> fixedordercollection(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just4) ).
fof(59,axiom,
! [X8] :
~ ( collection(X8)
& individual(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just9) ).
fof(74,axiom,
! [X8] :
( tptpcol_6_108546(X8)
=> tptpcol_5_106498(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just29) ).
fof(76,axiom,
! [X8] :
( tptpcol_3_98305(X8)
=> tptpcol_2_98304(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just23) ).
fof(78,axiom,
! [X8] :
( tptpcol_2_98304(X8)
=> tptpcol_1_65536(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just21) ).
fof(80,axiom,
! [X8] :
( tptpcol_5_106498(X8)
=> tptpcol_4_106497(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just27) ).
fof(82,axiom,
! [X8] :
( tptpcol_4_106497(X8)
=> tptpcol_3_98305(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just25) ).
fof(93,axiom,
! [X8] :
( tptpcol_11_109125(X8)
=> tptpcol_10_109061(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just39) ).
fof(95,axiom,
! [X8] :
( tptpcol_7_108547(X8)
=> tptpcol_6_108546(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just31) ).
fof(97,axiom,
! [X8] :
( tptpcol_8_109059(X8)
=> tptpcol_7_108547(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just33) ).
fof(99,axiom,
! [X8] :
( tptpcol_9_109060(X8)
=> tptpcol_8_109059(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just35) ).
fof(101,axiom,
! [X8] :
( tptpcol_10_109061(X8)
=> tptpcol_9_109060(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just37) ).
fof(141,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just17) ).
fof(142,axiom,
! [X8] :
( tptpcol_0_0(X8)
=> individual(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just16) ).
fof(144,axiom,
! [X8] :
( fixedordercollection(X8)
=> collection(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just14) ).
fof(145,axiom,
! [X8] :
( tptpcol_1_65536(X8)
=> tptpcol_0_0(X8) ),
file('/tmp/tmptYl4aK/sel_CSR040+1.p_1',just19) ).
fof(147,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(assume_negation,[status(cth)],[1]) ).
fof(148,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_simplification,[status(thm)],[147,theory(equality)]) ).
fof(149,negated_conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
& tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(fof_nnf,[status(thm)],[148]) ).
cnf(150,negated_conjecture,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[149]) ).
fof(269,plain,
! [X8] :
( ~ tptpcol_12_109157(X8)
| tptpcol_11_109125(X8) ),
inference(fof_nnf,[status(thm)],[43]) ).
fof(270,plain,
! [X9] :
( ~ tptpcol_12_109157(X9)
| tptpcol_11_109125(X9) ),
inference(variable_rename,[status(thm)],[269]) ).
cnf(271,plain,
( tptpcol_11_109125(X1)
| ~ tptpcol_12_109157(X1) ),
inference(split_conjunct,[status(thm)],[270]) ).
fof(273,plain,
! [X8] :
( ~ tptpcol_13_109173(X8)
| tptpcol_12_109157(X8) ),
inference(fof_nnf,[status(thm)],[45]) ).
fof(274,plain,
! [X9] :
( ~ tptpcol_13_109173(X9)
| tptpcol_12_109157(X9) ),
inference(variable_rename,[status(thm)],[273]) ).
cnf(275,plain,
( tptpcol_12_109157(X1)
| ~ tptpcol_13_109173(X1) ),
inference(split_conjunct,[status(thm)],[274]) ).
fof(277,plain,
! [X8] :
( ~ tptpcol_14_109181(X8)
| tptpcol_13_109173(X8) ),
inference(fof_nnf,[status(thm)],[47]) ).
fof(278,plain,
! [X9] :
( ~ tptpcol_14_109181(X9)
| tptpcol_13_109173(X9) ),
inference(variable_rename,[status(thm)],[277]) ).
cnf(279,plain,
( tptpcol_13_109173(X1)
| ~ tptpcol_14_109181(X1) ),
inference(split_conjunct,[status(thm)],[278]) ).
fof(281,plain,
! [X8] :
( ~ tptpcol_15_109185(X8)
| tptpcol_14_109181(X8) ),
inference(fof_nnf,[status(thm)],[49]) ).
fof(282,plain,
! [X9] :
( ~ tptpcol_15_109185(X9)
| tptpcol_14_109181(X9) ),
inference(variable_rename,[status(thm)],[281]) ).
cnf(283,plain,
( tptpcol_14_109181(X1)
| ~ tptpcol_15_109185(X1) ),
inference(split_conjunct,[status(thm)],[282]) ).
fof(296,plain,
! [X8] :
( ~ firstordercollection(X8)
| fixedordercollection(X8) ),
inference(fof_nnf,[status(thm)],[58]) ).
fof(297,plain,
! [X9] :
( ~ firstordercollection(X9)
| fixedordercollection(X9) ),
inference(variable_rename,[status(thm)],[296]) ).
cnf(298,plain,
( fixedordercollection(X1)
| ~ firstordercollection(X1) ),
inference(split_conjunct,[status(thm)],[297]) ).
fof(299,plain,
! [X8] :
( ~ collection(X8)
| ~ individual(X8) ),
inference(fof_nnf,[status(thm)],[59]) ).
fof(300,plain,
! [X9] :
( ~ collection(X9)
| ~ individual(X9) ),
inference(variable_rename,[status(thm)],[299]) ).
cnf(301,plain,
( ~ individual(X1)
| ~ collection(X1) ),
inference(split_conjunct,[status(thm)],[300]) ).
fof(340,plain,
! [X8] :
( ~ tptpcol_6_108546(X8)
| tptpcol_5_106498(X8) ),
inference(fof_nnf,[status(thm)],[74]) ).
fof(341,plain,
! [X9] :
( ~ tptpcol_6_108546(X9)
| tptpcol_5_106498(X9) ),
inference(variable_rename,[status(thm)],[340]) ).
cnf(342,plain,
( tptpcol_5_106498(X1)
| ~ tptpcol_6_108546(X1) ),
inference(split_conjunct,[status(thm)],[341]) ).
fof(344,plain,
! [X8] :
( ~ tptpcol_3_98305(X8)
| tptpcol_2_98304(X8) ),
inference(fof_nnf,[status(thm)],[76]) ).
fof(345,plain,
! [X9] :
( ~ tptpcol_3_98305(X9)
| tptpcol_2_98304(X9) ),
inference(variable_rename,[status(thm)],[344]) ).
cnf(346,plain,
( tptpcol_2_98304(X1)
| ~ tptpcol_3_98305(X1) ),
inference(split_conjunct,[status(thm)],[345]) ).
fof(348,plain,
! [X8] :
( ~ tptpcol_2_98304(X8)
| tptpcol_1_65536(X8) ),
inference(fof_nnf,[status(thm)],[78]) ).
fof(349,plain,
! [X9] :
( ~ tptpcol_2_98304(X9)
| tptpcol_1_65536(X9) ),
inference(variable_rename,[status(thm)],[348]) ).
cnf(350,plain,
( tptpcol_1_65536(X1)
| ~ tptpcol_2_98304(X1) ),
inference(split_conjunct,[status(thm)],[349]) ).
fof(352,plain,
! [X8] :
( ~ tptpcol_5_106498(X8)
| tptpcol_4_106497(X8) ),
inference(fof_nnf,[status(thm)],[80]) ).
fof(353,plain,
! [X9] :
( ~ tptpcol_5_106498(X9)
| tptpcol_4_106497(X9) ),
inference(variable_rename,[status(thm)],[352]) ).
cnf(354,plain,
( tptpcol_4_106497(X1)
| ~ tptpcol_5_106498(X1) ),
inference(split_conjunct,[status(thm)],[353]) ).
fof(356,plain,
! [X8] :
( ~ tptpcol_4_106497(X8)
| tptpcol_3_98305(X8) ),
inference(fof_nnf,[status(thm)],[82]) ).
fof(357,plain,
! [X9] :
( ~ tptpcol_4_106497(X9)
| tptpcol_3_98305(X9) ),
inference(variable_rename,[status(thm)],[356]) ).
cnf(358,plain,
( tptpcol_3_98305(X1)
| ~ tptpcol_4_106497(X1) ),
inference(split_conjunct,[status(thm)],[357]) ).
fof(382,plain,
! [X8] :
( ~ tptpcol_11_109125(X8)
| tptpcol_10_109061(X8) ),
inference(fof_nnf,[status(thm)],[93]) ).
fof(383,plain,
! [X9] :
( ~ tptpcol_11_109125(X9)
| tptpcol_10_109061(X9) ),
inference(variable_rename,[status(thm)],[382]) ).
cnf(384,plain,
( tptpcol_10_109061(X1)
| ~ tptpcol_11_109125(X1) ),
inference(split_conjunct,[status(thm)],[383]) ).
fof(386,plain,
! [X8] :
( ~ tptpcol_7_108547(X8)
| tptpcol_6_108546(X8) ),
inference(fof_nnf,[status(thm)],[95]) ).
fof(387,plain,
! [X9] :
( ~ tptpcol_7_108547(X9)
| tptpcol_6_108546(X9) ),
inference(variable_rename,[status(thm)],[386]) ).
cnf(388,plain,
( tptpcol_6_108546(X1)
| ~ tptpcol_7_108547(X1) ),
inference(split_conjunct,[status(thm)],[387]) ).
fof(390,plain,
! [X8] :
( ~ tptpcol_8_109059(X8)
| tptpcol_7_108547(X8) ),
inference(fof_nnf,[status(thm)],[97]) ).
fof(391,plain,
! [X9] :
( ~ tptpcol_8_109059(X9)
| tptpcol_7_108547(X9) ),
inference(variable_rename,[status(thm)],[390]) ).
cnf(392,plain,
( tptpcol_7_108547(X1)
| ~ tptpcol_8_109059(X1) ),
inference(split_conjunct,[status(thm)],[391]) ).
fof(394,plain,
! [X8] :
( ~ tptpcol_9_109060(X8)
| tptpcol_8_109059(X8) ),
inference(fof_nnf,[status(thm)],[99]) ).
fof(395,plain,
! [X9] :
( ~ tptpcol_9_109060(X9)
| tptpcol_8_109059(X9) ),
inference(variable_rename,[status(thm)],[394]) ).
cnf(396,plain,
( tptpcol_8_109059(X1)
| ~ tptpcol_9_109060(X1) ),
inference(split_conjunct,[status(thm)],[395]) ).
fof(398,plain,
! [X8] :
( ~ tptpcol_10_109061(X8)
| tptpcol_9_109060(X8) ),
inference(fof_nnf,[status(thm)],[101]) ).
fof(399,plain,
! [X9] :
( ~ tptpcol_10_109061(X9)
| tptpcol_9_109060(X9) ),
inference(variable_rename,[status(thm)],[398]) ).
cnf(400,plain,
( tptpcol_9_109060(X1)
| ~ tptpcol_10_109061(X1) ),
inference(split_conjunct,[status(thm)],[399]) ).
cnf(501,plain,
firstordercollection(c_tptpcol_16_62187),
inference(split_conjunct,[status(thm)],[141]) ).
fof(502,plain,
! [X8] :
( ~ tptpcol_0_0(X8)
| individual(X8) ),
inference(fof_nnf,[status(thm)],[142]) ).
fof(503,plain,
! [X9] :
( ~ tptpcol_0_0(X9)
| individual(X9) ),
inference(variable_rename,[status(thm)],[502]) ).
cnf(504,plain,
( individual(X1)
| ~ tptpcol_0_0(X1) ),
inference(split_conjunct,[status(thm)],[503]) ).
fof(506,plain,
! [X8] :
( ~ fixedordercollection(X8)
| collection(X8) ),
inference(fof_nnf,[status(thm)],[144]) ).
fof(507,plain,
! [X9] :
( ~ fixedordercollection(X9)
| collection(X9) ),
inference(variable_rename,[status(thm)],[506]) ).
cnf(508,plain,
( collection(X1)
| ~ fixedordercollection(X1) ),
inference(split_conjunct,[status(thm)],[507]) ).
fof(509,plain,
! [X8] :
( ~ tptpcol_1_65536(X8)
| tptpcol_0_0(X8) ),
inference(fof_nnf,[status(thm)],[145]) ).
fof(510,plain,
! [X9] :
( ~ tptpcol_1_65536(X9)
| tptpcol_0_0(X9) ),
inference(variable_rename,[status(thm)],[509]) ).
cnf(511,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_1_65536(X1) ),
inference(split_conjunct,[status(thm)],[510]) ).
cnf(513,plain,
( tptpcol_13_109173(X1)
| ~ tptpcol_15_109185(X1) ),
inference(spm,[status(thm)],[279,283,theory(equality)]) ).
cnf(516,plain,
( collection(X1)
| ~ firstordercollection(X1) ),
inference(spm,[status(thm)],[508,298,theory(equality)]) ).
cnf(517,plain,
( tptpcol_9_109060(X1)
| ~ tptpcol_11_109125(X1) ),
inference(spm,[status(thm)],[400,384,theory(equality)]) ).
cnf(518,plain,
( tptpcol_3_98305(X1)
| ~ tptpcol_5_106498(X1) ),
inference(spm,[status(thm)],[358,354,theory(equality)]) ).
cnf(519,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_2_98304(X1) ),
inference(spm,[status(thm)],[511,350,theory(equality)]) ).
cnf(752,plain,
collection(c_tptpcol_16_62187),
inference(spm,[status(thm)],[516,501,theory(equality)]) ).
cnf(766,plain,
( tptpcol_8_109059(X1)
| ~ tptpcol_11_109125(X1) ),
inference(spm,[status(thm)],[396,517,theory(equality)]) ).
cnf(789,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_3_98305(X1) ),
inference(spm,[status(thm)],[519,346,theory(equality)]) ).
cnf(1210,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_5_106498(X1) ),
inference(spm,[status(thm)],[789,518,theory(equality)]) ).
cnf(1211,plain,
( tptpcol_0_0(X1)
| ~ tptpcol_6_108546(X1) ),
inference(spm,[status(thm)],[1210,342,theory(equality)]) ).
cnf(1213,plain,
( individual(X1)
| ~ tptpcol_6_108546(X1) ),
inference(spm,[status(thm)],[504,1211,theory(equality)]) ).
cnf(1215,plain,
( ~ collection(X1)
| ~ tptpcol_6_108546(X1) ),
inference(spm,[status(thm)],[301,1213,theory(equality)]) ).
cnf(1217,plain,
( ~ collection(X1)
| ~ tptpcol_7_108547(X1) ),
inference(spm,[status(thm)],[1215,388,theory(equality)]) ).
cnf(1221,plain,
( ~ collection(X1)
| ~ tptpcol_8_109059(X1) ),
inference(spm,[status(thm)],[1217,392,theory(equality)]) ).
cnf(1224,plain,
( ~ collection(X1)
| ~ tptpcol_11_109125(X1) ),
inference(spm,[status(thm)],[1221,766,theory(equality)]) ).
cnf(1226,plain,
( ~ collection(X1)
| ~ tptpcol_12_109157(X1) ),
inference(spm,[status(thm)],[1224,271,theory(equality)]) ).
cnf(1228,plain,
( ~ collection(X1)
| ~ tptpcol_13_109173(X1) ),
inference(spm,[status(thm)],[1226,275,theory(equality)]) ).
cnf(1238,plain,
( ~ collection(X1)
| ~ tptpcol_15_109185(X1) ),
inference(spm,[status(thm)],[1228,513,theory(equality)]) ).
cnf(1242,negated_conjecture,
~ collection(c_tptpcol_16_62187),
inference(spm,[status(thm)],[1238,150,theory(equality)]) ).
cnf(1244,negated_conjecture,
$false,
inference(rw,[status(thm)],[1242,752,theory(equality)]) ).
cnf(1245,negated_conjecture,
$false,
inference(cn,[status(thm)],[1244,theory(equality)]) ).
cnf(1246,negated_conjecture,
$false,
1245,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR040+1.p
% --creating new selector for [CSR002+0.ax]
% -running prover on /tmp/tmptYl4aK/sel_CSR040+1.p_1 with time limit 29
% -prover status Theorem
% Problem CSR040+1.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR040+1.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR040+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
%
%------------------------------------------------------------------------------