%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : PUZ008-3 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:30:44 PM UTC 2026
% Result : Unsatisfiable 0.48s 0.49s
% Output : Proof 6.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : PUZ008-3 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.03 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n011.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Sun Sep 27 22:29:15 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.48/0.49 Command-line arguments: --no-flatten-goal
% 0.48/0.49
% 0.48/0.49 % SZS status Unsatisfiable
% 0.48/0.49
% 3.90/1.00 % SZS output start Proof
% 3.90/1.00 Axiom 1 (great_eq_base): greater_or_equal(X, n0) = true.
% 3.90/1.00 Axiom 2 (no_missionaries_is_safe): safe(n0, X) = true.
% 3.90/1.00 Axiom 3 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 3.90/1.00 Axiom 4 (great_eq_recursive): ifeq(greater_or_equal(X, Y), true, greater_or_equal(s(X), s(Y)), true) = true.
% 3.90/1.00 Axiom 5 (same_or_more_missionaries_is_safe): ifeq(greater_or_equal(X, Y), true, safe(X, Y), true) = true.
% 3.90/1.00 Axiom 6 (start_on_west_bank): achievable(west(m(s(s(s(n0)))), c(s(s(s(n0))))), boatonwest, east(m(n0), c(n0))) = true.
% 3.90/1.00 Axiom 7 (cannibal_east_to_west): ifeq(achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(W)))), true, ifeq(safe(Z, W), true, ifeq(safe(X, s(Y)), true, achievable(west(m(X), c(s(Y))), boatonwest, east(m(Z), c(W))), true), true), true) = true.
% 3.90/1.00 Axiom 8 (missionary_east_to_west): ifeq(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(W))), true, ifeq(safe(s(X), Y), true, ifeq(safe(Z, W), true, achievable(west(m(s(X)), c(Y)), boatonwest, east(m(Z), c(W))), true), true), true) = true.
% 3.90/1.00 Axiom 9 (missionary_and_cannibal_east_to_west): ifeq(achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))), true, ifeq(safe(s(X), s(Y)), true, ifeq(safe(Z, W), true, achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))), true), true), true) = true.
% 3.90/1.00 Axiom 10 (two_cannibals_west_to_east): ifeq(achievable(west(m(X), c(s(s(Y)))), boatonwest, east(m(Z), c(W))), true, ifeq(safe(Z, s(s(W))), true, ifeq(safe(X, Y), true, achievable(west(m(X), c(Y)), boatoneast, east(m(Z), c(s(s(W))))), true), true), true) = true.
% 3.90/1.00 Axiom 11 (missionary_and_cannibal_west_to_east): ifeq(achievable(west(m(s(X)), c(s(Y))), boatonwest, east(m(Z), c(W))), true, ifeq(safe(s(Z), s(W)), true, ifeq(safe(X, Y), true, achievable(west(m(X), c(Y)), boatoneast, east(m(s(Z)), c(s(W)))), true), true), true) = true.
% 3.90/1.01 Axiom 12 (two_missionaries_west_to_east): ifeq(achievable(west(m(s(s(X))), c(Y)), boatonwest, east(m(Z), c(W))), true, ifeq(safe(s(s(Z)), W), true, ifeq(safe(X, Y), true, achievable(west(m(X), c(Y)), boatoneast, east(m(s(s(Z))), c(W))), true), true), true) = true.
% 3.90/1.01
% 3.90/1.01 Goal 1 (prove_can_get_to_east_bank): achievable(west(m(n0), c(n0)), X, east(m(s(s(s(n0)))), c(s(s(s(n0)))))) = true.
% 3.90/1.01 The goal is true when:
% 3.90/1.01 X = boatoneast
% 3.90/1.02
% 3.90/1.02 Proof:
% 3.90/1.02 achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0))))))
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(true, true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true)
% 3.90/1.02 = { by axiom 2 (no_missionaries_is_safe) R->L }
% 3.90/1.02 ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(true, true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 3.90/1.02 ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 4 (great_eq_recursive) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 1 (great_eq_base) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 4 (great_eq_recursive) }
% 3.90/1.02 ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) }
% 3.90/1.02 ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(s(n0))), true, greater_or_equal(s(s(s(n0))), s(s(s(n0)))), true), true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 4 (great_eq_recursive) }
% 3.90/1.02 ifeq(ifeq(true, true, safe(s(s(s(n0))), s(s(s(n0)))), true), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) }
% 3.90/1.02 ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(true, true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.02 = { by axiom 8 (missionary_east_to_west) R->L }
% 3.90/1.02 ifeq(ifeq(achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(true, true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.02 = { by axiom 2 (no_missionaries_is_safe) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.02 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.02 ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(s(n0))), true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 4 (great_eq_recursive) R->L }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), n0), true, greater_or_equal(s(s(n0)), s(n0)), true), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 1 (great_eq_base) }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(n0)), true), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 3 (ifeq_axiom) }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(n0)), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 4 (great_eq_recursive) }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), s(s(n0))), true), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 3 (ifeq_axiom) }
% 3.90/1.03 ifeq(ifeq(ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.03 ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.03 = { by axiom 7 (cannibal_east_to_west) R->L }
% 3.90/1.03 ifeq(ifeq(ifeq(ifeq(achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 2 (no_missionaries_is_safe) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(n0)), true, safe(s(s(s(n0))), s(n0)), true), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 1 (great_eq_base) R->L }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), n0), true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 4 (great_eq_recursive) }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), s(n0)), true), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.04 = { by axiom 3 (ifeq_axiom) }
% 3.90/1.04 ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.05 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.05 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.05 = { by axiom 9 (missionary_and_cannibal_east_to_west) R->L }
% 3.90/1.05 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 3.90/1.05 = { by axiom 3 (ifeq_axiom) R->L }
% 3.90/1.05 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.05 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 5.05/1.05 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.06 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.06 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.06 = { by axiom 1 (great_eq_base) R->L }
% 5.05/1.06 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.06 = { by axiom 4 (great_eq_recursive) }
% 5.05/1.06 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.06 = { by axiom 3 (ifeq_axiom) }
% 5.05/1.06 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.06 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.07 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.07 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 5.05/1.07 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(s(n0))), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.07 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.07 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.07 = { by axiom 4 (great_eq_recursive) R->L }
% 5.05/1.07 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.08 = { by axiom 1 (great_eq_base) }
% 5.05/1.08 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.08 = { by axiom 3 (ifeq_axiom) }
% 5.05/1.08 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.08 = { by axiom 4 (great_eq_recursive) }
% 5.05/1.08 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.08 = { by axiom 3 (ifeq_axiom) }
% 5.05/1.08 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.09 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.09 = { by axiom 7 (cannibal_east_to_west) R->L }
% 5.05/1.09 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.09 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.10 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 5.05/1.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), n0), true, safe(s(s(s(n0))), n0), true), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.10 = { by axiom 1 (great_eq_base) }
% 5.05/1.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), n0), true), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.10 = { by axiom 3 (ifeq_axiom) }
% 5.05/1.10 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.11 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.11 = { by axiom 2 (no_missionaries_is_safe) R->L }
% 5.05/1.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.11 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.11 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.11 = { by axiom 7 (cannibal_east_to_west) R->L }
% 5.05/1.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.12 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.12 = { by axiom 5 (same_or_more_missionaries_is_safe) R->L }
% 5.05/1.12 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(n0)), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.13 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.13 = { by axiom 1 (great_eq_base) R->L }
% 5.05/1.13 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), n0), true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.13 = { by axiom 4 (great_eq_recursive) }
% 5.05/1.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.14 = { by axiom 3 (ifeq_axiom) }
% 5.05/1.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.14 = { by axiom 3 (ifeq_axiom) R->L }
% 5.05/1.14 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.05/1.15 = { by axiom 2 (no_missionaries_is_safe) R->L }
% 5.05/1.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.15 = { by axiom 3 (ifeq_axiom) R->L }
% 5.81/1.15 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.15 = { by axiom 6 (start_on_west_bank) R->L }
% 5.81/1.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(s(n0)))), c(s(s(s(n0))))), boatonwest, east(m(n0), c(n0))), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatoneast, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.16 = { by axiom 10 (two_cannibals_west_to_east) }
% 5.81/1.16 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.17 = { by axiom 3 (ifeq_axiom) }
% 5.81/1.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(n0, s(n0)), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.17 = { by axiom 2 (no_missionaries_is_safe) }
% 5.81/1.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.17 = { by axiom 3 (ifeq_axiom) }
% 5.81/1.17 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), s(s(n0))), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.18 = { by axiom 3 (ifeq_axiom) R->L }
% 5.81/1.18 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.18 = { by axiom 4 (great_eq_recursive) R->L }
% 5.81/1.18 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(n0)), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.18 = { by axiom 3 (ifeq_axiom) R->L }
% 5.81/1.19 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(n0)), true), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.19 = { by axiom 1 (great_eq_base) R->L }
% 5.81/1.19 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), n0), true, greater_or_equal(s(s(n0)), s(n0)), true), true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.19 = { by axiom 4 (great_eq_recursive) }
% 5.81/1.19 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(s(n0))), true), true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.19 = { by axiom 3 (ifeq_axiom) }
% 5.81/1.20 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(s(n0))), true, safe(s(s(s(n0))), s(s(n0))), true), true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.20 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 5.81/1.20 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 5.81/1.20 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.20 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(s(n0)))), c(s(s(n0)))), boatonwest, east(m(n0), c(s(n0)))), true, ifeq(safe(n0, s(s(s(n0)))), true, ifeq(safe(s(s(s(n0))), n0), true, achievable(west(m(s(s(s(n0)))), c(n0)), boatoneast, east(m(n0), c(s(s(s(n0)))))), true), true), true), true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.20 = { by axiom 10 (two_cannibals_west_to_east) }
% 6.23/1.21 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.21 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.21 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(n0, s(s(n0))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.21 = { by axiom 2 (no_missionaries_is_safe) }
% 6.23/1.21 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.21 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.21 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), s(n0)), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.21 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.22 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.22 = { by axiom 4 (great_eq_recursive) R->L }
% 6.23/1.22 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), n0), true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.22 = { by axiom 1 (great_eq_base) }
% 6.23/1.22 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(s(n0))), s(n0)), true), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.22 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.22 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), s(n0)), true, safe(s(s(s(n0))), s(n0)), true), true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.22 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.22 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.23 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.23 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(s(n0)))), c(s(n0))), boatonwest, east(m(n0), c(s(s(n0))))), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(n0)), c(s(n0))), boatoneast, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.23 = { by axiom 12 (two_missionaries_west_to_east) }
% 6.23/1.23 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.23 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.23 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(s(n0)), s(s(n0))), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 4 (great_eq_recursive) R->L }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 1 (great_eq_base) R->L }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 4 (great_eq_recursive) }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(s(n0))), true, safe(s(s(n0)), s(s(n0))), true), true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.24 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.24 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(safe(s(n0), s(n0)), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 4 (great_eq_recursive) R->L }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 1 (great_eq_base) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, safe(s(n0), s(n0)), true), true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(ifeq(achievable(west(m(s(s(n0))), c(s(s(n0)))), boatonwest, east(m(s(n0)), c(s(n0)))), true, ifeq(safe(s(s(s(n0))), s(n0)), true, ifeq(safe(n0, s(s(n0))), true, achievable(west(m(n0), c(s(s(n0)))), boatoneast, east(m(s(s(s(n0)))), c(s(n0)))), true), true), true), true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.25 = { by axiom 12 (two_missionaries_west_to_east) }
% 6.23/1.25 ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(safe(s(s(s(n0))), n0), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, safe(s(s(s(n0))), n0), true), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 1 (great_eq_base) R->L }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(s(s(n0))), n0), true, safe(s(s(s(n0))), n0), true), true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(true, true, ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(safe(n0, s(s(s(n0)))), true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 2 (no_missionaries_is_safe) }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(true, true, achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.26 ifeq(ifeq(ifeq(achievable(west(m(n0), c(s(s(s(n0))))), boatonwest, east(m(s(s(s(n0)))), c(n0))), true, ifeq(safe(s(s(s(n0))), s(s(n0))), true, ifeq(safe(n0, s(n0)), true, achievable(west(m(n0), c(s(n0))), boatoneast, east(m(s(s(s(n0)))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 10 (two_cannibals_west_to_east) }
% 6.23/1.26 ifeq(ifeq(true, true, ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.26 ifeq(ifeq(safe(s(n0), s(n0)), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.26 ifeq(ifeq(ifeq(true, true, safe(s(n0), s(n0)), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 4 (great_eq_recursive) R->L }
% 6.23/1.26 ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.26 = { by axiom 1 (great_eq_base) }
% 6.23/1.27 ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, safe(s(n0), s(n0)), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.27 ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, safe(s(n0), s(n0)), true), true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.27 ifeq(ifeq(true, true, ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.27 ifeq(ifeq(safe(s(s(n0)), s(s(n0))), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.27 ifeq(ifeq(ifeq(true, true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 4 (great_eq_recursive) R->L }
% 6.23/1.27 ifeq(ifeq(ifeq(ifeq(greater_or_equal(s(n0), s(n0)), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) R->L }
% 6.23/1.27 ifeq(ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 1 (great_eq_base) R->L }
% 6.23/1.27 ifeq(ifeq(ifeq(ifeq(ifeq(greater_or_equal(n0, n0), true, greater_or_equal(s(n0), s(n0)), true), true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 4 (great_eq_recursive) }
% 6.23/1.27 ifeq(ifeq(ifeq(ifeq(true, true, greater_or_equal(s(s(n0)), s(s(n0))), true), true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.27 ifeq(ifeq(ifeq(greater_or_equal(s(s(n0)), s(s(n0))), true, safe(s(s(n0)), s(s(n0))), true), true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 5 (same_or_more_missionaries_is_safe) }
% 6.23/1.27 ifeq(ifeq(true, true, achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 3 (ifeq_axiom) }
% 6.23/1.27 ifeq(achievable(west(m(s(n0)), c(s(n0))), boatonwest, east(m(s(s(n0))), c(s(s(n0))))), true, ifeq(safe(s(s(s(n0))), s(s(s(n0)))), true, ifeq(safe(n0, n0), true, achievable(west(m(n0), c(n0)), boatoneast, east(m(s(s(s(n0)))), c(s(s(s(n0)))))), true), true), true)
% 6.23/1.27 = { by axiom 11 (missionary_and_cannibal_west_to_east) }
% 6.23/1.27 true
% 6.23/1.27 % SZS output end Proof
% 6.23/1.27
% 6.23/1.27 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------