%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.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 09:35:26 AM UTC 2026
% Result : Unsatisfiable 181.57s 23.28s
% Output : Proof 183.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : BOO020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.24 % Computer : n018.cluster.edu
% 0.10/0.24 % Model : x86_64 x86_64
% 0.10/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.24 % Memory : 8046.5625MB
% 0.10/0.24 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Mon Sep 28 21:06:40 UTC 2026
% 0.10/0.25 % CPUTime :
% 0.10/0.25 Running run_twee /export/starexec/sandbox2/benchmark/theBenchmark.p
% 181.57/23.28 Command-line arguments: --flatten --complete-subsets
% 181.57/23.28
% 181.57/23.28 % SZS status Unsatisfiable
% 181.57/23.28
% 182.35/23.39 % SZS output start Proof
% 182.35/23.39 Axiom 1 (frink1): add(X, X) = X.
% 182.35/23.39 Axiom 2 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 182.35/23.39 Axiom 3 (frink2): ifeq(add(add(add(X, Y), Z), W), add(add(Y, Z), X), add(add(add(X, Y), Z), inverse(W)), n0) = n0.
% 182.35/23.39 Axiom 4 (frink3): ifeq(add(add(add(X, Y), Z), inverse(W)), n0, add(add(add(X, Y), Z), W), add(add(Y, Z), X)) = add(add(Y, Z), X).
% 182.35/23.39
% 182.35/23.39 Lemma 5: add(add(X, Y), inverse(X)) = n0.
% 182.35/23.39 Proof:
% 182.35/23.39 add(add(X, Y), inverse(X))
% 182.35/23.39 = { by axiom 2 (ifeq_axiom) R->L }
% 182.35/23.39 ifeq(add(add(X, Y), X), add(add(X, Y), X), add(add(X, Y), inverse(X)), n0)
% 182.35/23.39 = { by axiom 1 (frink1) R->L }
% 182.35/23.39 ifeq(add(add(X, Y), X), add(add(X, Y), X), add(add(add(X, X), Y), inverse(X)), n0)
% 182.35/23.39 = { by axiom 1 (frink1) R->L }
% 182.35/23.39 ifeq(add(add(add(X, X), Y), X), add(add(X, Y), X), add(add(add(X, X), Y), inverse(X)), n0)
% 182.35/23.39 = { by axiom 3 (frink2) }
% 182.35/23.39 n0
% 182.35/23.39
% 182.35/23.39 Lemma 6: add(X, inverse(X)) = n0.
% 182.35/23.39 Proof:
% 182.35/23.39 add(X, inverse(X))
% 182.35/23.39 = { by axiom 1 (frink1) R->L }
% 182.35/23.39 add(add(X, X), inverse(X))
% 182.35/23.39 = { by lemma 5 }
% 182.35/23.39 n0
% 182.35/23.39
% 182.35/23.39 Lemma 7: add(add(X, Y), Z) = add(add(Z, X), Y).
% 182.35/23.39 Proof:
% 182.35/23.39 add(add(X, Y), Z)
% 182.35/23.39 = { by axiom 4 (frink3) R->L }
% 182.35/23.39 ifeq(add(add(add(Z, X), Y), inverse(add(add(Z, X), Y))), n0, add(add(add(Z, X), Y), add(add(Z, X), Y)), add(add(X, Y), Z))
% 182.35/23.39 = { by lemma 6 }
% 182.35/23.39 ifeq(n0, n0, add(add(add(Z, X), Y), add(add(Z, X), Y)), add(add(X, Y), Z))
% 182.35/23.39 = { by axiom 2 (ifeq_axiom) }
% 182.35/23.39 add(add(add(Z, X), Y), add(add(Z, X), Y))
% 182.35/23.39 = { by axiom 1 (frink1) }
% 182.35/23.39 add(add(Z, X), Y)
% 182.35/23.39
% 182.35/23.39 Lemma 8: add(n0, inverse(X)) = n0.
% 182.35/23.39 Proof:
% 182.35/23.39 add(n0, inverse(X))
% 182.35/23.39 = { by lemma 6 R->L }
% 182.35/23.39 add(add(X, inverse(X)), inverse(X))
% 182.35/23.39 = { by lemma 5 }
% 182.35/23.39 n0
% 182.35/23.39
% 182.35/23.39 Lemma 9: add(n0, Y) = add(n0, X).
% 182.35/23.39 Proof:
% 182.35/23.39 add(n0, Y)
% 182.35/23.39 = { by lemma 5 R->L }
% 182.35/23.39 add(add(add(Z, W), inverse(Z)), Y)
% 182.35/23.39 = { by axiom 2 (ifeq_axiom) R->L }
% 182.35/23.39 ifeq(n0, n0, add(add(add(Z, W), inverse(Z)), Y), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by lemma 8 R->L }
% 182.35/23.39 ifeq(add(n0, inverse(Y)), n0, add(add(add(Z, W), inverse(Z)), Y), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by lemma 5 R->L }
% 182.35/23.39 ifeq(add(add(add(Z, W), inverse(Z)), inverse(Y)), n0, add(add(add(Z, W), inverse(Z)), Y), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by axiom 4 (frink3) }
% 182.35/23.39 add(add(W, inverse(Z)), Z)
% 182.35/23.39 = { by axiom 4 (frink3) R->L }
% 182.35/23.39 ifeq(add(add(add(Z, W), inverse(Z)), inverse(X)), n0, add(add(add(Z, W), inverse(Z)), X), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by lemma 5 }
% 182.35/23.39 ifeq(add(n0, inverse(X)), n0, add(add(add(Z, W), inverse(Z)), X), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by lemma 8 }
% 182.35/23.39 ifeq(n0, n0, add(add(add(Z, W), inverse(Z)), X), add(add(W, inverse(Z)), Z))
% 182.35/23.39 = { by axiom 2 (ifeq_axiom) }
% 182.35/23.39 add(add(add(Z, W), inverse(Z)), X)
% 182.35/23.39 = { by lemma 5 }
% 182.35/23.39 add(n0, X)
% 182.35/23.39
% 182.35/23.39 Lemma 10: add(n0, X) = n0.
% 182.35/23.40 Proof:
% 182.35/23.40 add(n0, X)
% 182.35/23.40 = { by lemma 9 }
% 182.35/23.40 add(n0, n0)
% 182.35/23.40 = { by axiom 1 (frink1) }
% 182.35/23.40 n0
% 182.35/23.40
% 182.35/23.40 Lemma 11: add(X, n0) = n0.
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, n0)
% 182.35/23.40 = { by axiom 1 (frink1) R->L }
% 182.35/23.40 add(add(X, n0), add(X, n0))
% 182.35/23.40 = { by lemma 7 R->L }
% 182.35/23.40 add(add(n0, add(X, n0)), X)
% 182.35/23.40 = { by lemma 10 }
% 182.35/23.40 add(n0, X)
% 182.35/23.40 = { by lemma 9 R->L }
% 182.35/23.40 add(n0, Y)
% 182.35/23.40 = { by lemma 10 }
% 182.35/23.40 n0
% 182.35/23.40
% 182.35/23.40 Lemma 12: add(add(X, Y), Y) = add(Y, X).
% 182.35/23.40 Proof:
% 182.35/23.40 add(add(X, Y), Y)
% 182.35/23.40 = { by lemma 7 R->L }
% 182.35/23.40 add(add(Y, Y), X)
% 182.35/23.40 = { by axiom 1 (frink1) }
% 182.35/23.40 add(Y, X)
% 182.35/23.40
% 182.35/23.40 Lemma 13: add(add(X, Y), X) = add(X, Y).
% 182.35/23.40 Proof:
% 182.35/23.40 add(add(X, Y), X)
% 182.35/23.40 = { by lemma 7 }
% 182.35/23.40 add(add(X, X), Y)
% 182.35/23.40 = { by axiom 1 (frink1) }
% 182.35/23.40 add(X, Y)
% 182.35/23.40
% 182.35/23.40 Lemma 14: add(X, add(Y, X)) = add(X, Y).
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, add(Y, X))
% 182.35/23.40 = { by lemma 12 R->L }
% 182.35/23.40 add(add(add(Y, X), X), X)
% 182.35/23.40 = { by lemma 12 }
% 182.35/23.40 add(add(X, Y), X)
% 182.35/23.40 = { by lemma 13 }
% 182.35/23.40 add(X, Y)
% 182.35/23.40
% 182.35/23.40 Lemma 15: add(add(X, Y), Z) = add(Y, add(Z, X)).
% 182.35/23.40 Proof:
% 182.35/23.40 add(add(X, Y), Z)
% 182.35/23.40 = { by axiom 4 (frink3) R->L }
% 182.35/23.40 ifeq(add(add(add(Z, X), Y), inverse(Y)), n0, add(add(add(Z, X), Y), Y), add(add(X, Y), Z))
% 182.35/23.40 = { by lemma 7 R->L }
% 182.35/23.40 ifeq(add(add(Y, inverse(Y)), add(Z, X)), n0, add(add(add(Z, X), Y), Y), add(add(X, Y), Z))
% 182.35/23.40 = { by lemma 6 }
% 182.35/23.40 ifeq(add(n0, add(Z, X)), n0, add(add(add(Z, X), Y), Y), add(add(X, Y), Z))
% 182.35/23.40 = { by lemma 10 }
% 182.35/23.40 ifeq(n0, n0, add(add(add(Z, X), Y), Y), add(add(X, Y), Z))
% 182.35/23.40 = { by axiom 2 (ifeq_axiom) }
% 182.35/23.40 add(add(add(Z, X), Y), Y)
% 182.35/23.40 = { by lemma 12 }
% 182.35/23.40 add(Y, add(Z, X))
% 182.35/23.40
% 182.35/23.40 Lemma 16: add(Y, X) = add(X, Y).
% 182.35/23.40 Proof:
% 182.35/23.40 add(Y, X)
% 182.35/23.40 = { by lemma 14 R->L }
% 182.35/23.40 add(Y, add(X, Y))
% 182.35/23.40 = { by lemma 13 R->L }
% 182.35/23.40 add(Y, add(add(X, Y), X))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 add(add(X, Y), add(X, Y))
% 182.35/23.40 = { by axiom 1 (frink1) }
% 182.35/23.40 add(X, Y)
% 182.35/23.40
% 182.35/23.40 Lemma 17: add(Y, add(X, Z)) = add(X, add(Y, Z)).
% 182.35/23.40 Proof:
% 182.35/23.40 add(Y, add(X, Z))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 add(add(Z, Y), X)
% 182.35/23.40 = { by axiom 1 (frink1) R->L }
% 182.35/23.40 add(add(add(Z, Y), X), add(add(Z, Y), X))
% 182.35/23.40 = { by axiom 2 (ifeq_axiom) R->L }
% 182.35/23.40 ifeq(n0, n0, add(add(add(Z, Y), X), add(add(Z, Y), X)), add(add(Y, X), Z))
% 182.35/23.40 = { by lemma 6 R->L }
% 182.35/23.40 ifeq(add(add(add(Z, Y), X), inverse(add(add(Z, Y), X))), n0, add(add(add(Z, Y), X), add(add(Z, Y), X)), add(add(Y, X), Z))
% 182.35/23.40 = { by axiom 4 (frink3) }
% 182.35/23.40 add(add(Y, X), Z)
% 182.35/23.40 = { by lemma 15 }
% 182.35/23.40 add(X, add(Z, Y))
% 182.35/23.40 = { by lemma 16 R->L }
% 182.35/23.40 add(X, add(Y, Z))
% 182.35/23.40
% 182.35/23.40 Lemma 18: add(X, add(Y, inverse(X))) = n0.
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, add(Y, inverse(X)))
% 182.35/23.40 = { by lemma 16 }
% 182.35/23.40 add(X, add(inverse(X), Y))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 add(add(Y, X), inverse(X))
% 182.35/23.40 = { by lemma 7 R->L }
% 182.35/23.40 add(add(X, inverse(X)), Y)
% 182.35/23.40 = { by lemma 6 }
% 182.35/23.40 add(n0, Y)
% 182.35/23.40 = { by lemma 9 R->L }
% 182.35/23.40 add(n0, Z)
% 182.35/23.40 = { by lemma 10 }
% 182.35/23.40 n0
% 182.35/23.40
% 182.35/23.40 Lemma 19: ifeq(add(X, add(inverse(Y), add(Z, W))), n0, add(X, add(Y, add(Z, W))), add(X, add(Z, W))) = add(X, add(Z, W)).
% 182.35/23.40 Proof:
% 182.35/23.40 ifeq(add(X, add(inverse(Y), add(Z, W))), n0, add(X, add(Y, add(Z, W))), add(X, add(Z, W)))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 ifeq(add(X, add(inverse(Y), add(Z, W))), n0, add(X, add(Y, add(Z, W))), add(add(W, X), Z))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 ifeq(add(X, add(inverse(Y), add(Z, W))), n0, add(add(add(Z, W), X), Y), add(add(W, X), Z))
% 182.35/23.40 = { by lemma 15 R->L }
% 182.35/23.40 ifeq(add(add(add(Z, W), X), inverse(Y)), n0, add(add(add(Z, W), X), Y), add(add(W, X), Z))
% 182.35/23.40 = { by axiom 4 (frink3) }
% 182.35/23.40 add(add(W, X), Z)
% 182.35/23.40 = { by lemma 15 }
% 182.35/23.40 add(X, add(Z, W))
% 182.35/23.40
% 182.35/23.40 Lemma 20: add(X, add(Y, add(Z, inverse(inverse(X))))) = add(Y, add(Z, inverse(inverse(X)))).
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, add(Y, add(Z, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 17 }
% 182.35/23.40 add(X, add(Z, add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 17 }
% 182.35/23.40 add(Z, add(X, add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by axiom 2 (ifeq_axiom) R->L }
% 182.35/23.40 ifeq(n0, n0, add(Z, add(X, add(Y, inverse(inverse(X))))), add(Z, add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 11 R->L }
% 182.35/23.40 ifeq(add(Z, n0), n0, add(Z, add(X, add(Y, inverse(inverse(X))))), add(Z, add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 18 R->L }
% 182.35/23.40 ifeq(add(Z, add(inverse(X), add(Y, inverse(inverse(X))))), n0, add(Z, add(X, add(Y, inverse(inverse(X))))), add(Z, add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 19 }
% 182.35/23.40 add(Z, add(Y, inverse(inverse(X))))
% 182.35/23.40 = { by lemma 17 R->L }
% 182.35/23.40 add(Y, add(Z, inverse(inverse(X))))
% 182.35/23.40
% 182.35/23.40 Lemma 21: add(add(X, Y), Z) = add(X, add(Z, Y)).
% 182.35/23.40 Proof:
% 182.35/23.40 add(add(X, Y), Z)
% 182.35/23.40 = { by lemma 16 }
% 182.35/23.40 add(Z, add(X, Y))
% 182.35/23.40 = { by lemma 17 R->L }
% 182.35/23.40 add(X, add(Z, Y))
% 182.35/23.40
% 182.35/23.40 Lemma 22: add(X, add(Y, inverse(inverse(X)))) = add(Y, inverse(inverse(X))).
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, add(Y, inverse(inverse(X))))
% 182.35/23.40 = { by axiom 1 (frink1) R->L }
% 182.35/23.40 add(X, add(add(Y, inverse(inverse(X))), add(Y, inverse(inverse(X)))))
% 182.35/23.40 = { by lemma 20 }
% 182.35/23.40 add(add(Y, inverse(inverse(X))), add(Y, inverse(inverse(X))))
% 182.35/23.40 = { by lemma 21 }
% 182.35/23.40 add(Y, add(add(Y, inverse(inverse(X))), inverse(inverse(X))))
% 182.35/23.40 = { by lemma 12 }
% 182.35/23.40 add(Y, add(inverse(inverse(X)), Y))
% 182.35/23.40 = { by lemma 14 }
% 182.35/23.40 add(Y, inverse(inverse(X)))
% 182.35/23.40
% 182.35/23.40 Lemma 23: add(X, inverse(inverse(X))) = inverse(inverse(X)).
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, inverse(inverse(X)))
% 182.35/23.40 = { by axiom 1 (frink1) R->L }
% 182.35/23.40 add(X, add(inverse(inverse(X)), inverse(inverse(X))))
% 182.35/23.40 = { by lemma 22 }
% 182.35/23.40 add(inverse(inverse(X)), inverse(inverse(X)))
% 182.35/23.40 = { by axiom 1 (frink1) }
% 182.35/23.40 inverse(inverse(X))
% 182.35/23.40
% 182.35/23.40 Lemma 24: add(X, add(inverse(inverse(X)), Y)) = add(Y, inverse(inverse(X))).
% 182.35/23.40 Proof:
% 182.35/23.40 add(X, add(inverse(inverse(X)), Y))
% 182.35/23.40 = { by lemma 16 }
% 182.35/23.40 add(X, add(Y, inverse(inverse(X))))
% 182.35/23.40 = { by lemma 22 }
% 183.16/23.40 add(Y, inverse(inverse(X)))
% 183.16/23.40
% 183.16/23.40 Lemma 25: add(X, add(Y, inverse(inverse(Z)))) = add(X, add(Y, Z)).
% 183.16/23.40 Proof:
% 183.16/23.40 add(X, add(Y, inverse(inverse(Z))))
% 183.16/23.40 = { by lemma 17 }
% 183.16/23.40 add(Y, add(X, inverse(inverse(Z))))
% 183.16/23.40 = { by lemma 16 }
% 183.16/23.40 add(Y, add(inverse(inverse(Z)), X))
% 183.16/23.40 = { by lemma 21 R->L }
% 183.16/23.40 add(add(Y, X), inverse(inverse(Z)))
% 183.16/23.40 = { by lemma 24 R->L }
% 183.16/23.40 add(Z, add(inverse(inverse(Z)), add(Y, X)))
% 183.16/23.40 = { by axiom 2 (ifeq_axiom) R->L }
% 183.16/23.40 ifeq(n0, n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 11 R->L }
% 183.16/23.40 ifeq(add(add(Y, X), n0), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 18 R->L }
% 183.16/23.40 ifeq(add(add(Y, X), add(Z, add(inverse(inverse(inverse(Z))), inverse(Z)))), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 16 R->L }
% 183.16/23.40 ifeq(add(add(Y, X), add(Z, add(inverse(Z), inverse(inverse(inverse(Z)))))), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 23 }
% 183.16/23.40 ifeq(add(add(Y, X), add(Z, inverse(inverse(inverse(Z))))), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 17 R->L }
% 183.16/23.40 ifeq(add(Z, add(add(Y, X), inverse(inverse(inverse(Z))))), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 16 R->L }
% 183.16/23.40 ifeq(add(Z, add(inverse(inverse(inverse(Z))), add(Y, X))), n0, add(Z, add(inverse(inverse(Z)), add(Y, X))), add(Z, add(Y, X)))
% 183.16/23.40 = { by lemma 19 }
% 183.16/23.40 add(Z, add(Y, X))
% 183.16/23.40 = { by lemma 17 R->L }
% 183.16/23.40 add(Y, add(Z, X))
% 183.16/23.40 = { by lemma 16 R->L }
% 183.16/23.40 add(Y, add(X, Z))
% 183.16/23.40 = { by lemma 17 R->L }
% 183.16/23.40 add(X, add(Y, Z))
% 183.16/23.40
% 183.16/23.40 Lemma 26: inverse(inverse(X)) = X.
% 183.16/23.40 Proof:
% 183.16/23.40 inverse(inverse(X))
% 183.16/23.40 = { by lemma 23 R->L }
% 183.16/23.40 add(X, inverse(inverse(X)))
% 183.16/23.40 = { by axiom 1 (frink1) R->L }
% 183.16/23.41 add(add(X, inverse(inverse(X))), add(X, inverse(inverse(X))))
% 183.16/23.41 = { by lemma 25 }
% 183.16/23.41 add(add(X, inverse(inverse(X))), add(X, X))
% 183.16/23.41 = { by lemma 21 }
% 183.16/23.41 add(X, add(add(X, X), inverse(inverse(X))))
% 183.16/23.41 = { by lemma 25 }
% 183.16/23.41 add(X, add(add(X, X), X))
% 183.16/23.41 = { by lemma 12 }
% 183.16/23.41 add(X, add(X, X))
% 183.16/23.41 = { by lemma 14 }
% 183.16/23.41 add(X, X)
% 183.16/23.41 = { by axiom 1 (frink1) }
% 183.16/23.41 X
% 183.16/23.41
% 183.16/23.41 Lemma 27: add(Y, add(Z, X)) = add(X, add(Y, Z)).
% 183.16/23.41 Proof:
% 183.16/23.41 add(Y, add(Z, X))
% 183.16/23.41 = { by lemma 16 }
% 183.16/23.41 add(add(Z, X), Y)
% 183.16/23.41 = { by lemma 7 }
% 183.16/23.41 add(add(Y, Z), X)
% 183.16/23.41 = { by lemma 15 }
% 183.16/23.41 add(Z, add(X, Y))
% 183.16/23.41 = { by lemma 17 R->L }
% 183.16/23.41 add(X, add(Z, Y))
% 183.16/23.41 = { by lemma 16 R->L }
% 183.16/23.41 add(X, add(Y, Z))
% 183.16/23.41
% 183.16/23.41 Lemma 28: add(X, add(Y, Z)) = add(Z, add(Y, X)).
% 183.16/23.41 Proof:
% 183.16/23.41 add(X, add(Y, Z))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(Y, add(X, Z))
% 183.16/23.41 = { by lemma 15 R->L }
% 183.16/23.41 add(add(Z, Y), X)
% 183.16/23.41 = { by lemma 16 }
% 183.16/23.41 add(X, add(Z, Y))
% 183.16/23.41 = { by lemma 27 R->L }
% 183.16/23.41 add(Z, add(Y, X))
% 183.16/23.41
% 183.16/23.41 Lemma 29: add(add(X, inverse(Y)), Y) = n0.
% 183.16/23.41 Proof:
% 183.16/23.41 add(add(X, inverse(Y)), Y)
% 183.16/23.41 = { by axiom 4 (frink3) R->L }
% 183.16/23.41 ifeq(add(add(add(Y, X), inverse(Y)), inverse(Z)), n0, add(add(add(Y, X), inverse(Y)), Z), add(add(X, inverse(Y)), Y))
% 183.16/23.41 = { by lemma 5 }
% 183.16/23.41 ifeq(add(n0, inverse(Z)), n0, add(add(add(Y, X), inverse(Y)), Z), add(add(X, inverse(Y)), Y))
% 183.16/23.41 = { by lemma 8 }
% 183.16/23.41 ifeq(n0, n0, add(add(add(Y, X), inverse(Y)), Z), add(add(X, inverse(Y)), Y))
% 183.16/23.41 = { by axiom 2 (ifeq_axiom) }
% 183.16/23.41 add(add(add(Y, X), inverse(Y)), Z)
% 183.16/23.41 = { by lemma 5 }
% 183.16/23.41 add(n0, Z)
% 183.16/23.41 = { by lemma 10 }
% 183.16/23.41 n0
% 183.16/23.41
% 183.16/23.41 Lemma 30: add(X, add(Y, add(Z, W))) = add(Y, add(Z, add(W, X))).
% 183.16/23.41 Proof:
% 183.16/23.41 add(X, add(Y, add(Z, W)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(Y, add(X, add(Z, W)))
% 183.16/23.41 = { by lemma 27 R->L }
% 183.16/23.41 add(Y, add(Z, add(W, X)))
% 183.16/23.41
% 183.16/23.41 Lemma 31: add(add(X, Y), add(Z, inverse(Y))) = n0.
% 183.16/23.41 Proof:
% 183.16/23.41 add(add(X, Y), add(Z, inverse(Y)))
% 183.16/23.41 = { by lemma 7 }
% 183.16/23.41 add(add(add(Z, inverse(Y)), X), Y)
% 183.16/23.41 = { by lemma 7 }
% 183.16/23.41 add(add(add(X, Z), inverse(Y)), Y)
% 183.16/23.41 = { by lemma 29 }
% 183.16/23.41 n0
% 183.16/23.41
% 183.16/23.41 Lemma 32: add(X, add(Y, add(inverse(add(Z, inverse(W))), W))) = add(X, add(Y, W)).
% 183.16/23.41 Proof:
% 183.16/23.41 add(X, add(Y, add(inverse(add(Z, inverse(W))), W)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(Y, add(X, add(inverse(add(Z, inverse(W))), W)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(Y, add(inverse(add(Z, inverse(W))), add(X, W)))
% 183.16/23.41 = { by lemma 16 }
% 183.16/23.41 add(Y, add(inverse(add(Z, inverse(W))), add(W, X)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(inverse(add(Z, inverse(W))), add(Y, add(W, X)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(inverse(add(Z, inverse(W))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 17 }
% 183.16/23.41 add(W, add(inverse(add(Z, inverse(W))), add(Y, X)))
% 183.16/23.41 = { by axiom 2 (ifeq_axiom) R->L }
% 183.16/23.41 ifeq(n0, n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 11 R->L }
% 183.16/23.41 ifeq(add(add(Y, X), n0), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by axiom 3 (frink2) R->L }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(add(W, W), add(Z, inverse(W))), inverse(add(Z, inverse(W)))), add(add(W, add(Z, inverse(W))), W), add(add(add(W, W), add(Z, inverse(W))), inverse(inverse(add(Z, inverse(W))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by axiom 1 (frink1) }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(W, add(Z, inverse(W))), inverse(add(Z, inverse(W)))), add(add(W, add(Z, inverse(W))), W), add(add(add(W, W), add(Z, inverse(W))), inverse(inverse(add(Z, inverse(W))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by axiom 1 (frink1) }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(W, add(Z, inverse(W))), inverse(add(Z, inverse(W)))), add(add(W, add(Z, inverse(W))), W), add(add(W, add(Z, inverse(W))), inverse(inverse(add(Z, inverse(W))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 15 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), add(add(W, add(Z, inverse(W))), W), add(add(W, add(Z, inverse(W))), inverse(inverse(add(Z, inverse(W))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 13 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), add(W, add(Z, inverse(W))), add(add(W, add(Z, inverse(W))), inverse(inverse(add(Z, inverse(W))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 15 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), add(W, add(Z, inverse(W))), add(add(Z, inverse(W)), add(inverse(inverse(add(Z, inverse(W)))), W)), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 16 R->L }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), add(add(Z, inverse(W)), W), add(add(Z, inverse(W)), add(inverse(inverse(add(Z, inverse(W)))), W)), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 16 R->L }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), add(add(Z, inverse(W)), W), add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W)))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 29 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(Z, inverse(W)), add(inverse(add(Z, inverse(W))), W)), n0, add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W)))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 12 R->L }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(add(add(inverse(add(Z, inverse(W))), W), add(Z, inverse(W))), add(Z, inverse(W))), n0, add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W)))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 31 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(add(n0, add(Z, inverse(W))), n0, add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W)))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 10 }
% 183.16/23.41 ifeq(add(add(Y, X), ifeq(n0, n0, add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W)))))), n0)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by axiom 2 (ifeq_axiom) }
% 183.16/23.41 ifeq(add(add(Y, X), add(add(Z, inverse(W)), add(W, inverse(inverse(add(Z, inverse(W))))))), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 17 R->L }
% 183.16/23.41 ifeq(add(add(Z, inverse(W)), add(add(Y, X), add(W, inverse(inverse(add(Z, inverse(W))))))), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 20 }
% 183.16/23.41 ifeq(add(add(Y, X), add(W, inverse(inverse(add(Z, inverse(W)))))), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 16 R->L }
% 183.16/23.41 ifeq(add(add(W, inverse(inverse(add(Z, inverse(W))))), add(Y, X)), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.41 = { by lemma 21 }
% 183.16/23.41 ifeq(add(W, add(add(Y, X), inverse(inverse(add(Z, inverse(W)))))), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.42 = { by lemma 16 R->L }
% 183.16/23.42 ifeq(add(W, add(inverse(inverse(add(Z, inverse(W)))), add(Y, X))), n0, add(W, add(inverse(add(Z, inverse(W))), add(Y, X))), add(W, add(Y, X)))
% 183.16/23.42 = { by lemma 19 }
% 183.16/23.42 add(W, add(Y, X))
% 183.16/23.42 = { by lemma 17 R->L }
% 183.16/23.42 add(Y, add(W, X))
% 183.16/23.42 = { by lemma 16 R->L }
% 183.16/23.42 add(Y, add(X, W))
% 183.16/23.42 = { by lemma 17 R->L }
% 183.16/23.42 add(X, add(Y, W))
% 183.16/23.42
% 183.16/23.42 Lemma 33: ifeq(add(X, add(add(Y, Z), inverse(W))), n0, add(X, add(W, add(Y, Z))), add(X, add(Y, Z))) = add(X, add(Y, Z)).
% 183.16/23.42 Proof:
% 183.16/23.42 ifeq(add(X, add(add(Y, Z), inverse(W))), n0, add(X, add(W, add(Y, Z))), add(X, add(Y, Z)))
% 183.16/23.42 = { by lemma 17 }
% 183.16/23.42 ifeq(add(X, add(add(Y, Z), inverse(W))), n0, add(W, add(X, add(Y, Z))), add(X, add(Y, Z)))
% 183.16/23.42 = { by lemma 16 }
% 183.16/23.42 ifeq(add(X, add(inverse(W), add(Y, Z))), n0, add(W, add(X, add(Y, Z))), add(X, add(Y, Z)))
% 183.16/23.42 = { by lemma 17 }
% 183.16/23.42 ifeq(add(inverse(W), add(X, add(Y, Z))), n0, add(W, add(X, add(Y, Z))), add(X, add(Y, Z)))
% 183.16/23.42 = { by lemma 27 }
% 183.16/23.42 ifeq(add(inverse(W), add(X, add(Y, Z))), n0, add(W, add(X, add(Y, Z))), add(Z, add(X, Y)))
% 183.16/23.42 = { by lemma 30 R->L }
% 183.16/23.42 ifeq(add(inverse(W), add(X, add(Y, Z))), n0, add(Z, add(W, add(X, Y))), add(Z, add(X, Y)))
% 183.16/23.42 = { by lemma 30 R->L }
% 183.16/23.42 ifeq(add(Z, add(inverse(W), add(X, Y))), n0, add(Z, add(W, add(X, Y))), add(Z, add(X, Y)))
% 183.16/23.42 = { by lemma 19 }
% 183.16/23.42 add(Z, add(X, Y))
% 183.16/23.42 = { by lemma 27 R->L }
% 183.16/23.42 add(X, add(Y, Z))
% 183.16/23.42
% 183.16/23.42 Goal 1 (prove_huntington): tuple(add(add(a, b), c), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, a)) = tuple(add(a, add(b, c)), b, add(a, b)).
% 183.16/23.42 Proof:
% 183.16/23.42 tuple(add(add(a, b), c), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, a))
% 183.16/23.42 = { by lemma 16 R->L }
% 183.16/23.42 tuple(add(add(a, b), c), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(a, b))
% 183.16/23.42 = { by axiom 1 (frink1) R->L }
% 183.16/23.42 tuple(add(add(a, b), c), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.42 = { by lemma 33 R->L }
% 183.16/23.42 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b))), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(a, b))
% 183.16/23.42 = { by axiom 1 (frink1) }
% 183.16/23.42 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b))), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.42 = { by lemma 12 R->L }
% 183.16/23.42 tuple(add(add(a, b), c), ifeq(add(add(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b)), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.42 = { by lemma 13 }
% 183.16/23.42 tuple(add(add(a, b), c), ifeq(add(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b)), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 13 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b)), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 14 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b)), n0, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 16 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(b)), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 16 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 33 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(inverse(b), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), inverse(inverse(a)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 17 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(b), inverse(inverse(a)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 23 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(b), add(a, inverse(inverse(a))))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 28 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(inverse(a)), add(a, inverse(b)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 16 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(add(a, inverse(b)), inverse(inverse(a)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 7 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(add(add(add(a, inverse(b)), inverse(inverse(a))), inverse(add(a, inverse(b)))), inverse(add(inverse(a), inverse(b)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 5 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(add(n0, inverse(add(inverse(a), inverse(b)))), n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 10 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(ifeq(n0, n0, add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by axiom 2 (ifeq_axiom) }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(inverse(b), add(inverse(a), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 17 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(inverse(a), add(inverse(b), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 27 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(a), inverse(b))), n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 29 }
% 183.16/23.43 tuple(add(add(a, b), c), ifeq(n0, n0, add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by axiom 2 (ifeq_axiom) }
% 183.16/23.43 tuple(add(add(a, b), c), add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), add(a, b))
% 183.16/23.43 = { by lemma 16 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b), add(a, b))
% 183.16/23.43 = { by axiom 1 (frink1) R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, b)), add(a, b))
% 183.16/23.43 = { by lemma 26 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(inverse(inverse(b)), b)), add(a, b))
% 183.16/23.43 = { by lemma 21 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b), inverse(inverse(b))), add(a, b))
% 183.16/23.43 = { by lemma 24 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(b, add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b))), add(a, b))
% 183.16/23.43 = { by lemma 17 }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(b, add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b))), add(a, b))
% 183.16/23.43 = { by lemma 17 }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), add(b, b))), add(a, b))
% 183.16/23.43 = { by lemma 21 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b)))), b), b)), add(a, b))
% 183.16/23.43 = { by lemma 16 }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(b, add(inverse(add(a, inverse(b))), inverse(add(inverse(a), inverse(b))))), b)), add(a, b))
% 183.16/23.43 = { by lemma 28 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(inverse(a), inverse(b))), add(inverse(add(a, inverse(b))), b)), b)), add(a, b))
% 183.16/23.43 = { by lemma 21 R->L }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(add(inverse(add(inverse(a), inverse(b))), b), inverse(add(a, inverse(b)))), b)), add(a, b))
% 183.16/23.43 = { by lemma 16 }
% 183.16/23.43 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), add(inverse(add(inverse(a), inverse(b))), b)), b)), add(a, b))
% 183.16/23.43 = { by axiom 1 (frink1) R->L }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(add(inverse(add(a, inverse(b))), add(inverse(add(inverse(a), inverse(b))), b)), add(inverse(add(a, inverse(b))), add(inverse(add(inverse(a), inverse(b))), b))), b)), add(a, b))
% 183.16/23.44 = { by lemma 32 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(add(inverse(add(a, inverse(b))), add(inverse(add(inverse(a), inverse(b))), b)), add(inverse(add(a, inverse(b))), b)), b)), add(a, b))
% 183.16/23.44 = { by lemma 21 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), add(add(inverse(add(a, inverse(b))), b), add(inverse(add(inverse(a), inverse(b))), b))), b)), add(a, b))
% 183.16/23.44 = { by lemma 32 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), add(add(inverse(add(a, inverse(b))), b), b)), b)), add(a, b))
% 183.16/23.44 = { by lemma 12 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), add(b, inverse(add(a, inverse(b))))), b)), add(a, b))
% 183.16/23.44 = { by lemma 14 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(add(inverse(add(a, inverse(b))), b), b)), add(a, b))
% 183.16/23.44 = { by lemma 21 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, b))), add(a, b))
% 183.16/23.44 = { by lemma 25 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by axiom 2 (ifeq_axiom) R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(n0, n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 11 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), n0), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 11 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(b, n0)), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 31 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(b, add(add(a, inverse(b)), add(inverse(inverse(add(a, inverse(b)))), inverse(inverse(b)))))), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 16 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(b, add(add(a, inverse(b)), add(inverse(inverse(b)), inverse(inverse(add(a, inverse(b)))))))), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 22 }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(b, add(inverse(inverse(b)), inverse(inverse(add(a, inverse(b))))))), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 16 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(b, add(inverse(inverse(add(a, inverse(b)))), inverse(inverse(b))))), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 17 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), ifeq(add(inverse(inverse(b)), add(inverse(inverse(add(a, inverse(b)))), add(b, inverse(inverse(b))))), n0, add(inverse(inverse(b)), add(inverse(add(a, inverse(b))), add(b, inverse(inverse(b))))), add(inverse(inverse(b)), add(b, inverse(inverse(b))))), add(a, b))
% 183.16/23.44 = { by lemma 19 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(b, inverse(inverse(b)))), add(a, b))
% 183.16/23.44 = { by lemma 25 }
% 183.16/23.44 tuple(add(add(a, b), c), add(inverse(inverse(b)), add(b, b)), add(a, b))
% 183.16/23.44 = { by lemma 17 R->L }
% 183.16/23.44 tuple(add(add(a, b), c), add(b, add(inverse(inverse(b)), b)), add(a, b))
% 183.16/23.44 = { by lemma 24 }
% 183.16/23.44 tuple(add(add(a, b), c), add(b, inverse(inverse(b))), add(a, b))
% 183.16/23.44 = { by lemma 23 }
% 183.16/23.44 tuple(add(add(a, b), c), inverse(inverse(b)), add(a, b))
% 183.16/23.44 = { by lemma 26 }
% 183.16/23.44 tuple(add(add(a, b), c), b, add(a, b))
% 183.16/23.44 = { by lemma 7 R->L }
% 183.16/23.44 tuple(add(add(b, c), a), b, add(a, b))
% 183.16/23.44 = { by lemma 12 R->L }
% 183.16/23.44 tuple(add(add(a, add(b, c)), add(b, c)), b, add(a, b))
% 183.16/23.44 = { by lemma 13 R->L }
% 183.16/23.44 tuple(add(add(add(a, add(b, c)), a), add(b, c)), b, add(a, b))
% 183.16/23.44 = { by lemma 7 R->L }
% 183.16/23.44 tuple(add(add(a, add(b, c)), add(a, add(b, c))), b, add(a, b))
% 183.16/23.44 = { by axiom 1 (frink1) }
% 183.16/23.44 tuple(add(a, add(b, c)), b, add(a, b))
% 183.16/23.44 % SZS output end Proof
% 183.16/23.44
% 183.16/23.44 RESULT: Unsatisfiable (the axioms are contradictory).
%------------------------------------------------------------------------------