%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR036+3 : 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:10:16 EST 2010
% Result : Theorem 132.09s
% Output : CNFRefutation 132.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 34
% Syntax : Number of formulae : 149 ( 90 unt; 0 def)
% Number of atoms : 216 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 125 ( 58 ~; 59 |; 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 : 32 ( 32 usr; 32 con; 0-0 aty)
% Number of variables : 65 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(6,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_867) ).
fof(11,axiom,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1300) ).
fof(49,axiom,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3715) ).
fof(55,axiom,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1975) ).
fof(83,axiom,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_4373) ).
fof(86,axiom,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_176) ).
fof(95,axiom,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2287) ).
fof(107,axiom,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2218) ).
fof(113,axiom,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_487) ).
fof(133,axiom,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_227) ).
fof(145,axiom,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3349) ).
fof(147,axiom,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3764) ).
fof(161,axiom,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_4247) ).
fof(164,axiom,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1760) ).
fof(184,axiom,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2146) ).
fof(186,axiom,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2142) ).
fof(188,axiom,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_512) ).
fof(229,axiom,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1731) ).
fof(238,axiom,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2671) ).
fof(258,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3978) ).
fof(294,axiom,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3803) ).
fof(310,axiom,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3781) ).
fof(311,axiom,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_793) ).
fof(324,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3253) ).
fof(344,axiom,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_3329) ).
fof(360,axiom,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_2510) ).
fof(367,axiom,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_615) ).
fof(374,axiom,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_759) ).
fof(379,axiom,
! [X5,X11] :
( disjointwith(X5,X11)
=> disjointwith(X11,X5) ),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_7584) ).
fof(386,axiom,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1708) ).
fof(392,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_1248) ).
fof(414,axiom,
! [X7,X3,X8] :
( ( disjointwith(X7,X3)
& genls(X8,X7) )
=> disjointwith(X8,X3) ),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_7586) ).
fof(416,axiom,
! [X2,X7,X8] :
( ( disjointwith(X2,X7)
& genls(X8,X7) )
=> disjointwith(X2,X8) ),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',ax2_7585) ).
fof(530,conjecture,
( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
file('/tmp/tmpsxCYfn/sel_CSR036+3.p_3',query136) ).
fof(531,negated_conjecture,
~ ( mtvisible(c_tptp_member974_mt)
=> disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(assume_negation,[status(cth)],[530]) ).
cnf(545,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[6]) ).
cnf(554,plain,
genls(c_tptpcol_15_22076,c_tptpcol_14_22072),
inference(split_conjunct,[status(thm)],[11]) ).
cnf(646,plain,
genls(c_tptpcol_7_21508,c_tptpcol_6_20484),
inference(split_conjunct,[status(thm)],[49]) ).
cnf(661,plain,
genls(c_tptpcol_14_22072,c_tptpcol_13_22071),
inference(split_conjunct,[status(thm)],[55]) ).
cnf(727,plain,
genls(c_tptpcol_12_22055,c_tptpcol_11_22023),
inference(split_conjunct,[status(thm)],[83]) ).
cnf(734,plain,
genls(c_tptpcol_4_65539,c_tptpcol_3_65538),
inference(split_conjunct,[status(thm)],[86]) ).
cnf(757,plain,
genls(c_tptpcol_7_72707,c_tptpcol_6_71683),
inference(split_conjunct,[status(thm)],[95]) ).
cnf(787,plain,
genls(c_tptpcol_13_22071,c_tptpcol_12_22055),
inference(split_conjunct,[status(thm)],[107]) ).
cnf(799,plain,
genls(c_tptpcol_11_22023,c_tptpcol_10_22022),
inference(split_conjunct,[status(thm)],[113]) ).
cnf(847,plain,
genls(c_tptpcol_10_72710,c_tptpcol_9_72709),
inference(split_conjunct,[status(thm)],[133]) ).
cnf(881,plain,
genls(c_tptpcol_5_20483,c_tptpcol_4_16387),
inference(split_conjunct,[status(thm)],[145]) ).
cnf(883,plain,
genls(c_tptpcol_13_72791,c_tptpcol_12_72775),
inference(split_conjunct,[status(thm)],[147]) ).
cnf(911,plain,
genls(c_tptpcol_15_72793,c_tptpcol_14_72792),
inference(split_conjunct,[status(thm)],[161]) ).
cnf(916,plain,
genls(c_tptpcol_14_72792,c_tptpcol_13_72791),
inference(split_conjunct,[status(thm)],[164]) ).
cnf(964,plain,
genls(c_tptpcol_12_72775,c_tptpcol_11_72774),
inference(split_conjunct,[status(thm)],[184]) ).
cnf(968,plain,
genls(c_tptpcol_8_72708,c_tptpcol_7_72707),
inference(split_conjunct,[status(thm)],[186]) ).
cnf(972,plain,
genls(c_tptpcol_16_72795,c_tptpcol_15_72793),
inference(split_conjunct,[status(thm)],[188]) ).
cnf(1079,plain,
genls(c_tptpcol_9_22021,c_tptpcol_8_22020),
inference(split_conjunct,[status(thm)],[229]) ).
cnf(1096,plain,
genls(c_tptpcol_8_22020,c_tptpcol_7_21508),
inference(split_conjunct,[status(thm)],[238]) ).
cnf(1144,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(split_conjunct,[status(thm)],[258]) ).
cnf(1227,plain,
genls(c_tptpcol_10_22022,c_tptpcol_9_22021),
inference(split_conjunct,[status(thm)],[294]) ).
cnf(1267,plain,
genls(c_tptpcol_5_69635,c_tptpcol_4_65539),
inference(split_conjunct,[status(thm)],[310]) ).
cnf(1268,plain,
genls(c_tptpcol_6_20484,c_tptpcol_5_20483),
inference(split_conjunct,[status(thm)],[311]) ).
cnf(1293,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(split_conjunct,[status(thm)],[324]) ).
cnf(1332,plain,
genls(c_tptpcol_6_71683,c_tptpcol_5_69635),
inference(split_conjunct,[status(thm)],[344]) ).
cnf(1365,plain,
genls(c_tptpcol_4_16387,c_tptpcol_3_16386),
inference(split_conjunct,[status(thm)],[360]) ).
cnf(1384,plain,
genls(c_tptpcol_9_72709,c_tptpcol_8_72708),
inference(split_conjunct,[status(thm)],[367]) ).
cnf(1401,plain,
genls(c_tptpcol_11_72774,c_tptpcol_10_72710),
inference(split_conjunct,[status(thm)],[374]) ).
fof(1414,plain,
! [X5,X11] :
( ~ disjointwith(X5,X11)
| disjointwith(X11,X5) ),
inference(fof_nnf,[status(thm)],[379]) ).
fof(1415,plain,
! [X12,X13] :
( ~ disjointwith(X12,X13)
| disjointwith(X13,X12) ),
inference(variable_rename,[status(thm)],[1414]) ).
cnf(1416,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
inference(split_conjunct,[status(thm)],[1415]) ).
cnf(1433,plain,
genls(c_tptpcol_3_65538,c_tptpcol_2_65537),
inference(split_conjunct,[status(thm)],[386]) ).
cnf(1447,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(split_conjunct,[status(thm)],[392]) ).
fof(1503,plain,
! [X7,X3,X8] :
( ~ disjointwith(X7,X3)
| ~ genls(X8,X7)
| disjointwith(X8,X3) ),
inference(fof_nnf,[status(thm)],[414]) ).
fof(1504,plain,
! [X9,X10,X11] :
( ~ disjointwith(X9,X10)
| ~ genls(X11,X9)
| disjointwith(X11,X10) ),
inference(variable_rename,[status(thm)],[1503]) ).
cnf(1505,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
inference(split_conjunct,[status(thm)],[1504]) ).
fof(1507,plain,
! [X2,X7,X8] :
( ~ disjointwith(X2,X7)
| ~ genls(X8,X7)
| disjointwith(X2,X8) ),
inference(fof_nnf,[status(thm)],[416]) ).
fof(1508,plain,
! [X9,X10,X11] :
( ~ disjointwith(X9,X10)
| ~ genls(X11,X10)
| disjointwith(X9,X11) ),
inference(variable_rename,[status(thm)],[1507]) ).
cnf(1509,plain,
( disjointwith(X1,X2)
| ~ genls(X2,X3)
| ~ disjointwith(X1,X3) ),
inference(split_conjunct,[status(thm)],[1508]) ).
fof(1783,negated_conjecture,
( mtvisible(c_tptp_member974_mt)
& ~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795) ),
inference(fof_nnf,[status(thm)],[531]) ).
cnf(1784,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_16_72795),
inference(split_conjunct,[status(thm)],[1783]) ).
cnf(1792,plain,
disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1),
inference(spm,[status(thm)],[1416,1447,theory(equality)]) ).
cnf(2223,plain,
( disjointwith(X1,c_tptpcol_16_72795)
| ~ disjointwith(X1,c_tptpcol_15_72793) ),
inference(spm,[status(thm)],[1509,972,theory(equality)]) ).
cnf(2245,plain,
( disjointwith(X1,c_tptpcol_3_16386)
| ~ disjointwith(X1,c_tptpcol_2_2) ),
inference(spm,[status(thm)],[1509,1144,theory(equality)]) ).
cnf(2249,plain,
( disjointwith(X1,c_tptpcol_7_21508)
| ~ disjointwith(X1,c_tptpcol_6_20484) ),
inference(spm,[status(thm)],[1509,646,theory(equality)]) ).
cnf(2250,plain,
( disjointwith(X1,c_tptpcol_6_20484)
| ~ disjointwith(X1,c_tptpcol_5_20483) ),
inference(spm,[status(thm)],[1509,1268,theory(equality)]) ).
cnf(2252,plain,
( disjointwith(X1,c_tptpcol_2_2)
| ~ disjointwith(X1,c_tptpcol_1_1) ),
inference(spm,[status(thm)],[1509,1293,theory(equality)]) ).
cnf(2267,plain,
( disjointwith(X1,c_tptpcol_5_20483)
| ~ disjointwith(X1,c_tptpcol_4_16387) ),
inference(spm,[status(thm)],[1509,881,theory(equality)]) ).
cnf(2271,plain,
( disjointwith(X1,c_tptpcol_3_65538)
| ~ disjointwith(X1,c_tptpcol_2_65537) ),
inference(spm,[status(thm)],[1509,1433,theory(equality)]) ).
cnf(2272,plain,
( disjointwith(X1,c_tptpcol_7_72707)
| ~ disjointwith(X1,c_tptpcol_6_71683) ),
inference(spm,[status(thm)],[1509,757,theory(equality)]) ).
cnf(2273,plain,
( disjointwith(X1,c_tptpcol_6_71683)
| ~ disjointwith(X1,c_tptpcol_5_69635) ),
inference(spm,[status(thm)],[1509,1332,theory(equality)]) ).
cnf(2281,plain,
( disjointwith(X1,c_tptpcol_15_72793)
| ~ disjointwith(X1,c_tptpcol_14_72792) ),
inference(spm,[status(thm)],[1509,911,theory(equality)]) ).
cnf(2283,plain,
( disjointwith(X1,c_tptpcol_10_72710)
| ~ disjointwith(X1,c_tptpcol_9_72709) ),
inference(spm,[status(thm)],[1509,847,theory(equality)]) ).
cnf(2284,plain,
( disjointwith(X1,c_tptpcol_9_72709)
| ~ disjointwith(X1,c_tptpcol_8_72708) ),
inference(spm,[status(thm)],[1509,1384,theory(equality)]) ).
cnf(2285,plain,
( disjointwith(X1,c_tptpcol_8_22020)
| ~ disjointwith(X1,c_tptpcol_7_21508) ),
inference(spm,[status(thm)],[1509,1096,theory(equality)]) ).
cnf(2286,plain,
( disjointwith(X1,c_tptpcol_12_72775)
| ~ disjointwith(X1,c_tptpcol_11_72774) ),
inference(spm,[status(thm)],[1509,964,theory(equality)]) ).
cnf(2287,plain,
( disjointwith(X1,c_tptpcol_13_72791)
| ~ disjointwith(X1,c_tptpcol_12_72775) ),
inference(spm,[status(thm)],[1509,883,theory(equality)]) ).
cnf(2288,plain,
( disjointwith(X1,c_tptpcol_14_72792)
| ~ disjointwith(X1,c_tptpcol_13_72791) ),
inference(spm,[status(thm)],[1509,916,theory(equality)]) ).
cnf(2289,plain,
( disjointwith(X1,c_tptpcol_11_72774)
| ~ disjointwith(X1,c_tptpcol_10_72710) ),
inference(spm,[status(thm)],[1509,1401,theory(equality)]) ).
cnf(2290,plain,
( disjointwith(X1,c_tptpcol_8_72708)
| ~ disjointwith(X1,c_tptpcol_7_72707) ),
inference(spm,[status(thm)],[1509,968,theory(equality)]) ).
cnf(2292,plain,
( disjointwith(X1,c_tptpcol_5_69635)
| ~ disjointwith(X1,c_tptpcol_4_65539) ),
inference(spm,[status(thm)],[1509,1267,theory(equality)]) ).
cnf(2298,plain,
( disjointwith(c_tptpcol_15_22076,X1)
| ~ disjointwith(c_tptpcol_14_22072,X1) ),
inference(spm,[status(thm)],[1505,554,theory(equality)]) ).
cnf(2301,plain,
( disjointwith(c_tptpcol_2_65537,X1)
| ~ disjointwith(c_tptpcol_1_65536,X1) ),
inference(spm,[status(thm)],[1505,545,theory(equality)]) ).
cnf(2305,plain,
( disjointwith(c_tptpcol_14_22072,X1)
| ~ disjointwith(c_tptpcol_13_22071,X1) ),
inference(spm,[status(thm)],[1505,661,theory(equality)]) ).
cnf(2314,plain,
( disjointwith(c_tptpcol_4_16387,X1)
| ~ disjointwith(c_tptpcol_3_16386,X1) ),
inference(spm,[status(thm)],[1505,1365,theory(equality)]) ).
cnf(2329,plain,
( disjointwith(c_tptpcol_13_22071,X1)
| ~ disjointwith(c_tptpcol_12_22055,X1) ),
inference(spm,[status(thm)],[1505,787,theory(equality)]) ).
cnf(2344,plain,
( disjointwith(c_tptpcol_12_22055,X1)
| ~ disjointwith(c_tptpcol_11_22023,X1) ),
inference(spm,[status(thm)],[1505,727,theory(equality)]) ).
cnf(2345,plain,
( disjointwith(c_tptpcol_11_22023,X1)
| ~ disjointwith(c_tptpcol_10_22022,X1) ),
inference(spm,[status(thm)],[1505,799,theory(equality)]) ).
cnf(2346,plain,
( disjointwith(c_tptpcol_4_65539,X1)
| ~ disjointwith(c_tptpcol_3_65538,X1) ),
inference(spm,[status(thm)],[1505,734,theory(equality)]) ).
cnf(2351,plain,
( disjointwith(c_tptpcol_10_22022,X1)
| ~ disjointwith(c_tptpcol_9_22021,X1) ),
inference(spm,[status(thm)],[1505,1227,theory(equality)]) ).
cnf(2370,plain,
( disjointwith(c_tptpcol_9_22021,X1)
| ~ disjointwith(c_tptpcol_8_22020,X1) ),
inference(spm,[status(thm)],[1505,1079,theory(equality)]) ).
cnf(3982,negated_conjecture,
~ disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(spm,[status(thm)],[1784,2223,theory(equality)]) ).
cnf(5377,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_6_71683)
| ~ disjointwith(c_tptpcol_14_22072,c_tptpcol_5_69635) ),
inference(spm,[status(thm)],[2273,2298,theory(equality)]) ).
cnf(5635,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707)
| ~ disjointwith(c_tptpcol_14_22072,c_tptpcol_5_69635) ),
inference(spm,[status(thm)],[2272,5377,theory(equality)]) ).
cnf(5727,plain,
( disjointwith(c_tptpcol_8_22020,X1)
| ~ disjointwith(X1,c_tptpcol_7_21508) ),
inference(spm,[status(thm)],[1416,2285,theory(equality)]) ).
cnf(5798,plain,
( disjointwith(X1,c_tptpcol_14_72792)
| ~ disjointwith(X1,c_tptpcol_12_72775) ),
inference(spm,[status(thm)],[2288,2287,theory(equality)]) ).
cnf(5813,plain,
( disjointwith(c_tptpcol_11_72774,X1)
| ~ disjointwith(X1,c_tptpcol_10_72710) ),
inference(spm,[status(thm)],[1416,2289,theory(equality)]) ).
cnf(5839,plain,
( disjointwith(c_tptpcol_8_72708,X1)
| ~ disjointwith(X1,c_tptpcol_7_72707) ),
inference(spm,[status(thm)],[1416,2290,theory(equality)]) ).
cnf(6201,plain,
( disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2)
| ~ disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1) ),
inference(spm,[status(thm)],[2301,2252,theory(equality)]) ).
cnf(6223,plain,
( disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2)
| $false ),
inference(rw,[status(thm)],[6201,1792,theory(equality)]) ).
cnf(6224,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_2_2),
inference(cn,[status(thm)],[6223,theory(equality)]) ).
cnf(6230,plain,
disjointwith(c_tptpcol_2_65537,c_tptpcol_3_16386),
inference(spm,[status(thm)],[2245,6224,theory(equality)]) ).
cnf(6240,plain,
disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537),
inference(spm,[status(thm)],[1416,6230,theory(equality)]) ).
cnf(6426,plain,
( disjointwith(c_tptpcol_14_22072,c_tptpcol_5_69635)
| ~ disjointwith(c_tptpcol_13_22071,c_tptpcol_4_65539) ),
inference(spm,[status(thm)],[2305,2292,theory(equality)]) ).
cnf(6909,plain,
( disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538)
| ~ disjointwith(c_tptpcol_3_16386,c_tptpcol_2_65537) ),
inference(spm,[status(thm)],[2314,2271,theory(equality)]) ).
cnf(6925,plain,
( disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538)
| $false ),
inference(rw,[status(thm)],[6909,6240,theory(equality)]) ).
cnf(6926,plain,
disjointwith(c_tptpcol_4_16387,c_tptpcol_3_65538),
inference(cn,[status(thm)],[6925,theory(equality)]) ).
cnf(6934,plain,
disjointwith(c_tptpcol_3_65538,c_tptpcol_4_16387),
inference(spm,[status(thm)],[1416,6926,theory(equality)]) ).
cnf(8932,plain,
( disjointwith(c_tptpcol_4_65539,c_tptpcol_5_20483)
| ~ disjointwith(c_tptpcol_3_65538,c_tptpcol_4_16387) ),
inference(spm,[status(thm)],[2346,2267,theory(equality)]) ).
cnf(8953,plain,
( disjointwith(c_tptpcol_4_65539,c_tptpcol_5_20483)
| $false ),
inference(rw,[status(thm)],[8932,6934,theory(equality)]) ).
cnf(8954,plain,
disjointwith(c_tptpcol_4_65539,c_tptpcol_5_20483),
inference(cn,[status(thm)],[8953,theory(equality)]) ).
cnf(9226,plain,
disjointwith(c_tptpcol_4_65539,c_tptpcol_6_20484),
inference(spm,[status(thm)],[2250,8954,theory(equality)]) ).
cnf(9491,plain,
disjointwith(c_tptpcol_4_65539,c_tptpcol_7_21508),
inference(spm,[status(thm)],[2249,9226,theory(equality)]) ).
cnf(22979,plain,
disjointwith(c_tptpcol_8_22020,c_tptpcol_4_65539),
inference(spm,[status(thm)],[5727,9491,theory(equality)]) ).
cnf(26938,plain,
disjointwith(c_tptpcol_9_22021,c_tptpcol_4_65539),
inference(spm,[status(thm)],[2370,22979,theory(equality)]) ).
cnf(30643,plain,
disjointwith(c_tptpcol_10_22022,c_tptpcol_4_65539),
inference(spm,[status(thm)],[2351,26938,theory(equality)]) ).
cnf(33716,plain,
disjointwith(c_tptpcol_11_22023,c_tptpcol_4_65539),
inference(spm,[status(thm)],[2345,30643,theory(equality)]) ).
cnf(36816,plain,
disjointwith(c_tptpcol_12_22055,c_tptpcol_4_65539),
inference(spm,[status(thm)],[2344,33716,theory(equality)]) ).
cnf(39792,plain,
disjointwith(c_tptpcol_13_22071,c_tptpcol_4_65539),
inference(spm,[status(thm)],[2329,36816,theory(equality)]) ).
cnf(41720,plain,
( disjointwith(c_tptpcol_14_22072,c_tptpcol_5_69635)
| $false ),
inference(rw,[status(thm)],[6426,39792,theory(equality)]) ).
cnf(41721,plain,
disjointwith(c_tptpcol_14_22072,c_tptpcol_5_69635),
inference(cn,[status(thm)],[41720,theory(equality)]) ).
cnf(41737,plain,
( disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707)
| $false ),
inference(rw,[status(thm)],[5635,41721,theory(equality)]) ).
cnf(41738,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_7_72707),
inference(cn,[status(thm)],[41737,theory(equality)]) ).
cnf(41797,plain,
disjointwith(c_tptpcol_8_72708,c_tptpcol_15_22076),
inference(spm,[status(thm)],[5839,41738,theory(equality)]) ).
cnf(41810,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_8_72708),
inference(spm,[status(thm)],[1416,41797,theory(equality)]) ).
cnf(41829,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_9_72709),
inference(spm,[status(thm)],[2284,41810,theory(equality)]) ).
cnf(41846,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_10_72710),
inference(spm,[status(thm)],[2283,41829,theory(equality)]) ).
cnf(41872,plain,
disjointwith(c_tptpcol_11_72774,c_tptpcol_15_22076),
inference(spm,[status(thm)],[5813,41846,theory(equality)]) ).
cnf(41885,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_11_72774),
inference(spm,[status(thm)],[1416,41872,theory(equality)]) ).
cnf(41896,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_12_72775),
inference(spm,[status(thm)],[2286,41885,theory(equality)]) ).
cnf(41919,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_14_72792),
inference(spm,[status(thm)],[5798,41896,theory(equality)]) ).
cnf(41952,plain,
disjointwith(c_tptpcol_15_22076,c_tptpcol_15_72793),
inference(spm,[status(thm)],[2281,41919,theory(equality)]) ).
cnf(41956,plain,
$false,
inference(sr,[status(thm)],[41952,3982,theory(equality)]) ).
cnf(41957,plain,
$false,
41956,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR036+3.p
% --creating new selector for [CSR002+2.ax]
% eprover: CPU time limit exceeded, terminating
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmpsxCYfn/sel_CSR036+3.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpsxCYfn/sel_CSR036+3.p_2 with time limit 80
% -prover status ResourceOut
% --creating new selector for [CSR002+2.ax]
% -running prover on /tmp/tmpsxCYfn/sel_CSR036+3.p_3 with time limit 74
% -prover status Theorem
% Problem CSR036+3.p solved in phase 2.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR036+3.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR036+3.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
%
%------------------------------------------------------------------------------