%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR039+5 : TPTP v5.0.0. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %s
% Computer : art05.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:38 EST 2010
% Result : Theorem 222.99s
% Output : CNFRefutation 228.72s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR039+5.p
% --creating new selector for [CSR002+4.ax]
% eprover: CPU time limit exceeded, terminating
% eprover: CPU time limit exceeded, terminating
% -running prover on /tmp/tmp1DAOuU/sel_CSR039+5.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmp1DAOuU/sel_CSR039+5.p_2 with time limit 51
% -prover status ResourceOut
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmp1DAOuU/sel_CSR039+5.p_3 with time limit 47
% -prover status Theorem
% Problem CSR039+5.p solved in phase 2.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR039+5.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR039+5.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(10, axiom,genls(c_tptpcol_5_16388,c_tptpcol_4_16387),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_148971)).
% fof(63, axiom,genls(c_tptpcol_14_93774,c_tptpcol_13_93766),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_170628)).
% fof(69, axiom,disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_140894)).
% fof(120, axiom,genls(c_tptpcol_2_2,c_tptpcol_1_1),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_261764)).
% fof(148, axiom,genls(c_tptpcol_9_18439,c_tptpcol_8_18438),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_147058)).
% fof(214, axiom,genls(c_tptpcol_3_16386,c_tptpcol_2_2),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_150165)).
% fof(222, axiom,genls(c_tptpcol_15_93775,c_tptpcol_14_93774),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_269943)).
% fof(230, axiom,genls(c_tptpcol_10_18567,c_tptpcol_9_18439),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_25138)).
% fof(328, axiom,genls(c_tptpcol_3_81921,c_tptpcol_2_65537),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_76715)).
% fof(369, axiom,genls(c_tptpcol_8_18438,c_tptpcol_7_18437),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_219531)).
% fof(416, axiom,genls(c_tptpcol_12_93765,c_tptpcol_11_93764),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_238394)).
% fof(460, axiom,genls(c_tptpcol_10_93700,c_tptpcol_9_93699),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_165193)).
% fof(464, axiom,genls(c_tptpcol_2_65537,c_tptpcol_1_65536),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_261490)).
% fof(485, axiom,genls(c_tptpcol_13_18664,c_tptpcol_12_18663),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_54760)).
% fof(504, axiom,genls(c_tptpcol_6_18436,c_tptpcol_5_16388),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_62685)).
% fof(532, axiom,genls(c_tptpcol_4_90113,c_tptpcol_3_81921),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_48340)).
% fof(682, axiom,genls(c_tptpcol_12_18663,c_tptpcol_11_18631),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_164914)).
% fof(719, axiom,genls(c_tptpcol_7_93186,c_tptpcol_6_92162),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_277557)).
% fof(748, axiom,genls(c_tptpcol_11_93764,c_tptpcol_10_93700),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_192138)).
% fof(871, axiom,genls(c_tptpcol_8_93698,c_tptpcol_7_93186),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_125562)).
% fof(910, axiom,genls(c_tptpcol_6_92162,c_tptpcol_5_90114),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_115368)).
% fof(1114, axiom,genls(c_tptpcol_9_93699,c_tptpcol_8_93698),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_67477)).
% fof(1307, axiom,genls(c_tptpcol_4_16387,c_tptpcol_3_16386),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_252194)).
% fof(1465, axiom,genls(c_tptpcol_7_18437,c_tptpcol_6_18436),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_131781)).
% fof(1570, axiom,![X2]:![X8]:(disjointwith(X2,X8)=>disjointwith(X8,X2)),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_540135)).
% fof(1572, axiom,![X4]:![X10]:![X5]:((disjointwith(X4,X10)&genls(X5,X4))=>disjointwith(X5,X10)),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_540137)).
% fof(1573, axiom,![X3]:![X4]:![X5]:((disjointwith(X3,X4)&genls(X5,X4))=>disjointwith(X3,X5)),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_540136)).
% fof(1640, axiom,genls(c_tptpcol_13_93766,c_tptpcol_12_93765),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_267151)).
% fof(1798, axiom,genls(c_tptpcol_5_90114,c_tptpcol_4_90113),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_317306)).
% fof(1859, axiom,genls(c_tptpcol_11_18631,c_tptpcol_10_18567),file('/tmp/tmp1DAOuU/sel_CSR039+5.p_3', ax4_127655)).
% fof(2129, 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/tmp1DAOuU/sel_CSR039+5.p_3', query239)).
% fof(2130, 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)],[2129])).
% cnf(2140,plain,(genls(c_tptpcol_5_16388,c_tptpcol_4_16387)),inference(split_conjunct,[status(thm)],[10])).
% cnf(2211,plain,(genls(c_tptpcol_14_93774,c_tptpcol_13_93766)),inference(split_conjunct,[status(thm)],[63])).
% cnf(2217,plain,(disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[69])).
% cnf(2272,plain,(genls(c_tptpcol_2_2,c_tptpcol_1_1)),inference(split_conjunct,[status(thm)],[120])).
% cnf(2306,plain,(genls(c_tptpcol_9_18439,c_tptpcol_8_18438)),inference(split_conjunct,[status(thm)],[148])).
% cnf(2393,plain,(genls(c_tptpcol_3_16386,c_tptpcol_2_2)),inference(split_conjunct,[status(thm)],[214])).
% cnf(2403,plain,(genls(c_tptpcol_15_93775,c_tptpcol_14_93774)),inference(split_conjunct,[status(thm)],[222])).
% cnf(2411,plain,(genls(c_tptpcol_10_18567,c_tptpcol_9_18439)),inference(split_conjunct,[status(thm)],[230])).
% cnf(2545,plain,(genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),inference(split_conjunct,[status(thm)],[328])).
% cnf(2603,plain,(genls(c_tptpcol_8_18438,c_tptpcol_7_18437)),inference(split_conjunct,[status(thm)],[369])).
% cnf(2670,plain,(genls(c_tptpcol_12_93765,c_tptpcol_11_93764)),inference(split_conjunct,[status(thm)],[416])).
% cnf(2720,plain,(genls(c_tptpcol_10_93700,c_tptpcol_9_93699)),inference(split_conjunct,[status(thm)],[460])).
% cnf(2724,plain,(genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[464])).
% cnf(2751,plain,(genls(c_tptpcol_13_18664,c_tptpcol_12_18663)),inference(split_conjunct,[status(thm)],[485])).
% cnf(2770,plain,(genls(c_tptpcol_6_18436,c_tptpcol_5_16388)),inference(split_conjunct,[status(thm)],[504])).
% cnf(2800,plain,(genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),inference(split_conjunct,[status(thm)],[532])).
% cnf(2978,plain,(genls(c_tptpcol_12_18663,c_tptpcol_11_18631)),inference(split_conjunct,[status(thm)],[682])).
% cnf(3019,plain,(genls(c_tptpcol_7_93186,c_tptpcol_6_92162)),inference(split_conjunct,[status(thm)],[719])).
% cnf(3054,plain,(genls(c_tptpcol_11_93764,c_tptpcol_10_93700)),inference(split_conjunct,[status(thm)],[748])).
% cnf(3206,plain,(genls(c_tptpcol_8_93698,c_tptpcol_7_93186)),inference(split_conjunct,[status(thm)],[871])).
% cnf(3247,plain,(genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),inference(split_conjunct,[status(thm)],[910])).
% cnf(3485,plain,(genls(c_tptpcol_9_93699,c_tptpcol_8_93698)),inference(split_conjunct,[status(thm)],[1114])).
% cnf(3730,plain,(genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),inference(split_conjunct,[status(thm)],[1307])).
% cnf(3910,plain,(genls(c_tptpcol_7_18437,c_tptpcol_6_18436)),inference(split_conjunct,[status(thm)],[1465])).
% fof(4037, plain,![X2]:![X8]:(~(disjointwith(X2,X8))|disjointwith(X8,X2)),inference(fof_nnf,[status(thm)],[1570])).
% fof(4038, plain,![X9]:![X10]:(~(disjointwith(X9,X10))|disjointwith(X10,X9)),inference(variable_rename,[status(thm)],[4037])).
% cnf(4039,plain,(disjointwith(X1,X2)|~disjointwith(X2,X1)),inference(split_conjunct,[status(thm)],[4038])).
% fof(4041, plain,![X4]:![X10]:![X5]:((~(disjointwith(X4,X10))|~(genls(X5,X4)))|disjointwith(X5,X10)),inference(fof_nnf,[status(thm)],[1572])).
% fof(4042, plain,![X11]:![X12]:![X13]:((~(disjointwith(X11,X12))|~(genls(X13,X11)))|disjointwith(X13,X12)),inference(variable_rename,[status(thm)],[4041])).
% cnf(4043,plain,(disjointwith(X1,X2)|~genls(X1,X3)|~disjointwith(X3,X2)),inference(split_conjunct,[status(thm)],[4042])).
% fof(4044, plain,![X3]:![X4]:![X5]:((~(disjointwith(X3,X4))|~(genls(X5,X4)))|disjointwith(X3,X5)),inference(fof_nnf,[status(thm)],[1573])).
% fof(4045, plain,![X6]:![X7]:![X8]:((~(disjointwith(X6,X7))|~(genls(X8,X7)))|disjointwith(X6,X8)),inference(variable_rename,[status(thm)],[4044])).
% cnf(4046,plain,(disjointwith(X1,X2)|~genls(X2,X3)|~disjointwith(X1,X3)),inference(split_conjunct,[status(thm)],[4045])).
% cnf(4147,plain,(genls(c_tptpcol_13_93766,c_tptpcol_12_93765)),inference(split_conjunct,[status(thm)],[1640])).
% cnf(4351,plain,(genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),inference(split_conjunct,[status(thm)],[1798])).
% cnf(4418,plain,(genls(c_tptpcol_11_18631,c_tptpcol_10_18567)),inference(split_conjunct,[status(thm)],[1859])).
% fof(4736, 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)],[2130])).
% cnf(4737,negated_conjecture,(~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),inference(split_conjunct,[status(thm)],[4736])).
% cnf(5045,plain,(disjointwith(X1,c_tptpcol_4_16387)|~disjointwith(X1,c_tptpcol_3_16386)),inference(spm,[status(thm)],[4046,3730,theory(equality)])).
% cnf(5047,plain,(disjointwith(X1,c_tptpcol_2_65537)|~disjointwith(X1,c_tptpcol_1_65536)),inference(spm,[status(thm)],[4046,2724,theory(equality)])).
% cnf(5067,plain,(disjointwith(X1,c_tptpcol_7_93186)|~disjointwith(X1,c_tptpcol_6_92162)),inference(spm,[status(thm)],[4046,3019,theory(equality)])).
% cnf(5068,plain,(disjointwith(X1,c_tptpcol_6_92162)|~disjointwith(X1,c_tptpcol_5_90114)),inference(spm,[status(thm)],[4046,3247,theory(equality)])).
% cnf(5072,plain,(disjointwith(X1,c_tptpcol_3_81921)|~disjointwith(X1,c_tptpcol_2_65537)),inference(spm,[status(thm)],[4046,2545,theory(equality)])).
% cnf(5074,plain,(disjointwith(X1,c_tptpcol_9_93699)|~disjointwith(X1,c_tptpcol_8_93698)),inference(spm,[status(thm)],[4046,3485,theory(equality)])).
% cnf(5075,plain,(disjointwith(X1,c_tptpcol_8_93698)|~disjointwith(X1,c_tptpcol_7_93186)),inference(spm,[status(thm)],[4046,3206,theory(equality)])).
% cnf(5078,plain,(disjointwith(X1,c_tptpcol_11_93764)|~disjointwith(X1,c_tptpcol_10_93700)),inference(spm,[status(thm)],[4046,3054,theory(equality)])).
% cnf(5080,plain,(disjointwith(X1,c_tptpcol_10_93700)|~disjointwith(X1,c_tptpcol_9_93699)),inference(spm,[status(thm)],[4046,2720,theory(equality)])).
% cnf(5084,plain,(disjointwith(X1,c_tptpcol_4_90113)|~disjointwith(X1,c_tptpcol_3_81921)),inference(spm,[status(thm)],[4046,2800,theory(equality)])).
% cnf(5093,plain,(disjointwith(c_tptpcol_15_93775,X1)|~disjointwith(c_tptpcol_14_93774,X1)),inference(spm,[status(thm)],[4043,2403,theory(equality)])).
% cnf(5095,plain,(disjointwith(c_tptpcol_13_18664,X1)|~disjointwith(c_tptpcol_12_18663,X1)),inference(spm,[status(thm)],[4043,2751,theory(equality)])).
% cnf(5096,plain,(disjointwith(c_tptpcol_5_16388,X1)|~disjointwith(c_tptpcol_4_16387,X1)),inference(spm,[status(thm)],[4043,2140,theory(equality)])).
% cnf(5102,plain,(disjointwith(c_tptpcol_14_93774,X1)|~disjointwith(c_tptpcol_13_93766,X1)),inference(spm,[status(thm)],[4043,2211,theory(equality)])).
% cnf(5103,plain,(disjointwith(c_tptpcol_13_93766,X1)|~disjointwith(c_tptpcol_12_93765,X1)),inference(spm,[status(thm)],[4043,4147,theory(equality)])).
% cnf(5104,plain,(disjointwith(c_tptpcol_11_18631,X1)|~disjointwith(c_tptpcol_10_18567,X1)),inference(spm,[status(thm)],[4043,4418,theory(equality)])).
% cnf(5108,plain,(disjointwith(c_tptpcol_2_2,X1)|~disjointwith(c_tptpcol_1_1,X1)),inference(spm,[status(thm)],[4043,2272,theory(equality)])).
% cnf(5110,plain,(disjointwith(c_tptpcol_9_18439,X1)|~disjointwith(c_tptpcol_8_18438,X1)),inference(spm,[status(thm)],[4043,2306,theory(equality)])).
% cnf(5111,plain,(disjointwith(c_tptpcol_8_18438,X1)|~disjointwith(c_tptpcol_7_18437,X1)),inference(spm,[status(thm)],[4043,2603,theory(equality)])).
% cnf(5117,plain,(disjointwith(c_tptpcol_3_16386,X1)|~disjointwith(c_tptpcol_2_2,X1)),inference(spm,[status(thm)],[4043,2393,theory(equality)])).
% cnf(5118,plain,(disjointwith(c_tptpcol_10_18567,X1)|~disjointwith(c_tptpcol_9_18439,X1)),inference(spm,[status(thm)],[4043,2411,theory(equality)])).
% cnf(5125,plain,(disjointwith(c_tptpcol_7_18437,X1)|~disjointwith(c_tptpcol_6_18436,X1)),inference(spm,[status(thm)],[4043,3910,theory(equality)])).
% cnf(5129,plain,(disjointwith(c_tptpcol_12_93765,X1)|~disjointwith(c_tptpcol_11_93764,X1)),inference(spm,[status(thm)],[4043,2670,theory(equality)])).
% cnf(5134,plain,(disjointwith(c_tptpcol_12_18663,X1)|~disjointwith(c_tptpcol_11_18631,X1)),inference(spm,[status(thm)],[4043,2978,theory(equality)])).
% cnf(5135,plain,(disjointwith(c_tptpcol_6_18436,X1)|~disjointwith(c_tptpcol_5_16388,X1)),inference(spm,[status(thm)],[4043,2770,theory(equality)])).
% cnf(5142,plain,(disjointwith(c_tptpcol_5_90114,X1)|~disjointwith(c_tptpcol_4_90113,X1)),inference(spm,[status(thm)],[4043,4351,theory(equality)])).
% cnf(13909,plain,(disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537)),inference(spm,[status(thm)],[5047,2217,theory(equality)])).
% cnf(14095,plain,(disjointwith(c_tptpcol_7_93186,X1)|~disjointwith(X1,c_tptpcol_6_92162)),inference(spm,[status(thm)],[4039,5067,theory(equality)])).
% cnf(14159,plain,(disjointwith(c_tptpcol_8_93698,X1)|~disjointwith(X1,c_tptpcol_7_93186)),inference(spm,[status(thm)],[4039,5075,theory(equality)])).
% cnf(14321,negated_conjecture,(~disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4737,5093,theory(equality)])).
% cnf(15199,plain,(disjointwith(c_tptpcol_2_2,c_tptpcol_3_81921)|~disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537)),inference(spm,[status(thm)],[5108,5072,theory(equality)])).
% cnf(15214,plain,(disjointwith(c_tptpcol_2_2,c_tptpcol_3_81921)|$false),inference(rw,[status(thm)],[15199,13909,theory(equality)])).
% cnf(15215,plain,(disjointwith(c_tptpcol_2_2,c_tptpcol_3_81921)),inference(cn,[status(thm)],[15214,theory(equality)])).
% cnf(15674,plain,(disjointwith(c_tptpcol_3_16386,c_tptpcol_4_90113)|~disjointwith(c_tptpcol_2_2,c_tptpcol_3_81921)),inference(spm,[status(thm)],[5117,5084,theory(equality)])).
% cnf(15692,plain,(disjointwith(c_tptpcol_3_16386,c_tptpcol_4_90113)|$false),inference(rw,[status(thm)],[15674,15215,theory(equality)])).
% cnf(15693,plain,(disjointwith(c_tptpcol_3_16386,c_tptpcol_4_90113)),inference(cn,[status(thm)],[15692,theory(equality)])).
% cnf(15731,plain,(disjointwith(c_tptpcol_4_90113,c_tptpcol_3_16386)),inference(spm,[status(thm)],[4039,15693,theory(equality)])).
% cnf(16614,plain,(disjointwith(c_tptpcol_13_18664,X1)|~disjointwith(c_tptpcol_11_18631,X1)),inference(spm,[status(thm)],[5095,5134,theory(equality)])).
% cnf(17039,plain,(disjointwith(c_tptpcol_5_90114,c_tptpcol_4_16387)|~disjointwith(c_tptpcol_4_90113,c_tptpcol_3_16386)),inference(spm,[status(thm)],[5142,5045,theory(equality)])).
% cnf(17063,plain,(disjointwith(c_tptpcol_5_90114,c_tptpcol_4_16387)|$false),inference(rw,[status(thm)],[17039,15731,theory(equality)])).
% cnf(17064,plain,(disjointwith(c_tptpcol_5_90114,c_tptpcol_4_16387)),inference(cn,[status(thm)],[17063,theory(equality)])).
% cnf(17196,plain,(disjointwith(c_tptpcol_4_16387,c_tptpcol_5_90114)),inference(spm,[status(thm)],[4039,17064,theory(equality)])).
% cnf(17216,plain,(disjointwith(c_tptpcol_4_16387,c_tptpcol_6_92162)),inference(spm,[status(thm)],[5068,17196,theory(equality)])).
% cnf(18594,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_6_92162)),inference(spm,[status(thm)],[5096,17216,theory(equality)])).
% cnf(21289,plain,(disjointwith(c_tptpcol_13_18664,c_tptpcol_11_93764)|~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(spm,[status(thm)],[5078,16614,theory(equality)])).
% cnf(21818,plain,(disjointwith(c_tptpcol_11_93764,c_tptpcol_13_18664)|~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(spm,[status(thm)],[4039,21289,theory(equality)])).
% cnf(22221,plain,(disjointwith(c_tptpcol_12_93765,c_tptpcol_13_18664)|~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(spm,[status(thm)],[5129,21818,theory(equality)])).
% cnf(22545,plain,(disjointwith(c_tptpcol_13_93766,c_tptpcol_13_18664)|~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(spm,[status(thm)],[5103,22221,theory(equality)])).
% cnf(22725,plain,(disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664)|~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(spm,[status(thm)],[5102,22545,theory(equality)])).
% cnf(22727,plain,(~disjointwith(c_tptpcol_11_18631,c_tptpcol_10_93700)),inference(sr,[status(thm)],[22725,14321,theory(equality)])).
% cnf(22728,plain,(~disjointwith(c_tptpcol_11_18631,c_tptpcol_9_93699)),inference(spm,[status(thm)],[22727,5080,theory(equality)])).
% cnf(28285,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_6_18436)|~disjointwith(c_tptpcol_5_16388,c_tptpcol_6_92162)),inference(spm,[status(thm)],[14095,5135,theory(equality)])).
% cnf(28312,plain,(disjointwith(c_tptpcol_7_9
% 3186,c_tptpcol_6_18436)|$false),inference(rw,[status(thm)],[28285,18594,theory(equality)])).
% cnf(28313,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_6_18436)),inference(cn,[status(thm)],[28312,theory(equality)])).
% cnf(28328,plain,(disjointwith(c_tptpcol_6_18436,c_tptpcol_7_93186)),inference(spm,[status(thm)],[4039,28313,theory(equality)])).
% cnf(28346,plain,(disjointwith(c_tptpcol_7_18437,c_tptpcol_7_93186)),inference(spm,[status(thm)],[5125,28328,theory(equality)])).
% cnf(28359,plain,(disjointwith(c_tptpcol_8_18438,c_tptpcol_7_93186)),inference(spm,[status(thm)],[5111,28346,theory(equality)])).
% cnf(28371,plain,(disjointwith(c_tptpcol_9_18439,c_tptpcol_7_93186)),inference(spm,[status(thm)],[5110,28359,theory(equality)])).
% cnf(28383,plain,(disjointwith(c_tptpcol_10_18567,c_tptpcol_7_93186)),inference(spm,[status(thm)],[5118,28371,theory(equality)])).
% cnf(28394,plain,(disjointwith(c_tptpcol_11_18631,c_tptpcol_7_93186)),inference(spm,[status(thm)],[5104,28383,theory(equality)])).
% cnf(30125,plain,(disjointwith(c_tptpcol_8_93698,c_tptpcol_11_18631)),inference(spm,[status(thm)],[14159,28394,theory(equality)])).
% cnf(30220,plain,(disjointwith(c_tptpcol_11_18631,c_tptpcol_8_93698)),inference(spm,[status(thm)],[4039,30125,theory(equality)])).
% cnf(30354,plain,(disjointwith(c_tptpcol_11_18631,c_tptpcol_9_93699)),inference(spm,[status(thm)],[5074,30220,theory(equality)])).
% cnf(30358,plain,($false),inference(sr,[status(thm)],[30354,22728,theory(equality)])).
% cnf(30359,plain,($false),30358,['proof']).
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------