%------------------------------------------------------------------------------
% File : Twee---2.7
% Problem : CSR056+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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:41:01 AM UTC 2026
% Result : Theorem 135.18s 17.39s
% Output : Proof 136.77s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR056+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.06/0.19 % Computer : n016.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Mon Sep 28 22:25:48 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_twee /export/starexec/sandbox/benchmark/theBenchmark.p
% 135.18/17.39 Command-line arguments: --flatten --complete-subsets
% 135.18/17.39
% 135.18/17.39 % SZS status Theorem
% 135.18/17.39
% 135.99/17.49 % SZS output start Proof
% 135.99/17.49 Axiom 1 (query106): mtvisible(c_tptp_member3717_mt) = true.
% 135.99/17.49 Axiom 2 (ax1_920): mtvisible(c_corecyclmt) = true.
% 135.99/17.49 Axiom 3 (ax1_1131): mtvisible(c_universalvocabularymt) = true.
% 135.99/17.50 Axiom 4 (ax1_1077): mtvisible(c_basekb) = true.
% 135.99/17.50 Axiom 5 (ax1_107): genlinverse(c_tptptypes_9_401, c_tptptypes_8_400) = true.
% 135.99/17.50 Axiom 6 (ax1_143): genlinverse(c_tptptypes_8_692, c_tptptypes_7_691) = true.
% 135.99/17.50 Axiom 7 (ax1_2): disjointwith(c_intangible, c_partiallytangible) = true.
% 135.99/17.50 Axiom 8 (ax1_34): genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt) = true.
% 135.99/17.50 Axiom 9 (ax1_1): genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt) = true.
% 135.99/17.50 Axiom 10 (ax1_279): genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt) = true.
% 135.99/17.50 Axiom 11 (ax1_254): genlmt(c_tptp_spindleheadmt, c_cyclistsmt) = true.
% 135.99/17.50 Axiom 12 (ifeq_axiom): ifeq(X, X, Y, Z) = Y.
% 135.99/17.50 Axiom 13 (ax1_40): ifeq(mtvisible(c_cyclistsmt), true, artsupplies(c_tptpartsupplies), true) = true.
% 135.99/17.50 Axiom 14 (ax1_238): ifeq(artsupplies(X), true, supplies(X), true) = true.
% 135.99/17.50 Axiom 15 (ax1_1123): ifeq(mtvisible(X), true, ifeq(genlmt(X, Y), true, mtvisible(Y), true), true) = true.
% 135.99/17.50 Axiom 16 (ax1_202): ifeq(supplies(X), true, ifeq(mtvisible(c_tptp_spindleheadmt), true, tptpofobject(X, f_tptpquantityfn_14(n_232)), true), true) = true.
% 135.99/17.50
% 135.99/17.50 Lemma 17: mtvisible(c_corecyclmt) = mtvisible(c_tptp_member3717_mt).
% 135.99/17.50 Proof:
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by axiom 2 (ax1_920) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50
% 135.99/17.50 Lemma 18: mtvisible(c_universalvocabularymt) = mtvisible(c_corecyclmt).
% 135.99/17.50 Proof:
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by axiom 3 (ax1_1131) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50
% 135.99/17.50 Lemma 19: mtvisible(c_basekb) = mtvisible(c_universalvocabularymt).
% 135.99/17.50 Proof:
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50 = { by axiom 4 (ax1_1077) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50
% 135.99/17.50 Lemma 20: genlinverse(c_tptptypes_9_401, c_tptptypes_8_400) = mtvisible(c_basekb).
% 135.99/17.50 Proof:
% 135.99/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 135.99/17.50 = { by axiom 5 (ax1_107) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by lemma 19 R->L }
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50
% 135.99/17.50 Lemma 21: genlinverse(c_tptptypes_8_692, c_tptptypes_7_691) = genlinverse(c_tptptypes_9_401, c_tptptypes_8_400).
% 135.99/17.50 Proof:
% 135.99/17.50 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 135.99/17.50 = { by axiom 6 (ax1_143) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by lemma 19 R->L }
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50 = { by lemma 20 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 135.99/17.50
% 135.99/17.50 Lemma 22: disjointwith(c_intangible, c_partiallytangible) = genlinverse(c_tptptypes_8_692, c_tptptypes_7_691).
% 135.99/17.50 Proof:
% 135.99/17.50 disjointwith(c_intangible, c_partiallytangible)
% 135.99/17.50 = { by axiom 7 (ax1_2) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by lemma 19 R->L }
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50 = { by lemma 20 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 135.99/17.50 = { by lemma 21 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 135.99/17.50
% 135.99/17.50 Lemma 23: genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt) = disjointwith(c_intangible, c_partiallytangible).
% 135.99/17.50 Proof:
% 135.99/17.50 genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)
% 135.99/17.50 = { by axiom 8 (ax1_34) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by lemma 19 R->L }
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50 = { by lemma 20 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 135.99/17.50 = { by lemma 21 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 135.99/17.50 = { by lemma 22 R->L }
% 135.99/17.50 disjointwith(c_intangible, c_partiallytangible)
% 135.99/17.50
% 135.99/17.50 Lemma 24: genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt) = genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt).
% 135.99/17.50 Proof:
% 135.99/17.50 genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)
% 135.99/17.50 = { by axiom 9 (ax1_1) }
% 135.99/17.50 true
% 135.99/17.50 = { by axiom 1 (query106) R->L }
% 135.99/17.50 mtvisible(c_tptp_member3717_mt)
% 135.99/17.50 = { by lemma 17 R->L }
% 135.99/17.50 mtvisible(c_corecyclmt)
% 135.99/17.50 = { by lemma 18 R->L }
% 135.99/17.50 mtvisible(c_universalvocabularymt)
% 135.99/17.50 = { by lemma 19 R->L }
% 135.99/17.50 mtvisible(c_basekb)
% 135.99/17.50 = { by lemma 20 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 135.99/17.50 = { by lemma 21 R->L }
% 135.99/17.50 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 135.99/17.50 = { by lemma 22 R->L }
% 135.99/17.50 disjointwith(c_intangible, c_partiallytangible)
% 135.99/17.50 = { by lemma 23 R->L }
% 135.99/17.50 genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)
% 135.99/17.50
% 135.99/17.50 Lemma 25: ifeq(mtvisible(X), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)) = genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt).
% 135.99/17.50 Proof:
% 135.99/17.50 ifeq(mtvisible(X), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 135.99/17.50 = { by lemma 24 }
% 135.99/17.50 ifeq(mtvisible(X), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 135.99/17.50 = { by lemma 24 }
% 135.99/17.50 ifeq(mtvisible(X), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), mtvisible(Y), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 135.99/17.50 = { by lemma 24 }
% 135.99/17.50 ifeq(mtvisible(X), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), mtvisible(Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 135.99/17.50 = { by lemma 24 }
% 135.99/17.50 ifeq(mtvisible(X), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(genlmt(X, Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), mtvisible(Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 135.99/17.50 = { by lemma 23 }
% 135.99/17.50 ifeq(mtvisible(X), disjointwith(c_intangible, c_partiallytangible), ifeq(genlmt(X, Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), mtvisible(Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 135.99/17.50 = { by lemma 23 }
% 135.99/17.50 ifeq(mtvisible(X), disjointwith(c_intangible, c_partiallytangible), ifeq(genlmt(X, Y), disjointwith(c_intangible, c_partiallytangible), mtvisible(Y), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 135.99/17.50 = { by lemma 23 }
% 135.99/17.50 ifeq(mtvisible(X), disjointwith(c_intangible, c_partiallytangible), ifeq(genlmt(X, Y), disjointwith(c_intangible, c_partiallytangible), mtvisible(Y), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 135.99/17.50 = { by lemma 23 }
% 135.99/17.50 ifeq(mtvisible(X), disjointwith(c_intangible, c_partiallytangible), ifeq(genlmt(X, Y), disjointwith(c_intangible, c_partiallytangible), mtvisible(Y), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 135.99/17.50 = { by lemma 22 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(genlmt(X, Y), disjointwith(c_intangible, c_partiallytangible), mtvisible(Y), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 135.99/17.50 = { by lemma 22 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), mtvisible(Y), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 135.99/17.50 = { by lemma 22 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), mtvisible(Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), disjointwith(c_intangible, c_partiallytangible))
% 135.99/17.50 = { by lemma 22 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), mtvisible(Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 135.99/17.50 = { by lemma 21 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), mtvisible(Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 135.99/17.50 = { by lemma 21 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), mtvisible(Y), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 135.99/17.50 = { by lemma 21 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), mtvisible(Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 135.99/17.50 = { by lemma 21 }
% 135.99/17.50 ifeq(mtvisible(X), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), mtvisible(Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 135.99/17.50 = { by lemma 20 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_basekb), ifeq(genlmt(X, Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), mtvisible(Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 135.99/17.50 = { by lemma 20 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_basekb), ifeq(genlmt(X, Y), mtvisible(c_basekb), mtvisible(Y), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 135.99/17.50 = { by lemma 20 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_basekb), ifeq(genlmt(X, Y), mtvisible(c_basekb), mtvisible(Y), mtvisible(c_basekb)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 135.99/17.50 = { by lemma 20 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_basekb), ifeq(genlmt(X, Y), mtvisible(c_basekb), mtvisible(Y), mtvisible(c_basekb)), mtvisible(c_basekb))
% 135.99/17.50 = { by lemma 19 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_universalvocabularymt), ifeq(genlmt(X, Y), mtvisible(c_basekb), mtvisible(Y), mtvisible(c_basekb)), mtvisible(c_basekb))
% 135.99/17.50 = { by lemma 19 }
% 135.99/17.50 ifeq(mtvisible(X), mtvisible(c_universalvocabularymt), ifeq(genlmt(X, Y), mtvisible(c_universalvocabularymt), mtvisible(Y), mtvisible(c_basekb)), mtvisible(c_basekb))
% 136.77/17.50 = { by lemma 19 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_universalvocabularymt), ifeq(genlmt(X, Y), mtvisible(c_universalvocabularymt), mtvisible(Y), mtvisible(c_universalvocabularymt)), mtvisible(c_basekb))
% 136.77/17.50 = { by lemma 19 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_universalvocabularymt), ifeq(genlmt(X, Y), mtvisible(c_universalvocabularymt), mtvisible(Y), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.50 = { by lemma 18 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_corecyclmt), ifeq(genlmt(X, Y), mtvisible(c_universalvocabularymt), mtvisible(Y), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.50 = { by lemma 18 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_corecyclmt), ifeq(genlmt(X, Y), mtvisible(c_corecyclmt), mtvisible(Y), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.50 = { by lemma 18 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_corecyclmt), ifeq(genlmt(X, Y), mtvisible(c_corecyclmt), mtvisible(Y), mtvisible(c_corecyclmt)), mtvisible(c_universalvocabularymt))
% 136.77/17.50 = { by lemma 18 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_corecyclmt), ifeq(genlmt(X, Y), mtvisible(c_corecyclmt), mtvisible(Y), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.50 = { by lemma 17 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_tptp_member3717_mt), ifeq(genlmt(X, Y), mtvisible(c_corecyclmt), mtvisible(Y), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.50 = { by lemma 17 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_tptp_member3717_mt), ifeq(genlmt(X, Y), mtvisible(c_tptp_member3717_mt), mtvisible(Y), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.50 = { by lemma 17 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_tptp_member3717_mt), ifeq(genlmt(X, Y), mtvisible(c_tptp_member3717_mt), mtvisible(Y), mtvisible(c_tptp_member3717_mt)), mtvisible(c_corecyclmt))
% 136.77/17.50 = { by lemma 17 }
% 136.77/17.50 ifeq(mtvisible(X), mtvisible(c_tptp_member3717_mt), ifeq(genlmt(X, Y), mtvisible(c_tptp_member3717_mt), mtvisible(Y), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.50 = { by axiom 1 (query106) }
% 136.77/17.50 ifeq(mtvisible(X), true, ifeq(genlmt(X, Y), mtvisible(c_tptp_member3717_mt), mtvisible(Y), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.50 = { by axiom 1 (query106) }
% 136.77/17.50 ifeq(mtvisible(X), true, ifeq(genlmt(X, Y), true, mtvisible(Y), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.50 = { by axiom 1 (query106) }
% 136.77/17.50 ifeq(mtvisible(X), true, ifeq(genlmt(X, Y), true, mtvisible(Y), true), mtvisible(c_tptp_member3717_mt))
% 136.77/17.50 = { by axiom 1 (query106) }
% 136.77/17.50 ifeq(mtvisible(X), true, ifeq(genlmt(X, Y), true, mtvisible(Y), true), true)
% 136.77/17.50 = { by axiom 15 (ax1_1123) }
% 136.77/17.50 true
% 136.77/17.50 = { by axiom 1 (query106) R->L }
% 136.77/17.50 mtvisible(c_tptp_member3717_mt)
% 136.77/17.50 = { by lemma 17 R->L }
% 136.77/17.50 mtvisible(c_corecyclmt)
% 136.77/17.50 = { by lemma 18 R->L }
% 136.77/17.50 mtvisible(c_universalvocabularymt)
% 136.77/17.50 = { by lemma 19 R->L }
% 136.77/17.50 mtvisible(c_basekb)
% 136.77/17.50 = { by lemma 20 R->L }
% 136.77/17.50 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 136.77/17.50 = { by lemma 21 R->L }
% 136.77/17.50 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 136.77/17.50 = { by lemma 22 R->L }
% 136.77/17.50 disjointwith(c_intangible, c_partiallytangible)
% 136.77/17.50 = { by lemma 23 R->L }
% 136.77/17.50 genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)
% 136.77/17.50 = { by lemma 24 R->L }
% 136.77/17.50 genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)
% 136.77/17.50
% 136.77/17.50 Lemma 26: genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt) = mtvisible(c_tptp_spindleheadmt).
% 136.77/17.50 Proof:
% 136.77/17.50 genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)
% 136.77/17.50 = { by lemma 25 R->L }
% 136.77/17.50 ifeq(mtvisible(c_tptp_member3717_mt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 17 R->L }
% 136.77/17.50 ifeq(mtvisible(c_corecyclmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 18 R->L }
% 136.77/17.50 ifeq(mtvisible(c_universalvocabularymt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 19 R->L }
% 136.77/17.50 ifeq(mtvisible(c_basekb), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 20 R->L }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 21 R->L }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 22 R->L }
% 136.77/17.50 ifeq(disjointwith(c_intangible, c_partiallytangible), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 23 R->L }
% 136.77/17.50 ifeq(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 24 R->L }
% 136.77/17.50 ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by axiom 12 (ifeq_axiom) }
% 136.77/17.50 ifeq(genlmt(c_tptp_member3717_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by axiom 10 (ax1_279) }
% 136.77/17.50 ifeq(true, genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by axiom 1 (query106) R->L }
% 136.77/17.50 ifeq(mtvisible(c_tptp_member3717_mt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 17 R->L }
% 136.77/17.50 ifeq(mtvisible(c_corecyclmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 18 R->L }
% 136.77/17.50 ifeq(mtvisible(c_universalvocabularymt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 19 R->L }
% 136.77/17.50 ifeq(mtvisible(c_basekb), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 20 R->L }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 21 R->L }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 22 R->L }
% 136.77/17.50 ifeq(disjointwith(c_intangible, c_partiallytangible), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 23 R->L }
% 136.77/17.50 ifeq(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 24 R->L }
% 136.77/17.50 ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by axiom 12 (ifeq_axiom) }
% 136.77/17.50 mtvisible(c_tptp_spindleheadmt)
% 136.77/17.50
% 136.77/17.50 Goal 1 (query106_1): tptpofobject(c_tptpartsupplies, X) = true.
% 136.77/17.50 The goal is true when:
% 136.77/17.50 X = f_tptpquantityfn_14(n_232)
% 136.77/17.50
% 136.77/17.50 Proof:
% 136.77/17.50 tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232))
% 136.77/17.50 = { by axiom 12 (ifeq_axiom) R->L }
% 136.77/17.50 ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 24 }
% 136.77/17.50 ifeq(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 23 }
% 136.77/17.50 ifeq(disjointwith(c_intangible, c_partiallytangible), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 22 }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 21 }
% 136.77/17.50 ifeq(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 20 }
% 136.77/17.50 ifeq(mtvisible(c_basekb), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.50 = { by lemma 19 }
% 136.77/17.50 ifeq(mtvisible(c_universalvocabularymt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 }
% 136.77/17.51 ifeq(mtvisible(c_corecyclmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 }
% 136.77/17.51 ifeq(mtvisible(c_tptp_member3717_mt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) }
% 136.77/17.51 ifeq(true, genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 14 (ax1_238) R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), true, supplies(c_tptpartsupplies), true), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), true, supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), supplies(c_tptpartsupplies), mtvisible(c_corecyclmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_corecyclmt), supplies(c_tptpartsupplies), mtvisible(c_corecyclmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_corecyclmt), supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 19 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), supplies(c_tptpartsupplies), mtvisible(c_basekb)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 19 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_basekb), supplies(c_tptpartsupplies), mtvisible(c_basekb)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 20 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), mtvisible(c_basekb), supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 20 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 21 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 21 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 22 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 22 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 23 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 23 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 24 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 24 R->L }
% 136.77/17.51 ifeq(ifeq(artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 12 (ifeq_axiom) R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 25 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_spindleheadmt, c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 11 (ax1_254) }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(true, genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(mtvisible(c_tptp_member3717_mt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(mtvisible(c_corecyclmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(mtvisible(c_universalvocabularymt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 19 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(mtvisible(c_basekb), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 20 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 21 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 22 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(disjointwith(c_intangible, c_partiallytangible), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 23 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 24 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 26 R->L }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 12 (ifeq_axiom) }
% 136.77/17.51 ifeq(ifeq(ifeq(ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 12 (ifeq_axiom) }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 24 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 24 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), artsupplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 23 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), disjointwith(c_intangible, c_partiallytangible), artsupplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 23 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), disjointwith(c_intangible, c_partiallytangible), artsupplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 22 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), artsupplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 22 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 21 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 21 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 20 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_basekb), artsupplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 20 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_basekb), artsupplies(c_tptpartsupplies), mtvisible(c_basekb)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 19 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_universalvocabularymt), artsupplies(c_tptpartsupplies), mtvisible(c_basekb)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 19 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_universalvocabularymt), artsupplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_corecyclmt), artsupplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 18 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_corecyclmt), artsupplies(c_tptpartsupplies), mtvisible(c_corecyclmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_tptp_member3717_mt), artsupplies(c_tptpartsupplies), mtvisible(c_corecyclmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by lemma 17 }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), mtvisible(c_tptp_member3717_mt), artsupplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), true, artsupplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) }
% 136.77/17.51 ifeq(ifeq(ifeq(mtvisible(c_cyclistsmt), true, artsupplies(c_tptpartsupplies), true), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 13 (ax1_40) }
% 136.77/17.51 ifeq(ifeq(true, genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.51 = { by axiom 1 (query106) R->L }
% 136.77/17.52 ifeq(ifeq(mtvisible(c_tptp_member3717_mt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 17 R->L }
% 136.77/17.52 ifeq(ifeq(mtvisible(c_corecyclmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 18 R->L }
% 136.77/17.52 ifeq(ifeq(mtvisible(c_universalvocabularymt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 19 R->L }
% 136.77/17.52 ifeq(ifeq(mtvisible(c_basekb), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 20 R->L }
% 136.77/17.52 ifeq(ifeq(genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 21 R->L }
% 136.77/17.52 ifeq(ifeq(genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 22 R->L }
% 136.77/17.52 ifeq(ifeq(disjointwith(c_intangible, c_partiallytangible), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 23 R->L }
% 136.77/17.52 ifeq(ifeq(genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 24 R->L }
% 136.77/17.52 ifeq(ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by axiom 12 (ifeq_axiom) }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by axiom 12 (ifeq_axiom) R->L }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 26 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 24 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 24 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 24 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt))
% 136.77/17.52 = { by lemma 24 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 136.77/17.52 = { by lemma 23 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), ifeq(mtvisible(c_tptp_spindleheadmt), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 136.77/17.52 = { by lemma 23 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), ifeq(mtvisible(c_tptp_spindleheadmt), disjointwith(c_intangible, c_partiallytangible), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 136.77/17.52 = { by lemma 23 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), ifeq(mtvisible(c_tptp_spindleheadmt), disjointwith(c_intangible, c_partiallytangible), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), disjointwith(c_intangible, c_partiallytangible)), genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt))
% 136.77/17.52 = { by lemma 23 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), disjointwith(c_intangible, c_partiallytangible), ifeq(mtvisible(c_tptp_spindleheadmt), disjointwith(c_intangible, c_partiallytangible), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 136.77/17.52 = { by lemma 22 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(mtvisible(c_tptp_spindleheadmt), disjointwith(c_intangible, c_partiallytangible), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 136.77/17.52 = { by lemma 22 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), disjointwith(c_intangible, c_partiallytangible)), disjointwith(c_intangible, c_partiallytangible))
% 136.77/17.52 = { by lemma 22 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), disjointwith(c_intangible, c_partiallytangible))
% 136.77/17.52 = { by lemma 22 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 136.77/17.52 = { by lemma 21 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 136.77/17.52 = { by lemma 21 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 136.77/17.52 = { by lemma 21 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_8_692, c_tptptypes_7_691))
% 136.77/17.52 = { by lemma 21 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 136.77/17.52 = { by lemma 20 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_basekb), ifeq(mtvisible(c_tptp_spindleheadmt), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 136.77/17.52 = { by lemma 20 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_basekb), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_basekb), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 136.77/17.52 = { by lemma 20 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_basekb), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_basekb), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_basekb)), genlinverse(c_tptptypes_9_401, c_tptptypes_8_400))
% 136.77/17.52 = { by lemma 20 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_basekb), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_basekb), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_basekb)), mtvisible(c_basekb))
% 136.77/17.52 = { by lemma 19 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_basekb), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_basekb)), mtvisible(c_basekb))
% 136.77/17.52 = { by lemma 19 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_universalvocabularymt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_basekb)), mtvisible(c_basekb))
% 136.77/17.52 = { by lemma 19 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_universalvocabularymt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_universalvocabularymt)), mtvisible(c_basekb))
% 136.77/17.52 = { by lemma 19 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_universalvocabularymt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_universalvocabularymt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.52 = { by lemma 18 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_corecyclmt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_universalvocabularymt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.52 = { by lemma 18 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_corecyclmt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_corecyclmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_universalvocabularymt)), mtvisible(c_universalvocabularymt))
% 136.77/17.52 = { by lemma 18 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_corecyclmt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_corecyclmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_corecyclmt)), mtvisible(c_universalvocabularymt))
% 136.77/17.52 = { by lemma 18 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_corecyclmt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_corecyclmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.52 = { by lemma 17 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_corecyclmt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.52 = { by lemma 17 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_tptp_member3717_mt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_corecyclmt)), mtvisible(c_corecyclmt))
% 136.77/17.52 = { by lemma 17 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_tptp_member3717_mt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_tptp_member3717_mt)), mtvisible(c_corecyclmt))
% 136.77/17.52 = { by lemma 17 }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), mtvisible(c_tptp_member3717_mt), ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_tptp_member3717_mt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.52 = { by axiom 1 (query106) }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), true, ifeq(mtvisible(c_tptp_spindleheadmt), mtvisible(c_tptp_member3717_mt), tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.52 = { by axiom 1 (query106) }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), true, ifeq(mtvisible(c_tptp_spindleheadmt), true, tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), mtvisible(c_tptp_member3717_mt)), mtvisible(c_tptp_member3717_mt))
% 136.77/17.52 = { by axiom 1 (query106) }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), true, ifeq(mtvisible(c_tptp_spindleheadmt), true, tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), true), mtvisible(c_tptp_member3717_mt))
% 136.77/17.52 = { by axiom 1 (query106) }
% 136.77/17.52 ifeq(supplies(c_tptpartsupplies), true, ifeq(mtvisible(c_tptp_spindleheadmt), true, tptpofobject(c_tptpartsupplies, f_tptpquantityfn_14(n_232)), true), true)
% 136.77/17.52 = { by axiom 16 (ax1_202) }
% 136.77/17.52 true
% 136.77/17.52 = { by axiom 1 (query106) R->L }
% 136.77/17.52 mtvisible(c_tptp_member3717_mt)
% 136.77/17.52 = { by lemma 17 R->L }
% 136.77/17.52 mtvisible(c_corecyclmt)
% 136.77/17.52 = { by lemma 18 R->L }
% 136.77/17.52 mtvisible(c_universalvocabularymt)
% 136.77/17.52 = { by lemma 19 R->L }
% 136.77/17.52 mtvisible(c_basekb)
% 136.77/17.52 = { by lemma 20 R->L }
% 136.77/17.52 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 136.77/17.52 = { by lemma 21 R->L }
% 136.77/17.52 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 136.77/17.52 = { by lemma 22 R->L }
% 136.77/17.52 disjointwith(c_intangible, c_partiallytangible)
% 136.77/17.52 = { by lemma 23 R->L }
% 136.77/17.52 genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)
% 136.77/17.52 = { by lemma 24 R->L }
% 136.77/17.52 genlmt(c_tptpgeo_member8_mt, c_tptpgeo_spindleheadmt)
% 136.77/17.52 = { by lemma 24 }
% 136.77/17.52 genlmt(c_tptp_member3205_mt, c_tptp_spindleheadmt)
% 136.77/17.52 = { by lemma 23 }
% 136.77/17.52 disjointwith(c_intangible, c_partiallytangible)
% 136.77/17.52 = { by lemma 22 }
% 136.77/17.52 genlinverse(c_tptptypes_8_692, c_tptptypes_7_691)
% 136.77/17.52 = { by lemma 21 }
% 136.77/17.52 genlinverse(c_tptptypes_9_401, c_tptptypes_8_400)
% 136.77/17.52 = { by lemma 20 }
% 136.77/17.52 mtvisible(c_basekb)
% 136.77/17.52 = { by lemma 19 }
% 136.77/17.52 mtvisible(c_universalvocabularymt)
% 136.77/17.52 = { by lemma 18 }
% 136.77/17.52 mtvisible(c_corecyclmt)
% 136.77/17.52 = { by lemma 17 }
% 136.77/17.52 mtvisible(c_tptp_member3717_mt)
% 136.77/17.52 = { by axiom 1 (query106) }
% 136.77/17.52 true
% 136.77/17.52 % SZS output end Proof
% 136.77/17.52
% 136.77/17.52 RESULT: Theorem (the conjecture is true).
%------------------------------------------------------------------------------