%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS153+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 03:32:03 EDT 2022 % Result : Theorem 15.30s 15.56s % Output : Proof 15.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.08 % Problem : KRS153+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.09 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.09/0.28 % Computer : n026.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 600 % 0.09/0.28 % DateTime : Tue Jun 7 20:55:01 EDT 2022 % 0.09/0.28 % CPUTime : % 15.30/15.56 % SZS status Theorem % 15.30/15.56 (* PROOF-FOUND *) % 15.30/15.56 (* BEGIN-PROOF *) % 15.30/15.56 % SZS output start Proof % 15.30/15.56 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 15.30/15.56 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 15.30/15.56 3. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### NotNot 2 % 15.30/15.56 4. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Definition-Pseudo(xsd_string) 3 % 15.30/15.56 5. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 15.30/15.56 6. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Definition-Pseudo(xsd_string) 5 % 15.30/15.56 7. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 4 6 % 15.30/15.56 8. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 7 % 15.30/15.56 9. ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) (-. ((-. (cC100 (iV16439))) /\ (cC104 (iV16439)))) ### Axiom % 15.30/15.56 10. (-. (cC106 (iV16439))) ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) ### Definition-Pseudo(cC106) 9 % 15.30/15.56 11. (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y)))) ### Axiom % 15.30/15.56 12. (-. (cC28 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ### Definition-Pseudo(cC28) 11 % 15.30/15.56 13. (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y)))) ### Axiom % 15.30/15.56 14. (-. (cC130 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) ### Definition-Pseudo(cC130) 13 % 15.30/15.56 15. (cowlThing (iV16439)) (-. (cowlThing (iV16439))) ### Axiom % 15.30/15.56 16. ((cC28 (iV16439)) /\ (cC106 (iV16439))) (-. ((cC28 (iV16439)) /\ (cC106 (iV16439)))) ### Axiom % 15.30/15.56 17. (-. (cC108 (iV16439))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) ### Definition-Pseudo(cC108) 16 % 15.30/15.56 18. (Ex Y, ((rR1 (iV16439) Y) /\ (-. (cC102 Y)))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (-. (cC102 Y))))) ### Axiom % 15.30/15.56 19. (-. (cC104 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (-. (cC102 Y)))) ### Definition-Pseudo(cC104) 18 % 15.30/15.56 20. (rR1 (iV16440) (iV16463)) (-. (rR1 (iV16440) (iV16463))) ### Axiom % 15.30/15.56 21. (-. (cC16 (iV16463))) (cC16 (iV16463)) ### Axiom % 15.30/15.56 22. (-. (-. (cC16 (iV16463)))) (-. (cC16 (iV16463))) ### NotNot 21 % 15.30/15.56 23. (-. ((rR1 (iV16440) (iV16463)) /\ (-. (cC16 (iV16463))))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) ### NotAnd 20 22 % 15.30/15.56 24. (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC16 Y))))) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) ### NotExists 23 % 15.30/15.56 25. (-. (cC80 (iV16440))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) ### Definition-Pseudo(cC80) 24 % 15.30/15.56 26. (cowlThing (iV16440)) (-. (cowlThing (iV16440))) ### Axiom % 15.30/15.56 27. (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y)))) ### Axiom % 15.30/15.56 28. (cC78 (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) ### Definition-Pseudo(cC78) 27 % 15.30/15.56 29. (-. (-. (cC78 (iV16440)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) ### NotNot 28 % 15.30/15.56 30. (-. ((-. (cC78 (iV16440))) /\ (cC80 (iV16440)))) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) ### NotAnd 29 25 % 15.30/15.56 31. (-. (cC82 (iV16440))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) ### Definition-Pseudo(cC82) 30 % 15.30/15.56 32. (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y))) ### Axiom % 15.30/15.56 33. (cC96 (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) ### Definition-Pseudo(cC96) 32 % 15.30/15.56 34. (-. (-. (cC96 (iV16440)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) ### NotNot 33 % 15.30/15.56 35. (-. ((-. (cC96 (iV16440))) /\ (cC82 (iV16440)))) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) ### NotAnd 34 31 % 15.30/15.56 36. (-. (cC98 (iV16440))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) ### Definition-Pseudo(cC98) 35 % 15.30/15.56 37. (cowlThing (iV16448)) (-. (cowlThing (iV16448))) ### Axiom % 15.30/15.56 38. (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y)))) ### Axiom % 15.30/15.56 39. (cC36 (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) ### Definition-Pseudo(cC36) 38 % 15.30/15.56 40. (-. (-. (cC36 (iV16448)))) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) ### NotNot 39 % 15.30/15.56 41. (cTOP (iV16448)) (-. (cTOP (iV16448))) ### Axiom % 15.30/15.56 42. (-. ((-. (cC36 (iV16448))) /\ (cTOP (iV16448)))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) ### NotAnd 40 41 % 15.30/15.56 43. (-. (cC38 (iV16448))) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) ### Definition-Pseudo(cC38) 42 % 15.30/15.56 44. (rR1 (iV16453) (iV16461)) (-. (rR1 (iV16453) (iV16461))) ### Axiom % 15.30/15.56 45. (-. (cC12 (iV16461))) (cC12 (iV16461)) ### Axiom % 15.30/15.56 46. (-. (-. (cC12 (iV16461)))) (-. (cC12 (iV16461))) ### NotNot 45 % 15.30/15.56 47. (-. ((rR1 (iV16453) (iV16461)) /\ (-. (cC12 (iV16461))))) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) ### NotAnd 44 46 % 15.30/15.56 48. (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC12 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) ### NotExists 47 % 15.30/15.56 49. (-. (cC60 (iV16453))) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) ### Definition-Pseudo(cC60) 48 % 15.30/15.56 50. (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y)))) ### Axiom % 15.30/15.56 51. (cC58 (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC58) 50 % 15.30/15.56 52. (-. (-. (cC58 (iV16453)))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) ### NotNot 51 % 15.30/15.56 53. (-. ((cC60 (iV16453)) /\ (-. (cC58 (iV16453))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) ### NotAnd 49 52 % 15.30/15.56 54. (-. (cC62 (iV16453))) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC62) 53 % 15.30/15.56 55. (cowlThing (iV16453)) (-. (cowlThing (iV16453))) ### Axiom % 15.30/15.56 56. (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y))) ### Axiom % 15.30/15.56 57. (cC74 (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) ### Definition-Pseudo(cC74) 56 % 15.30/15.56 58. (-. (-. (cC74 (iV16453)))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) ### NotNot 57 % 15.30/15.56 59. (-. ((-. (cC74 (iV16453))) /\ (cC62 (iV16453)))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) ### NotAnd 58 54 % 15.30/15.56 60. (-. (cC76 (iV16453))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC76) 59 % 15.30/15.56 61. (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y)))) ### Axiom % 15.30/15.56 62. (cC40 (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) ### Definition-Pseudo(cC40) 61 % 15.30/15.56 63. (-. (-. (cC40 (iV16455)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) ### NotNot 62 % 15.30/15.56 64. (rR1 (iV16455) (iV16460)) (-. (rR1 (iV16455) (iV16460))) ### Axiom % 15.30/15.56 65. (-. (cC8 (iV16460))) (cC8 (iV16460)) ### Axiom % 15.30/15.56 66. (-. (-. (cC8 (iV16460)))) (-. (cC8 (iV16460))) ### NotNot 65 % 15.30/15.56 67. (-. ((rR1 (iV16455) (iV16460)) /\ (-. (cC8 (iV16460))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) ### NotAnd 64 66 % 15.30/15.56 68. (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC8 Y))))) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) ### NotExists 67 % 15.30/15.56 69. (-. (cC42 (iV16455))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) ### Definition-Pseudo(cC42) 68 % 15.30/15.56 70. (-. ((-. (cC40 (iV16455))) /\ (cC42 (iV16455)))) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) ### NotAnd 63 69 % 15.30/15.56 71. (-. (cC44 (iV16455))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) ### Definition-Pseudo(cC44) 70 % 15.30/15.56 72. (cowlThing (iV16455)) (-. (cowlThing (iV16455))) ### Axiom % 15.30/15.56 73. (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y))) ### Axiom % 15.30/15.56 74. (cC54 (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC54) 73 % 15.30/15.56 75. (-. (-. (cC54 (iV16455)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) ### NotNot 74 % 15.30/15.56 76. (-. ((cC44 (iV16455)) /\ (-. (cC54 (iV16455))))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) ### NotAnd 71 75 % 15.30/15.56 77. (-. (cC56 (iV16455))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC56) 76 % 15.30/15.56 78. (cowlThing (iV16457)) (-. (cowlThing (iV16457))) ### Axiom % 15.30/15.56 79. (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y)))) ### Axiom % 15.30/15.56 80. (cC36 (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) ### Definition-Pseudo(cC36) 79 % 15.30/15.56 81. (-. (-. (cC36 (iV16457)))) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) ### NotNot 80 % 15.30/15.56 82. (cTOP (iV16457)) (-. (cTOP (iV16457))) ### Axiom % 15.30/15.56 83. (-. ((-. (cC36 (iV16457))) /\ (cTOP (iV16457)))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) ### NotAnd 81 82 % 15.30/15.56 84. (-. (cC38 (iV16457))) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) ### Definition-Pseudo(cC38) 83 % 15.30/15.56 85. (-. (cC8 (iV16459))) (cC8 (iV16459)) ### Axiom % 15.30/15.56 86. ((cC8 (iV16459)) /\ (cC12 (iV16459))) (-. (cC8 (iV16459))) ### And 85 % 15.30/15.56 87. (cC64 (iV16459)) (-. (cC8 (iV16459))) ### Definition-Pseudo(cC64) 86 % 15.30/15.56 88. (-. (-. (cC64 (iV16459)))) (-. (cC8 (iV16459))) ### NotNot 87 % 15.30/15.56 89. (cC12 (iV16459)) (-. (cC12 (iV16459))) ### Axiom % 15.30/15.56 90. ((-. (cC8 (iV16459))) /\ (-. (cC12 (iV16459)))) (cC12 (iV16459)) ### And 89 % 15.30/15.56 91. (cC66 (iV16459)) (cC12 (iV16459)) ### Definition-Pseudo(cC66) 90 % 15.30/15.56 92. (-. (-. (cC66 (iV16459)))) (cC12 (iV16459)) ### NotNot 91 % 15.30/15.56 93. (-. ((-. (cC64 (iV16459))) /\ (-. (cC66 (iV16459))))) (cC12 (iV16459)) (-. (cC8 (iV16459))) ### NotAnd 88 92 % 15.30/15.56 94. (-. (cC68 (iV16459))) (-. (cC8 (iV16459))) (cC12 (iV16459)) ### Definition-Pseudo(cC68) 93 % 15.30/15.56 95. (cowlThing (iV16459)) (-. (cowlThing (iV16459))) ### Axiom % 15.30/15.56 96. (-. (cC2 (iV16459))) (cC2 (iV16459)) ### Axiom % 15.30/15.56 97. ((cC2 (iV16459)) /\ (cC12 (iV16459))) (-. (cC2 (iV16459))) ### And 96 % 15.30/15.56 98. (cC84 (iV16459)) (-. (cC2 (iV16459))) ### Definition-Pseudo(cC84) 97 % 15.30/15.56 99. (-. (-. (cC84 (iV16459)))) (-. (cC2 (iV16459))) ### NotNot 98 % 15.30/15.56 100. (cC12 (iV16459)) (-. (cC12 (iV16459))) ### Axiom % 15.30/15.56 101. ((-. (cC12 (iV16459))) /\ (-. (cC2 (iV16459)))) (cC12 (iV16459)) ### And 100 % 15.30/15.56 102. (cC86 (iV16459)) (cC12 (iV16459)) ### Definition-Pseudo(cC86) 101 % 15.30/15.56 103. (-. (-. (cC86 (iV16459)))) (cC12 (iV16459)) ### NotNot 102 % 15.30/15.56 104. (-. ((-. (cC84 (iV16459))) /\ (-. (cC86 (iV16459))))) (cC12 (iV16459)) (-. (cC2 (iV16459))) ### NotAnd 99 103 % 15.30/15.56 105. (-. (cC88 (iV16459))) (-. (cC2 (iV16459))) (cC12 (iV16459)) ### Definition-Pseudo(cC88) 104 % 15.30/15.56 106. (-. (cC8 (iV16459))) (cC8 (iV16459)) ### Axiom % 15.30/15.56 107. ((cC8 (iV16459)) /\ (cC4 (iV16459))) (-. (cC8 (iV16459))) ### And 106 % 15.30/15.56 108. (cC46 (iV16459)) (-. (cC8 (iV16459))) ### Definition-Pseudo(cC46) 107 % 15.30/15.56 109. (-. (-. (cC46 (iV16459)))) (-. (cC8 (iV16459))) ### NotNot 108 % 15.30/15.56 110. (cC4 (iV16459)) (-. (cC4 (iV16459))) ### Axiom % 15.30/15.56 111. ((-. (cC8 (iV16459))) /\ (-. (cC4 (iV16459)))) (cC4 (iV16459)) ### And 110 % 15.30/15.56 112. (cC48 (iV16459)) (cC4 (iV16459)) ### Definition-Pseudo(cC48) 111 % 15.30/15.56 113. (-. (-. (cC48 (iV16459)))) (cC4 (iV16459)) ### NotNot 112 % 15.30/15.56 114. (-. ((-. (cC46 (iV16459))) /\ (-. (cC48 (iV16459))))) (cC4 (iV16459)) (-. (cC8 (iV16459))) ### NotAnd 109 113 % 15.30/15.56 115. (-. (cC50 (iV16459))) (-. (cC8 (iV16459))) (cC4 (iV16459)) ### Definition-Pseudo(cC50) 114 % 15.30/15.56 116. (cC4 (iV16459)) (-. (cC4 (iV16459))) ### Axiom % 15.30/15.56 117. ((-. (cC2 (iV16459))) /\ (-. (cC4 (iV16459)))) (cC4 (iV16459)) ### And 116 % 15.30/15.56 118. (cC32 (iV16459)) (cC4 (iV16459)) ### Definition-Pseudo(cC32) 117 % 15.30/15.56 119. (-. (-. (cC32 (iV16459)))) (cC4 (iV16459)) ### NotNot 118 % 15.30/15.56 120. (-. (cC2 (iV16459))) (cC2 (iV16459)) ### Axiom % 15.30/15.56 121. ((cC4 (iV16459)) /\ (cC2 (iV16459))) (-. (cC2 (iV16459))) ### And 120 % 15.30/15.56 122. (cC30 (iV16459)) (-. (cC2 (iV16459))) ### Definition-Pseudo(cC30) 121 % 15.30/15.56 123. (-. (-. (cC30 (iV16459)))) (-. (cC2 (iV16459))) ### NotNot 122 % 15.30/15.56 124. (-. ((-. (cC32 (iV16459))) /\ (-. (cC30 (iV16459))))) (-. (cC2 (iV16459))) (cC4 (iV16459)) ### NotAnd 119 123 % 15.30/15.56 125. (-. (cC34 (iV16459))) (cC4 (iV16459)) (-. (cC2 (iV16459))) ### Definition-Pseudo(cC34) 124 % 15.30/15.56 126. (cowlThing (iV16460)) (-. (cowlThing (iV16460))) ### Axiom % 15.30/15.56 127. (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y)))) ### Axiom % 15.30/15.56 128. (cC36 (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) ### Definition-Pseudo(cC36) 127 % 15.30/15.56 129. (-. (-. (cC36 (iV16460)))) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) ### NotNot 128 % 15.30/15.56 130. (cTOP (iV16460)) (-. (cTOP (iV16460))) ### Axiom % 15.30/15.56 131. (-. ((-. (cC36 (iV16460))) /\ (cTOP (iV16460)))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) ### NotAnd 129 130 % 15.30/15.56 132. (-. (cC38 (iV16460))) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) ### Definition-Pseudo(cC38) 131 % 15.30/15.56 133. (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y)))) ### Axiom % 15.30/15.56 134. (cC40 (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) ### Definition-Pseudo(cC40) 133 % 15.30/15.56 135. (-. (-. (cC40 (iV16461)))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) ### NotNot 134 % 15.30/15.56 136. (rR1 (iV16461) (iV16462)) (-. (rR1 (iV16461) (iV16462))) ### Axiom % 15.30/15.56 137. (-. (cC8 (iV16462))) (cC8 (iV16462)) ### Axiom % 15.30/15.56 138. (-. (-. (cC8 (iV16462)))) (-. (cC8 (iV16462))) ### NotNot 137 % 15.30/15.56 139. (-. ((rR1 (iV16461) (iV16462)) /\ (-. (cC8 (iV16462))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) ### NotAnd 136 138 % 15.30/15.56 140. (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC8 Y))))) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) ### NotExists 139 % 15.30/15.56 141. (-. (cC42 (iV16461))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) ### Definition-Pseudo(cC42) 140 % 15.30/15.56 142. (-. ((-. (cC40 (iV16461))) /\ (cC42 (iV16461)))) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) ### NotAnd 135 141 % 15.30/15.56 143. (-. (cC44 (iV16461))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) ### Definition-Pseudo(cC44) 142 % 15.30/15.56 144. (cowlThing (iV16461)) (-. (cowlThing (iV16461))) ### Axiom % 15.30/15.56 145. (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y))) ### Axiom % 15.30/15.56 146. (cC54 (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC54) 145 % 15.30/15.56 147. (-. (-. (cC54 (iV16461)))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) ### NotNot 146 % 15.30/15.56 148. (-. ((cC44 (iV16461)) /\ (-. (cC54 (iV16461))))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) ### NotAnd 143 147 % 15.30/15.56 149. (-. (cC56 (iV16461))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC56) 148 % 15.30/15.56 150. (cowlThing (iV16462)) (-. (cowlThing (iV16462))) ### Axiom % 15.30/15.56 151. (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y)))) ### Axiom % 15.30/15.56 152. (cC36 (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) ### Definition-Pseudo(cC36) 151 % 15.30/15.56 153. (-. (-. (cC36 (iV16462)))) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) ### NotNot 152 % 15.30/15.56 154. (cTOP (iV16462)) (-. (cTOP (iV16462))) ### Axiom % 15.30/15.56 155. (-. ((-. (cC36 (iV16462))) /\ (cTOP (iV16462)))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) ### NotAnd 153 154 % 15.30/15.56 156. (-. (cC38 (iV16462))) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) ### Definition-Pseudo(cC38) 155 % 15.30/15.56 157. (rR1 (iV16463) (iV16464)) (-. (rR1 (iV16463) (iV16464))) ### Axiom % 15.30/15.56 158. (-. (cC12 (iV16464))) (cC12 (iV16464)) ### Axiom % 15.30/15.56 159. (-. (-. (cC12 (iV16464)))) (-. (cC12 (iV16464))) ### NotNot 158 % 15.30/15.56 160. (-. ((rR1 (iV16463) (iV16464)) /\ (-. (cC12 (iV16464))))) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) ### NotAnd 157 159 % 15.30/15.56 161. (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC12 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) ### NotExists 160 % 15.30/15.56 162. (-. (cC60 (iV16463))) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) ### Definition-Pseudo(cC60) 161 % 15.30/15.56 163. (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y)))) ### Axiom % 15.30/15.56 164. (cC58 (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC58) 163 % 15.30/15.57 165. (-. (-. (cC58 (iV16463)))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) ### NotNot 164 % 15.30/15.57 166. (-. ((cC60 (iV16463)) /\ (-. (cC58 (iV16463))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) ### NotAnd 162 165 % 15.30/15.57 167. (-. (cC62 (iV16463))) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC62) 166 % 15.30/15.57 168. (cowlThing (iV16463)) (-. (cowlThing (iV16463))) ### Axiom % 15.30/15.57 169. (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y))) ### Axiom % 15.30/15.57 170. (cC74 (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) ### Definition-Pseudo(cC74) 169 % 15.30/15.57 171. (-. (-. (cC74 (iV16463)))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) ### NotNot 170 % 15.30/15.57 172. (-. ((-. (cC74 (iV16463))) /\ (cC62 (iV16463)))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) ### NotAnd 171 167 % 15.30/15.57 173. (-. (cC76 (iV16463))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) ### Definition-Pseudo(cC76) 172 % 15.30/15.57 174. (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y)))) ### Axiom % 15.30/15.57 175. (cC40 (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) ### Definition-Pseudo(cC40) 174 % 15.30/15.57 176. (-. (-. (cC40 (iV16464)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) ### NotNot 175 % 15.30/15.57 177. (rR1 (iV16464) (iV16465)) (-. (rR1 (iV16464) (iV16465))) ### Axiom % 15.30/15.57 178. (-. (cC8 (iV16465))) (cC8 (iV16465)) ### Axiom % 15.30/15.57 179. (-. (-. (cC8 (iV16465)))) (-. (cC8 (iV16465))) ### NotNot 178 % 15.30/15.57 180. (-. ((rR1 (iV16464) (iV16465)) /\ (-. (cC8 (iV16465))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) ### NotAnd 177 179 % 15.30/15.57 181. (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC8 Y))))) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) ### NotExists 180 % 15.30/15.57 182. (-. (cC42 (iV16464))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) ### Definition-Pseudo(cC42) 181 % 15.30/15.57 183. (-. ((-. (cC40 (iV16464))) /\ (cC42 (iV16464)))) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) ### NotAnd 176 182 % 15.30/15.57 184. (-. (cC44 (iV16464))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) ### Definition-Pseudo(cC44) 183 % 15.30/15.57 185. (cowlThing (iV16464)) (-. (cowlThing (iV16464))) ### Axiom % 15.30/15.57 186. (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y))) ### Axiom % 15.30/15.57 187. (cC54 (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC54) 186 % 15.30/15.57 188. (-. (-. (cC54 (iV16464)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) ### NotNot 187 % 15.30/15.57 189. (-. ((cC44 (iV16464)) /\ (-. (cC54 (iV16464))))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) ### NotAnd 184 188 % 15.30/15.57 190. (-. (cC56 (iV16464))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) ### Definition-Pseudo(cC56) 189 % 15.30/15.57 191. (cowlThing (iV16465)) (-. (cowlThing (iV16465))) ### Axiom % 15.30/15.57 192. (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y)))) ### Axiom % 15.30/15.57 193. (cC36 (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) ### Definition-Pseudo(cC36) 192 % 15.30/15.57 194. (-. (-. (cC36 (iV16465)))) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) ### NotNot 193 % 15.30/15.57 195. (cTOP (iV16465)) (-. (cTOP (iV16465))) ### Axiom % 15.30/15.57 196. (-. ((-. (cC36 (iV16465))) /\ (cTOP (iV16465)))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) ### NotAnd 194 195 % 15.30/15.57 197. (-. (cC38 (iV16465))) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) ### Definition-Pseudo(cC38) 196 % 15.30/15.57 198. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (Ex Y, ((rR1 (iV16439) Y) /\ (-. (cC102 Y)))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 8 10 12 14 15 17 19 25 26 31 36 37 43 54 55 60 49 71 72 77 69 78 84 94 95 105 115 125 126 132 143 144 149 141 150 156 167 168 173 162 184 185 190 182 191 197 % 15.30/15.57 199. (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (cowlThing (iV16439)) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (-. (cC102 Y)))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cC130) 198 % 15.30/15.57 200. (cC104 (iV16439)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### Definition-Pseudo(cC104) 199 % 15.30/15.57 201. (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ((-. (cC100 (iV16439))) /\ (cC104 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (cowlThing (iV16439)) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### And 200 % 15.30/15.57 202. (cC106 (iV16439)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### Definition-Pseudo(cC106) 201 % 15.30/15.57 203. (cC28 (iV16439)) (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC106 (iV16439)) ### Definition-Pseudo(cC28) 202 % 15.30/15.57 204. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### And 203 % 15.30/15.57 205. (cC108 (iV16439)) (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cC108) 204 % 15.30/15.57 206. ((cC108 (iV16439)) /\ (cC130 (iV16439))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### And 205 % 15.30/15.57 207. (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (-. (cC76 Y))))) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cTEST) 206 % 15.30/15.57 208. (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC94 Y)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) ### Definition-Pseudo(cC78) 207 % 15.30/15.57 209. (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (-. (Ex Y, ((rR1 (iV16448) Y) /\ (-. (cC34 Y))))) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) ### Definition-Pseudo(cC96) 208 % 15.30/15.57 210. (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (-. (cC56 Y))))) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) ### Definition-Pseudo(cC36) 209 % 15.30/15.57 211. (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) ### Definition-Pseudo(cC58) 210 % 15.30/15.57 212. (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (-. (cC38 Y))))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) ### Definition-Pseudo(cC74) 211 % 15.30/15.57 213. (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC52 Y)))) (cowlThing (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) ### Definition-Pseudo(cC40) 212 % 15.30/15.57 214. (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (-. (Ex Y, ((rR1 (iV16457) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) ### Definition-Pseudo(cC54) 213 % 15.30/15.57 215. (-. (cC36 (iV16457))) (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cowlThing (iV16457)) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (-. (Ex Y, ((rR1 (iV16460) Y) /\ (-. (cC34 Y))))) (cTOP (iV16460)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) (-. (cC54 (iV16455))) ### Definition-Pseudo(cC36) 214 % 15.30/15.57 216. (-. (cC36 (iV16460))) (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (-. (cC38 Y))))) (cTOP (iV16460)) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) (-. (cC36 (iV16457))) ### Definition-Pseudo(cC36) 215 % 15.30/15.57 217. (-. (cC40 (iV16461))) (-. (cC36 (iV16457))) (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cowlThing (iV16457)) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (cTOP (iV16460)) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC52 Y)))) (cowlThing (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) (-. (cC54 (iV16455))) (-. (cC36 (iV16460))) ### Definition-Pseudo(cC40) 216 % 15.30/15.57 218. (-. (cC54 (iV16461))) (-. (cC36 (iV16460))) (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (-. (Ex Y, ((rR1 (iV16462) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16462)) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (cTOP (iV16460)) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) (-. (cC36 (iV16457))) (-. (cC40 (iV16461))) ### Definition-Pseudo(cC54) 217 % 15.30/15.57 219. (-. (cC36 (iV16462))) (-. (cC40 (iV16461))) (-. (cC36 (iV16457))) (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cowlThing (iV16457)) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (cTOP (iV16460)) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (cowlThing (iV16462)) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC72 Y)))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) (-. (cC54 (iV16455))) (-. (cC36 (iV16460))) (-. (cC54 (iV16461))) ### Definition-Pseudo(cC36) 218 % 15.30/15.57 220. (-. (cC74 (iV16463))) (-. (cC54 (iV16461))) (-. (cC36 (iV16460))) (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16463) Y) /\ (-. (cC56 Y))))) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (cowlThing (iV16462)) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (cTOP (iV16460)) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) (-. (cC36 (iV16457))) (-. (cC40 (iV16461))) (-. (cC36 (iV16462))) ### Definition-Pseudo(cC74) 219 % 15.30/15.57 221. (-. (cC58 (iV16463))) (-. (cC36 (iV16462))) (-. (cC40 (iV16461))) (-. (cC36 (iV16457))) (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cowlThing (iV16457)) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (cTOP (iV16460)) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (cowlThing (iV16462)) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (cowlThing (iV16463)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (-. (cC38 Y))))) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) (-. (cC54 (iV16455))) (-. (cC36 (iV16460))) (-. (cC54 (iV16461))) (-. (cC74 (iV16463))) ### Definition-Pseudo(cC58) 220 % 15.30/15.57 222. (-. (cC40 (iV16464))) (-. (cC74 (iV16463))) (-. (cC54 (iV16461))) (-. (cC36 (iV16460))) (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC52 Y)))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (cowlThing (iV16463)) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (cowlThing (iV16462)) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (cTOP (iV16460)) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) (-. (cC36 (iV16457))) (-. (cC40 (iV16461))) (-. (cC36 (iV16462))) (-. (cC58 (iV16463))) ### Definition-Pseudo(cC40) 221 % 15.30/15.57 223. (-. (cC54 (iV16464))) (-. (cC58 (iV16463))) (-. (cC36 (iV16462))) (-. (cC40 (iV16461))) (-. (cC36 (iV16457))) (-. (cC40 (iV16455))) (-. (cC58 (iV16453))) (-. (cC96 (iV16440))) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (-. (cC16 (iV16463))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (cowlThing (iV16448)) (cTOP (iV16448)) (-. (cC12 (iV16461))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (-. (cC8 (iV16460))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cowlThing (iV16457)) (cTOP (iV16457)) (-. (cC8 (iV16459))) (cC12 (iV16459)) (cowlThing (iV16459)) (-. (cC2 (iV16459))) (cC4 (iV16459)) (cowlThing (iV16460)) (cTOP (iV16460)) (-. (cC8 (iV16462))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16461)) (cowlThing (iV16462)) (cTOP (iV16462)) (-. (cC12 (iV16464))) (rR1 (iV16463) (iV16464)) (cowlThing (iV16463)) (-. (cC8 (iV16465))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (cowlThing (iV16465)) (-. (Ex Y, ((rR1 (iV16465) Y) /\ (-. (cC34 Y))))) (cTOP (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC78 (iV16440))) (-. (cC36 (iV16448))) (-. (cC74 (iV16453))) (-. (cC54 (iV16455))) (-. (cC36 (iV16460))) (-. (cC54 (iV16461))) (-. (cC74 (iV16463))) (-. (cC40 (iV16464))) ### Definition-Pseudo(cC54) 222 % 15.30/15.58 224. (-. (cC36 (iV16465))) (-. (cC40 (iV16464))) (-. (cC74 (iV16463))) (-. (cC54 (iV16461))) (-. (cC36 (iV16460))) (-. (cC54 (iV16455))) (-. (cC74 (iV16453))) (-. (cC36 (iV16448))) (-. (cC78 (iV16440))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cC130 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC80 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC82 (iV16440)) /\ ((cC98 (iV16440)) /\ ((cowlThing (iV16448)) /\ ((cC38 (iV16448)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC76 (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC44 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC56 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16457)) /\ ((cC38 (iV16457)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC50 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cowlThing (iV16460)) /\ ((cC38 (iV16460)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC42 (iV16461)) /\ ((cowlThing (iV16462)) /\ ((cC38 (iV16462)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC76 (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cowlThing (iV16465)) /\ (cC38 (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cTOP (iV16465)) (cowlThing (iV16465)) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (cC8 (iV16465))) (cowlThing (iV16463)) (rR1 (iV16463) (iV16464)) (-. (cC12 (iV16464))) (cTOP (iV16462)) (cowlThing (iV16462)) (cowlThing (iV16461)) (rR1 (iV16461) (iV16462)) (-. (cC8 (iV16462))) (cTOP (iV16460)) (cowlThing (iV16460)) (cC4 (iV16459)) (-. (cC2 (iV16459))) (cowlThing (iV16459)) (cC12 (iV16459)) (-. (cC8 (iV16459))) (cTOP (iV16457)) (cowlThing (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (-. (cC8 (iV16460))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (-. (cC12 (iV16461))) (cTOP (iV16448)) (cowlThing (iV16448)) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (cC16 (iV16463))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (-. (cC96 (iV16440))) (-. (cC58 (iV16453))) (-. (cC40 (iV16455))) (-. (cC36 (iV16457))) (-. (cC40 (iV16461))) (-. (cC36 (iV16462))) (-. (cC58 (iV16463))) (-. (cC54 (iV16464))) ### Definition-Pseudo(cC36) 223 % 15.30/15.58 % SZS output end Proof % 15.30/15.58 (* END-PROOF *) %------------------------------------------------------------------------------