%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : SWX187-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n008.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 01:45:31 PM UTC 2026
% Result : Unsatisfiable 62.35s 8.23s
% Output : Proof 63.72s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX187-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.18 % Computer : n008.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 15:07:24 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 62.35/8.23 Command-line arguments: --lhs-weight 1 --flip-ordering --normalise-queue-percent 10 --cp-renormalise-threshold 10 --complete-subsets --ground-joining-incomplete-limit 15 --flatten-every 2
% 62.35/8.23
% 62.35/8.23 % SZS status Unsatisfiable
% 62.35/8.23
% 62.35/8.28 % SZS output start Proof
% 62.35/8.28 Axiom 1 (axiom_001): notb(bfalse) = btrue.
% 62.35/8.28 Axiom 2 (axiom_021): eq(X, X) = btrue.
% 62.35/8.28 Axiom 3 (axiom_022): eq2(X, X) = btrue.
% 62.35/8.28 Axiom 4 (axiom_020): eq2(z, s(X)) = bfalse.
% 62.35/8.28 Axiom 5 (axiom_004): impl(btrue, X) = X.
% 62.35/8.28 Axiom 6 (axiom_008): x2(z, s(X)) = btrue.
% 62.35/8.28 Axiom 7 (axiom_006): x2(s(X), s(Y)) = x2(X, Y).
% 62.35/8.28 Axiom 8 (axiom_014): rotate(z, X) = X.
% 62.35/8.28 Axiom 9 (axiom_023): eq3(X, X) = btrue.
% 62.35/8.28 Axiom 10 (axiom_010): x(nil, X) = X.
% 62.35/8.28 Axiom 11 (axiom_003): length(cons(X, Y)) = s(length(Y)).
% 62.35/8.28 Axiom 12 (axiom_011): x(cons(X, Y), Z) = cons(X, x(Y, Z)).
% 62.35/8.28 Axiom 13 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 62.35/8.28 Axiom 14 (axiom_013): rotate(s(X), cons(Y, Z)) = rotate(X, x(Z, cons(Y, nil))).
% 62.35/8.28 Axiom 15 (axiom_024): ifeq(eq2(X, Y), bfalse, eq(cons(X, Z), cons(Y, W)), bfalse) = bfalse.
% 62.35/8.28 Axiom 16 (axiom_025): ifeq(eq2(X, Y), btrue, eq(cons(X, Z), cons(Y, W)), eq(Z, W)) = eq(Z, W).
% 62.35/8.28 Axiom 17 (axiom_015): prop_rot_inj0(X, Y, Z, W) = impl(eq3(x2(X, length(W)), btrue), impl(eq3(x2(Y, length(Z)), btrue), impl(eq(W, Z), impl(notb(eq(rotate(s(z), W), W)), impl(eq(rotate(X, W), rotate(Y, Z)), eq2(X, Y)))))).
% 62.35/8.28
% 62.35/8.28 Lemma 18: x(X, cons(Y, nil)) = rotate(s(z), cons(Y, X)).
% 62.35/8.28 Proof:
% 62.35/8.28 x(X, cons(Y, nil))
% 62.35/8.28 = { by axiom 8 (axiom_014) R->L }
% 62.35/8.28 rotate(z, x(X, cons(Y, nil)))
% 63.72/8.28 = { by axiom 14 (axiom_013) R->L }
% 63.72/8.28 rotate(s(z), cons(Y, X))
% 63.72/8.28
% 63.72/8.28 Lemma 19: rotate(s(X), cons(Y, nil)) = rotate(X, cons(Y, nil)).
% 63.72/8.28 Proof:
% 63.72/8.28 rotate(s(X), cons(Y, nil))
% 63.72/8.28 = { by axiom 14 (axiom_013) }
% 63.72/8.28 rotate(X, x(nil, cons(Y, nil)))
% 63.72/8.28 = { by axiom 10 (axiom_010) }
% 63.72/8.28 rotate(X, cons(Y, nil))
% 63.72/8.28
% 63.72/8.28 Lemma 20: rotate(s(z), cons(X, cons(Y, Z))) = cons(Y, rotate(s(z), cons(X, Z))).
% 63.72/8.28 Proof:
% 63.72/8.28 rotate(s(z), cons(X, cons(Y, Z)))
% 63.72/8.28 = { by lemma 18 R->L }
% 63.72/8.28 x(cons(Y, Z), cons(X, nil))
% 63.72/8.28 = { by axiom 12 (axiom_011) }
% 63.72/8.28 cons(Y, x(Z, cons(X, nil)))
% 63.72/8.29 = { by lemma 18 }
% 63.72/8.29 cons(Y, rotate(s(z), cons(X, Z)))
% 63.72/8.29
% 63.72/8.29 Lemma 21: rotate(X, cons(Y, rotate(s(z), cons(Z, W)))) = rotate(s(X), cons(Z, cons(Y, W))).
% 63.72/8.29 Proof:
% 63.72/8.29 rotate(X, cons(Y, rotate(s(z), cons(Z, W))))
% 63.72/8.29 = { by lemma 18 R->L }
% 63.72/8.29 rotate(X, cons(Y, x(W, cons(Z, nil))))
% 63.72/8.29 = { by axiom 12 (axiom_011) R->L }
% 63.72/8.29 rotate(X, x(cons(Y, W), cons(Z, nil)))
% 63.72/8.29 = { by axiom 14 (axiom_013) R->L }
% 63.72/8.29 rotate(s(X), cons(Z, cons(Y, W)))
% 63.72/8.29
% 63.72/8.29 Goal 1 (goal): eq3(prop_rot_inj0(X, Y, Z, W), bfalse) = btrue.
% 63.72/8.29 The goal is true when:
% 63.72/8.29 X = z
% 63.72/8.29 Y = s(s(z))
% 63.72/8.29 Z = cons(s(X), cons(z, cons(s(X), cons(z, nil))))
% 63.72/8.29 W = cons(s(X), cons(z, cons(s(X), cons(z, nil))))
% 63.72/8.29
% 63.72/8.29 Proof:
% 63.72/8.29 eq3(prop_rot_inj0(z, s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), bfalse)
% 63.72/8.29 = { by axiom 17 (axiom_015) }
% 63.72/8.29 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), impl(notb(eq(rotate(s(z), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(rotate(z, cons(s(X), cons(z, cons(s(X), cons(z, nil))))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), eq2(z, s(s(z)))))))), bfalse)
% 63.72/8.29 = { by axiom 2 (axiom_021) }
% 63.72/8.29 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(btrue, impl(notb(eq(rotate(s(z), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(rotate(z, cons(s(X), cons(z, cons(s(X), cons(z, nil))))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), eq2(z, s(s(z)))))))), bfalse)
% 63.72/8.29 = { by axiom 5 (axiom_004) }
% 63.72/8.29 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(rotate(s(z), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(rotate(z, cons(s(X), cons(z, cons(s(X), cons(z, nil))))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), eq2(z, s(s(z))))))), bfalse)
% 63.72/8.29 = { by axiom 4 (axiom_020) }
% 63.72/8.30 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(rotate(s(z), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(rotate(z, cons(s(X), cons(z, cons(s(X), cons(z, nil))))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 8 (axiom_014) }
% 63.72/8.30 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(rotate(s(z), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by lemma 20 }
% 63.72/8.30 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 11 (axiom_003) }
% 63.72/8.30 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 11 (axiom_003) }
% 63.72/8.30 eq3(impl(eq3(x2(z, s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(eq3(x2(s(s(z)), s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 6 (axiom_008) }
% 63.72/8.30 eq3(impl(eq3(btrue, btrue), impl(eq3(x2(s(s(z)), s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 9 (axiom_023) }
% 63.72/8.30 eq3(impl(btrue, impl(eq3(x2(s(s(z)), s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)))), bfalse)
% 63.72/8.30 = { by axiom 5 (axiom_004) }
% 63.72/8.31 eq3(impl(eq3(x2(s(s(z)), s(length(cons(z, cons(s(X), cons(z, nil)))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 7 (axiom_006) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), length(cons(z, cons(s(X), cons(z, nil))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 11 (axiom_003) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(notb(eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 13 (ifeq_axiom) R->L }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(notb(ifeq(bfalse, bfalse, eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), bfalse)), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 4 (axiom_020) R->L }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(notb(ifeq(eq2(z, s(X)), bfalse, eq(cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))), cons(s(X), cons(z, cons(s(X), cons(z, nil))))), bfalse)), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 15 (axiom_024) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(notb(bfalse), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 1 (axiom_001) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(btrue, impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse))), bfalse)
% 63.72/8.31 = { by axiom 5 (axiom_004) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(s(z)), cons(s(X), cons(z, cons(s(X), cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.31 = { by lemma 21 R->L }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(z), cons(z, rotate(s(z), cons(s(X), cons(s(X), cons(z, nil))))))), bfalse)), bfalse)
% 63.72/8.31 = { by lemma 20 }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(s(z), cons(z, cons(s(X), rotate(s(z), cons(s(X), cons(z, nil))))))), bfalse)), bfalse)
% 63.72/8.31 = { by lemma 21 R->L }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(z, cons(s(X), rotate(s(z), cons(z, rotate(s(z), cons(s(X), cons(z, nil)))))))), bfalse)), bfalse)
% 63.72/8.31 = { by lemma 21 }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), rotate(z, cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil))))))), bfalse)), bfalse)
% 63.72/8.31 = { by axiom 8 (axiom_014) }
% 63.72/8.31 eq3(impl(eq3(x2(s(z), s(length(cons(s(X), cons(z, nil))))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.31 = { by axiom 7 (axiom_006) }
% 63.72/8.31 eq3(impl(eq3(x2(z, length(cons(s(X), cons(z, nil)))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.31 = { by axiom 11 (axiom_003) }
% 63.72/8.31 eq3(impl(eq3(x2(z, s(length(cons(z, nil)))), btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.31 = { by axiom 6 (axiom_008) }
% 63.72/8.32 eq3(impl(eq3(btrue, btrue), impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.32 = { by axiom 9 (axiom_023) }
% 63.72/8.32 eq3(impl(btrue, impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse)), bfalse)
% 63.72/8.32 = { by axiom 5 (axiom_004) }
% 63.72/8.32 eq3(impl(eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 13 (ifeq_axiom) R->L }
% 63.72/8.32 eq3(impl(ifeq(btrue, btrue, eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 3 (axiom_022) R->L }
% 63.72/8.32 eq3(impl(ifeq(eq2(s(X), s(X)), btrue, eq(cons(s(X), cons(z, cons(s(X), cons(z, nil)))), cons(s(X), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil)))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 16 (axiom_025) }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(s(z)), cons(s(X), cons(z, cons(z, nil))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 21 R->L }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(z), cons(z, rotate(s(z), cons(s(X), cons(z, nil)))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 21 R->L }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(z), cons(z, rotate(z, cons(z, rotate(s(z), cons(s(X), nil))))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 19 }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(z), cons(z, rotate(z, cons(z, rotate(z, cons(s(X), nil))))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 8 (axiom_014) }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(z), cons(z, rotate(z, cons(z, cons(s(X), nil)))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 8 (axiom_014) }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), rotate(s(z), cons(z, cons(z, cons(s(X), nil))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 20 }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), cons(z, rotate(s(z), cons(z, cons(s(X), nil))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 20 }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), cons(z, cons(s(X), rotate(s(z), cons(z, nil))))), bfalse), bfalse)
% 63.72/8.32 = { by lemma 19 }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), cons(z, cons(s(X), rotate(z, cons(z, nil))))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 8 (axiom_014) }
% 63.72/8.32 eq3(impl(eq(cons(z, cons(s(X), cons(z, nil))), cons(z, cons(s(X), cons(z, nil)))), bfalse), bfalse)
% 63.72/8.32 = { by axiom 2 (axiom_021) }
% 63.72/8.32 eq3(impl(btrue, bfalse), bfalse)
% 63.72/8.32 = { by axiom 5 (axiom_004) }
% 63.72/8.32 eq3(bfalse, bfalse)
% 63.72/8.32 = { by axiom 9 (axiom_023) }
% 63.72/8.32 btrue
% 63.72/8.32 % SZS output end Proof
% 63.72/8.32
% 63.72/8.32 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------