%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : PUZ008-1 : TPTP v8.1.0. Released v1.0.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n023.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 18:21:07 EDT 2022 % Result : Unsatisfiable 7.19s 7.17s % Output : Proof 7.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ008-1 : TPTP v8.1.0. Released v1.0.0. % 0.03/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Sun May 29 02:35:57 EDT 2022 % 0.13/0.35 % CPUTime : % 7.19/7.17 % SZS status Unsatisfiable % 7.19/7.17 % SZS output start Proof % 7.19/7.17 The input problem is unsatisfiable because % 7.19/7.17 % 7.19/7.17 [1] the following set of Horn clauses is unsatisfiable: % 7.19/7.17 % 7.19/7.17 achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))) ==> achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))) ==> achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))) ==> achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))) ==> achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))) ==> achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))) ==> achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))) % 7.19/7.17 achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))) ==> achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))) ==> achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))) % 7.19/7.17 achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))) ==> achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))) ==> achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 achievable(west(m(s(X)), c(s(s(X)))), Y, east(Z, W)) % 7.19/7.17 achievable(west(m(s(X)), c(s(s(s(X))))), Y, east(Z, W)) % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(W))))) % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(s(W)))))) % 7.19/7.17 achievable(west(m(s(s(s(n0)))), c(s(s(s(n0))))), boatonwest, east(m(n0), c(n0))) % 7.19/7.17 achievable(west(m(n0), c(n0)), X, east(m(s(s(s(n0)))), c(s(s(s(n0)))))) ==> \bottom % 7.19/7.17 % 7.19/7.17 This holds because % 7.19/7.17 % 7.19/7.17 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 7.19/7.17 % 7.19/7.17 E: % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(W))))) = true__ % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(s(W)))))) = true__ % 7.19/7.17 achievable(west(m(s(X)), c(s(s(X)))), Y, east(Z, W)) = true__ % 7.19/7.17 achievable(west(m(s(X)), c(s(s(s(X))))), Y, east(Z, W)) = true__ % 7.19/7.17 achievable(west(m(s(s(s(n0)))), c(s(s(s(n0))))), boatonwest, east(m(n0), c(n0))) = true__ % 7.19/7.17 f1(achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f1(true__, X, Y, Z, W) = achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))) % 7.19/7.17 f10(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))), X, Y, Z, W) = true__ % 7.19/7.17 f10(true__, X, Y, Z, W) = achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f11(achievable(west(m(n0), c(n0)), X, east(m(s(s(s(n0)))), c(s(s(s(n0))))))) = true__ % 7.19/7.17 f11(true__) = false__ % 7.19/7.17 f2(achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))), X, Y, Z, W) = true__ % 7.19/7.17 f2(true__, X, Y, Z, W) = achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f3(achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f3(true__, X, Y, Z, W) = achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))) % 7.19/7.17 f4(achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))), X, Y, Z, W) = true__ % 7.19/7.17 f4(true__, X, Y, Z, W) = achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f5(achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f5(true__, X, Y, Z, W) = achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))) % 7.19/7.17 f6(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f6(true__, X, Y, Z, W) = achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f7(achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f7(true__, X, Y, Z, W) = achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))) % 7.19/7.17 f8(achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f8(true__, X, Y, Z, W) = achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f9(achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) = true__ % 7.19/7.17 f9(true__, X, Y, Z, W) = achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))) % 7.19/7.17 G: % 7.19/7.17 true__ = false__ % 7.19/7.17 % 7.19/7.17 This holds because % 7.19/7.17 % 7.19/7.17 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 7.19/7.17 % 7.19/7.17 % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(W))))) -> true__ % 7.19/7.17 achievable(west(X, Y), Z, east(m(s(W)), c(s(s(s(W)))))) -> true__ % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))) -> f1(true__, X, Y, Z, W) % 7.19/7.17 achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))) -> f5(true__, X, Y, Z, W) % 7.19/7.17 achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))) -> f2(true__, X, Y, Z, W) % 7.19/7.17 achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))) -> f6(true__, X, Y, Z, W) % 7.19/7.17 achievable(west(m(s(X)), c(s(s(X)))), Y, east(Z, W)) -> true__ % 7.19/7.17 achievable(west(m(s(X)), c(s(s(s(X))))), Y, east(Z, W)) -> true__ % 7.19/7.17 achievable(west(m(s(s(s(n0)))), c(s(s(s(n0))))), boatonwest, east(m(n0), c(n0))) -> true__ % 7.19/7.17 f1(achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) -> true__ % 7.19/7.17 f1(f2(true__, Y0, Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.17 f1(f6(true__, X0, s(Y1), Y2, Y3), s(X0), Y1, Y2, Y3) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(X3), s(X3)) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(X3), s(s(X3))) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(X3), s(s(s(X3)))) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(X3), s(s(s(s(X3))))) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(Y2), X3) -> f5(true__, Y0, Y1, Y2, s(X3)) % 7.19/7.17 f1(true__, Y0, Y1, s(s(X3)), s(s(X3))) -> true__ % 7.19/7.17 f1(true__, Y0, Y1, s(s(X3)), s(s(s(X3)))) -> true__ % 7.19/7.17 f1(true__, Y0, s(Y0), s(Y2), Y3) -> true__ % 7.19/7.17 f1(true__, Y0, s(s(Y0)), s(Y2), Y3) -> true__ % 7.19/7.17 f1(true__, s(X0), Y1, Y2, s(Y2)) -> true__ % 7.19/7.17 f1(true__, s(X0), Y1, Y2, s(s(Y2))) -> true__ % 7.19/7.17 f1(true__, s(X0), s(X0), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(X0), s(X0), Y2, s(Y3)) -> true__ % 7.19/7.17 f1(true__, s(X0), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(X0), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(X0), s(s(s(s(X0)))), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(Y0), Y1, Y2, s(s(s(Y2)))) -> true__ % 7.19/7.17 f1(true__, s(Y0), Y1, Y2, s(s(s(s(Y2))))) -> true__ % 7.19/7.17 f1(true__, s(Y1), Y1, Y2, s(Y3)) -> true__ % 7.19/7.17 f1(true__, s(s(X0)), Y1, Y2, s(s(s(Y2)))) -> true__ % 7.19/7.17 f1(true__, s(s(X0)), Y1, Y2, s(s(s(s(Y2))))) -> true__ % 7.19/7.17 f1(true__, s(s(X0)), Y1, Y2, s(s(s(s(s(Y2)))))) -> true__ % 7.19/7.17 f1(true__, s(s(X0)), s(X0), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(s(Y1)), Y1, Y2, s(Y3)) -> true__ % 7.19/7.17 f1(true__, s(s(n0)), s(s(n0)), s(n0), n0) -> true__ % 7.19/7.17 f1(true__, s(s(s(X0))), s(X0), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(s(s(X0))), s(X0), Y2, s(Y3)) -> true__ % 7.19/7.17 f1(true__, s(s(s(X0))), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.17 f1(true__, s(s(s(Y1))), Y1, Y2, s(Y3)) -> true__ % 7.19/7.17 f1(true__, s(s(s(n0))), s(n0), n0, s(n0)) -> true__ % 7.19/7.17 f1(true__, s(s(s(n0))), s(s(n0)), n0, n0) -> true__ % 7.19/7.17 f10(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))), X, Y, Z, W) -> true__ % 7.19/7.17 f10(f1(true__, Y0, Y1, s(Y2), Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.17 f10(f5(true__, Y0, Y1, Y2, s(Y3)), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.17 f10(true__, X, Y, Z, W) -> achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))) % 7.19/7.17 f11(achievable(west(m(n0), c(n0)), X, east(m(s(s(s(n0)))), c(s(s(s(n0))))))) -> true__ % 7.19/7.17 f11(f1(true__, n0, n0, s(s(s(n0))), s(s(n0)))) -> true__ % 7.19/7.17 f11(f5(true__, n0, n0, s(s(n0)), s(s(s(n0))))) -> true__ % 7.19/7.17 f11(true__) -> false__ % 7.19/7.17 f2(achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))), X, Y, Z, W) -> true__ % 7.19/7.17 f2(f1(true__, Y0, Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.17 f2(f5(true__, Y0, Y1, X2, s(Y3)), Y0, Y1, s(X2), Y3) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(X2), s(s(s(s(X2))))) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(X3), s(X3)) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(X3), s(s(X3))) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(X3), s(s(s(X3)))) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(s(X2)), s(X2)) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(s(s(X2))), s(X2)) -> true__ % 7.19/7.17 f2(true__, Y0, Y1, s(s(s(X2))), s(s(X2))) -> true__ % 7.19/7.17 f2(true__, Y0, s(Y0), s(X1), Y3) -> true__ % 7.19/7.17 f2(true__, Y0, s(Y1), s(X3), s(X3)) -> true__ % 7.19/7.17 f2(true__, Y0, s(Y1), s(Y3), Y3) -> true__ % 7.19/7.17 f2(true__, Y0, s(Y1), s(s(Y3)), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(Y1), s(s(s(X2))), s(X2)) -> true__ % 7.19/7.18 f2(true__, Y0, s(Y1), s(s(s(Y3))), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(Y0)), s(X1), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(s(Y0))), s(Y2), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(s(Y0))), s(s(X1)), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(s(s(Y0)))), s(Y2), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(s(s(Y0)))), s(s(X1)), Y3) -> true__ % 7.19/7.18 f2(true__, Y0, s(s(s(s(s(Y0))))), s(s(X1)), Y3) -> true__ % 7.19/7.18 f2(true__, s(X0), s(X0), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(X0), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(X0), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(X0), s(s(s(s(X0)))), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(Y0), X1, Y2, Y3) -> f6(true__, Y0, s(X1), Y2, Y3) % 7.19/7.18 f2(true__, s(Y0), Y1, Y2, s(Y2)) -> true__ % 7.19/7.18 f2(true__, s(Y0), Y1, Y2, s(s(Y2))) -> true__ % 7.19/7.18 f2(true__, s(s(X0)), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(s(X0)), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.18 f2(true__, s(s(s(n0))), s(s(n0)), n0, n0) -> true__ % 7.19/7.18 f3(achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f3(f2(true__, Y0, s(Y1), Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f3(f6(true__, X0, s(s(Y1)), Y2, Y3), s(X0), Y1, Y2, Y3) -> true__ % 7.19/7.18 f3(true__, X, Y, Z, W) -> achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))) % 7.19/7.18 f4(achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))), X, Y, Z, W) -> true__ % 7.19/7.18 f4(f1(true__, Y0, Y1, Y2, s(Y3)), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f4(f5(true__, Y0, Y1, X2, s(s(Y3))), Y0, Y1, s(X2), Y3) -> true__ % 7.19/7.18 f4(true__, X, Y, Z, W) -> achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))) % 7.19/7.18 f5(achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f5(f2(true__, s(Y0), X1, Y2, Y3), Y0, s(X1), Y2, Y3) -> true__ % 7.19/7.18 f5(f6(true__, Y0, Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, X2, s(s(s(s(X2))))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, X2, s(s(s(s(s(X2)))))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, Y2, s(s(Y2))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, Y2, s(s(s(Y2)))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, s(X3), s(s(X3))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, s(X3), s(s(s(X3)))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, s(s(X3)), s(s(X3))) -> true__ % 7.19/7.18 f5(true__, Y0, Y1, s(s(X3)), s(s(s(X3)))) -> true__ % 7.19/7.18 f5(true__, Y0, s(X1), Y3, s(Y3)) -> true__ % 7.19/7.18 f5(true__, Y0, s(X1), s(Y3), s(Y3)) -> true__ % 7.19/7.18 f5(true__, Y0, s(Y0), Y2, s(Y3)) -> true__ % 7.19/7.18 f5(true__, Y0, s(Y1), s(s(X2)), s(X2)) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(X1)), s(X2), s(X2)) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(X1)), s(Y3), Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(X1)), s(s(X2)), s(X2)) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(X1)), s(s(Y3)), Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(Y0)), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(Y0))), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(Y0))), s(Y2), Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(Y0)))), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(Y0)))), Y2, s(Y3)) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(Y0)))), s(Y2), Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(s(Y0))))), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(s(Y0))))), s(Y2), Y3) -> true__ % 7.19/7.18 f5(true__, Y0, s(s(s(s(s(s(Y0)))))), s(Y2), Y3) -> true__ % 7.19/7.18 f5(true__, s(X0), s(X0), Y2, s(Y3)) -> true__ % 7.19/7.18 f5(true__, s(X0), s(X0), Y2, s(s(X2))) -> true__ % 7.19/7.18 f5(true__, s(X0), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, s(X0), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, s(Y0), Y1, X2, s(s(s(s(X2))))) -> true__ % 7.19/7.18 f5(true__, s(Y0), Y1, X2, s(s(s(s(s(X2)))))) -> true__ % 7.19/7.18 f5(true__, s(Y1), Y1, Y2, s(s(X2))) -> true__ % 7.19/7.18 f5(true__, s(n0), s(s(s(n0))), s(n0), n0) -> true__ % 7.19/7.18 f5(true__, s(s(X0)), s(X0), Y2, s(Y3)) -> true__ % 7.19/7.18 f5(true__, s(s(X0)), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f5(true__, s(s(X0)), s(s(X0)), Y2, s(Y3)) -> true__ % 7.19/7.18 f5(true__, s(s(n0)), s(s(n0)), n0, s(n0)) -> true__ % 7.19/7.18 f5(true__, s(s(n0)), s(s(s(n0))), n0, n0) -> true__ % 7.19/7.18 f6(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f6(f1(true__, Y0, Y1, s(Y2), X3), Y0, Y1, Y2, s(X3)) -> true__ % 7.19/7.18 f6(f5(true__, Y0, Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f6(true__, X0, s(s(s(s(X0)))), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, X0, s(s(s(s(s(X0))))), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, X0, s(s(s(s(s(X0))))), s(Y2), Y3) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, Y2, s(s(Y2))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, Y2, s(s(s(Y2)))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, Y2, s(s(s(s(Y2))))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, Y2, s(s(s(s(s(Y2)))))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, s(X3), s(s(X3))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, s(X3), s(s(s(X3)))) -> true__ % 7.19/7.18 f6(true__, Y0, Y1, s(s(X2)), s(s(X2))) -> true__ % 7.19/7.18 f6(true__, Y0, s(Y1), Y2, s(Y2)) -> true__ % 7.19/7.18 f6(true__, Y0, s(Y1), Y2, s(s(s(s(Y2))))) -> true__ % 7.19/7.18 f6(true__, Y0, s(Y1), s(X2), s(X2)) -> true__ % 7.19/7.18 f6(true__, Y0, s(Y1), s(s(X2)), s(X2)) -> true__ % 7.19/7.18 f6(true__, Y0, s(Y1), s(s(X2)), s(s(X2))) -> true__ % 7.19/7.18 f6(true__, Y0, s(s(X1)), s(X2), s(X2)) -> true__ % 7.19/7.18 f6(true__, Y0, s(s(X1)), s(Y3), Y3) -> true__ % 7.19/7.18 f6(true__, Y0, s(s(Y0)), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, Y0, s(s(s(Y0))), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, Y0, s(s(s(s(Y0)))), s(X1), Y3) -> true__ % 7.19/7.18 f6(true__, Y1, s(Y1), Y2, s(X2)) -> true__ % 7.19/7.18 f6(true__, s(X0), s(X0), Y2, s(s(X2))) -> true__ % 7.19/7.18 f6(true__, s(X0), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, s(X0), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, s(Y0), Y1, Y2, s(s(s(Y2)))) -> true__ % 7.19/7.18 f6(true__, s(Y0), Y1, Y2, s(s(s(s(Y2))))) -> true__ % 7.19/7.18 f6(true__, s(Y0), Y1, Y2, s(s(s(s(s(Y2)))))) -> true__ % 7.19/7.18 f6(true__, s(Y0), Y1, Y2, s(s(s(s(s(s(Y2))))))) -> true__ % 7.19/7.18 f6(true__, s(Y1), Y1, Y2, s(s(X2))) -> true__ % 7.19/7.18 f6(true__, s(Y1), s(Y1), Y2, s(X2)) -> true__ % 7.19/7.18 f6(true__, s(s(X0)), s(X0), Y2, s(Y3)) -> true__ % 7.19/7.18 f6(true__, s(s(X0)), s(X0), Y2, s(s(X2))) -> true__ % 7.19/7.18 f6(true__, s(s(X0)), s(s(X0)), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, s(s(X0)), s(s(s(X0))), Y2, Y3) -> true__ % 7.19/7.18 f6(true__, s(s(Y1)), Y1, Y2, s(s(X2))) -> true__ % 7.19/7.18 f6(true__, s(s(n0)), s(s(s(n0))), n0, n0) -> true__ % 7.19/7.18 f7(achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f7(f2(true__, s(s(Y0)), X1, Y2, Y3), Y0, s(X1), Y2, Y3) -> true__ % 7.19/7.18 f7(f6(true__, s(Y0), Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f7(true__, X, Y, Z, W) -> achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))) % 7.19/7.18 f8(achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f8(f1(true__, Y0, Y1, s(s(Y2)), X3), Y0, Y1, Y2, s(X3)) -> true__ % 7.19/7.18 f8(f5(true__, Y0, Y1, s(Y2), Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f8(true__, X, Y, Z, W) -> achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))) % 7.19/7.18 f9(achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))), X, Y, Z, W) -> true__ % 7.19/7.18 f9(f2(true__, s(Y0), Y1, Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f9(f6(true__, Y0, s(Y1), Y2, Y3), Y0, Y1, Y2, Y3) -> true__ % 7.19/7.18 f9(true__, X, Y, Z, W) -> achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))) % 7.19/7.18 false__ -> true__ % 7.19/7.18 with the LPO induced by % 7.19/7.18 f11 > n0 > f10 > f8 > f9 > f3 > f7 > boatoneast > f4 > achievable > f2 > boatonwest > f1 > f5 > f6 > s > east > c > m > west > false__ > true__ % 7.19/7.18 % 7.19/7.18 % SZS output end Proof % 7.19/7.18 %------------------------------------------------------------------------------