%------------------------------------------------------------------------------ % File : Faust---1.0 % Problem : PUZ056-2.005 : TPTP v3.4.2. Released v3.5.0. % Transfm : none % Format : tptp % Command : faust %s % Computer : art02.cs.miami.edu % Model : i686 i686 % CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz % Memory : 1003MB % OS : Linux 2.6.17-1.2142_FC4 % CPULimit : 600s % DateTime : Wed May 6 15:12:51 EDT 2009 % Result : Unsatisfiable 158.1s % Output : Refutation 158.1s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % Proof found in: 158 seconds % START OF PROOF SEQUENCE % cnf(neq3,plain, % % cnf(148190256,derived,(neq(s0,s2)),inference(rewrite,[status(thm)],[neq3]),[]). % % cnf(rule2,plain, % % cnf(148147832,derived,(~p(A,B,C,D,E)|~neq(A,B)|~neq(A,F)|p(A,F,C,D,E)),inference(rewrite,[status(thm)],[rule2]),[]). % % cnf(neq2,plain, % % cnf(148186464,derived,(neq(s0,s1)),inference(rewrite,[status(thm)],[neq2]),[]). % % cnf(156025624,derived,(~p(s0,s1,A,B,C)|~neq(s0,D)|p(s0,D,A,B,C)),inference(resolution,[status(thm)],[148147832,148186464]),[]). % % cnf(rule1,plain, % % cnf(148139216,derived,(~p(A,B,C,D,E)|p(F,B,C,D,E)),inference(rewrite,[status(thm)],[rule1]),[]). % % cnf(goal,plain, % % cnf(148224704,derived,(~p(s2,s2,s2,s2,s2)),inference(rewrite,[status(thm)],[goal]),[]). % % cnf(158214616,derived,(~p(A,s2,s2,s2,s2)),inference(resolution,[status(thm)],[148139216,148224704]),[]). % % cnf(158396440,derived,(~p(s0,s1,s2,s2,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148190256,156025624,158214616]),[]). % % cnf(158450992,derived,(~p(A,s1,s2,s2,s2)),inference(resolution,[status(thm)],[158396440,148139216]),[]). % % cnf(neq4,plain, % % cnf(148194000,derived,(neq(s1,s0)),inference(rewrite,[status(thm)],[neq4]),[]). % % cnf(rule3,plain, % % cnf(148156368,derived,(~p(A,B,C,D,E)|~neq(A,C)|~neq(A,F)|~neq(B,C)|~neq(B,F)|p(A,B,F,D,E)),inference(rewrite,[status(thm)],[rule3]),[]). % % cnf(163843008,derived,(~p(s1,A,s0,B,C)|~neq(s1,D)|~neq(A,s0)|~neq(A,D)|p(s1,A,D,B,C)),inference(resolution,[status(thm)],[148156368,148194000]),[]). % % cnf(neq6,plain, % % cnf(148201344,derived,(neq(s1,s2)),inference(rewrite,[status(thm)],[neq6]),[]). % % cnf(181218016,derived,(~p(s1,s1,s0,A,B)|p(s1,s1,s2,A,B)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148194000,163843008,148201344]),[]). % % cnf(neq7,plain, % % cnf(148205088,derived,(neq(s2,s0)),inference(rewrite,[status(thm)],[neq7]),[]). % % cnf(157720784,derived,(~p(s2,s0,A,B,C)|~neq(s2,D)|p(s2,D,A,B,C)),inference(resolution,[status(thm)],[148147832,148205088]),[]). % % cnf(neq8,plain, % % cnf(148208704,derived,(neq(s2,s1)),inference(rewrite,[status(thm)],[neq8]),[]). % % cnf(160032624,derived,(~p(s2,s0,A,B,C)|p(s2,s1,A,B,C)),inference(resolution,[status(thm)],[157720784,148208704]),[]). % % cnf(rule4,plain, % % cnf(148165032,derived,(~p(A,B,C,D,E)|~neq(A,D)|~neq(A,F)|~neq(B,D)|~neq(B,F)|~neq(C,D)|~neq(C,F)|p(A,B,C,F,E)),inference(rewrite,[status(thm)],[rule4]),[]). % % cnf(156644488,derived,(~p(s0,A,B,C,D)|~neq(s0,C)|~neq(A,C)|~neq(A,s2)|~neq(B,C)|~neq(B,s2)|p(s0,A,B,s2,D)),inference(resolution,[status(thm)],[148165032,148190256]),[]). % % cnf(168496544,derived,(~p(s0,s0,s0,A,B)|~neq(s0,A)|p(s0,s0,s0,s2,B)),inference(resolution,[status(thm)],[156644488,148190256]),[]). % % cnf(157732152,derived,(~p(s2,A,B,C,D)|~neq(s2,A)|p(s2,s0,B,C,D)),inference(resolution,[status(thm)],[148147832,148205088]),[]). % % cnf(163851032,derived,(~p(s1,A,B,C,D)|~neq(s1,B)|~neq(A,B)|~neq(A,s0)|p(s1,A,s0,C,D)),inference(resolution,[status(thm)],[148156368,148194000]),[]). % % cnf(156509408,derived,(~p(s0,A,B,C,D)|~neq(s0,B)|~neq(A,B)|~neq(A,s2)|p(s0,A,s2,C,D)),inference(resolution,[status(thm)],[148156368,148190256]),[]). % % cnf(156599016,derived,(~p(s0,A,s1,B,C)|~neq(A,s1)|~neq(A,s2)|p(s0,A,s2,B,C)),inference(resolution,[status(thm)],[156509408,148186464]),[]). % % cnf(160118656,derived,(p(s2,s1,A,B,C)|~p(D,s0,A,B,C)),inference(resolution,[status(thm)],[160032624,148139216]),[]). % % cnf(160312808,derived,(~p(D,s0,A,B,C)|p(E,s1,A,B,C)),inference(resolution,[status(thm)],[160118656,148139216]),[]). % % cnf(180656328,derived,(~p(s0,s0,s1,A,B)|p(C,s1,s2,A,B)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148190256,148186464,156599016,160312808]),[]). % % cnf(160604400,derived,(~p(s2,s1,A,B,C)|p(s2,s0,A,B,C)),inference(resolution,[status(thm)],[157732152,148208704]),[]). % % cnf(160721224,derived,(p(s2,s0,A,B,C)|~p(D,s1,A,B,C)),inference(resolution,[status(thm)],[160604400,148139216]),[]). % % cnf(160932360,derived,(~p(D,s1,A,B,C)|p(E,s0,A,B,C)),inference(resolution,[status(thm)],[160721224,148139216]),[]). % % cnf(186196280,derived,(p(C,s1,s2,A,B)|~p(D,s1,s1,A,B)),inference(resolution,[status(thm)],[180656328,160932360]),[]). % % cnf(rule5,plain, % % cnf(148173792,derived,(~p(A,B,C,D,E)|~neq(A,E)|~neq(A,F)|~neq(B,E)|~neq(B,F)|~neq(C,E)|~neq(C,F)|~neq(D,E)|~neq(D,F)|p(A,B,C,D,F)),inference(rewrite,[status(thm)],[rule5]),[]). % % cnf(164094696,derived,(~p(s1,A,B,C,s0)|~neq(s1,D)|~neq(A,s0)|~neq(A,D)|~neq(B,s0)|~neq(B,D)|~neq(C,s0)|~neq(C,D)|p(s1,A,B,C,D)),inference(resolution,[status(thm)],[148173792,148194000]),[]). % % cnf(184066968,derived,(~p(s1,s1,s1,s1,s0)|p(s1,s1,s1,s1,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148194000,164094696,148201344]),[]). % % cnf(156086160,derived,(~p(s0,A,B,C,D)|~neq(s0,B)|~neq(A,B)|~neq(A,s1)|p(s0,A,s1,C,D)),inference(resolution,[status(thm)],[148156368,148186464]),[]). % % cnf(160049480,derived,(~neq(s2,D)|p(s2,D,A,B,C)|~p(E,s0,A,B,C)),inference(resolution,[status(thm)],[157720784,148139216]),[]). % % cnf(165046448,derived,(p(s2,s0,A,B,C)|~p(D,s0,A,B,C)),inference(resolution,[status(thm)],[160049480,148205088]),[]). % % cnf(165157816,derived,(~p(D,s0,A,B,C)|p(E,s0,A,B,C)),inference(resolution,[status(thm)],[165046448,148139216]),[]). % % cnf(194576680,derived,(~p(s0,s0,A,B,C)|~neq(s0,A)|p(D,s0,s1,B,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148186464,156086160,165157816]),[]). % % cnf(158268416,derived,(~p(s1,A,B,C,D)|~neq(s1,A)|p(s1,s0,B,C,D)),inference(resolution,[status(thm)],[148147832,148194000]),[]). % % cnf(162919256,derived,(~p(s2,A,B,C,D)|~neq(s2,C)|~neq(A,C)|~neq(A,s1)|~neq(B,C)|~neq(B,s1)|p(s2,A,B,s1,D)),inference(resolution,[status(thm)],[148165032,148208704]),[]). % % cnf(163289824,derived,(~p(s2,s2,s2,A,B)|~neq(s2,A)|p(s2,s2,s2,s1,B)),inference(resolution,[status(thm)],[162919256,148208704]),[]). % % cnf(156456624,derived,(~p(s0,A,B,C,D)|~neq(s0,A)|p(s0,s2,B,C,D)),inference(resolution,[status(thm)],[148147832,148190256]),[]). % % cnf(156467104,derived,(~p(s0,s1,A,B,C)|p(s0,s2,A,B,C)),inference(resolution,[status(thm)],[156456624,148186464]),[]). % % cnf(158485728,derived,(p(s0,s2,A,B,C)|~p(D,s1,A,B,C)),inference(resolution,[status(thm)],[156467104,148139216]),[]). % % cnf(158587056,derived,(~p(D,s1,A,B,C)|p(E,s2,A,B,C)),inference(resolution,[status(thm)],[158485728,148139216]),[]). % % cnf(160077584,derived,(~p(s2,s0,A,B,C)|p(D,s2,A,B,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148208704,157720784,158587056]),[]). % % cnf(160248352,derived,(p(D,s2,A,B,C)|~p(E,s0,A,B,C)),inference(resolution,[status(thm)],[160077584,148139216]),[]). % % cnf(180651832,derived,(~p(s0,s0,s1,A,B)|p(C,s2,s2,A,B)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148190256,148186464,156599016,160248352]),[]). % % cnf(156452696,derived,(~p(s0,s2,A,B,C)|~neq(s0,D)|p(s0,D,A,B,C)),inference(resolution,[status(thm)],[148147832,148190256]),[]). % % cnf(156461616,derived,(~p(s0,s2,A,B,C)|p(s0,s1,A,B,C)),inference(resolution,[status(thm)],[156452696,148186464]),[]). % % cnf(158572376,derived,(~p(s0,s2,A,B,C)|p(D,s1,A,B,C)),inference(resolution,[status(thm)],[156461616,148139216]),[]). % % cnf(160673912,derived,(p(s2,s0,A,B,C)|~p(s0,s2,A,B,C)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148208704,157732152,158572376]),[]). % % cnf(160785608,derived,(~p(s0,s2,A,B,C)|p(D,s0,A,B,C)),inference(resolution,[status(thm)],[160673912,148139216]),[]). % % cnf(185955408,derived,(p(C,s2,s2,A,B)|~p(s0,s2,s1,A,B)),inference(resolution,[status(thm)],[180651832,160785608]),[]). % % cnf(162851672,derived,(~p(s2,A,B,C,D)|~neq(s2,B)|~neq(A,B)|~neq(A,s1)|p(s2,A,s1,C,D)),inference(resolution,[status(thm)],[148156368,148208704]),[]). % % cnf(163031336,derived,(~p(s2,s2,A,B,C)|~neq(s2,A)|p(s2,s2,s1,B,C)),inference(resolution,[status(thm)],[162851672,148208704]),[]). % % cnf(init,plain, % % cnf(148220872,derived,(p(s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[init]),[]). % % cnf(158153088,derived,(p(A,s0,s0,s0,s0)),inference(resolution,[status(thm)],[148139216,148220872]),[]). % % cnf(158335912,derived,(~neq(A,s0)|~neq(A,B)|p(A,B,s0,s0,s0)),inference(resolution,[status(thm)],[148147832,158153088]),[]). % % cnf(158788184,derived,(p(s1,s2,s0,s0,s0)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148194000,158335912,148201344]),[]). % % cnf(158880648,derived,(p(A,s2,s0,s0,s0)),inference(resolution,[status(thm)],[158788184,148139216]),[]). % % cnf(222386984,derived,(p(s2,s2,s1,s0,s0)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148205088,163031336,158880648]),[]). % % cnf(224439832,derived,(p(A,s2,s1,s0,s0)),inference(resolution,[status(thm)],[148139216,222386984]),[]). % % cnf(226123096,derived,(p(A,s2,s2,s0,s0)),inference(resolution,[status(thm)],[185955408,224439832]),[]). % % cnf(229258648,derived,(p(s2,s2,s2,s1,s0)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148205088,163289824,226123096]),[]). % % cnf(232873560,derived,(p(A,s2,s2,s1,s0)),inference(resolution,[status(thm)],[148139216,229258648]),[]). % % cnf(234410352,derived,(p(s1,s0,s2,s1,s0)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148201344,158268416,232873560]),[]). % % cnf(237857152,derived,(p(A,s0,s2,s1,s0)),inference(resolution,[status(thm)],[148139216,234410352]),[]). % % cnf(261751152,derived,(p(A,s0,s1,s1,s0)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148190256,194576680,237857152]),[]). % % cnf(270286920,derived,(p(s2,s1,s1,s1,s0)),inference(resolution,[status(thm)],[160032624,261751152]),[]). % % cnf(274848640,derived,(p(A,s1,s1,s1,s0)),inference(resolution,[status(thm)],[148139216,270286920]),[]). % % cnf(282559808,derived,(p(s1,s1,s1,s1,s2)),inference(resolution,[status(thm)],[184066968,274848640]),[]). % % cnf(294164568,derived,(p(A,s1,s2,s1,s2)),inference(resolution,[status(thm)],[186196280,282559808]),[]). % % cnf(299553872,derived,(p(s1,s1,s0,s1,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148194000,148201344,163851032,294164568]),[]). % % cnf(305915984,derived,(p(A,s1,s0,s1,s2)),inference(resolution,[status(thm)],[148139216,299553872]),[]). % % cnf(316106760,derived,(p(s2,s0,s0,s1,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148208704,157732152,305915984]),[]). % % cnf(325279888,derived,(p(A,s0,s0,s1,s2)),inference(resolution,[status(thm)],[148139216,316106760]),[]). % % cnf(331170032,derived,(p(s0,s0,s0,s2,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[148186464,168496544,325279888]),[]). % % cnf(338351648,derived,(p(A,s0,s0,s2,s2)),inference(resolution,[status(thm)],[148139216,331170032]),[]). % % cnf(347692496,derived,(p(s2,s1,s0,s2,s2)),inference(resolution,[status(thm)],[160032624,338351648]),[]). % % cnf(370261272,derived,(p(A,s1,s0,s2,s2)),inference(resolution,[status(thm)],[148139216,347692496]),[]). % % cnf(383107344,derived,(p(s1,s1,s2,s2,s2)),inference(resolution,[status(thm)],[181218016,370261272]),[]). % % cnf(contradiction,derived,$false,inference(resolution,[status(thm)],[158450992,383107344]),[]). % % END OF PROOF SEQUENCE % %------------------------------------------------------------------------------