%------------------------------------------------------------------------------ % File : Faust---1.0 % Problem : PLA031-1.001 : TPTP v3.4.2. Released v3.5.0. % Transfm : none % Format : tptp % Command : faust %s % Computer : art03.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:08:36 EDT 2009 % Result : Unsatisfiable 117.9s % Output : Refutation 117.9s % 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: 117 seconds % START OF PROOF SEQUENCE % cnf(walk2,plain, % % cnf(167487176,derived,(~s(A,B,C,D,E,F)|~path(D,G)|s(A,B,C,G,E,F)),inference(rewrite,[status(thm)],[walk2]),[]). % % cnf(map10,plain, % % cnf(167791760,derived,(path(p2_1,s2)),inference(rewrite,[status(thm)],[map10]),[]). % % cnf(181208376,derived,(~s(A,B,C,p2_1,D,E)|s(A,B,C,s2,D,E)),inference(resolution,[status(thm)],[167487176,167791760]),[]). % % cnf(map11,plain, % % cnf(167795312,derived,(path(s1,p2_1)),inference(rewrite,[status(thm)],[map11]),[]). % % cnf(181221664,derived,(~s(A,B,C,s1,D,E)|s(A,B,C,p2_1,D,E)),inference(resolution,[status(thm)],[167487176,167795312]),[]). % % cnf(drive2,plain, % % cnf(167445776,derived,(~s(A,B,truck2,C,D,E)|~link(E,F)|s(A,B,truck2,C,D,F)),inference(rewrite,[status(thm)],[drive2]),[]). % % cnf(map16,plain, % % cnf(167818920,derived,(link(s2,s0)),inference(rewrite,[status(thm)],[map16]),[]). % % cnf(180298432,derived,(~s(A,B,truck2,C,D,s2)|s(A,B,truck2,C,D,s0)),inference(resolution,[status(thm)],[167445776,167818920]),[]). % % cnf(neq26,plain, % % cnf(167597896,derived,(neq(s1,truck2)),inference(rewrite,[status(thm)],[neq26]),[]). % % cnf(board3,plain, % % cnf(167383712,derived,(~s(A,B,C,D,E,C)|~neq(D,truck2)|s(A,B,truck2,D,E,C)),inference(rewrite,[status(thm)],[board3]),[]). % % cnf(walk1,plain, % % cnf(167478480,derived,(~s(A,B,C,D,E,F)|~path(C,G)|s(A,B,G,D,E,F)),inference(rewrite,[status(thm)],[walk1]),[]). % % cnf(map6,plain, % % cnf(167776976,derived,(path(p2_0,s2)),inference(rewrite,[status(thm)],[map6]),[]). % % cnf(181057928,derived,(~s(A,B,p2_0,C,D,E)|s(A,B,s2,C,D,E)),inference(resolution,[status(thm)],[167478480,167776976]),[]). % % cnf(map7,plain, % % cnf(167780528,derived,(path(s0,p2_0)),inference(rewrite,[status(thm)],[map7]),[]). % % cnf(181072704,derived,(~s(A,B,s0,C,D,E)|s(A,B,p2_0,C,D,E)),inference(resolution,[status(thm)],[167478480,167780528]),[]). % % cnf(init,plain, % % cnf(167829904,derived,(s(s2,s2,s0,s1,s0,s2)),inference(rewrite,[status(thm)],[init]),[]). % % cnf(181513512,derived,(s(s2,s2,p2_0,s1,s0,s2)),inference(resolution,[status(thm)],[181072704,167829904]),[]). % % cnf(182515848,derived,(s(s2,s2,s2,s1,s0,s2)),inference(resolution,[status(thm)],[181057928,181513512]),[]). % % cnf(189160640,derived,(s(s2,s2,truck2,s1,s0,s2)),inference(forward_subsumption_resolution__resolution,[status(thm)],[167597896,167383712,182515848]),[]). % % cnf(201189504,derived,(s(s2,s2,truck2,s1,s0,s0)),inference(resolution,[status(thm)],[180298432,189160640]),[]). % % cnf(221042368,derived,(s(s2,s2,truck2,p2_1,s0,s0)),inference(resolution,[status(thm)],[181221664,201189504]),[]). % % cnf(260948000,derived,(s(s2,s2,truck2,s2,s0,s0)),inference(resolution,[status(thm)],[181208376,221042368]),[]). % % cnf(drive1,plain, % % cnf(167438000,derived,(~s(A,B,truck1,C,D,E)|~link(D,F)|s(A,B,truck1,C,F,E)),inference(rewrite,[status(thm)],[drive1]),[]). % % cnf(map15,plain, % % cnf(167815144,derived,(link(s0,s2)),inference(rewrite,[status(thm)],[map15]),[]). % % cnf(181284176,derived,(~s(A,B,truck1,C,s0,D)|s(A,B,truck1,C,s2,D)),inference(resolution,[status(thm)],[167438000,167815144]),[]). % % cnf(board2,plain, % % cnf(167368336,derived,(s(A,B,C,D,C,E)|~s(A,B,truck1,D,C,E)),inference(rewrite,[status(thm)],[board2]),[]). % % cnf(goal,plain, % % cnf(167838040,derived,(~s(s2,s1,s2,s2,s2,s0)),inference(rewrite,[status(thm)],[goal]),[]). % % cnf(176185584,derived,(~s(s2,s1,truck1,s2,s2,s0)),inference(resolution,[status(thm)],[167368336,167838040]),[]). % % cnf(417532832,derived,(~s(s2,s1,truck1,s2,s0,s0)),inference(resolution,[status(thm)],[181284176,176185584]),[]). % % cnf(map14,plain, % % cnf(167811592,derived,(link(s1,s0)),inference(rewrite,[status(thm)],[map14]),[]). % % cnf(181244888,derived,(~s(A,B,truck1,C,s1,D)|s(A,B,truck1,C,s0,D)),inference(resolution,[status(thm)],[167438000,167811592]),[]). % % cnf(423662896,derived,(~s(s2,s1,truck1,s2,s1,s0)),inference(resolution,[status(thm)],[417532832,181244888]),[]). % % cnf(load6,plain, % % cnf(167317936,derived,(s(A,B,C,D,B,E)|~s(A,truck1,C,D,B,E)),inference(rewrite,[status(thm)],[load6]),[]). % % cnf(425572296,derived,(~s(s2,truck1,truck1,s2,s1,s0)),inference(resolution,[status(thm)],[423662896,167317936]),[]). % % cnf(map18,plain, % % cnf(167826280,derived,(link(s2,s1)),inference(rewrite,[status(thm)],[map18]),[]). % % cnf(180237784,derived,(~s(A,B,truck1,C,s2,D)|s(A,B,truck1,C,s1,D)),inference(resolution,[status(thm)],[167438000,167826280]),[]). % % cnf(430085016,derived,(~s(s2,truck1,truck1,s2,s2,s0)),inference(resolution,[status(thm)],[425572296,180237784]),[]). % % cnf(load5,plain, % % cnf(167308304,derived,(~s(A,B,C,D,B,E)|s(A,truck1,C,D,B,E)),inference(rewrite,[status(thm)],[load5]),[]). % % cnf(439833312,derived,(~s(s2,s2,truck1,s2,s2,s0)),inference(resolution,[status(thm)],[430085016,167308304]),[]). % % cnf(452605800,derived,(~s(s2,s2,truck1,s2,s0,s0)),inference(resolution,[status(thm)],[439833312,181284176]),[]). % % cnf(board1,plain, % % cnf(167362296,derived,(~s(A,B,C,D,C,E)|~neq(D,truck1)|s(A,B,truck1,D,C,E)),inference(rewrite,[status(thm)],[board1]),[]). % % cnf(neq33,plain, % % cnf(167627824,derived,(neq(s2,truck1)),inference(rewrite,[status(thm)],[neq33]),[]). % % cnf(180349920,derived,(~s(A,B,C,s2,C,D)|s(A,B,truck1,s2,C,D)),inference(resolution,[status(thm)],[167362296,167627824]),[]). % % cnf(473556256,derived,(~s(s2,s2,s0,s2,s0,s0)),inference(resolution,[status(thm)],[452605800,180349920]),[]). % % cnf(board4,plain, % % cnf(167393400,derived,(s(A,B,C,D,E,C)|~s(A,B,truck2,D,E,C)),inference(rewrite,[status(thm)],[board4]),[]). % % cnf(contradiction,derived,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[260948000,473556256,167393400]),[]). % % END OF PROOF SEQUENCE % %------------------------------------------------------------------------------