%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR039+2 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %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 : Tue Dec 28 23:10:48 EST 2010
% Result : Theorem 123.35s
% Output : Solution 123.35s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP12506/CSR039+2.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP12506/CSR039+2.tptp
% SZS output start Solution for /tmp/SystemOnTPTP12506/CSR039+2.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 12674
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.92 CPU 2.02 WC
% PrfWatch: 3.92 CPU 4.03 WC
% PrfWatch: 5.91 CPU 6.03 WC
% # Preprocessing time : 0.080 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:(disjointwith(X1,X2)=>disjointwith(X2,X1)),file('/tmp/SRASS.s.p', ax1_1120)).
% fof(4, axiom,![X6]:![X7]:![X8]:((disjointwith(X6,X7)&genls(X8,X7))=>disjointwith(X6,X8)),file('/tmp/SRASS.s.p', ax1_1121)).
% fof(5, axiom,![X7]:![X9]:![X8]:((disjointwith(X7,X9)&genls(X8,X7))=>disjointwith(X8,X9)),file('/tmp/SRASS.s.p', ax1_1122)).
% fof(19, axiom,![X1]:![X2]:![X12]:((genls(X1,X2)&genls(X2,X12))=>genls(X1,X12)),file('/tmp/SRASS.s.p', ax1_1109)).
% fof(36, axiom,genls(c_tptpcol_15_93775,c_tptpcol_14_93774),file('/tmp/SRASS.s.p', ax1_182)).
% fof(37, axiom,genls(c_tptpcol_13_18664,c_tptpcol_12_18663),file('/tmp/SRASS.s.p', ax1_208)).
% fof(47, axiom,genls(c_tptpcol_12_18663,c_tptpcol_11_18631),file('/tmp/SRASS.s.p', ax1_109)).
% fof(48, axiom,disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),file('/tmp/SRASS.s.p', ax1_152)).
% fof(51, axiom,genls(c_tptpcol_14_93774,c_tptpcol_13_93766),file('/tmp/SRASS.s.p', ax1_191)).
% fof(250, axiom,genls(c_tptpcol_2_2,c_tptpcol_1_1),file('/tmp/SRASS.s.p', ax1_145)).
% fof(313, axiom,genls(c_tptpcol_2_65537,c_tptpcol_1_65536),file('/tmp/SRASS.s.p', ax1_348)).
% fof(492, axiom,genls(c_tptpcol_7_93186,c_tptpcol_6_92162),file('/tmp/SRASS.s.p', ax1_14)).
% fof(495, axiom,genls(c_tptpcol_5_16388,c_tptpcol_4_16387),file('/tmp/SRASS.s.p', ax1_23)).
% fof(500, axiom,genls(c_tptpcol_3_81921,c_tptpcol_2_65537),file('/tmp/SRASS.s.p', ax1_41)).
% fof(501, axiom,genls(c_tptpcol_10_18567,c_tptpcol_9_18439),file('/tmp/SRASS.s.p', ax1_43)).
% fof(506, axiom,genls(c_tptpcol_12_93765,c_tptpcol_11_93764),file('/tmp/SRASS.s.p', ax1_72)).
% fof(509, axiom,genls(c_tptpcol_13_93766,c_tptpcol_12_93765),file('/tmp/SRASS.s.p', ax1_78)).
% fof(525, axiom,genls(c_tptpcol_11_18631,c_tptpcol_10_18567),file('/tmp/SRASS.s.p', ax1_175)).
% fof(544, axiom,genls(c_tptpcol_9_18439,c_tptpcol_8_18438),file('/tmp/SRASS.s.p', ax1_255)).
% fof(552, axiom,genls(c_tptpcol_4_16387,c_tptpcol_3_16386),file('/tmp/SRASS.s.p', ax1_285)).
% fof(565, axiom,genls(c_tptpcol_8_93698,c_tptpcol_7_93186),file('/tmp/SRASS.s.p', ax1_345)).
% fof(566, axiom,genls(c_tptpcol_6_18436,c_tptpcol_5_16388),file('/tmp/SRASS.s.p', ax1_351)).
% fof(567, axiom,genls(c_tptpcol_8_18438,c_tptpcol_7_18437),file('/tmp/SRASS.s.p', ax1_353)).
% fof(572, axiom,genls(c_tptpcol_9_93699,c_tptpcol_8_93698),file('/tmp/SRASS.s.p', ax1_370)).
% fof(573, axiom,genls(c_tptpcol_11_93764,c_tptpcol_10_93700),file('/tmp/SRASS.s.p', ax1_372)).
% fof(575, axiom,genls(c_tptpcol_4_90113,c_tptpcol_3_81921),file('/tmp/SRASS.s.p', ax1_376)).
% fof(576, axiom,genls(c_tptpcol_10_93700,c_tptpcol_9_93699),file('/tmp/SRASS.s.p', ax1_379)).
% fof(578, axiom,genls(c_tptpcol_3_16386,c_tptpcol_2_2),file('/tmp/SRASS.s.p', ax1_385)).
% fof(588, axiom,genls(c_tptpcol_6_92162,c_tptpcol_5_90114),file('/tmp/SRASS.s.p', ax1_417)).
% fof(605, axiom,genls(c_tptpcol_5_90114,c_tptpcol_4_90113),file('/tmp/SRASS.s.p', ax1_476)).
% fof(607, axiom,genls(c_tptpcol_7_18437,c_tptpcol_6_18436),file('/tmp/SRASS.s.p', ax1_483)).
% fof(1132, 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/SRASS.s.p', query89)).
% fof(1133, 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)],[1132])).
% fof(1137, plain,![X1]:![X2]:(~(disjointwith(X1,X2))|disjointwith(X2,X1)),inference(fof_nnf,[status(thm)],[1])).
% fof(1138, plain,![X3]:![X4]:(~(disjointwith(X3,X4))|disjointwith(X4,X3)),inference(variable_rename,[status(thm)],[1137])).
% cnf(1139,plain,(disjointwith(X1,X2)|~disjointwith(X2,X1)),inference(split_conjunct,[status(thm)],[1138])).
% fof(1144, plain,![X6]:![X7]:![X8]:((~(disjointwith(X6,X7))|~(genls(X8,X7)))|disjointwith(X6,X8)),inference(fof_nnf,[status(thm)],[4])).
% fof(1145, plain,![X9]:![X10]:![X11]:((~(disjointwith(X9,X10))|~(genls(X11,X10)))|disjointwith(X9,X11)),inference(variable_rename,[status(thm)],[1144])).
% cnf(1146,plain,(disjointwith(X1,X2)|~genls(X2,X3)|~disjointwith(X1,X3)),inference(split_conjunct,[status(thm)],[1145])).
% fof(1147, plain,![X7]:![X9]:![X8]:((~(disjointwith(X7,X9))|~(genls(X8,X7)))|disjointwith(X8,X9)),inference(fof_nnf,[status(thm)],[5])).
% fof(1148, plain,![X10]:![X11]:![X12]:((~(disjointwith(X10,X11))|~(genls(X12,X10)))|disjointwith(X12,X11)),inference(variable_rename,[status(thm)],[1147])).
% cnf(1149,plain,(disjointwith(X1,X2)|~genls(X1,X3)|~disjointwith(X3,X2)),inference(split_conjunct,[status(thm)],[1148])).
% fof(1181, plain,![X1]:![X2]:![X12]:((~(genls(X1,X2))|~(genls(X2,X12)))|genls(X1,X12)),inference(fof_nnf,[status(thm)],[19])).
% fof(1182, plain,![X13]:![X14]:![X15]:((~(genls(X13,X14))|~(genls(X14,X15)))|genls(X13,X15)),inference(variable_rename,[status(thm)],[1181])).
% cnf(1183,plain,(genls(X1,X2)|~genls(X3,X2)|~genls(X1,X3)),inference(split_conjunct,[status(thm)],[1182])).
% cnf(1218,plain,(genls(c_tptpcol_15_93775,c_tptpcol_14_93774)),inference(split_conjunct,[status(thm)],[36])).
% cnf(1219,plain,(genls(c_tptpcol_13_18664,c_tptpcol_12_18663)),inference(split_conjunct,[status(thm)],[37])).
% cnf(1232,plain,(genls(c_tptpcol_12_18663,c_tptpcol_11_18631)),inference(split_conjunct,[status(thm)],[47])).
% cnf(1233,plain,(disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[48])).
% cnf(1236,plain,(genls(c_tptpcol_14_93774,c_tptpcol_13_93766)),inference(split_conjunct,[status(thm)],[51])).
% cnf(1730,plain,(genls(c_tptpcol_2_2,c_tptpcol_1_1)),inference(split_conjunct,[status(thm)],[250])).
% cnf(1881,plain,(genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[313])).
% cnf(2268,plain,(genls(c_tptpcol_7_93186,c_tptpcol_6_92162)),inference(split_conjunct,[status(thm)],[492])).
% cnf(2271,plain,(genls(c_tptpcol_5_16388,c_tptpcol_4_16387)),inference(split_conjunct,[status(thm)],[495])).
% cnf(2276,plain,(genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),inference(split_conjunct,[status(thm)],[500])).
% cnf(2277,plain,(genls(c_tptpcol_10_18567,c_tptpcol_9_18439)),inference(split_conjunct,[status(thm)],[501])).
% cnf(2282,plain,(genls(c_tptpcol_12_93765,c_tptpcol_11_93764)),inference(split_conjunct,[status(thm)],[506])).
% cnf(2285,plain,(genls(c_tptpcol_13_93766,c_tptpcol_12_93765)),inference(split_conjunct,[status(thm)],[509])).
% cnf(2301,plain,(genls(c_tptpcol_11_18631,c_tptpcol_10_18567)),inference(split_conjunct,[status(thm)],[525])).
% cnf(2320,plain,(genls(c_tptpcol_9_18439,c_tptpcol_8_18438)),inference(split_conjunct,[status(thm)],[544])).
% cnf(2328,plain,(genls(c_tptpcol_4_16387,c_tptpcol_3_16386)),inference(split_conjunct,[status(thm)],[552])).
% cnf(2341,plain,(genls(c_tptpcol_8_93698,c_tptpcol_7_93186)),inference(split_conjunct,[status(thm)],[565])).
% cnf(2342,plain,(genls(c_tptpcol_6_18436,c_tptpcol_5_16388)),inference(split_conjunct,[status(thm)],[566])).
% cnf(2343,plain,(genls(c_tptpcol_8_18438,c_tptpcol_7_18437)),inference(split_conjunct,[status(thm)],[567])).
% cnf(2348,plain,(genls(c_tptpcol_9_93699,c_tptpcol_8_93698)),inference(split_conjunct,[status(thm)],[572])).
% cnf(2349,plain,(genls(c_tptpcol_11_93764,c_tptpcol_10_93700)),inference(split_conjunct,[status(thm)],[573])).
% cnf(2351,plain,(genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),inference(split_conjunct,[status(thm)],[575])).
% cnf(2352,plain,(genls(c_tptpcol_10_93700,c_tptpcol_9_93699)),inference(split_conjunct,[status(thm)],[576])).
% cnf(2354,plain,(genls(c_tptpcol_3_16386,c_tptpcol_2_2)),inference(split_conjunct,[status(thm)],[578])).
% cnf(2364,plain,(genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),inference(split_conjunct,[status(thm)],[588])).
% cnf(2381,plain,(genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),inference(split_conjunct,[status(thm)],[605])).
% cnf(2383,plain,(genls(c_tptpcol_7_18437,c_tptpcol_6_18436)),inference(split_conjunct,[status(thm)],[607])).
% fof(3864, 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)],[1133])).
% cnf(3865,negated_conjecture,(~disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),inference(split_conjunct,[status(thm)],[3864])).
% cnf(4495,plain,(disjointwith(c_tptpcol_4_90113,X1)|~disjointwith(c_tptpcol_3_81921,X1)),inference(spm,[status(thm)],[1149,2351,theory(equality)])).
% cnf(4496,plain,(disjointwith(c_tptpcol_10_93700,X1)|~disjointwith(c_tptpcol_9_93699,X1)),inference(spm,[status(thm)],[1149,2352,theory(equality)])).
% cnf(4497,plain,(disjointwith(c_tptpcol_9_93699,X1)|~disjointwith(c_tptpcol_8_93698,X1)),inference(spm,[status(thm)],[1149,2348,theory(equality)])).
% cnf(4501,plain,(disjointwith(c_tptpcol_6_18436,X1)|~disjointwith(c_tptpcol_5_16388,X1)),inference(spm,[status(thm)],[1149,2342,theory(equality)])).
% cnf(4502,plain,(disjointwith(c_tptpcol_8_93698,X1)|~disjointwith(c_tptpcol_7_93186,X1)),inference(spm,[status(thm)],[1149,2341,theory(equality)])).
% cnf(4531,plain,(disjointwith(c_tptpcol_3_16386,X1)|~disjointwith(c_tptpcol_2_2,X1)),inference(spm,[status(thm)],[1149,2354,theory(equality)])).
% cnf(4567,plain,(disjointwith(c_tptpcol_11_93764,X1)|~disjointwith(c_tptpcol_10_93700,X1)),inference(spm,[status(thm)],[1149,2349,theory(equality)])).
% cnf(4568,plain,(disjointwith(c_tptpcol_12_93765,X1)|~disjointwith(c_tptpcol_11_93764,X1)),inference(spm,[status(thm)],[1149,2282,theory(equality)])).
% cnf(4600,plain,(disjointwith(c_tptpcol_2_2,X1)|~disjointwith(c_tptpcol_1_1,X1)),inference(spm,[status(thm)],[1149,1730,theory(equality)])).
% cnf(4612,plain,(disjointwith(c_tptpcol_13_93766,X1)|~disjointwith(c_tptpcol_12_93765,X1)),inference(spm,[status(thm)],[1149,2285,theory(equality)])).
% cnf(4619,plain,(disjointwith(c_tptpcol_14_93774,X1)|~disjointwith(c_tptpcol_13_93766,X1)),inference(spm,[status(thm)],[1149,1236,theory(equality)])).
% cnf(4620,plain,(disjointwith(c_tptpcol_15_93775,X1)|~disjointwith(c_tptpcol_14_93774,X1)),inference(spm,[status(thm)],[1149,1218,theory(equality)])).
% cnf(4634,plain,(disjointwith(X1,c_tptpcol_5_90114)|~disjointwith(X1,c_tptpcol_4_90113)),inference(spm,[status(thm)],[1146,2381,theory(equality)])).
% cnf(4647,plain,(disjointwith(X1,c_tptpcol_7_18437)|~disjointwith(X1,c_tptpcol_6_18436)),inference(spm,[status(thm)],[1146,2383,theory(equality)])).
% cnf(4670,plain,(disjointwith(X1,c_tptpcol_8_18438)|~disjointwith(X1,c_tptpcol_7_18437)),inference(spm,[status(thm)],[1146,2343,theory(equality)])).
% cnf(4721,plain,(disjointwith(X1,c_tptpcol_9_18439)|~disjointwith(X1,c_tptpcol_8_18438)),inference(spm,[status(thm)],[1146,2320,theory(equality)])).
% cnf(4722,plain,(disjointwith(X1,c_tptpcol_10_18567)|~disjointwith(X1,c_tptpcol_9_18439)),inference(spm,[status(thm)],[1146,2277,theory(equality)])).
% cnf(4730,plain,(disjointwith(X1,c_tptpcol_4_16387)|~disjointwith(X1,c_tptpcol_3_16386)),inference(spm,[status(thm)],[1146,2328,theory(equality)])).
% cnf(4731,plain,(disjointwith(X1,c_tptpcol_5_16388)|~disjointwith(X1,c_tptpcol_4_16387)),inference(spm,[status(thm)],[1146,2271,theory(equality)])).
% cnf(4736,plain,(disjointwith(X1,c_tptpcol_6_92162)|~disjointwith(X1,c_tptpcol_5_90114)),inference(spm,[status(thm)],[1146,2364,theory(equality)])).
% cnf(4737,plain,(disjointwith(X1,c_tptpcol_7_93186)|~disjointwith(X1,c_tptpcol_6_92162)),inference(spm,[status(thm)],[1146,2268,theory(equality)])).
% cnf(4763,plain,(disjointwith(X1,c_tptpcol_11_18631)|~disjointwith(X1,c_tptpcol_10_18567)),inference(spm,[status(thm)],[1146,2301,theory(equality)])).
% cnf(4765,plain,(disjointwith(X1,c_tptpcol_12_18663)|~disjointwith(X1,c_tptpcol_11_18631)),inference(spm,[status(thm)],[1146,1232,theory(equality)])).
% cnf(4768,plain,(disjointwith(X1,c_tptpcol_13_18664)|~disjointwith(X1,c_tptpcol_12_18663)),inference(spm,[status(thm)],[1146,1219,theory(equality)])).
% cnf(5547,plain,(genls(X1,c_tptpcol_1_65536)|~genls(X1,c_tptpcol_2_65537)),inference(spm,[status(thm)],[1183,1881,theory(equality)])).
% cnf(8758,plain,(disjointwith(X1,c_tptpcol_4_90113)|~disjointwith(c_tptpcol_3_81921,X1)),inference(spm,[status(thm)],[1139,4495,theory(equality)])).
% cnf(8792,plain,(disjointwith(c_tptpcol_10_93700,X1)|~disjointwith(c_tptpcol_8_93698,X1)),inference(spm,[status(thm)],[4496,4497,theory(equality)])).
% cnf(8851,plain,(disjointwith(X1,c_tptpcol_6_18436)|~disjointwith(c_tptpcol_5_16388,X1)),inference(spm,[status(thm)],[1139,4501,theory(equality)])).
% cnf(9392,plain,(disjointwith(c_tptpcol_8_93698,c_tptpcol_13_18664)|~disjointwith(c_tptpcol_7_93186,c_tptpcol_12_18663)),inference(spm,[status(thm)],[4768,4502,theory(equality)])).
% cnf(12300,plain,(disjointwith(c_tptpcol_3_16386,X1)|~disjointwith(c_tptpcol_1_1,X1)),inference(spm,[status(thm)],[4531,4600,theory(equality)])).
% cnf(39420,plain,(disjointwith(c_tptpcol_3_16386,c_tptpcol_1_65536)),inference(spm,[status(thm)],[12300,1233,theory(equality)])).
% cnf(39435,plain,(disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386)),inference(spm,[status(thm)],[1139,39420,theory(equality)])).
% cnf(43155,plain,(genls(c_tptpcol_3_81921,c_tptpcol_1_65536)),inference(spm,[status(thm)],[5547,2276,theory(equality)])).
% cnf(43230,plain,(disjointwith(c_tptpcol_3_81921,X1)|~disjointwith(c_tptpcol_1_65536,X1)),inference(spm,[status(thm)],[1149,43155,theory(equality)])).
% cnf(67590,plain,(disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)|~disjointwith(c_tptpcol_1_65536,c_tptpcol_3_16386)),inference(spm,[status(thm)],[4730,43230,theory(equality)])).
% cnf(67731,plain,(disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)|$false),inference(rw,[status(thm)],[67590,39435,theory(equality)])).
% cnf(67732,plain,(disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)),inference(cn,[status(thm)],[67731,theory(equality)])).
% cnf(88047,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113)|~disjointwith(c_tptpcol_3_81921,c_tptpcol_4_16387)),inference(spm,[status(thm)],[8758,4731,theory(equality)])).
% cnf(88074,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113)|$false),inference(rw,[status(thm)],[88047,67732,theory(equality)])).
% cnf(88075,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_4_90113)),inference(cn,[status(thm)],[88074,theory(equality)])).
% cnf(88678,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_5_90114)),inference(spm,[status(thm)],[4634,88075,theory(equality)])).
% cnf(89235,plain,(disjointwith(c_tptpcol_5_16388,c_tptpcol_6_92162)),inference(spm,[status(thm)],[4736,88678,theory(equality)])).
% cnf(91050,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_6_18436)|~disjointwith(c_tptpcol_5_16388,c_tptpcol_6_92162)),inference(spm,[status(thm)],[8851,4737,theory(equality)])).
% cnf(91081,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_6_18436)|$false),inference(rw,[status(thm)],[91050,89235,theory(equality)])).
% cnf(91082,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_6_18436)),inference(cn,[status(thm)],[91081,theory(equality)])).
% cnf(92928,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_7_18437)),inference(spm,[status(thm)],[4647,91082,theory(equality)])).
% cnf(94536,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_8_18438)),inference(spm,[status(thm)],[4670,92928,theory(equality)])).
% cnf(96949,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_9_18439)),inference(spm,[status(thm)],[4721,94536,theory(equality)])).
% cnf(99673,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_10_18567)),inference(spm,[status(thm)],[4722,96949,theory(equality)])).
% cnf(103924,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_11_18631)),inference(spm,[status(thm)],[4763,99673,theory(equality)])).
% cnf(109746,plain,(disjointwith(c_tptpcol_7_93186,c_tptpcol_12_18663)),inference(spm,[status(thm)],[4765,103924,theory(equality)])).
% cnf(109758,plain,(disjointwith(c_tptpcol_8_93698,c_tptpcol_13_18664)|$false),inference(rw,[status(thm)],[9392,109746,theory(equality)])).
% cnf(109759,plain,(disjointwith(c_tptpcol_8_93698,c_tptpcol_13_18664)),inference(cn,[status(thm)],[109758,theory(equality)])).
% cnf(109783,plain,(disjointwith(c_tptpcol_10_93700,c_tptpcol_13_18664)),inference(spm,[status(thm)],[8792,109759,theory(equality)])).
% cnf(109805,plain,(disjointwith(c_tptpcol_11_93764,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4567,109783,theory(equality)])).
% cnf(109919,plain,(disjointwith(c_tptpcol_12_93765,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4568,109805,theory(equality)])).
% cnf(109942,plain,(disjointwith(c_tptpcol_13_93766,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4612,109919,theory(equality)])).
% cnf(109958,plain,(disjointwith(c_tptpcol_14_93774,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4619,109942,theory(equality)])).
% cnf(109965,plain,(disjointwith(c_tptpcol_15_93775,c_tptpcol_13_18664)),inference(spm,[status(thm)],[4620,109958,theory(equality)])).
% cnf(109968,plain,($false),inference(sr,[status(thm)],[109965,3865,theory(equality)])).
% cnf(109969,plain,($false),109968,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 13799
% # ...of these trivial : 1329
% # ...subsumed : 2865
% # ...remaining for further processing: 9605
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 6
% # Backward-rewritten : 11
% # Generated clauses : 88984
% # ...of the previous two non-trivial : 76441
% # Contextual simplify-reflections : 1
% # Paramodulations : 88984
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 9588
% # Positive orientable unit clauses: 4396
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1887
% # Non-unit-clauses : 3305
% # Current number of unprocessed clauses: 63753
% # ...number of literals in the above : 123922
% # Clause-clause subsumption calls (NU) : 2243175
% # Rec. Clause-clause subsumption calls : 2216026
% # Unit Clause-clause subsumption calls : 1331981
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 13
% # Indexed BW rewrite successes : 10
% # Backwards rewriting index: 9225 leaves, 1.01+/-0.174 terms/leaf
% # Paramod-from index: 5490 leaves, 1.00+/-0.036 terms/leaf
% # Paramod-into index: 8362 leaves, 1.01+/-0.149 terms/leaf
% # -------------------------------------------------
% # User time : 6.128 s
% # System time : 0.110 s
% # Total time : 6.238 s
% # Maximum resident set size: 0 pages
% PrfWatch: 7.36 CPU 7.48 WC
% FINAL PrfWatch: 7.36 CPU 7.48 WC
% SZS output end Solution for /tmp/SystemOnTPTP12506/CSR039+2.tptp
%
%------------------------------------------------------------------------------