%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : PLA003-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n032.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Mon Jul 18 17:26:26 EDT 2022 % Result : Unsatisfiable 11.71s 11.72s % Output : Proof 11.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : PLA003-1 : TPTP v8.1.0. Released v1.0.0. % 0.02/0.10 % Command : moca.sh %s % 0.10/0.28 % Computer : n032.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 600 % 0.10/0.28 % DateTime : Tue May 31 20:50:44 EDT 2022 % 0.10/0.28 % CPUTime : % 11.71/11.72 % SZS status Unsatisfiable % 11.71/11.72 % SZS output start Proof % 11.71/11.72 The input problem is unsatisfiable because % 11.71/11.72 % 11.71/11.72 [1] the following set of Horn clauses is unsatisfiable: % 11.71/11.72 % 11.71/11.72 can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas) ==> can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas) ==> can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 can(monkey(Location1, floor, the_ladder), ladder(Location1, floor), Bananas) ==> can(monkey(Location2, floor, the_ladder), ladder(Location2, floor), Bananas) % 11.71/11.72 can(monkey(Location1, floor, the_bananas), Ladder, bananas(Location1, floor)) ==> can(monkey(Location2, floor, the_bananas), Ladder, bananas(Location2, floor)) % 11.71/11.72 can(monkey(Location1, floor, nothing), Ladder, Bananas) ==> can(monkey(Location2, floor, nothing), Ladder, Bananas) % 11.71/11.72 can(monkey(Location, Height, the_ladder), ladder(Location, Any_height), Bananas) ==> can(monkey(Location, Height, nothing), ladder(Location, floor), Bananas) % 11.71/11.72 can(monkey(Location, Height, the_bananas), Ladder, bananas(Location, Height)) ==> can(monkey(Location, Height, nothing), Ladder, bananas(Location, floor)) % 11.71/11.72 can(monkey(Location, Height, nothing), Ladder, bananas(Location, Height)) ==> can(monkey(Location, Height, the_bananas), Ladder, bananas(Location, Height)) % 11.71/11.72 can(monkey(Location, Height, nothing), ladder(Location, Height), Bananas) ==> can(monkey(Location, Height, the_ladder), ladder(Location, Height), Bananas) % 11.71/11.72 can(monkey(l0, floor, nothing), ladder(l1, floor), bananas(l2, ceiling)) % 11.71/11.72 can(monkey(Somewhere, Some_height, the_bananas), Ladder, What) ==> \bottom % 11.71/11.72 % 11.71/11.72 This holds because % 11.71/11.72 % 11.71/11.72 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 11.71/11.72 % 11.71/11.72 E: % 11.71/11.72 can(monkey(l0, floor, nothing), ladder(l1, floor), bananas(l2, ceiling)) = true__ % 11.71/11.72 f1(can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas), Location1, Bananas) = true__ % 11.71/11.72 f1(true__, Location1, Bananas) = can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 f10(can(monkey(Somewhere, Some_height, the_bananas), Ladder, What)) = true__ % 11.71/11.72 f10(true__) = false__ % 11.71/11.72 f2(can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas), Location1, Bananas) = true__ % 11.71/11.72 f2(true__, Location1, Bananas) = can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 f3(can(monkey(Location1, floor, the_ladder), ladder(Location1, floor), Bananas), Location2, Bananas) = true__ % 11.71/11.72 f3(true__, Location2, Bananas) = can(monkey(Location2, floor, the_ladder), ladder(Location2, floor), Bananas) % 11.71/11.72 f4(can(monkey(Location1, floor, the_bananas), Ladder, bananas(Location1, floor)), Location2, Ladder) = true__ % 11.71/11.72 f4(true__, Location2, Ladder) = can(monkey(Location2, floor, the_bananas), Ladder, bananas(Location2, floor)) % 11.71/11.72 f5(can(monkey(Location1, floor, nothing), Ladder, Bananas), Location2, Ladder, Bananas) = true__ % 11.71/11.72 f5(true__, Location2, Ladder, Bananas) = can(monkey(Location2, floor, nothing), Ladder, Bananas) % 11.71/11.72 f6(can(monkey(Location, Height, the_ladder), ladder(Location, Any_height), Bananas), Location, Height, Bananas) = true__ % 11.71/11.72 f6(true__, Location, Height, Bananas) = can(monkey(Location, Height, nothing), ladder(Location, floor), Bananas) % 11.71/11.72 f7(can(monkey(Location, Height, the_bananas), Ladder, bananas(Location, Height)), Location, Height, Ladder) = true__ % 11.71/11.72 f7(true__, Location, Height, Ladder) = can(monkey(Location, Height, nothing), Ladder, bananas(Location, floor)) % 11.71/11.72 f8(can(monkey(Location, Height, nothing), Ladder, bananas(Location, Height)), Location, Height, Ladder) = true__ % 11.71/11.72 f8(true__, Location, Height, Ladder) = can(monkey(Location, Height, the_bananas), Ladder, bananas(Location, Height)) % 11.71/11.72 f9(can(monkey(Location, Height, nothing), ladder(Location, Height), Bananas), Location, Height, Bananas) = true__ % 11.71/11.72 f9(true__, Location, Height, Bananas) = can(monkey(Location, Height, the_ladder), ladder(Location, Height), Bananas) % 11.71/11.72 G: % 11.71/11.72 true__ = false__ % 11.71/11.72 % 11.71/11.72 This holds because % 11.71/11.72 % 11.71/11.72 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 11.71/11.72 % 11.71/11.72 % 11.71/11.72 can(monkey(Location, Height, the_bananas), Ladder, bananas(Location, Height)) -> f8(true__, Location, Height, Ladder) % 11.71/11.72 can(monkey(Location, Height, the_ladder), ladder(Location, Height), Bananas) -> f9(true__, Location, Height, Bananas) % 11.71/11.72 can(monkey(Y0, ceiling, nothing), ladder(Y0, floor), bananas(l2, ceiling)) -> true__ % 11.71/11.72 can(monkey(Y3, floor, nothing), ladder(Y0, floor), bananas(l2, ceiling)) -> true__ % 11.71/11.72 can(monkey(l2, ceiling, nothing), ladder(l2, floor), bananas(l2, floor)) -> true__ % 11.71/11.72 f1(can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas), Location1, Bananas) -> true__ % 11.71/11.72 f1(true__, Location1, Bananas) -> can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 f10(can(monkey(Somewhere, Some_height, the_bananas), Ladder, What)) -> true__ % 11.71/11.72 f10(f8(true__, Y0, Y1, Y2)) -> true__ % 11.71/11.72 f10(true__) -> false__ % 11.71/11.72 f2(can(monkey(Location1, ceiling, nothing), ladder(Location1, floor), Bananas), Location1, Bananas) -> true__ % 11.71/11.72 f2(true__, Location1, Bananas) -> can(monkey(Location1, floor, nothing), ladder(Location1, floor), Bananas) % 11.71/11.72 f3(f9(true__, Y0, floor, Y1), Y2, Y1) -> true__ % 11.71/11.72 f3(true__, Location2, Bananas) -> f9(true__, Location2, floor, Bananas) % 11.71/11.72 f4(f8(true__, Y0, floor, Y1), Y2, Y1) -> true__ % 11.71/11.72 f4(true__, Location2, Ladder) -> f8(true__, Location2, floor, Ladder) % 11.71/11.72 f5(can(monkey(Location1, floor, nothing), Ladder, Bananas), Location2, Ladder, Bananas) -> true__ % 11.71/11.72 f5(true__, Location2, Ladder, Bananas) -> can(monkey(Location2, floor, nothing), Ladder, Bananas) % 11.71/11.72 f6(can(monkey(Location, Height, the_ladder), ladder(Location, Any_height), Bananas), Location, Height, Bananas) -> true__ % 11.71/11.72 f6(f9(true__, Y0, Y2, Y3), Y0, Y2, Y3) -> true__ % 11.71/11.72 f6(true__, Location, Height, Bananas) -> can(monkey(Location, Height, nothing), ladder(Location, floor), Bananas) % 11.71/11.72 f7(f8(true__, Y0, Y1, Y2), Y0, Y1, Y2) -> true__ % 11.71/11.72 f7(true__, Location, Height, Ladder) -> can(monkey(Location, Height, nothing), Ladder, bananas(Location, floor)) % 11.71/11.72 f8(can(monkey(Location, Height, nothing), Ladder, bananas(Location, Height)), Location, Height, Ladder) -> true__ % 11.71/11.72 f8(true__, l2, ceiling, ladder(l2, floor)) -> true__ % 11.71/11.72 f9(can(monkey(Location, Height, nothing), ladder(Location, Height), Bananas), Location, Height, Bananas) -> true__ % 11.71/11.72 f9(true__, Y2, floor, bananas(l2, ceiling)) -> true__ % 11.71/11.72 false__ -> true__ % 11.71/11.72 with the LPO induced by % 11.71/11.72 f4 > f1 > f7 > f6 > f2 > f5 > f3 > can > ladder > f8 > l2 > f9 > the_ladder > l0 > the_bananas > nothing > floor > f10 > ceiling > monkey > bananas > l1 > false__ > true__ % 11.71/11.72 % 11.71/11.72 % SZS output end Proof % 11.71/11.72 %------------------------------------------------------------------------------