%------------------------------------------------------------------------------ % File : Faust---1.0 % Problem : MSC015-1.005 : TPTP v3.4.2. Released v3.5.0. % Transfm : none % Format : tptp % Command : faust %s % Computer : art04.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 14:19:28 EDT 2009 % Result : Unsatisfiable 0.1s % Output : Refutation 0.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: 0 seconds % START OF PROOF SEQUENCE % cnf(rule4,plain, % % cnf(150698376,derived,(~p(A,s0,s1,s1,s1)|p(A,s1,s0,s0,s0)),inference(rewrite,[status(thm)],[rule4]),[]). % % cnf(rule3,plain, % % cnf(150688768,derived,(~p(A,B,s0,s1,s1)|p(A,B,s1,s0,s0)),inference(rewrite,[status(thm)],[rule3]),[]). % % cnf(rule2,plain, % % cnf(150683232,derived,(~p(A,B,C,s0,s1)|p(A,B,C,s1,s0)),inference(rewrite,[status(thm)],[rule2]),[]). % % cnf(rule1,plain, % % cnf(150677344,derived,(~p(A,B,C,D,s0)|p(A,B,C,D,s1)),inference(rewrite,[status(thm)],[rule1]),[]). % % cnf(init,plain, % % cnf(150670976,derived,(p(s0,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[init]),[]). % % cnf(158451160,derived,(p(s0,s0,s0,s0,s1)),inference(resolution,[status(thm)],[150677344,150670976]),[]). % % cnf(158479024,derived,(p(s0,s0,s0,s1,s0)),inference(resolution,[status(thm)],[150683232,158451160]),[]). % % cnf(158556184,derived,(p(s0,s0,s0,s1,s1)),inference(resolution,[status(thm)],[158479024,150677344]),[]). % % cnf(158600136,derived,(p(s0,s0,s1,s0,s0)),inference(resolution,[status(thm)],[150688768,158556184]),[]). % % cnf(158661232,derived,(p(s0,s0,s1,s0,s1)),inference(resolution,[status(thm)],[158600136,150677344]),[]). % % cnf(158677744,derived,(p(s0,s0,s1,s1,s0)),inference(resolution,[status(thm)],[158661232,150683232]),[]). % % cnf(158691120,derived,(p(s0,s0,s1,s1,s1)),inference(resolution,[status(thm)],[158677744,150677344]),[]). % % cnf(158799696,derived,(p(s0,s1,s0,s0,s0)),inference(resolution,[status(thm)],[150698376,158691120]),[]). % % cnf(158866240,derived,(p(s0,s1,s0,s0,s1)),inference(resolution,[status(thm)],[158799696,150677344]),[]). % % cnf(158886768,derived,(p(s0,s1,s0,s1,s0)),inference(resolution,[status(thm)],[158866240,150683232]),[]). % % cnf(158904080,derived,(p(s0,s1,s0,s1,s1)),inference(resolution,[status(thm)],[158886768,150677344]),[]). % % cnf(158925424,derived,(p(s0,s1,s1,s0,s0)),inference(resolution,[status(thm)],[158904080,150688768]),[]). % % cnf(158942792,derived,(p(s0,s1,s1,s0,s1)),inference(resolution,[status(thm)],[158925424,150677344]),[]). % % cnf(158965720,derived,(p(s0,s1,s1,s1,s0)),inference(resolution,[status(thm)],[158942792,150683232]),[]). % % cnf(158982224,derived,(p(s0,s1,s1,s1,s1)),inference(resolution,[status(thm)],[158965720,150677344]),[]). % % cnf(rule5,plain, % % cnf(150703928,derived,(~p(s0,s1,s1,s1,s1)|p(s1,s0,s0,s0,s0)),inference(rewrite,[status(thm)],[rule5]),[]). % % cnf(goal,plain, % % cnf(150707688,derived,(~p(s1,s1,s1,s1,s1)),inference(rewrite,[status(thm)],[goal]),[]). % % cnf(158498352,derived,(~p(s1,s1,s1,s1,s0)),inference(resolution,[status(thm)],[150677344,150707688]),[]). % % cnf(158517520,derived,(~p(s1,s1,s1,s0,s1)),inference(resolution,[status(thm)],[150683232,158498352]),[]). % % cnf(158576920,derived,(~p(s1,s1,s1,s0,s0)),inference(resolution,[status(thm)],[158517520,150677344]),[]). % % cnf(158619144,derived,(~p(s1,s1,s0,s1,s1)),inference(resolution,[status(thm)],[150688768,158576920]),[]). % % cnf(158718224,derived,(~p(s1,s1,s0,s1,s0)),inference(resolution,[status(thm)],[158619144,150677344]),[]). % % cnf(158742088,derived,(~p(s1,s1,s0,s0,s1)),inference(resolution,[status(thm)],[158718224,150683232]),[]). % % cnf(158766816,derived,(~p(s1,s1,s0,s0,s0)),inference(resolution,[status(thm)],[158742088,150677344]),[]). % % cnf(158820312,derived,(~p(s1,s0,s1,s1,s1)),inference(resolution,[status(thm)],[150698376,158766816]),[]). % % cnf(159020456,derived,(~p(s1,s0,s1,s1,s0)),inference(resolution,[status(thm)],[158820312,150677344]),[]). % % cnf(159051520,derived,(~p(s1,s0,s1,s0,s1)),inference(resolution,[status(thm)],[159020456,150683232]),[]). % % cnf(159083448,derived,(~p(s1,s0,s1,s0,s0)),inference(resolution,[status(thm)],[159051520,150677344]),[]). % % cnf(159119408,derived,(~p(s1,s0,s0,s1,s1)),inference(resolution,[status(thm)],[159083448,150688768]),[]). % % cnf(159146440,derived,(~p(s1,s0,s0,s1,s0)),inference(resolution,[status(thm)],[159119408,150677344]),[]). % % cnf(159179976,derived,(~p(s1,s0,s0,s0,s1)),inference(resolution,[status(thm)],[159146440,150683232]),[]). % % cnf(159202928,derived,(~p(s1,s0,s0,s0,s0)),inference(resolution,[status(thm)],[159179976,150677344]),[]). % % cnf(contradiction,derived,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[158982224,150703928,159202928]),[]). % % END OF PROOF SEQUENCE % %------------------------------------------------------------------------------