%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : CSR049+1 : TPTP v5.0.0. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art11.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 3.00GHz @ 3000MHz
% Memory : 2006MB
% OS : Linux 2.6.31.5-127.fc12.i686.PAE
% CPULimit : 300s
% DateTime : Tue Dec 28 23:33:49 EST 2010
% Result : Theorem 2.27s
% Output : Solution 2.27s
% 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/SystemOnTPTP27142/CSR049+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP27142/CSR049+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP27142/CSR049+1.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 27274
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.021 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', just84)).
% fof(3, axiom,![X6]:![X7]:![X8]:((disjointwith(X6,X7)&genls(X8,X7))=>disjointwith(X6,X8)),file('/tmp/SRASS.s.p', just85)).
% fof(4, axiom,![X7]:![X9]:![X8]:((disjointwith(X7,X9)&genls(X8,X7))=>disjointwith(X8,X9)),file('/tmp/SRASS.s.p', just86)).
% fof(18, axiom,genls(c_tptpcol_16_26926,c_tptpcol_15_26925),file('/tmp/SRASS.s.p', just35)).
% fof(19, axiom,genls(c_tptpcol_16_92269,c_tptpcol_15_92268),file('/tmp/SRASS.s.p', just65)).
% fof(22, axiom,disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),file('/tmp/SRASS.s.p', just67)).
% fof(23, axiom,genls(c_tptpcol_15_26925,c_tptpcol_14_26921),file('/tmp/SRASS.s.p', just33)).
% fof(24, axiom,genls(c_tptpcol_15_92268,c_tptpcol_14_92264),file('/tmp/SRASS.s.p', just63)).
% fof(52, axiom,genls(c_tptpcol_2_2,c_tptpcol_1_1),file('/tmp/SRASS.s.p', just7)).
% fof(53, axiom,genls(c_tptpcol_2_65537,c_tptpcol_1_65536),file('/tmp/SRASS.s.p', just37)).
% fof(81, axiom,genls(c_tptpcol_3_16386,c_tptpcol_2_2),file('/tmp/SRASS.s.p', just9)).
% fof(82, axiom,genls(c_tptpcol_4_24578,c_tptpcol_3_16386),file('/tmp/SRASS.s.p', just11)).
% fof(83, axiom,genls(c_tptpcol_5_24579,c_tptpcol_4_24578),file('/tmp/SRASS.s.p', just13)).
% fof(84, axiom,genls(c_tptpcol_6_26627,c_tptpcol_5_24579),file('/tmp/SRASS.s.p', just15)).
% fof(85, axiom,genls(c_tptpcol_7_26628,c_tptpcol_6_26627),file('/tmp/SRASS.s.p', just17)).
% fof(86, axiom,genls(c_tptpcol_8_26629,c_tptpcol_7_26628),file('/tmp/SRASS.s.p', just19)).
% fof(87, axiom,genls(c_tptpcol_9_26885,c_tptpcol_8_26629),file('/tmp/SRASS.s.p', just21)).
% fof(88, axiom,genls(c_tptpcol_10_26886,c_tptpcol_9_26885),file('/tmp/SRASS.s.p', just23)).
% fof(89, axiom,genls(c_tptpcol_11_26887,c_tptpcol_10_26886),file('/tmp/SRASS.s.p', just25)).
% fof(90, axiom,genls(c_tptpcol_12_26919,c_tptpcol_11_26887),file('/tmp/SRASS.s.p', just27)).
% fof(91, axiom,genls(c_tptpcol_13_26920,c_tptpcol_12_26919),file('/tmp/SRASS.s.p', just29)).
% fof(92, axiom,genls(c_tptpcol_14_26921,c_tptpcol_13_26920),file('/tmp/SRASS.s.p', just31)).
% fof(93, axiom,genls(c_tptpcol_3_81921,c_tptpcol_2_65537),file('/tmp/SRASS.s.p', just39)).
% fof(94, axiom,genls(c_tptpcol_4_90113,c_tptpcol_3_81921),file('/tmp/SRASS.s.p', just41)).
% fof(95, axiom,genls(c_tptpcol_5_90114,c_tptpcol_4_90113),file('/tmp/SRASS.s.p', just43)).
% fof(96, axiom,genls(c_tptpcol_6_92162,c_tptpcol_5_90114),file('/tmp/SRASS.s.p', just45)).
% fof(97, axiom,genls(c_tptpcol_7_92163,c_tptpcol_6_92162),file('/tmp/SRASS.s.p', just47)).
% fof(98, axiom,genls(c_tptpcol_8_92164,c_tptpcol_7_92163),file('/tmp/SRASS.s.p', just49)).
% fof(99, axiom,genls(c_tptpcol_9_92165,c_tptpcol_8_92164),file('/tmp/SRASS.s.p', just51)).
% fof(100, axiom,genls(c_tptpcol_10_92166,c_tptpcol_9_92165),file('/tmp/SRASS.s.p', just53)).
% fof(101, axiom,genls(c_tptpcol_11_92230,c_tptpcol_10_92166),file('/tmp/SRASS.s.p', just55)).
% fof(102, axiom,genls(c_tptpcol_12_92262,c_tptpcol_11_92230),file('/tmp/SRASS.s.p', just57)).
% fof(103, axiom,genls(c_tptpcol_13_92263,c_tptpcol_12_92262),file('/tmp/SRASS.s.p', just59)).
% fof(104, axiom,genls(c_tptpcol_14_92264,c_tptpcol_13_92263),file('/tmp/SRASS.s.p', just61)).
% fof(177, conjecture,(mtvisible(c_unitedstatesgeographypeoplemt)=>disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),file('/tmp/SRASS.s.p', query49)).
% fof(178, negated_conjecture,~((mtvisible(c_unitedstatesgeographypeoplemt)=>disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269))),inference(assume_negation,[status(cth)],[177])).
% fof(179, plain,![X1]:![X2]:(~(disjointwith(X1,X2))|disjointwith(X2,X1)),inference(fof_nnf,[status(thm)],[1])).
% fof(180, plain,![X3]:![X4]:(~(disjointwith(X3,X4))|disjointwith(X4,X3)),inference(variable_rename,[status(thm)],[179])).
% cnf(181,plain,(disjointwith(X1,X2)|~disjointwith(X2,X1)),inference(split_conjunct,[status(thm)],[180])).
% fof(185, plain,![X6]:![X7]:![X8]:((~(disjointwith(X6,X7))|~(genls(X8,X7)))|disjointwith(X6,X8)),inference(fof_nnf,[status(thm)],[3])).
% fof(186, plain,![X9]:![X10]:![X11]:((~(disjointwith(X9,X10))|~(genls(X11,X10)))|disjointwith(X9,X11)),inference(variable_rename,[status(thm)],[185])).
% cnf(187,plain,(disjointwith(X1,X2)|~genls(X2,X3)|~disjointwith(X1,X3)),inference(split_conjunct,[status(thm)],[186])).
% fof(188, plain,![X7]:![X9]:![X8]:((~(disjointwith(X7,X9))|~(genls(X8,X7)))|disjointwith(X8,X9)),inference(fof_nnf,[status(thm)],[4])).
% fof(189, plain,![X10]:![X11]:![X12]:((~(disjointwith(X10,X11))|~(genls(X12,X10)))|disjointwith(X12,X11)),inference(variable_rename,[status(thm)],[188])).
% cnf(190,plain,(disjointwith(X1,X2)|~genls(X1,X3)|~disjointwith(X3,X2)),inference(split_conjunct,[status(thm)],[189])).
% cnf(226,plain,(genls(c_tptpcol_16_26926,c_tptpcol_15_26925)),inference(split_conjunct,[status(thm)],[18])).
% cnf(227,plain,(genls(c_tptpcol_16_92269,c_tptpcol_15_92268)),inference(split_conjunct,[status(thm)],[19])).
% cnf(230,plain,(disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[22])).
% cnf(231,plain,(genls(c_tptpcol_15_26925,c_tptpcol_14_26921)),inference(split_conjunct,[status(thm)],[23])).
% cnf(232,plain,(genls(c_tptpcol_15_92268,c_tptpcol_14_92264)),inference(split_conjunct,[status(thm)],[24])).
% cnf(314,plain,(genls(c_tptpcol_2_2,c_tptpcol_1_1)),inference(split_conjunct,[status(thm)],[52])).
% cnf(315,plain,(genls(c_tptpcol_2_65537,c_tptpcol_1_65536)),inference(split_conjunct,[status(thm)],[53])).
% cnf(389,plain,(genls(c_tptpcol_3_16386,c_tptpcol_2_2)),inference(split_conjunct,[status(thm)],[81])).
% cnf(390,plain,(genls(c_tptpcol_4_24578,c_tptpcol_3_16386)),inference(split_conjunct,[status(thm)],[82])).
% cnf(391,plain,(genls(c_tptpcol_5_24579,c_tptpcol_4_24578)),inference(split_conjunct,[status(thm)],[83])).
% cnf(392,plain,(genls(c_tptpcol_6_26627,c_tptpcol_5_24579)),inference(split_conjunct,[status(thm)],[84])).
% cnf(393,plain,(genls(c_tptpcol_7_26628,c_tptpcol_6_26627)),inference(split_conjunct,[status(thm)],[85])).
% cnf(394,plain,(genls(c_tptpcol_8_26629,c_tptpcol_7_26628)),inference(split_conjunct,[status(thm)],[86])).
% cnf(395,plain,(genls(c_tptpcol_9_26885,c_tptpcol_8_26629)),inference(split_conjunct,[status(thm)],[87])).
% cnf(396,plain,(genls(c_tptpcol_10_26886,c_tptpcol_9_26885)),inference(split_conjunct,[status(thm)],[88])).
% cnf(397,plain,(genls(c_tptpcol_11_26887,c_tptpcol_10_26886)),inference(split_conjunct,[status(thm)],[89])).
% cnf(398,plain,(genls(c_tptpcol_12_26919,c_tptpcol_11_26887)),inference(split_conjunct,[status(thm)],[90])).
% cnf(399,plain,(genls(c_tptpcol_13_26920,c_tptpcol_12_26919)),inference(split_conjunct,[status(thm)],[91])).
% cnf(400,plain,(genls(c_tptpcol_14_26921,c_tptpcol_13_26920)),inference(split_conjunct,[status(thm)],[92])).
% cnf(401,plain,(genls(c_tptpcol_3_81921,c_tptpcol_2_65537)),inference(split_conjunct,[status(thm)],[93])).
% cnf(402,plain,(genls(c_tptpcol_4_90113,c_tptpcol_3_81921)),inference(split_conjunct,[status(thm)],[94])).
% cnf(403,plain,(genls(c_tptpcol_5_90114,c_tptpcol_4_90113)),inference(split_conjunct,[status(thm)],[95])).
% cnf(404,plain,(genls(c_tptpcol_6_92162,c_tptpcol_5_90114)),inference(split_conjunct,[status(thm)],[96])).
% cnf(405,plain,(genls(c_tptpcol_7_92163,c_tptpcol_6_92162)),inference(split_conjunct,[status(thm)],[97])).
% cnf(406,plain,(genls(c_tptpcol_8_92164,c_tptpcol_7_92163)),inference(split_conjunct,[status(thm)],[98])).
% cnf(407,plain,(genls(c_tptpcol_9_92165,c_tptpcol_8_92164)),inference(split_conjunct,[status(thm)],[99])).
% cnf(408,plain,(genls(c_tptpcol_10_92166,c_tptpcol_9_92165)),inference(split_conjunct,[status(thm)],[100])).
% cnf(409,plain,(genls(c_tptpcol_11_92230,c_tptpcol_10_92166)),inference(split_conjunct,[status(thm)],[101])).
% cnf(410,plain,(genls(c_tptpcol_12_92262,c_tptpcol_11_92230)),inference(split_conjunct,[status(thm)],[102])).
% cnf(411,plain,(genls(c_tptpcol_13_92263,c_tptpcol_12_92262)),inference(split_conjunct,[status(thm)],[103])).
% cnf(412,plain,(genls(c_tptpcol_14_92264,c_tptpcol_13_92263)),inference(split_conjunct,[status(thm)],[104])).
% fof(629, negated_conjecture,(mtvisible(c_unitedstatesgeographypeoplemt)&~(disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269))),inference(fof_nnf,[status(thm)],[178])).
% cnf(630,negated_conjecture,(~disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),inference(split_conjunct,[status(thm)],[629])).
% cnf(640,plain,(disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)),inference(spm,[status(thm)],[181,230,theory(equality)])).
% cnf(783,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_12_92262,X1)),inference(spm,[status(thm)],[190,411,theory(equality)])).
% cnf(784,plain,(disjointwith(c_tptpcol_12_92262,X1)|~disjointwith(c_tptpcol_11_92230,X1)),inference(spm,[status(thm)],[190,410,theory(equality)])).
% cnf(785,plain,(disjointwith(c_tptpcol_11_92230,X1)|~disjointwith(c_tptpcol_10_92166,X1)),inference(spm,[status(thm)],[190,409,theory(equality)])).
% cnf(786,plain,(disjointwith(c_tptpcol_10_92166,X1)|~disjointwith(c_tptpcol_9_92165,X1)),inference(spm,[status(thm)],[190,408,theory(equality)])).
% cnf(787,plain,(disjointwith(c_tptpcol_9_92165,X1)|~disjointwith(c_tptpcol_8_92164,X1)),inference(spm,[status(thm)],[190,407,theory(equality)])).
% cnf(788,plain,(disjointwith(c_tptpcol_8_92164,X1)|~disjointwith(c_tptpcol_7_92163,X1)),inference(spm,[status(thm)],[190,406,theory(equality)])).
% cnf(789,plain,(disjointwith(c_tptpcol_7_92163,X1)|~disjointwith(c_tptpcol_6_92162,X1)),inference(spm,[status(thm)],[190,405,theory(equality)])).
% cnf(790,plain,(disjointwith(c_tptpcol_6_92162,X1)|~disjointwith(c_tptpcol_5_90114,X1)),inference(spm,[status(thm)],[190,404,theory(equality)])).
% cnf(791,plain,(disjointwith(c_tptpcol_5_90114,X1)|~disjointwith(c_tptpcol_4_90113,X1)),inference(spm,[status(thm)],[190,403,theory(equality)])).
% cnf(792,plain,(disjointwith(c_tptpcol_4_90113,X1)|~disjointwith(c_tptpcol_3_81921,X1)),inference(spm,[status(thm)],[190,402,theory(equality)])).
% cnf(793,plain,(disjointwith(c_tptpcol_3_81921,X1)|~disjointwith(c_tptpcol_2_65537,X1)),inference(spm,[status(thm)],[190,401,theory(equality)])).
% cnf(805,plain,(disjointwith(c_tptpcol_2_65537,X1)|~disjointwith(c_tptpcol_1_65536,X1)),inference(spm,[status(thm)],[190,315,theory(equality)])).
% cnf(807,plain,(disjointwith(c_tptpcol_14_92264,X1)|~disjointwith(c_tptpcol_13_92263,X1)),inference(spm,[status(thm)],[190,412,theory(equality)])).
% cnf(809,plain,(disjointwith(c_tptpcol_15_92268,X1)|~disjointwith(c_tptpcol_14_92264,X1)),inference(spm,[status(thm)],[190,232,theory(equality)])).
% cnf(812,plain,(disjointwith(c_tptpcol_16_92269,X1)|~disjointwith(c_tptpcol_15_92268,X1)),inference(spm,[status(thm)],[190,227,theory(equality)])).
% cnf(824,plain,(disjointwith(X1,c_tptpcol_13_26920)|~disjointwith(X1,c_tptpcol_12_26919)),inference(spm,[status(thm)],[187,399,theory(equality)])).
% cnf(825,plain,(disjointwith(X1,c_tptpcol_12_26919)|~disjointwith(X1,c_tptpcol_11_26887)),inference(spm,[status(thm)],[187,398,theory(equality)])).
% cnf(826,plain,(disjointwith(X1,c_tptpcol_11_26887)|~disjointwith(X1,c_tptpcol_10_26886)),inference(spm,[status(thm)],[187,397,theory(equality)])).
% cnf(827,plain,(disjointwith(X1,c_tptpcol_10_26886)|~disjointwith(X1,c_tptpcol_9_26885)),inference(spm,[status(thm)],[187,396,theory(equality)])).
% cnf(828,plain,(disjointwith(X1,c_tptpcol_9_26885)|~disjointwith(X1,c_tptpcol_8_26629)),inference(spm,[status(thm)],[187,395,theory(equality)])).
% cnf(829,plain,(disjointwith(X1,c_tptpcol_8_26629)|~disjointwith(X1,c_tptpcol_7_26628)),inference(spm,[status(thm)],[187,394,theory(equality)])).
% cnf(830,plain,(disjointwith(X1,c_tptpcol_7_26628)|~disjointwith(X1,c_tptpcol_6_26627)),inference(spm,[status(thm)],[187,393,theory(equality)])).
% cnf(831,plain,(disjointwith(X1,c_tptpcol_6_26627)|~disjointwith(X1,c_tptpcol_5_24579)),inference(spm,[status(thm)],[187,392,theory(equality)])).
% cnf(832,plain,(disjointwith(X1,c_tptpcol_5_24579)|~disjointwith(X1,c_tptpcol_4_24578)),inference(spm,[status(thm)],[187,391,theory(equality)])).
% cnf(833,plain,(disjointwith(X1,c_tptpcol_4_24578)|~disjointwith(X1,c_tptpcol_3_16386)),inference(spm,[status(thm)],[187,390,theory(equality)])).
% cnf(834,plain,(disjointwith(X1,c_tptpcol_3_16386)|~disjointwith(X1,c_tptpcol_2_2)),inference(spm,[status(thm)],[187,389,theory(equality)])).
% cnf(836,plain,(disjointwith(X1,c_tptpcol_2_2)|~disjointwith(X1,c_tptpcol_1_1)),inference(spm,[status(thm)],[187,314,theory(equality)])).
% cnf(838,plain,(disjointwith(X1,c_tptpcol_14_26921)|~disjointwith(X1,c_tptpcol_13_26920)),inference(spm,[status(thm)],[187,400,theory(equality)])).
% cnf(840,plain,(disjointwith(X1,c_tptpcol_15_26925)|~disjointwith(X1,c_tptpcol_14_26921)),inference(spm,[status(thm)],[187,231,theory(equality)])).
% cnf(841,plain,(disjointwith(X1,c_tptpcol_16_26926)|~disjointwith(X1,c_tptpcol_15_26925)),inference(spm,[status(thm)],[187,226,theory(equality)])).
% cnf(1403,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_11_92230,X1)),inference(spm,[status(thm)],[783,784,theory(equality)])).
% cnf(1434,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_10_92166,X1)),inference(spm,[status(thm)],[1403,785,theory(equality)])).
% cnf(1472,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_9_92165,X1)),inference(spm,[status(thm)],[1434,786,theory(equality)])).
% cnf(1513,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_8_92164,X1)),inference(spm,[status(thm)],[1472,787,theory(equality)])).
% cnf(1557,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_7_92163,X1)),inference(spm,[status(thm)],[1513,788,theory(equality)])).
% cnf(1604,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_6_92162,X1)),inference(spm,[status(thm)],[1557,789,theory(equality)])).
% cnf(1662,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_5_90114,X1)),inference(spm,[status(thm)],[1604,790,theory(equality)])).
% cnf(1715,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_4_90113,X1)),inference(spm,[status(thm)],[1662,791,theory(equality)])).
% cnf(1775,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_3_81921,X1)),inference(spm,[status(thm)],[1715,792,theory(equality)])).
% cnf(1838,plain,(disjointwith(c_tptpcol_13_92263,X1)|~disjointwith(c_tptpcol_2_65537,X1)),inference(spm,[status(thm)],[1775,793,theory(equality)])).
% cnf(3239,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_11_26887)),inference(spm,[status(thm)],[812,825,theory(equality)])).
% cnf(3283,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_10_26886)),inference(spm,[status(thm)],[3239,826,theory(equality)])).
% cnf(3326,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_9_26885)),inference(spm,[status(thm)],[3283,827,theory(equality)])).
% cnf(3367,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_8_26629)),inference(spm,[status(thm)],[3326,828,theory(equality)])).
% cnf(3410,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_7_26628)),inference(spm,[status(thm)],[3367,829,theory(equality)])).
% cnf(3451,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_6_26627)),inference(spm,[status(thm)],[3410,830,theory(equality)])).
% cnf(3494,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_5_24579)),inference(spm,[status(thm)],[3451,831,theory(equality)])).
% cnf(3534,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|~disjointwith(c_tptpcol_15_92268,c_tptpcol_4_24578)),inference(spm,[status(thm)],[3494,832,theory(equality)])).
% cnf(3567,plain,(disjointwith(c_tptpcol_15_92268,c_tptpcol_4_24578)|~disjointwith(c_tptpcol_14_92264,c_tptpcol_3_16386)),inference(spm,[status(thm)],[809,833,theory(equality)])).
% cnf(3597,plain,(disjointwith(c_tptpcol_14_92264,c_tptpcol_3_16386)|~disjointwith(c_tptpcol_13_92263,c_tptpcol_2_2)),inference(spm,[status(thm)],[807,834,theory(equality)])).
% cnf(3700,plain,(disjointwith(c_tptpcol_13_92263,c_tptpcol_2_2)|~disjointwith(c_tptpcol_2_65537,c_tptpcol_1_1)),inference(spm,[status(thm)],[1838,836,theory(equality)])).
% cnf(4548,plain,(disjointwith(c_tptpcol_13_92263,c_tptpcol_2_2)|~disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)),inference(spm,[status(thm)],[3700,805,theory(equality)])).
% cnf(4549,plain,(disjointwith(c_tptpcol_13_92263,c_tptpcol_2_2)|$false),inference(rw,[status(thm)],[4548,640,theory(equality)])).
% cnf(4550,plain,(disjointwith(c_tptpcol_13_92263,c_tptpcol_2_2)),inference(cn,[status(thm)],[4549,theory(equality)])).
% cnf(4566,plain,(disjointwith(c_tptpcol_14_92264,c_tptpcol_3_16386)|$false),inference(rw,[status(thm)],[3597,4550,theory(equality)])).
% cnf(4567,plain,(disjointwith(c_tptpcol_14_92264,c_tptpcol_3_16386)),inference(cn,[status(thm)],[4566,theory(equality)])).
% cnf(4574,plain,(disjointwith(c_tptpcol_15_92268,c_tptpcol_4_24578)|$false),inference(rw,[status(thm)],[3567,4567,theory(equality)])).
% cnf(4575,plain,(disjointwith(c_tptpcol_15_92268,c_tptpcol_4_24578)),inference(cn,[status(thm)],[4574,theory(equality)])).
% cnf(4598,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)|$false),inference(rw,[status(thm)],[3534,4575,theory(equality)])).
% cnf(4599,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_12_26919)),inference(cn,[status(thm)],[4598,theory(equality)])).
% cnf(4619,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_13_26920)),inference(spm,[status(thm)],[824,4599,theory(equality)])).
% cnf(4786,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_14_26921)),inference(spm,[status(thm)],[838,4619,theory(equality)])).
% cnf(4862,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_15_26925)),inference(spm,[status(thm)],[840,4786,theory(equality)])).
% cnf(4885,plain,(disjointwith(c_tptpcol_16_92269,c_tptpcol_16_26926)),inference(spm,[status(thm)],[841,4862,theory(equality)])).
% cnf(4889,plain,(disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)),inference(spm,[status(thm)],[181,4885,theory(equality)])).
% cnf(4892,plain,($false),inference(sr,[status(thm)],[4889,630,theory(equality)])).
% cnf(4893,plain,($false),4892,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 1916
% # ...of these trivial : 40
% # ...subsumed : 172
% # ...remaining for further processing: 1704
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 30
% # Backward-rewritten : 143
% # Generated clauses : 3539
% # ...of the previous two non-trivial : 2874
% # Contextual simplify-reflections : 0
% # Paramodulations : 3539
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 1531
% # Positive orientable unit clauses: 153
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 1375
% # Current number of unprocessed clauses: 1123
% # ...number of literals in the above : 2241
% # Clause-clause subsumption calls (NU) : 359926
% # Rec. Clause-clause subsumption calls : 359815
% # Unit Clause-clause subsumption calls : 5275
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 28
% # Indexed BW rewrite successes : 28
% # Backwards rewriting index: 941 leaves, 1.02+/-0.291 terms/leaf
% # Paramod-from index: 323 leaves, 1.00+/-0.000 terms/leaf
% # Paramod-into index: 878 leaves, 1.01+/-0.199 terms/leaf
% # -------------------------------------------------
% # User time : 0.252 s
% # System time : 0.011 s
% # Total time : 0.263 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.41 CPU 0.47 WC
% FINAL PrfWatch: 0.41 CPU 0.47 WC
% SZS output end Solution for /tmp/SystemOnTPTP27142/CSR049+1.tptp
%
%------------------------------------------------------------------------------