%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR049+2 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art01.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:22:22 EST 2010
% Result : Theorem 238.72s
% Output : CNFRefutation 238.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 35
% Syntax : Number of formulae : 155 ( 98 unt; 0 def)
% Number of atoms : 220 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 123 ( 58 ~; 57 |; 3 &)
% ( 0 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 68 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(26,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_324) ).
fof(51,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_145) ).
fof(53,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_141) ).
fof(57,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_148) ).
fof(58,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_431) ).
fof(78,axiom,
! [X5,X9,X6] :
( ( disjointwith(X5,X9)
& genls(X6,X5) )
=> disjointwith(X6,X9) ),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_1122) ).
fof(79,axiom,
! [X2,X5,X6] :
( ( disjointwith(X2,X5)
& genls(X6,X5) )
=> disjointwith(X2,X6) ),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_1121) ).
fof(80,axiom,
! [X3,X7] :
( disjointwith(X3,X7)
=> disjointwith(X7,X3) ),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_1120) ).
fof(109,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_102) ).
fof(179,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_385) ).
fof(203,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_152) ).
fof(242,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_420) ).
fof(247,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_374) ).
fof(249,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_376) ).
fof(254,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_277) ).
fof(255,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_118) ).
fof(280,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_473) ).
fof(284,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_476) ).
fof(309,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_89) ).
fof(321,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_239) ).
fof(330,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_429) ).
fof(354,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_497) ).
fof(376,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_47) ).
fof(377,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_41) ).
fof(380,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_480) ).
fof(403,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_267) ).
fof(406,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_348) ).
fof(407,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_261) ).
fof(439,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_465) ).
fof(441,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_467) ).
fof(471,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_222) ).
fof(483,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_410) ).
fof(486,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_417) ).
fof(494,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',ax1_313) ).
fof(541,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/tmp/tmpMIgxrX/sel_CSR049+2.p_4',query99) ).
fof(542,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(assume_negation,[status(cth)],[541]) ).
cnf(602,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(split_conjunct,[status(thm)],[26]) ).
cnf(671,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(split_conjunct,[status(thm)],[51]) ).
cnf(675,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(split_conjunct,[status(thm)],[53]) ).
cnf(685,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(split_conjunct,[status(thm)],[57]) ).
cnf(686,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(split_conjunct,[status(thm)],[58]) ).
fof(738,plain,
! [X5,X9,X6] :
( ~ disjointwith(X5,X9)
| ~ genls(X6,X5)
| disjointwith(X6,X9) ),
inference(fof_nnf,[status(thm)],[78]) ).
fof(739,plain,
! [X10,X11,X12] :
( ~ disjointwith(X10,X11)
| ~ genls(X12,X10)
| disjointwith(X12,X11) ),
inference(variable_rename,[status(thm)],[738]) ).
cnf(740,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
inference(split_conjunct,[status(thm)],[739]) ).
fof(741,plain,
! [X2,X5,X6] :
( ~ disjointwith(X2,X5)
| ~ genls(X6,X5)
| disjointwith(X2,X6) ),
inference(fof_nnf,[status(thm)],[79]) ).
fof(742,plain,
! [X7,X8,X9] :
( ~ disjointwith(X7,X8)
| ~ genls(X9,X8)
| disjointwith(X7,X9) ),
inference(variable_rename,[status(thm)],[741]) ).
cnf(743,plain,
( disjointwith(X1,X2)
| ~ genls(X2,X3)
| ~ disjointwith(X1,X3) ),
inference(split_conjunct,[status(thm)],[742]) ).
fof(744,plain,
! [X3,X7] :
( ~ disjointwith(X3,X7)
| disjointwith(X7,X3) ),
inference(fof_nnf,[status(thm)],[80]) ).
fof(745,plain,
! [X8,X9] :
( ~ disjointwith(X8,X9)
| disjointwith(X9,X8) ),
inference(variable_rename,[status(thm)],[744]) ).
cnf(746,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
inference(split_conjunct,[status(thm)],[745]) ).
cnf(823,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(split_conjunct,[status(thm)],[109]) ).
cnf(1015,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(split_conjunct,[status(thm)],[179]) ).
cnf(1071,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[203]) ).
cnf(1176,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(split_conjunct,[status(thm)],[242]) ).
cnf(1187,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(split_conjunct,[status(thm)],[247]) ).
cnf(1191,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(split_conjunct,[status(thm)],[249]) ).
cnf(1202,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(split_conjunct,[status(thm)],[254]) ).
cnf(1203,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(split_conjunct,[status(thm)],[255]) ).
cnf(1263,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(split_conjunct,[status(thm)],[280]) ).
cnf(1273,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(split_conjunct,[status(thm)],[284]) ).
cnf(1340,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(split_conjunct,[status(thm)],[309]) ).
cnf(1372,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(split_conjunct,[status(thm)],[321]) ).
cnf(1391,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(split_conjunct,[status(thm)],[330]) ).
cnf(1447,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(split_conjunct,[status(thm)],[354]) ).
cnf(1507,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(split_conjunct,[status(thm)],[376]) ).
cnf(1508,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(split_conjunct,[status(thm)],[377]) ).
cnf(1513,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(split_conjunct,[status(thm)],[380]) ).
cnf(1574,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(split_conjunct,[status(thm)],[403]) ).
cnf(1579,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[406]) ).
cnf(1580,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(split_conjunct,[status(thm)],[407]) ).
cnf(1653,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(split_conjunct,[status(thm)],[439]) ).
cnf(1657,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(split_conjunct,[status(thm)],[441]) ).
cnf(1738,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(split_conjunct,[status(thm)],[471]) ).
cnf(1770,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(split_conjunct,[status(thm)],[483]) ).
cnf(1775,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(split_conjunct,[status(thm)],[486]) ).
cnf(1797,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(split_conjunct,[status(thm)],[494]) ).
fof(1907,negated_conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
& ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(fof_nnf,[status(thm)],[542]) ).
cnf(1908,negated_conjecture,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(split_conjunct,[status(thm)],[1907]) ).
cnf(1910,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(spm,[status(thm)],[746,1071,theory(equality)]) ).
cnf(2425,plain,
( disjointwith(X1,c_tptpcol_16_92269)
| ~ disjointwith(X1,c_tptpcol_15_92268) ),
inference(spm,[status(thm)],[743,1574,theory(equality)]) ).
cnf(2432,plain,
( disjointwith(X1,c_tptpcol_3_81921)
| ~ disjointwith(X1,c_tptpcol_2_65537) ),
inference(spm,[status(thm)],[743,1508,theory(equality)]) ).
cnf(2434,plain,
( disjointwith(X1,c_tptpcol_2_65537)
| ~ disjointwith(X1,c_tptpcol_1_65536) ),
inference(spm,[status(thm)],[743,1579,theory(equality)]) ).
cnf(2458,plain,
( disjointwith(X1,c_tptpcol_2_2)
| ~ disjointwith(X1,c_tptpcol_1_1) ),
inference(spm,[status(thm)],[743,671,theory(equality)]) ).
cnf(2459,plain,
( disjointwith(X1,c_tptpcol_12_26919)
| ~ disjointwith(X1,c_tptpcol_11_26887) ),
inference(spm,[status(thm)],[743,675,theory(equality)]) ).
cnf(2460,plain,
( disjointwith(X1,c_tptpcol_11_26887)
| ~ disjointwith(X1,c_tptpcol_10_26886) ),
inference(spm,[status(thm)],[743,1391,theory(equality)]) ).
cnf(2461,plain,
( disjointwith(X1,c_tptpcol_9_92165)
| ~ disjointwith(X1,c_tptpcol_8_92164) ),
inference(spm,[status(thm)],[743,685,theory(equality)]) ).
cnf(2462,plain,
( disjointwith(X1,c_tptpcol_8_92164)
| ~ disjointwith(X1,c_tptpcol_7_92163) ),
inference(spm,[status(thm)],[743,1176,theory(equality)]) ).
cnf(2481,plain,
( disjointwith(X1,c_tptpcol_15_92268)
| ~ disjointwith(X1,c_tptpcol_14_92264) ),
inference(spm,[status(thm)],[743,823,theory(equality)]) ).
cnf(2482,plain,
( disjointwith(X1,c_tptpcol_14_92264)
| ~ disjointwith(X1,c_tptpcol_13_92263) ),
inference(spm,[status(thm)],[743,1657,theory(equality)]) ).
cnf(2492,plain,
( disjointwith(X1,c_tptpcol_4_90113)
| ~ disjointwith(X1,c_tptpcol_3_81921) ),
inference(spm,[status(thm)],[743,1191,theory(equality)]) ).
cnf(2497,plain,
( disjointwith(X1,c_tptpcol_13_26920)
| ~ disjointwith(X1,c_tptpcol_12_26919) ),
inference(spm,[status(thm)],[743,1653,theory(equality)]) ).
cnf(2502,plain,
( disjointwith(X1,c_tptpcol_12_92262)
| ~ disjointwith(X1,c_tptpcol_11_92230) ),
inference(spm,[status(thm)],[743,1340,theory(equality)]) ).
cnf(2511,plain,
( disjointwith(X1,c_tptpcol_10_26886)
| ~ disjointwith(X1,c_tptpcol_9_26885) ),
inference(spm,[status(thm)],[743,1202,theory(equality)]) ).
cnf(2512,plain,
( disjointwith(X1,c_tptpcol_9_26885)
| ~ disjointwith(X1,c_tptpcol_8_26629) ),
inference(spm,[status(thm)],[743,1770,theory(equality)]) ).
cnf(2520,plain,
( disjointwith(X1,c_tptpcol_13_92263)
| ~ disjointwith(X1,c_tptpcol_12_92262) ),
inference(spm,[status(thm)],[743,1263,theory(equality)]) ).
cnf(2523,plain,
( disjointwith(X1,c_tptpcol_11_92230)
| ~ disjointwith(X1,c_tptpcol_10_92166) ),
inference(spm,[status(thm)],[743,1507,theory(equality)]) ).
cnf(2524,plain,
( disjointwith(X1,c_tptpcol_8_26629)
| ~ disjointwith(X1,c_tptpcol_7_26628) ),
inference(spm,[status(thm)],[743,1372,theory(equality)]) ).
cnf(2529,plain,
( disjointwith(X1,c_tptpcol_10_92166)
| ~ disjointwith(X1,c_tptpcol_9_92165) ),
inference(spm,[status(thm)],[743,1447,theory(equality)]) ).
cnf(2534,plain,
( disjointwith(c_tptpcol_16_26926,X1)
| ~ disjointwith(c_tptpcol_15_26925,X1) ),
inference(spm,[status(thm)],[740,686,theory(equality)]) ).
cnf(2539,plain,
( disjointwith(c_tptpcol_3_16386,X1)
| ~ disjointwith(c_tptpcol_2_2,X1) ),
inference(spm,[status(thm)],[740,1015,theory(equality)]) ).
cnf(2555,plain,
( disjointwith(c_tptpcol_7_92163,X1)
| ~ disjointwith(c_tptpcol_6_92162,X1) ),
inference(spm,[status(thm)],[740,602,theory(equality)]) ).
cnf(2556,plain,
( disjointwith(c_tptpcol_6_92162,X1)
| ~ disjointwith(c_tptpcol_5_90114,X1) ),
inference(spm,[status(thm)],[740,1775,theory(equality)]) ).
cnf(2573,plain,
( disjointwith(c_tptpcol_15_26925,X1)
| ~ disjointwith(c_tptpcol_14_26921,X1) ),
inference(spm,[status(thm)],[740,1513,theory(equality)]) ).
cnf(2606,plain,
( disjointwith(c_tptpcol_14_26921,X1)
| ~ disjointwith(c_tptpcol_13_26920,X1) ),
inference(spm,[status(thm)],[740,1797,theory(equality)]) ).
cnf(2610,plain,
( disjointwith(c_tptpcol_6_26627,X1)
| ~ disjointwith(c_tptpcol_5_24579,X1) ),
inference(spm,[status(thm)],[740,1187,theory(equality)]) ).
cnf(2627,plain,
( disjointwith(c_tptpcol_5_24579,X1)
| ~ disjointwith(c_tptpcol_4_24578,X1) ),
inference(spm,[status(thm)],[740,1203,theory(equality)]) ).
cnf(2628,plain,
( disjointwith(c_tptpcol_4_24578,X1)
| ~ disjointwith(c_tptpcol_3_16386,X1) ),
inference(spm,[status(thm)],[740,1738,theory(equality)]) ).
cnf(2631,plain,
( disjointwith(c_tptpcol_5_90114,X1)
| ~ disjointwith(c_tptpcol_4_90113,X1) ),
inference(spm,[status(thm)],[740,1273,theory(equality)]) ).
cnf(2635,plain,
( disjointwith(c_tptpcol_7_26628,X1)
| ~ disjointwith(c_tptpcol_6_26627,X1) ),
inference(spm,[status(thm)],[740,1580,theory(equality)]) ).
cnf(5873,negated_conjecture,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(spm,[status(thm)],[1908,2425,theory(equality)]) ).
cnf(6035,plain,
( disjointwith(c_tptpcol_3_81921,X1)
| ~ disjointwith(X1,c_tptpcol_2_65537) ),
inference(spm,[status(thm)],[746,2432,theory(equality)]) ).
cnf(7379,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_2_2),
inference(spm,[status(thm)],[2458,1910,theory(equality)]) ).
cnf(7381,plain,
disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536),
inference(spm,[status(thm)],[746,7379,theory(equality)]) ).
cnf(7522,plain,
( disjointwith(c_tptpcol_8_92164,X1)
| ~ disjointwith(X1,c_tptpcol_7_92163) ),
inference(spm,[status(thm)],[746,2462,theory(equality)]) ).
cnf(8258,plain,
( disjointwith(c_tptpcol_4_90113,X1)
| ~ disjointwith(X1,c_tptpcol_3_81921) ),
inference(spm,[status(thm)],[746,2492,theory(equality)]) ).
cnf(8381,plain,
( disjointwith(c_tptpcol_13_26920,X1)
| ~ disjointwith(X1,c_tptpcol_12_26919) ),
inference(spm,[status(thm)],[746,2497,theory(equality)]) ).
cnf(8762,plain,
( disjointwith(c_tptpcol_10_92166,X1)
| ~ disjointwith(X1,c_tptpcol_9_92165) ),
inference(spm,[status(thm)],[746,2529,theory(equality)]) ).
cnf(8995,plain,
( disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)
| ~ disjointwith(c_tptpcol_2_2,c_tptpcol_1_65536) ),
inference(spm,[status(thm)],[2539,2434,theory(equality)]) ).
cnf(9038,plain,
( disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537)
| $false ),
inference(rw,[status(thm)],[8995,7381,theory(equality)]) ).
cnf(9039,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(cn,[status(thm)],[9038,theory(equality)]) ).
cnf(10441,plain,
( disjointwith(X1,c_tptpcol_7_92163)
| ~ disjointwith(c_tptpcol_6_92162,X1) ),
inference(spm,[status(thm)],[746,2555,theory(equality)]) ).
cnf(41136,plain,
( disjointwith(c_tptpcol_3_81921,c_tptpcol_4_24578)
| ~ disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537) ),
inference(spm,[status(thm)],[6035,2628,theory(equality)]) ).
cnf(41151,plain,
( disjointwith(c_tptpcol_3_81921,c_tptpcol_4_24578)
| $false ),
inference(rw,[status(thm)],[41136,9039,theory(equality)]) ).
cnf(41152,plain,
disjointwith(c_tptpcol_3_81921,c_tptpcol_4_24578),
inference(cn,[status(thm)],[41151,theory(equality)]) ).
cnf(41305,plain,
disjointwith(c_tptpcol_4_24578,c_tptpcol_3_81921),
inference(spm,[status(thm)],[746,41152,theory(equality)]) ).
cnf(41444,plain,
disjointwith(c_tptpcol_5_24579,c_tptpcol_3_81921),
inference(spm,[status(thm)],[2627,41305,theory(equality)]) ).
cnf(41628,plain,
disjointwith(c_tptpcol_6_26627,c_tptpcol_3_81921),
inference(spm,[status(thm)],[2610,41444,theory(equality)]) ).
cnf(51275,plain,
( disjointwith(c_tptpcol_4_90113,c_tptpcol_7_26628)
| ~ disjointwith(c_tptpcol_6_26627,c_tptpcol_3_81921) ),
inference(spm,[status(thm)],[8258,2635,theory(equality)]) ).
cnf(51301,plain,
( disjointwith(c_tptpcol_4_90113,c_tptpcol_7_26628)
| $false ),
inference(rw,[status(thm)],[51275,41628,theory(equality)]) ).
cnf(51302,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_7_26628),
inference(cn,[status(thm)],[51301,theory(equality)]) ).
cnf(57163,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_8_26629),
inference(spm,[status(thm)],[2524,51302,theory(equality)]) ).
cnf(62223,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_9_26885),
inference(spm,[status(thm)],[2512,57163,theory(equality)]) ).
cnf(67335,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_10_26886),
inference(spm,[status(thm)],[2511,62223,theory(equality)]) ).
cnf(72800,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_11_26887),
inference(spm,[status(thm)],[2460,67335,theory(equality)]) ).
cnf(78151,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_12_26919),
inference(spm,[status(thm)],[2459,72800,theory(equality)]) ).
cnf(82373,plain,
disjointwith(c_tptpcol_13_26920,c_tptpcol_4_90113),
inference(spm,[status(thm)],[8381,78151,theory(equality)]) ).
cnf(86983,plain,
disjointwith(c_tptpcol_14_26921,c_tptpcol_4_90113),
inference(spm,[status(thm)],[2606,82373,theory(equality)]) ).
cnf(92527,plain,
disjointwith(c_tptpcol_15_26925,c_tptpcol_4_90113),
inference(spm,[status(thm)],[2573,86983,theory(equality)]) ).
cnf(97553,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_4_90113),
inference(spm,[status(thm)],[2534,92527,theory(equality)]) ).
cnf(97564,plain,
disjointwith(c_tptpcol_4_90113,c_tptpcol_16_26926),
inference(spm,[status(thm)],[746,97553,theory(equality)]) ).
cnf(97585,plain,
disjointwith(c_tptpcol_5_90114,c_tptpcol_16_26926),
inference(spm,[status(thm)],[2631,97564,theory(equality)]) ).
cnf(97630,plain,
disjointwith(c_tptpcol_6_92162,c_tptpcol_16_26926),
inference(spm,[status(thm)],[2556,97585,theory(equality)]) ).
cnf(97680,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_7_92163),
inference(spm,[status(thm)],[10441,97630,theory(equality)]) ).
cnf(97737,plain,
disjointwith(c_tptpcol_8_92164,c_tptpcol_16_26926),
inference(spm,[status(thm)],[7522,97680,theory(equality)]) ).
cnf(97781,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_8_92164),
inference(spm,[status(thm)],[746,97737,theory(equality)]) ).
cnf(97847,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_9_92165),
inference(spm,[status(thm)],[2461,97781,theory(equality)]) ).
cnf(97952,plain,
disjointwith(c_tptpcol_10_92166,c_tptpcol_16_26926),
inference(spm,[status(thm)],[8762,97847,theory(equality)]) ).
cnf(98007,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_10_92166),
inference(spm,[status(thm)],[746,97952,theory(equality)]) ).
cnf(98092,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_11_92230),
inference(spm,[status(thm)],[2523,98007,theory(equality)]) ).
cnf(98211,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_12_92262),
inference(spm,[status(thm)],[2502,98092,theory(equality)]) ).
cnf(98295,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_13_92263),
inference(spm,[status(thm)],[2520,98211,theory(equality)]) ).
cnf(98346,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_14_92264),
inference(spm,[status(thm)],[2482,98295,theory(equality)]) ).
cnf(98514,plain,
disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(spm,[status(thm)],[2481,98346,theory(equality)]) ).
cnf(98521,plain,
$false,
inference(sr,[status(thm)],[98514,5873,theory(equality)]) ).
cnf(98522,plain,
$false,
98521,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR049+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/tmpMIgxrX/sel_CSR049+2.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpMIgxrX/sel_CSR049+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/tmpMIgxrX/sel_CSR049+2.p_3 with time limit 75
% -prover status ResourceOut
% --creating new selector for [CSR002+1.ax]
% -running prover on /tmp/tmpMIgxrX/sel_CSR049+2.p_4 with time limit 55
% -prover status Theorem
% Problem CSR049+2.p solved in phase 3.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR049+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR049+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
%
%------------------------------------------------------------------------------