%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR039+2 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art02.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:13:20 EST 2010
% Result : Theorem 201.37s
% Output : CNFRefutation 201.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 31
% Syntax : Number of formulae : 133 ( 79 unt; 0 def)
% Number of atoms : 195 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 123 ( 61 ~; 54 |; 3 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 30 con; 0-2 aty)
% Number of variables : 60 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(7,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_285) ).
fof(20,axiom,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_353) ).
fof(22,axiom,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_351) ).
fof(51,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_145) ).
fof(77,axiom,
! [X5,X9,X6] :
( ( disjointwith(X5,X9)
& genls(X6,X5) )
=> disjointwith(X6,X9) ),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_1122) ).
fof(78,axiom,
! [X2,X5,X6] :
( ( disjointwith(X2,X5)
& genls(X6,X5) )
=> disjointwith(X2,X6) ),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_1121) ).
fof(79,axiom,
! [X3,X7] :
( disjointwith(X3,X7)
=> disjointwith(X7,X3) ),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_1120) ).
fof(105,axiom,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_109) ).
fof(175,axiom,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_208) ).
fof(178,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_385) ).
fof(201,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_152) ).
fof(211,axiom,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_23) ).
fof(241,axiom,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_370) ).
fof(247,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_376) ).
fof(249,axiom,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_379) ).
fof(272,axiom,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_182) ).
fof(276,axiom,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_483) ).
fof(282,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_476) ).
fof(297,axiom,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_14) ).
fof(375,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_41) ).
fof(376,axiom,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_43) ).
fof(403,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_348) ).
fof(405,axiom,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_345) ).
fof(430,axiom,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_191) ).
fof(482,axiom,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_372) ).
fof(483,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_417) ).
fof(499,axiom,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_255) ).
fof(505,axiom,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_175) ).
fof(527,axiom,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_78) ).
fof(531,axiom,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',ax1_72) ).
fof(537,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
file('/tmp/tmpeBBqs_/sel_CSR039+2.p_4',query89) ).
fof(538,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
=> disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(assume_negation,[status(cth)],[537]) ).
cnf(555,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(split_conjunct,[status(thm)],[7]) ).
cnf(586,plain,
genls(c_tptpcol_8_18438,c_tptpcol_7_18437),
inference(split_conjunct,[status(thm)],[20]) ).
cnf(590,plain,
genls(c_tptpcol_6_18436,c_tptpcol_5_16388),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(667,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(split_conjunct,[status(thm)],[51]) ).
fof(733,plain,
! [X5,X9,X6] :
( ~ disjointwith(X5,X9)
| ~ genls(X6,X5)
| disjointwith(X6,X9) ),
inference(fof_nnf,[status(thm)],[77]) ).
fof(734,plain,
! [X10,X11,X12] :
( ~ disjointwith(X10,X11)
| ~ genls(X12,X10)
| disjointwith(X12,X11) ),
inference(variable_rename,[status(thm)],[733]) ).
cnf(735,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
inference(split_conjunct,[status(thm)],[734]) ).
fof(736,plain,
! [X2,X5,X6] :
( ~ disjointwith(X2,X5)
| ~ genls(X6,X5)
| disjointwith(X2,X6) ),
inference(fof_nnf,[status(thm)],[78]) ).
fof(737,plain,
! [X7,X8,X9] :
( ~ disjointwith(X7,X8)
| ~ genls(X9,X8)
| disjointwith(X7,X9) ),
inference(variable_rename,[status(thm)],[736]) ).
cnf(738,plain,
( disjointwith(X1,X2)
| ~ genls(X2,X3)
| ~ disjointwith(X1,X3) ),
inference(split_conjunct,[status(thm)],[737]) ).
fof(739,plain,
! [X3,X7] :
( ~ disjointwith(X3,X7)
| disjointwith(X7,X3) ),
inference(fof_nnf,[status(thm)],[79]) ).
fof(740,plain,
! [X8,X9] :
( ~ disjointwith(X8,X9)
| disjointwith(X9,X8) ),
inference(variable_rename,[status(thm)],[739]) ).
cnf(741,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
inference(split_conjunct,[status(thm)],[740]) ).
cnf(813,plain,
genls(c_tptpcol_12_18663,c_tptpcol_11_18631),
inference(split_conjunct,[status(thm)],[105]) ).
cnf(1005,plain,
genls(c_tptpcol_13_18664,c_tptpcol_12_18663),
inference(split_conjunct,[status(thm)],[175]) ).
cnf(1012,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(split_conjunct,[status(thm)],[178]) ).
cnf(1067,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[201]) ).
cnf(1093,plain,
genls(c_tptpcol_5_16388,c_tptpcol_4_16387),
inference(split_conjunct,[status(thm)],[211]) ).
cnf(1173,plain,
genls(c_tptpcol_9_93699,c_tptpcol_8_93698),
inference(split_conjunct,[status(thm)],[241]) ).
cnf(1187,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(split_conjunct,[status(thm)],[247]) ).
cnf(1191,plain,
genls(c_tptpcol_10_93700,c_tptpcol_9_93699),
inference(split_conjunct,[status(thm)],[249]) ).
cnf(1249,plain,
genls(c_tptpcol_15_93775,c_tptpcol_14_93774),
inference(split_conjunct,[status(thm)],[272]) ).
cnf(1257,plain,
genls(c_tptpcol_7_18437,c_tptpcol_6_18436),
inference(split_conjunct,[status(thm)],[276]) ).
cnf(1269,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(split_conjunct,[status(thm)],[282]) ).
cnf(1309,plain,
genls(c_tptpcol_7_93186,c_tptpcol_6_92162),
inference(split_conjunct,[status(thm)],[297]) ).
cnf(1502,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(split_conjunct,[status(thm)],[375]) ).
cnf(1503,plain,
genls(c_tptpcol_10_18567,c_tptpcol_9_18439),
inference(split_conjunct,[status(thm)],[376]) ).
cnf(1572,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[403]) ).
cnf(1574,plain,
genls(c_tptpcol_8_93698,c_tptpcol_7_93186),
inference(split_conjunct,[status(thm)],[405]) ).
cnf(1634,plain,
genls(c_tptpcol_14_93774,c_tptpcol_13_93766),
inference(split_conjunct,[status(thm)],[430]) ).
cnf(1767,plain,
genls(c_tptpcol_11_93764,c_tptpcol_10_93700),
inference(split_conjunct,[status(thm)],[482]) ).
cnf(1768,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(split_conjunct,[status(thm)],[483]) ).
cnf(1810,plain,
genls(c_tptpcol_9_18439,c_tptpcol_8_18438),
inference(split_conjunct,[status(thm)],[499]) ).
cnf(1822,plain,
genls(c_tptpcol_11_18631,c_tptpcol_10_18567),
inference(split_conjunct,[status(thm)],[505]) ).
cnf(1878,plain,
genls(c_tptpcol_13_93766,c_tptpcol_12_93765),
inference(split_conjunct,[status(thm)],[527]) ).
cnf(1886,plain,
genls(c_tptpcol_12_93765,c_tptpcol_11_93764),
inference(split_conjunct,[status(thm)],[531]) ).
fof(1899,negated_conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7))
& ~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664) ),
inference(fof_nnf,[status(thm)],[538]) ).
cnf(1900,negated_conjecture,
~ disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664),
inference(split_conjunct,[status(thm)],[1899]) ).
cnf(1902,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(spm,[status(thm)],[741,1067,theory(equality)]) ).
cnf(2411,plain,
( disjointwith(X1,c_tptpcol_4_16387)
| ~ disjointwith(X1,c_tptpcol_3_16386) ),
inference(spm,[status(thm)],[738,555,theory(equality)]) ).
cnf(2417,plain,
( disjointwith(X1,c_tptpcol_2_65537)
| ~ disjointwith(X1,c_tptpcol_1_65536) ),
inference(spm,[status(thm)],[738,1572,theory(equality)]) ).
cnf(2425,plain,
( disjointwith(X1,c_tptpcol_5_16388)
| ~ disjointwith(X1,c_tptpcol_4_16387) ),
inference(spm,[status(thm)],[738,1093,theory(equality)]) ).
cnf(2429,plain,
( disjointwith(X1,c_tptpcol_6_92162)
| ~ disjointwith(X1,c_tptpcol_5_90114) ),
inference(spm,[status(thm)],[738,1768,theory(equality)]) ).
cnf(2441,plain,
( disjointwith(X1,c_tptpcol_2_2)
| ~ disjointwith(X1,c_tptpcol_1_1) ),
inference(spm,[status(thm)],[738,667,theory(equality)]) ).
cnf(2452,plain,
( disjointwith(X1,c_tptpcol_14_93774)
| ~ disjointwith(X1,c_tptpcol_13_93766) ),
inference(spm,[status(thm)],[738,1634,theory(equality)]) ).
cnf(2457,plain,
( disjointwith(X1,c_tptpcol_7_93186)
| ~ disjointwith(X1,c_tptpcol_6_92162) ),
inference(spm,[status(thm)],[738,1309,theory(equality)]) ).
cnf(2479,plain,
( disjointwith(X1,c_tptpcol_8_93698)
| ~ disjointwith(X1,c_tptpcol_7_93186) ),
inference(spm,[status(thm)],[738,1574,theory(equality)]) ).
cnf(2497,plain,
( disjointwith(X1,c_tptpcol_10_93700)
| ~ disjointwith(X1,c_tptpcol_9_93699) ),
inference(spm,[status(thm)],[738,1191,theory(equality)]) ).
cnf(2498,plain,
( disjointwith(X1,c_tptpcol_9_93699)
| ~ disjointwith(X1,c_tptpcol_8_93698) ),
inference(spm,[status(thm)],[738,1173,theory(equality)]) ).
cnf(2503,plain,
( disjointwith(X1,c_tptpcol_5_90114)
| ~ disjointwith(X1,c_tptpcol_4_90113) ),
inference(spm,[status(thm)],[738,1269,theory(equality)]) ).
cnf(2512,plain,
( disjointwith(X1,c_tptpcol_13_93766)
| ~ disjointwith(X1,c_tptpcol_12_93765) ),
inference(spm,[status(thm)],[738,1878,theory(equality)]) ).
cnf(2513,plain,
( disjointwith(X1,c_tptpcol_11_93764)
| ~ disjointwith(X1,c_tptpcol_10_93700) ),
inference(spm,[status(thm)],[738,1767,theory(equality)]) ).
cnf(2516,plain,
( disjointwith(X1,c_tptpcol_12_93765)
| ~ disjointwith(X1,c_tptpcol_11_93764) ),
inference(spm,[status(thm)],[738,1886,theory(equality)]) ).
cnf(2517,plain,
( disjointwith(c_tptpcol_15_93775,X1)
| ~ disjointwith(c_tptpcol_14_93774,X1) ),
inference(spm,[status(thm)],[735,1249,theory(equality)]) ).
cnf(2518,plain,
( disjointwith(c_tptpcol_13_18664,X1)
| ~ disjointwith(c_tptpcol_12_18663,X1) ),
inference(spm,[status(thm)],[735,1005,theory(equality)]) ).
cnf(2522,plain,
( disjointwith(c_tptpcol_3_16386,X1)
| ~ disjointwith(c_tptpcol_2_2,X1) ),
inference(spm,[status(thm)],[735,1012,theory(equality)]) ).
cnf(2525,plain,
( disjointwith(c_tptpcol_3_81921,X1)
| ~ disjointwith(c_tptpcol_2_65537,X1) ),
inference(spm,[status(thm)],[735,1502,theory(equality)]) ).
cnf(2526,plain,
( disjointwith(c_tptpcol_10_18567,X1)
| ~ disjointwith(c_tptpcol_9_18439,X1) ),
inference(spm,[status(thm)],[735,1503,theory(equality)]) ).
cnf(2532,plain,
( disjointwith(c_tptpcol_8_18438,X1)
| ~ disjointwith(c_tptpcol_7_18437,X1) ),
inference(spm,[status(thm)],[735,586,theory(equality)]) ).
cnf(2533,plain,
( disjointwith(c_tptpcol_7_18437,X1)
| ~ disjointwith(c_tptpcol_6_18436,X1) ),
inference(spm,[status(thm)],[735,1257,theory(equality)]) ).
cnf(2534,plain,
( disjointwith(c_tptpcol_6_18436,X1)
| ~ disjointwith(c_tptpcol_5_16388,X1) ),
inference(spm,[status(thm)],[735,590,theory(equality)]) ).
cnf(2570,plain,
( disjointwith(c_tptpcol_12_18663,X1)
| ~ disjointwith(c_tptpcol_11_18631,X1) ),
inference(spm,[status(thm)],[735,813,theory(equality)]) ).
cnf(2571,plain,
( disjointwith(c_tptpcol_11_18631,X1)
| ~ disjointwith(c_tptpcol_10_18567,X1) ),
inference(spm,[status(thm)],[735,1822,theory(equality)]) ).
cnf(2583,plain,
( disjointwith(c_tptpcol_4_90113,X1)
| ~ disjointwith(c_tptpcol_3_81921,X1) ),
inference(spm,[status(thm)],[735,1187,theory(equality)]) ).
cnf(2624,plain,
( disjointwith(c_tptpcol_9_18439,X1)
| ~ disjointwith(c_tptpcol_8_18438,X1) ),
inference(spm,[status(thm)],[735,1810,theory(equality)]) ).
cnf(5817,negated_conjecture,
~ disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664),
inference(spm,[status(thm)],[1900,2517,theory(equality)]) ).
cnf(6488,plain,
( disjointwith(c_tptpcol_5_16388,X1)
| ~ disjointwith(X1,c_tptpcol_4_16387) ),
inference(spm,[status(thm)],[741,2425,theory(equality)]) ).
cnf(7623,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(spm,[status(thm)],[2441,1902,theory(equality)]) ).
cnf(7626,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(spm,[status(thm)],[741,7623,theory(equality)]) ).
cnf(8716,plain,
( disjointwith(X1,c_tptpcol_10_93700)
| ~ disjointwith(X1,c_tptpcol_8_93698) ),
inference(spm,[status(thm)],[2497,2498,theory(equality)]) ).
cnf(8886,plain,
( disjointwith(c_tptpcol_13_18664,c_tptpcol_12_93765)
| ~ disjointwith(c_tptpcol_12_18663,c_tptpcol_11_93764) ),
inference(spm,[status(thm)],[2516,2518,theory(equality)]) ).
cnf(9085,plain,
( disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)
| ~ disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536) ),
inference(spm,[status(thm)],[2522,2417,theory(equality)]) ).
cnf(9129,plain,
( disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)
| $false ),
inference(rw,[status(thm)],[9085,7626,theory(equality)]) ).
cnf(9130,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(cn,[status(thm)],[9129,theory(equality)]) ).
cnf(9155,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),
inference(spm,[status(thm)],[741,9130,theory(equality)]) ).
cnf(9394,plain,
( disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)
| ~ disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386) ),
inference(spm,[status(thm)],[2411,2525,theory(equality)]) ).
cnf(9457,plain,
( disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)
| $false ),
inference(rw,[status(thm)],[9394,9155,theory(equality)]) ).
cnf(9458,plain,
disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387),
inference(cn,[status(thm)],[9457,theory(equality)]) ).
cnf(25004,plain,
( disjointwith(c_tptpcol_13_18664,c_tptpcol_13_93766)
| ~ disjointwith(c_tptpcol_12_18663,c_tptpcol_11_93764) ),
inference(spm,[status(thm)],[2512,8886,theory(equality)]) ).
cnf(27461,plain,
( disjointwith(c_tptpcol_13_18664,c_tptpcol_14_93774)
| ~ disjointwith(c_tptpcol_12_18663,c_tptpcol_11_93764) ),
inference(spm,[status(thm)],[2452,25004,theory(equality)]) ).
cnf(28293,plain,
( disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664)
| ~ disjointwith(c_tptpcol_12_18663,c_tptpcol_11_93764) ),
inference(spm,[status(thm)],[741,27461,theory(equality)]) ).
cnf(28299,plain,
~ disjointwith(c_tptpcol_12_18663,c_tptpcol_11_93764),
inference(sr,[status(thm)],[28293,5817,theory(equality)]) ).
cnf(28316,plain,
~ disjointwith(c_tptpcol_12_18663,c_tptpcol_10_93700),
inference(spm,[status(thm)],[28299,2513,theory(equality)]) ).
cnf(45233,plain,
( disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113)
| ~ disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387) ),
inference(spm,[status(thm)],[6488,2583,theory(equality)]) ).
cnf(45279,plain,
( disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113)
| $false ),
inference(rw,[status(thm)],[45233,9458,theory(equality)]) ).
cnf(45280,plain,
disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113),
inference(cn,[status(thm)],[45279,theory(equality)]) ).
cnf(45501,plain,
disjointwith(c_tptpcol_5_16388,c_tptpcol_5_90114),
inference(spm,[status(thm)],[2503,45280,theory(equality)]) ).
cnf(45868,plain,
disjointwith(c_tptpcol_5_16388,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2429,45501,theory(equality)]) ).
cnf(46156,plain,
disjointwith(c_tptpcol_6_18436,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2534,45868,theory(equality)]) ).
cnf(46561,plain,
disjointwith(c_tptpcol_7_18437,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2533,46156,theory(equality)]) ).
cnf(47121,plain,
disjointwith(c_tptpcol_8_18438,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2532,46561,theory(equality)]) ).
cnf(48662,plain,
disjointwith(c_tptpcol_9_18439,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2624,47121,theory(equality)]) ).
cnf(51448,plain,
disjointwith(c_tptpcol_10_18567,c_tptpcol_6_92162),
inference(spm,[status(thm)],[2526,48662,theory(equality)]) ).
cnf(57535,plain,
( disjointwith(c_tptpcol_12_18663,c_tptpcol_10_93700)
| ~ disjointwith(c_tptpcol_11_18631,c_tptpcol_8_93698) ),
inference(spm,[status(thm)],[2570,8716,theory(equality)]) ).
cnf(57569,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_8_93698),
inference(sr,[status(thm)],[57535,28316,theory(equality)]) ).
cnf(57572,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_7_93186),
inference(spm,[status(thm)],[57569,2479,theory(equality)]) ).
cnf(57575,plain,
~ disjointwith(c_tptpcol_11_18631,c_tptpcol_6_92162),
inference(spm,[status(thm)],[57572,2457,theory(equality)]) ).
cnf(57702,plain,
~ disjointwith(c_tptpcol_10_18567,c_tptpcol_6_92162),
inference(spm,[status(thm)],[57575,2571,theory(equality)]) ).
cnf(57703,plain,
$false,
inference(rw,[status(thm)],[57702,51448,theory(equality)]) ).
cnf(57704,plain,
$false,
inference(cn,[status(thm)],[57703,theory(equality)]) ).
cnf(57705,plain,
$false,
57704,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR039+2.p
% --creating new selector for [CSR002+1.ax]
% eprover: CPU time limit exceeded, terminating
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpeBBqs_/sel_CSR039+2.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpeBBqs_/sel_CSR039+2.p_2 with time limit 81
% -prover status ResourceOut
% --creating new selector for [CSR002+1.ax]
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpeBBqs_/sel_CSR039+2.p_3 with time limit 74
% -prover status ResourceOut
% --creating new selector for [CSR002+1.ax]
% -running prover on /tmp/tmpeBBqs_/sel_CSR039+2.p_4 with time limit 55
% -prover status Theorem
% Problem CSR039+2.p solved in phase 3.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR039+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR039+2.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
%
%------------------------------------------------------------------------------