%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR061+5 : TPTP v5.0.0. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : Source/sine.py -e eprover -t %d %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 : Sat Dec 25 06:35:06 EST 2010
% Result : Theorem 210.59s
% Output : CNFRefutation 215.35s
% 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/CSR061+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/tmpVvMBiM/sel_CSR061+5.p_1 with time limit 29
% -prover status ResourceOut
% -running prover on /tmp/tmpVvMBiM/sel_CSR061+5.p_2 with time limit 51
% -prover status ResourceOut
% --creating new selector for [CSR002+4.ax]
% -running prover on /tmp/tmpVvMBiM/sel_CSR061+5.p_3 with time limit 48
% -prover status Theorem
% Problem CSR061+5.p solved in phase 2.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR061+5.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR061+5.p
% Solved 1 out of 1.
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(19, axiom,genls(c_tptpcol_10_118020,c_tptpcol_9_118019),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_108378)).
% fof(32, axiom,genls(c_tptpcol_6_116738,c_tptpcol_5_114690),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_88736)).
% fof(42, axiom,genls(c_tptpcol_9_118019,c_tptpcol_8_117763),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_62842)).
% fof(44, axiom,genls(c_tptpcol_8_114177,c_tptpcol_7_113665),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_260394)).
% fof(49, axiom,disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_153816)).
% fof(61, axiom,genls(c_tptpcol_6_112641,c_tptpcol_5_110593),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_53870)).
% fof(69, axiom,genls(c_tptpcol_7_117762,c_tptpcol_6_116738),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_266778)).
% fof(84, axiom,genls(c_tptpcol_5_114690,c_tptpcol_4_114689),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_317532)).
% fof(105, axiom,genls(c_tptpcol_11_118084,c_tptpcol_10_118020),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_137176)).
% fof(114, axiom,genls(c_tptpcol_12_118116,c_tptpcol_11_118084),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_49594)).
% fof(130, axiom,genls(c_tptpcol_5_110593,c_tptpcol_4_106497),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_224621)).
% fof(135, axiom,genls(c_tptpcol_13_118117,c_tptpcol_12_118116),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_3183)).
% fof(144, axiom,genls(c_tptpcol_7_113665,c_tptpcol_6_112641),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_225008)).
% fof(170, axiom,genls(c_tptpcol_4_114689,c_tptpcol_3_114688),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_118059)).
% fof(251, axiom,genls(c_tptpcol_8_117763,c_tptpcol_7_117762),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_54929)).
% fof(270, axiom,genls(c_tptpcol_14_118118,c_tptpcol_13_118117),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_196988)).
% fof(345, axiom,genls(c_tptpcol_4_106497,c_tptpcol_3_98305),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_35570)).
% fof(452, axiom,![X3]:![X10]:(disjointwith(X3,X10)=>disjointwith(X10,X3)),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_540135)).
% fof(453, axiom,![X6]:![X4]:![X7]:((disjointwith(X6,X4)&genls(X7,X6))=>disjointwith(X7,X4)),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_540137)).
% fof(454, axiom,![X2]:![X6]:![X7]:((disjointwith(X2,X6)&genls(X7,X6))=>disjointwith(X2,X7)),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', ax4_540136)).
% fof(477, conjecture,(mtvisible(c_timehasnoendmt)=>disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)),file('/tmp/tmpVvMBiM/sel_CSR061+5.p_3', query261)).
% fof(478, negated_conjecture,~((mtvisible(c_timehasnoendmt)=>disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118))),inference(assume_negation,[status(cth)],[477])).
% cnf(511,plain,(genls(c_tptpcol_10_118020,c_tptpcol_9_118019)),inference(split_conjunct,[status(thm)],[19])).
% cnf(540,plain,(genls(c_tptpcol_6_116738,c_tptpcol_5_114690)),inference(split_conjunct,[status(thm)],[32])).
% cnf(552,plain,(genls(c_tptpcol_9_118019,c_tptpcol_8_117763)),inference(split_conjunct,[status(thm)],[42])).
% cnf(554,plain,(genls(c_tptpcol_8_114177,c_tptpcol_7_113665)),inference(split_conjunct,[status(thm)],[44])).
% cnf(567,plain,(disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688)),inference(split_conjunct,[status(thm)],[49])).
% cnf(584,plain,(genls(c_tptpcol_6_112641,c_tptpcol_5_110593)),inference(split_conjunct,[status(thm)],[61])).
% cnf(599,plain,(genls(c_tptpcol_7_117762,c_tptpcol_6_116738)),inference(split_conjunct,[status(thm)],[69])).
% cnf(622,plain,(genls(c_tptpcol_5_114690,c_tptpcol_4_114689)),inference(split_conjunct,[status(thm)],[84])).
% cnf(667,plain,(genls(c_tptpcol_11_118084,c_tptpcol_10_118020)),inference(split_conjunct,[status(thm)],[105])).
% cnf(682,plain,(genls(c_tptpcol_12_118116,c_tptpcol_11_118084)),inference(split_conjunct,[status(thm)],[114])).
% cnf(716,plain,(genls(c_tptpcol_5_110593,c_tptpcol_4_106497)),inference(split_conjunct,[status(thm)],[130])).
% cnf(725,plain,(genls(c_tptpcol_13_118117,c_tptpcol_12_118116)),inference(split_conjunct,[status(thm)],[135])).
% cnf(740,plain,(genls(c_tptpcol_7_113665,c_tptpcol_6_112641)),inference(split_conjunct,[status(thm)],[144])).
% cnf(788,plain,(genls(c_tptpcol_4_114689,c_tptpcol_3_114688)),inference(split_conjunct,[status(thm)],[170])).
% cnf(924,plain,(genls(c_tptpcol_8_117763,c_tptpcol_7_117762)),inference(split_conjunct,[status(thm)],[251])).
% cnf(962,plain,(genls(c_tptpcol_14_118118,c_tptpcol_13_118117)),inference(split_conjunct,[status(thm)],[270])).
% cnf(1096,plain,(genls(c_tptpcol_4_106497,c_tptpcol_3_98305)),inference(split_conjunct,[status(thm)],[345])).
% fof(1275, plain,![X3]:![X10]:(~(disjointwith(X3,X10))|disjointwith(X10,X3)),inference(fof_nnf,[status(thm)],[452])).
% fof(1276, plain,![X11]:![X12]:(~(disjointwith(X11,X12))|disjointwith(X12,X11)),inference(variable_rename,[status(thm)],[1275])).
% cnf(1277,plain,(disjointwith(X1,X2)|~disjointwith(X2,X1)),inference(split_conjunct,[status(thm)],[1276])).
% fof(1278, plain,![X6]:![X4]:![X7]:((~(disjointwith(X6,X4))|~(genls(X7,X6)))|disjointwith(X7,X4)),inference(fof_nnf,[status(thm)],[453])).
% fof(1279, plain,![X8]:![X9]:![X10]:((~(disjointwith(X8,X9))|~(genls(X10,X8)))|disjointwith(X10,X9)),inference(variable_rename,[status(thm)],[1278])).
% cnf(1280,plain,(disjointwith(X1,X2)|~genls(X1,X3)|~disjointwith(X3,X2)),inference(split_conjunct,[status(thm)],[1279])).
% fof(1281, plain,![X2]:![X6]:![X7]:((~(disjointwith(X2,X6))|~(genls(X7,X6)))|disjointwith(X2,X7)),inference(fof_nnf,[status(thm)],[454])).
% fof(1282, plain,![X8]:![X9]:![X10]:((~(disjointwith(X8,X9))|~(genls(X10,X9)))|disjointwith(X8,X10)),inference(variable_rename,[status(thm)],[1281])).
% cnf(1283,plain,(disjointwith(X1,X2)|~genls(X2,X3)|~disjointwith(X1,X3)),inference(split_conjunct,[status(thm)],[1282])).
% fof(1325, negated_conjecture,(mtvisible(c_timehasnoendmt)&~(disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118))),inference(fof_nnf,[status(thm)],[478])).
% cnf(1326,negated_conjecture,(~disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)),inference(split_conjunct,[status(thm)],[1325])).
% cnf(1330,plain,(disjointwith(c_tptpcol_3_114688,c_tptpcol_3_98305)),inference(spm,[status(thm)],[1277,567,theory(equality)])).
% cnf(1683,plain,(disjointwith(X1,c_tptpcol_8_114177)|~disjointwith(X1,c_tptpcol_7_113665)),inference(spm,[status(thm)],[1283,554,theory(equality)])).
% cnf(1693,plain,(disjointwith(X1,c_tptpcol_6_116738)|~disjointwith(X1,c_tptpcol_5_114690)),inference(spm,[status(thm)],[1283,540,theory(equality)])).
% cnf(1694,plain,(disjointwith(X1,c_tptpcol_5_114690)|~disjointwith(X1,c_tptpcol_4_114689)),inference(spm,[status(thm)],[1283,622,theory(equality)])).
% cnf(1696,plain,(disjointwith(X1,c_tptpcol_8_117763)|~disjointwith(X1,c_tptpcol_7_117762)),inference(spm,[status(thm)],[1283,924,theory(equality)])).
% cnf(1697,plain,(disjointwith(X1,c_tptpcol_7_113665)|~disjointwith(X1,c_tptpcol_6_112641)),inference(spm,[status(thm)],[1283,740,theory(equality)])).
% cnf(1700,plain,(disjointwith(X1,c_tptpcol_6_112641)|~disjointwith(X1,c_tptpcol_5_110593)),inference(spm,[status(thm)],[1283,584,theory(equality)])).
% cnf(1701,plain,(disjointwith(X1,c_tptpcol_5_110593)|~disjointwith(X1,c_tptpcol_4_106497)),inference(spm,[status(thm)],[1283,716,theory(equality)])).
% cnf(1704,plain,(disjointwith(X1,c_tptpcol_7_117762)|~disjointwith(X1,c_tptpcol_6_116738)),inference(spm,[status(thm)],[1283,599,theory(equality)])).
% cnf(1712,plain,(disjointwith(X1,c_tptpcol_4_106497)|~disjointwith(X1,c_tptpcol_3_98305)),inference(spm,[status(thm)],[1283,1096,theory(equality)])).
% cnf(1716,plain,(disjointwith(c_tptpcol_14_118118,X1)|~disjointwith(c_tptpcol_13_118117,X1)),inference(spm,[status(thm)],[1280,962,theory(equality)])).
% cnf(1723,plain,(disjointwith(c_tptpcol_10_118020,X1)|~disjointwith(c_tptpcol_9_118019,X1)),inference(spm,[status(thm)],[1280,511,theory(equality)])).
% cnf(1724,plain,(disjointwith(c_tptpcol_9_118019,X1)|~disjointwith(c_tptpcol_8_117763,X1)),inference(spm,[status(thm)],[1280,552,theory(equality)])).
% cnf(1739,plain,(disjointwith(c_tptpcol_4_114689,X1)|~disjointwith(c_tptpcol_3_114688,X1)),inference(spm,[status(thm)],[1280,788,theory(equa
% lity)])).
% cnf(1743,plain,(disjointwith(c_tptpcol_11_118084,X1)|~disjointwith(c_tptpcol_10_118020,X1)),inference(spm,[status(thm)],[1280,667,theory(equality)])).
% cnf(1745,plain,(disjointwith(c_tptpcol_12_118116,X1)|~disjointwith(c_tptpcol_11_118084,X1)),inference(spm,[status(thm)],[1280,682,theory(equality)])).
% cnf(1747,plain,(disjointwith(c_tptpcol_13_118117,X1)|~disjointwith(c_tptpcol_12_118116,X1)),inference(spm,[status(thm)],[1280,725,theory(equality)])).
% cnf(2318,plain,(disjointwith(c_tptpcol_14_118118,c_tptpcol_6_112641)|~disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)),inference(spm,[status(thm)],[1700,1716,theory(equality)])).
% cnf(2321,plain,(disjointwith(c_tptpcol_14_118118,c_tptpcol_7_113665)|~disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)),inference(spm,[status(thm)],[1697,2318,theory(equality)])).
% cnf(2326,plain,(disjointwith(c_tptpcol_14_118118,c_tptpcol_8_114177)|~disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)),inference(spm,[status(thm)],[1683,2321,theory(equality)])).
% cnf(2334,plain,(disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)|~disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)),inference(spm,[status(thm)],[1277,2326,theory(equality)])).
% cnf(2336,plain,(~disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)),inference(sr,[status(thm)],[2334,1326,theory(equality)])).
% cnf(2371,plain,(disjointwith(X1,c_tptpcol_8_117763)|~disjointwith(X1,c_tptpcol_6_116738)),inference(spm,[status(thm)],[1696,1704,theory(equality)])).
% cnf(3234,plain,(disjointwith(c_tptpcol_4_114689,c_tptpcol_4_106497)|~disjointwith(c_tptpcol_3_114688,c_tptpcol_3_98305)),inference(spm,[status(thm)],[1712,1739,theory(equality)])).
% cnf(3237,plain,(disjointwith(c_tptpcol_4_114689,c_tptpcol_4_106497)|$false),inference(rw,[status(thm)],[3234,1330,theory(equality)])).
% cnf(3238,plain,(disjointwith(c_tptpcol_4_114689,c_tptpcol_4_106497)),inference(cn,[status(thm)],[3237,theory(equality)])).
% cnf(3251,plain,(disjointwith(c_tptpcol_4_106497,c_tptpcol_4_114689)),inference(spm,[status(thm)],[1277,3238,theory(equality)])).
% cnf(3285,plain,(disjointwith(c_tptpcol_4_106497,c_tptpcol_5_114690)),inference(spm,[status(thm)],[1694,3251,theory(equality)])).
% cnf(3347,plain,(disjointwith(c_tptpcol_4_106497,c_tptpcol_6_116738)),inference(spm,[status(thm)],[1693,3285,theory(equality)])).
% cnf(3507,plain,(disjointwith(c_tptpcol_13_118117,c_tptpcol_5_110593)|~disjointwith(c_tptpcol_12_118116,c_tptpcol_4_106497)),inference(spm,[status(thm)],[1747,1701,theory(equality)])).
% cnf(3518,plain,(~disjointwith(c_tptpcol_12_118116,c_tptpcol_4_106497)),inference(sr,[status(thm)],[3507,2336,theory(equality)])).
% cnf(3519,plain,(~disjointwith(c_tptpcol_11_118084,c_tptpcol_4_106497)),inference(spm,[status(thm)],[3518,1745,theory(equality)])).
% cnf(3520,plain,(~disjointwith(c_tptpcol_10_118020,c_tptpcol_4_106497)),inference(spm,[status(thm)],[3519,1743,theory(equality)])).
% cnf(3521,plain,(~disjointwith(c_tptpcol_9_118019,c_tptpcol_4_106497)),inference(spm,[status(thm)],[3520,1723,theory(equality)])).
% cnf(4720,plain,(disjointwith(c_tptpcol_4_106497,c_tptpcol_8_117763)),inference(spm,[status(thm)],[2371,3347,theory(equality)])).
% cnf(4755,plain,(disjointwith(c_tptpcol_8_117763,c_tptpcol_4_106497)),inference(spm,[status(thm)],[1277,4720,theory(equality)])).
% cnf(4804,plain,(disjointwith(c_tptpcol_9_118019,c_tptpcol_4_106497)),inference(spm,[status(thm)],[1724,4755,theory(equality)])).
% cnf(4806,plain,($false),inference(sr,[status(thm)],[4804,3521,theory(equality)])).
% cnf(4807,plain,($false),4806,['proof']).
% # SZS output end CNFRefutation
%
%------------------------------------------------------------------------------