%------------------------------------------------------------------------------
% File : SInE---0.4
% Problem : CSR061+2 : 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:34:36 EST 2010
% Result : Theorem 0.47s
% Output : CNFRefutation 0.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 21
% Syntax : Number of formulae : 87 ( 52 unt; 0 def)
% Number of atoms : 130 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 82 ( 39 ~; 35 |; 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 : 19 ( 19 usr; 19 con; 0-0 aty)
% Number of variables : 48 ( 0 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(9,axiom,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_68) ).
fof(20,axiom,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_215) ).
fof(22,axiom,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_356) ).
fof(34,axiom,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_129) ).
fof(35,axiom,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_387) ).
fof(37,axiom,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_235) ).
fof(43,axiom,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_393) ).
fof(44,axiom,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_422) ).
fof(50,axiom,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_160) ).
fof(54,axiom,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_499) ).
fof(56,axiom,
! [X5,X4,X6] :
( ( disjointwith(X5,X4)
& genls(X6,X5) )
=> disjointwith(X6,X4) ),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_1122) ).
fof(57,axiom,
! [X3,X5,X6] :
( ( disjointwith(X3,X5)
& genls(X6,X5) )
=> disjointwith(X3,X6) ),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_1121) ).
fof(58,axiom,
! [X1,X8] :
( disjointwith(X1,X8)
=> disjointwith(X8,X1) ),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_1120) ).
fof(62,axiom,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_258) ).
fof(70,axiom,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_489) ).
fof(71,axiom,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_487) ).
fof(76,axiom,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_361) ).
fof(79,axiom,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_100) ).
fof(90,axiom,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_70) ).
fof(93,axiom,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',ax1_401) ).
fof(96,conjecture,
( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
file('/tmp/tmpS2YUVa/sel_CSR061+2.p_1',query111) ).
fof(97,negated_conjecture,
~ ( mtvisible(c_timehasnoendmt)
=> disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(assume_negation,[status(cth)],[96]) ).
cnf(122,plain,
genls(c_tptpcol_4_106497,c_tptpcol_3_98305),
inference(split_conjunct,[status(thm)],[9]) ).
cnf(153,plain,
genls(c_tptpcol_7_113665,c_tptpcol_6_112641),
inference(split_conjunct,[status(thm)],[20]) ).
cnf(155,plain,
genls(c_tptpcol_8_117763,c_tptpcol_7_117762),
inference(split_conjunct,[status(thm)],[22]) ).
cnf(187,plain,
genls(c_tptpcol_11_118084,c_tptpcol_10_118020),
inference(split_conjunct,[status(thm)],[34]) ).
cnf(188,plain,
genls(c_tptpcol_9_118019,c_tptpcol_8_117763),
inference(split_conjunct,[status(thm)],[35]) ).
cnf(192,plain,
genls(c_tptpcol_4_114689,c_tptpcol_3_114688),
inference(split_conjunct,[status(thm)],[37]) ).
cnf(206,plain,
genls(c_tptpcol_6_112641,c_tptpcol_5_110593),
inference(split_conjunct,[status(thm)],[43]) ).
cnf(207,plain,
genls(c_tptpcol_13_118117,c_tptpcol_12_118116),
inference(split_conjunct,[status(thm)],[44]) ).
cnf(223,plain,
genls(c_tptpcol_10_118020,c_tptpcol_9_118019),
inference(split_conjunct,[status(thm)],[50]) ).
cnf(233,plain,
genls(c_tptpcol_14_118118,c_tptpcol_13_118117),
inference(split_conjunct,[status(thm)],[54]) ).
fof(237,plain,
! [X5,X4,X6] :
( ~ disjointwith(X5,X4)
| ~ genls(X6,X5)
| disjointwith(X6,X4) ),
inference(fof_nnf,[status(thm)],[56]) ).
fof(238,plain,
! [X7,X8,X9] :
( ~ disjointwith(X7,X8)
| ~ genls(X9,X7)
| disjointwith(X9,X8) ),
inference(variable_rename,[status(thm)],[237]) ).
cnf(239,plain,
( disjointwith(X1,X2)
| ~ genls(X1,X3)
| ~ disjointwith(X3,X2) ),
inference(split_conjunct,[status(thm)],[238]) ).
fof(240,plain,
! [X3,X5,X6] :
( ~ disjointwith(X3,X5)
| ~ genls(X6,X5)
| disjointwith(X3,X6) ),
inference(fof_nnf,[status(thm)],[57]) ).
fof(241,plain,
! [X7,X8,X9] :
( ~ disjointwith(X7,X8)
| ~ genls(X9,X8)
| disjointwith(X7,X9) ),
inference(variable_rename,[status(thm)],[240]) ).
cnf(242,plain,
( disjointwith(X1,X2)
| ~ genls(X2,X3)
| ~ disjointwith(X1,X3) ),
inference(split_conjunct,[status(thm)],[241]) ).
fof(243,plain,
! [X1,X8] :
( ~ disjointwith(X1,X8)
| disjointwith(X8,X1) ),
inference(fof_nnf,[status(thm)],[58]) ).
fof(244,plain,
! [X9,X10] :
( ~ disjointwith(X9,X10)
| disjointwith(X10,X9) ),
inference(variable_rename,[status(thm)],[243]) ).
cnf(245,plain,
( disjointwith(X1,X2)
| ~ disjointwith(X2,X1) ),
inference(split_conjunct,[status(thm)],[244]) ).
cnf(255,plain,
genls(c_tptpcol_12_118116,c_tptpcol_11_118084),
inference(split_conjunct,[status(thm)],[62]) ).
cnf(277,plain,
genls(c_tptpcol_5_110593,c_tptpcol_4_106497),
inference(split_conjunct,[status(thm)],[70]) ).
cnf(278,plain,
disjointwith(c_tptpcol_3_98305,c_tptpcol_3_114688),
inference(split_conjunct,[status(thm)],[71]) ).
cnf(291,plain,
genls(c_tptpcol_7_117762,c_tptpcol_6_116738),
inference(split_conjunct,[status(thm)],[76]) ).
cnf(298,plain,
genls(c_tptpcol_6_116738,c_tptpcol_5_114690),
inference(split_conjunct,[status(thm)],[79]) ).
cnf(329,plain,
genls(c_tptpcol_5_114690,c_tptpcol_4_114689),
inference(split_conjunct,[status(thm)],[90]) ).
cnf(336,plain,
genls(c_tptpcol_8_114177,c_tptpcol_7_113665),
inference(split_conjunct,[status(thm)],[93]) ).
fof(343,negated_conjecture,
( mtvisible(c_timehasnoendmt)
& ~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118) ),
inference(fof_nnf,[status(thm)],[97]) ).
cnf(344,negated_conjecture,
~ disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118),
inference(split_conjunct,[status(thm)],[343]) ).
cnf(346,plain,
disjointwith(c_tptpcol_3_114688,c_tptpcol_3_98305),
inference(spm,[status(thm)],[245,278,theory(equality)]) ).
cnf(440,plain,
( disjointwith(X1,c_tptpcol_14_118118)
| ~ disjointwith(X1,c_tptpcol_13_118117) ),
inference(spm,[status(thm)],[242,233,theory(equality)]) ).
cnf(444,plain,
( disjointwith(X1,c_tptpcol_4_106497)
| ~ disjointwith(X1,c_tptpcol_3_98305) ),
inference(spm,[status(thm)],[242,122,theory(equality)]) ).
cnf(445,plain,
( disjointwith(X1,c_tptpcol_12_118116)
| ~ disjointwith(X1,c_tptpcol_11_118084) ),
inference(spm,[status(thm)],[242,255,theory(equality)]) ).
cnf(446,plain,
( disjointwith(X1,c_tptpcol_8_117763)
| ~ disjointwith(X1,c_tptpcol_7_117762) ),
inference(spm,[status(thm)],[242,155,theory(equality)]) ).
cnf(447,plain,
( disjointwith(X1,c_tptpcol_7_117762)
| ~ disjointwith(X1,c_tptpcol_6_116738) ),
inference(spm,[status(thm)],[242,291,theory(equality)]) ).
cnf(448,plain,
( disjointwith(X1,c_tptpcol_6_116738)
| ~ disjointwith(X1,c_tptpcol_5_114690) ),
inference(spm,[status(thm)],[242,298,theory(equality)]) ).
cnf(449,plain,
( disjointwith(X1,c_tptpcol_10_118020)
| ~ disjointwith(X1,c_tptpcol_9_118019) ),
inference(spm,[status(thm)],[242,223,theory(equality)]) ).
cnf(450,plain,
( disjointwith(X1,c_tptpcol_11_118084)
| ~ disjointwith(X1,c_tptpcol_10_118020) ),
inference(spm,[status(thm)],[242,187,theory(equality)]) ).
cnf(451,plain,
( disjointwith(X1,c_tptpcol_9_118019)
| ~ disjointwith(X1,c_tptpcol_8_117763) ),
inference(spm,[status(thm)],[242,188,theory(equality)]) ).
cnf(452,plain,
( disjointwith(X1,c_tptpcol_4_114689)
| ~ disjointwith(X1,c_tptpcol_3_114688) ),
inference(spm,[status(thm)],[242,192,theory(equality)]) ).
cnf(454,plain,
( disjointwith(X1,c_tptpcol_13_118117)
| ~ disjointwith(X1,c_tptpcol_12_118116) ),
inference(spm,[status(thm)],[242,207,theory(equality)]) ).
cnf(455,plain,
( disjointwith(X1,c_tptpcol_5_114690)
| ~ disjointwith(X1,c_tptpcol_4_114689) ),
inference(spm,[status(thm)],[242,329,theory(equality)]) ).
cnf(457,plain,
( disjointwith(c_tptpcol_8_114177,X1)
| ~ disjointwith(c_tptpcol_7_113665,X1) ),
inference(spm,[status(thm)],[239,336,theory(equality)]) ).
cnf(458,plain,
( disjointwith(c_tptpcol_6_112641,X1)
| ~ disjointwith(c_tptpcol_5_110593,X1) ),
inference(spm,[status(thm)],[239,206,theory(equality)]) ).
cnf(459,plain,
( disjointwith(c_tptpcol_7_113665,X1)
| ~ disjointwith(c_tptpcol_6_112641,X1) ),
inference(spm,[status(thm)],[239,153,theory(equality)]) ).
cnf(469,plain,
( disjointwith(c_tptpcol_5_110593,X1)
| ~ disjointwith(c_tptpcol_4_106497,X1) ),
inference(spm,[status(thm)],[239,277,theory(equality)]) ).
cnf(707,plain,
( disjointwith(c_tptpcol_8_114177,c_tptpcol_14_118118)
| ~ disjointwith(c_tptpcol_7_113665,c_tptpcol_13_118117) ),
inference(spm,[status(thm)],[440,457,theory(equality)]) ).
cnf(708,plain,
~ disjointwith(c_tptpcol_7_113665,c_tptpcol_13_118117),
inference(sr,[status(thm)],[707,344,theory(equality)]) ).
cnf(759,plain,
disjointwith(c_tptpcol_3_114688,c_tptpcol_4_106497),
inference(spm,[status(thm)],[444,346,theory(equality)]) ).
cnf(761,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_3_114688),
inference(spm,[status(thm)],[245,759,theory(equality)]) ).
cnf(1081,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_4_114689),
inference(spm,[status(thm)],[452,761,theory(equality)]) ).
cnf(1223,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_5_114690),
inference(spm,[status(thm)],[455,1081,theory(equality)]) ).
cnf(1239,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_6_116738),
inference(spm,[status(thm)],[448,1223,theory(equality)]) ).
cnf(1292,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_7_117762),
inference(spm,[status(thm)],[447,1239,theory(equality)]) ).
cnf(1317,plain,
( disjointwith(c_tptpcol_7_113665,c_tptpcol_13_118117)
| ~ disjointwith(c_tptpcol_6_112641,c_tptpcol_12_118116) ),
inference(spm,[status(thm)],[454,459,theory(equality)]) ).
cnf(1325,plain,
~ disjointwith(c_tptpcol_6_112641,c_tptpcol_12_118116),
inference(sr,[status(thm)],[1317,708,theory(equality)]) ).
cnf(1406,plain,
disjointwith(c_tptpcol_4_106497,c_tptpcol_8_117763),
inference(spm,[status(thm)],[446,1292,theory(equality)]) ).
cnf(1766,plain,
( disjointwith(c_tptpcol_5_110593,c_tptpcol_9_118019)
| ~ disjointwith(c_tptpcol_4_106497,c_tptpcol_8_117763) ),
inference(spm,[status(thm)],[469,451,theory(equality)]) ).
cnf(1773,plain,
( disjointwith(c_tptpcol_5_110593,c_tptpcol_9_118019)
| $false ),
inference(rw,[status(thm)],[1766,1406,theory(equality)]) ).
cnf(1774,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_9_118019),
inference(cn,[status(thm)],[1773,theory(equality)]) ).
cnf(1873,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_10_118020),
inference(spm,[status(thm)],[449,1774,theory(equality)]) ).
cnf(1922,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_11_118084),
inference(spm,[status(thm)],[450,1873,theory(equality)]) ).
cnf(1987,plain,
disjointwith(c_tptpcol_5_110593,c_tptpcol_12_118116),
inference(spm,[status(thm)],[445,1922,theory(equality)]) ).
cnf(2073,plain,
disjointwith(c_tptpcol_6_112641,c_tptpcol_12_118116),
inference(spm,[status(thm)],[458,1987,theory(equality)]) ).
cnf(2076,plain,
$false,
inference(sr,[status(thm)],[2073,1325,theory(equality)]) ).
cnf(2077,plain,
$false,
2076,
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% % SZS status Started for /home/graph/tptp/TPTP/Problems/CSR/CSR061+2.p
% --creating new selector for [CSR002+1.ax]
% -running prover on /tmp/tmpS2YUVa/sel_CSR061+2.p_1 with time limit 29
% -prover status Theorem
% Problem CSR061+2.p solved in phase 0.
% % SZS status Theorem for /home/graph/tptp/TPTP/Problems/CSR/CSR061+2.p
% % SZS status Ended for /home/graph/tptp/TPTP/Problems/CSR/CSR061+2.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
%
%------------------------------------------------------------------------------