%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS161+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 : n032.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:04 EDT 2022 % Result : Theorem 24.24s 24.45s % Output : Proof 24.30s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : KRS161+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.10 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.09/0.28 % Computer : n032.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 07:58:50 EDT 2022 % 0.09/0.28 % CPUTime : % 24.24/24.45 % SZS status Theorem % 24.24/24.45 (* PROOF-FOUND *) % 24.24/24.45 (* BEGIN-PROOF *) % 24.24/24.45 % SZS output start Proof % 24.24/24.45 1. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 24.24/24.45 2. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 24.24/24.45 3. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### NotNot 2 % 24.24/24.45 4. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Definition-Pseudo(xsd_string) 3 % 24.24/24.45 5. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 24.24/24.45 6. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Definition-Pseudo(xsd_string) 5 % 24.24/24.45 7. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 4 6 % 24.24/24.45 8. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 7 % 24.24/24.45 9. (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y)))) ### Axiom % 24.24/24.45 10. (-. (cC130 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) ### Definition-Pseudo(cC130) 9 % 24.24/24.45 11. ((cC28 (iV16439)) /\ (cC106 (iV16439))) (-. ((cC28 (iV16439)) /\ (cC106 (iV16439)))) ### Axiom % 24.24/24.45 12. (-. (cC108 (iV16439))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) ### Definition-Pseudo(cC108) 11 % 24.24/24.45 13. (Ex Y, ((rR1 (iV16439) Y) /\ (cC102xcomp Y))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (cC102xcomp Y)))) ### Axiom % 24.24/24.45 14. (-. (cC104 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC102xcomp Y))) ### Definition-Pseudo(cC104) 13 % 24.24/24.45 15. ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) (-. ((cC104 (iV16439)) /\ (cC100xcomp (iV16439)))) ### Axiom % 24.24/24.45 16. (-. (cC106 (iV16439))) ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) ### Definition-Pseudo(cC106) 15 % 24.24/24.45 17. (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (-. (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y)))) ### Axiom % 24.24/24.45 18. (-. (cC28 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ### Definition-Pseudo(cC28) 17 % 24.24/24.45 19. (cowlThing (iV16439)) (-. (cowlThing (iV16439))) ### Axiom % 24.24/24.45 20. (rR1 (iV16439) (iV16440)) (-. (rR1 (iV16439) (iV16440))) ### Axiom % 24.24/24.45 21. (-. (cC98 (iV16440))) (cC98 (iV16440)) ### Axiom % 24.24/24.45 22. ((rR1 (iV16439) (iV16440)) => (cC98 (iV16440))) (-. (cC98 (iV16440))) (rR1 (iV16439) (iV16440)) ### Imply 20 21 % 24.24/24.45 23. (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (cC98 (iV16440))) ### All 22 % 24.24/24.45 24. (rR1 (iV16440) (iV16463)) (-. (rR1 (iV16440) (iV16463))) ### Axiom % 24.24/24.45 25. (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (Ex Y0, (ra_Px27 (iV16463) Y0)) ### Axiom % 24.24/24.45 26. (-. (-. (Ex Y0, (ra_Px27 (iV16463) Y0)))) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) ### NotNot 25 % 24.24/24.45 27. (-. (cC16xcomp (iV16463))) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) ### Definition-Pseudo(cC16xcomp) 26 % 24.24/24.45 28. (-. ((rR1 (iV16440) (iV16463)) /\ (cC16xcomp (iV16463)))) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) ### NotAnd 24 27 % 24.24/24.45 29. (-. (Ex Y, ((rR1 (iV16440) Y) /\ (cC16xcomp Y)))) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) ### NotExists 28 % 24.24/24.45 30. (-. (cC80 (iV16440))) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) ### Definition-Pseudo(cC80) 29 % 24.24/24.45 31. (Ex Y, (ra_Px28 (iV16440) Y)) (-. (Ex Y, (ra_Px28 (iV16440) Y))) ### Axiom % 24.24/24.45 32. (-. (cC78xcomp (iV16440))) (Ex Y, (ra_Px28 (iV16440) Y)) ### Definition-Pseudo(cC78xcomp) 31 % 24.24/24.45 33. (-. ((cC80 (iV16440)) /\ (cC78xcomp (iV16440)))) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) ### NotAnd 30 32 % 24.24/24.45 34. (-. (cC82 (iV16440))) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) ### Definition-Pseudo(cC82) 33 % 24.24/24.45 35. (cowlThing (iV16440)) (-. (cowlThing (iV16440))) ### Axiom % 24.24/24.45 36. (cTOP (iV16448)) (-. (cTOP (iV16448))) ### Axiom % 24.24/24.45 37. (Ex Y, (ra_Px7 (iV16448) Y)) (-. (Ex Y, (ra_Px7 (iV16448) Y))) ### Axiom % 24.24/24.45 38. (-. (cC36xcomp (iV16448))) (Ex Y, (ra_Px7 (iV16448) Y)) ### Definition-Pseudo(cC36xcomp) 37 % 24.24/24.45 39. (-. ((cTOP (iV16448)) /\ (cC36xcomp (iV16448)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) ### NotAnd 36 38 % 24.24/24.45 40. (-. (cC38 (iV16448))) (cC38 (iV16448)) ### Axiom % 24.24/24.45 41. ((cC38 (iV16448)) <=> ((cTOP (iV16448)) /\ (cC36xcomp (iV16448)))) (-. (cC38 (iV16448))) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) ### Equiv 39 40 % 24.24/24.45 42. (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (-. (cC38 (iV16448))) ### All 41 % 24.24/24.45 43. (cowlThing (iV16448)) (-. (cowlThing (iV16448))) ### Axiom % 24.24/24.45 44. (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y, (ra_Px25 (iV16453) Y))) ### Axiom % 24.24/24.45 45. (-. (cC74xcomp (iV16453))) (Ex Y, (ra_Px25 (iV16453) Y)) ### Definition-Pseudo(cC74xcomp) 44 % 24.24/24.45 46. (rR1 (iV16453) (iV16461)) (-. (rR1 (iV16453) (iV16461))) ### Axiom % 24.24/24.45 47. (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y0, (ra_Px18 (iV16461) Y0)) ### Axiom % 24.24/24.45 48. (-. (-. (Ex Y0, (ra_Px18 (iV16461) Y0)))) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) ### NotNot 47 % 24.24/24.45 49. (-. (cC12xcomp (iV16461))) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) ### Definition-Pseudo(cC12xcomp) 48 % 24.24/24.45 50. (-. ((rR1 (iV16453) (iV16461)) /\ (cC12xcomp (iV16461)))) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) ### NotAnd 46 49 % 24.24/24.45 51. (-. (Ex Y, ((rR1 (iV16453) Y) /\ (cC12xcomp Y)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) ### NotExists 50 % 24.24/24.45 52. (-. (cC60 (iV16453))) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) ### Definition-Pseudo(cC60) 51 % 24.24/24.45 53. (Ex Y, (ra_Px19 (iV16453) Y)) (-. (Ex Y, (ra_Px19 (iV16453) Y))) ### Axiom % 24.24/24.45 54. (-. (cC58xcomp (iV16453))) (Ex Y, (ra_Px19 (iV16453) Y)) ### Definition-Pseudo(cC58xcomp) 53 % 24.24/24.45 55. (-. ((cC60 (iV16453)) /\ (cC58xcomp (iV16453)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) ### NotAnd 52 54 % 24.24/24.45 56. (-. (cC62 (iV16453))) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) ### Definition-Pseudo(cC62) 55 % 24.24/24.45 57. (-. ((cC74xcomp (iV16453)) /\ (cC62 (iV16453)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) ### NotAnd 45 56 % 24.24/24.45 58. (-. (cC76 (iV16453))) (cC76 (iV16453)) ### Axiom % 24.24/24.45 59. ((cC76 (iV16453)) <=> ((cC74xcomp (iV16453)) /\ (cC62 (iV16453)))) (-. (cC76 (iV16453))) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) ### Equiv 57 58 % 24.24/24.45 60. (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (cC76 (iV16453))) ### All 59 % 24.24/24.45 61. (cowlThing (iV16453)) (-. (cowlThing (iV16453))) ### Axiom % 24.24/24.45 62. (Ex Y, (ra_Px16 (iV16455) Y)) (-. (Ex Y, (ra_Px16 (iV16455) Y))) ### Axiom % 24.24/24.45 63. (-. (cC54xcomp (iV16455))) (Ex Y, (ra_Px16 (iV16455) Y)) ### Definition-Pseudo(cC54xcomp) 62 % 24.24/24.45 64. (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y, (ra_Px10 (iV16455) Y))) ### Axiom % 24.24/24.45 65. (-. (cC40xcomp (iV16455))) (Ex Y, (ra_Px10 (iV16455) Y)) ### Definition-Pseudo(cC40xcomp) 64 % 24.24/24.45 66. (rR1 (iV16455) (iV16460)) (-. (rR1 (iV16455) (iV16460))) ### Axiom % 24.24/24.45 67. (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y0, (ra_Px9 (iV16460) Y0)) ### Axiom % 24.24/24.45 68. (-. (-. (Ex Y0, (ra_Px9 (iV16460) Y0)))) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) ### NotNot 67 % 24.24/24.45 69. (-. (cC8xcomp (iV16460))) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) ### Definition-Pseudo(cC8xcomp) 68 % 24.24/24.45 70. (-. ((rR1 (iV16455) (iV16460)) /\ (cC8xcomp (iV16460)))) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) ### NotAnd 66 69 % 24.24/24.45 71. (-. (Ex Y, ((rR1 (iV16455) Y) /\ (cC8xcomp Y)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) ### NotExists 70 % 24.24/24.45 72. (-. (cC42 (iV16455))) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) ### Definition-Pseudo(cC42) 71 % 24.24/24.45 73. (-. ((cC40xcomp (iV16455)) /\ (cC42 (iV16455)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) ### NotAnd 65 72 % 24.24/24.45 74. (-. (cC44 (iV16455))) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) ### Definition-Pseudo(cC44) 73 % 24.24/24.45 75. (-. ((cC54xcomp (iV16455)) /\ (cC44 (iV16455)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) ### NotAnd 63 74 % 24.24/24.45 76. (-. (cC56 (iV16455))) (cC56 (iV16455)) ### Axiom % 24.24/24.45 77. ((cC56 (iV16455)) <=> ((cC54xcomp (iV16455)) /\ (cC44 (iV16455)))) (-. (cC56 (iV16455))) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) ### Equiv 75 76 % 24.24/24.45 78. (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (-. (cC56 (iV16455))) ### All 77 % 24.24/24.45 79. (cowlThing (iV16455)) (-. (cowlThing (iV16455))) ### Axiom % 24.24/24.45 80. (cTOP (iV16457)) (-. (cTOP (iV16457))) ### Axiom % 24.24/24.45 81. (Ex Y, (ra_Px7 (iV16457) Y)) (-. (Ex Y, (ra_Px7 (iV16457) Y))) ### Axiom % 24.24/24.45 82. (-. (cC36xcomp (iV16457))) (Ex Y, (ra_Px7 (iV16457) Y)) ### Definition-Pseudo(cC36xcomp) 81 % 24.24/24.45 83. (-. ((cTOP (iV16457)) /\ (cC36xcomp (iV16457)))) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) ### NotAnd 80 82 % 24.24/24.45 84. (-. (cC38 (iV16457))) (cC38 (iV16457)) ### Axiom % 24.24/24.45 85. ((cC38 (iV16457)) <=> ((cTOP (iV16457)) /\ (cC36xcomp (iV16457)))) (-. (cC38 (iV16457))) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) ### Equiv 83 84 % 24.24/24.45 86. (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (-. (cC38 (iV16457))) ### All 85 % 24.24/24.45 87. (cowlThing (iV16457)) (-. (cowlThing (iV16457))) ### Axiom % 24.24/24.45 88. (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y, (ra_Px13 (iV16459) Y))) ### Axiom % 24.24/24.45 89. (-. (cC46xcomp (iV16459))) (Ex Y, (ra_Px13 (iV16459) Y)) ### Definition-Pseudo(cC46xcomp) 88 % 24.24/24.45 90. (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y0, (ra_Px14 (iV16459) Y0)) ### Axiom % 24.24/24.45 91. (-. (-. (Ex Y0, (ra_Px14 (iV16459) Y0)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) ### NotNot 90 % 24.24/24.45 92. (-. (cC48xcomp (iV16459))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) ### Definition-Pseudo(cC48xcomp) 91 % 24.24/24.45 93. (-. ((cC46xcomp (iV16459)) /\ (cC48xcomp (iV16459)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) ### NotAnd 89 92 % 24.24/24.45 94. (-. (cC50 (iV16459))) (cC50 (iV16459)) ### Axiom % 24.24/24.45 95. ((cC50 (iV16459)) <=> ((cC46xcomp (iV16459)) /\ (cC48xcomp (iV16459)))) (-. (cC50 (iV16459))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) ### Equiv 93 94 % 24.24/24.45 96. (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (cC50 (iV16459))) ### All 95 % 24.24/24.45 97. (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y, (ra_Px31 (iV16459) Y))) ### Axiom % 24.24/24.45 98. (-. (cC84xcomp (iV16459))) (Ex Y, (ra_Px31 (iV16459) Y)) ### Definition-Pseudo(cC84xcomp) 97 % 24.24/24.45 99. (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y0, (ra_Px32 (iV16459) Y0)) ### Axiom % 24.24/24.45 100. (-. (-. (Ex Y0, (ra_Px32 (iV16459) Y0)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) ### NotNot 99 % 24.24/24.45 101. (-. (cC86xcomp (iV16459))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) ### Definition-Pseudo(cC86xcomp) 100 % 24.24/24.45 102. (-. ((cC84xcomp (iV16459)) /\ (cC86xcomp (iV16459)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) ### NotAnd 98 101 % 24.24/24.45 103. (-. (cC88 (iV16459))) (cC88 (iV16459)) ### Axiom % 24.24/24.45 104. ((cC88 (iV16459)) <=> ((cC84xcomp (iV16459)) /\ (cC86xcomp (iV16459)))) (-. (cC88 (iV16459))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) ### Equiv 102 103 % 24.24/24.45 105. (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (cC88 (iV16459))) ### All 104 % 24.24/24.45 106. (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y, (ra_Px4 (iV16459) Y))) ### Axiom % 24.24/24.45 107. (-. (cC30xcomp (iV16459))) (Ex Y, (ra_Px4 (iV16459) Y)) ### Definition-Pseudo(cC30xcomp) 106 % 24.24/24.45 108. (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y0, (ra_Px5 (iV16459) Y0)) ### Axiom % 24.24/24.45 109. (-. (-. (Ex Y0, (ra_Px5 (iV16459) Y0)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) ### NotNot 108 % 24.24/24.45 110. (-. (cC32xcomp (iV16459))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) ### Definition-Pseudo(cC32xcomp) 109 % 24.24/24.45 111. (-. ((cC30xcomp (iV16459)) /\ (cC32xcomp (iV16459)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) ### NotAnd 107 110 % 24.24/24.45 112. (-. (cC34 (iV16459))) (cC34 (iV16459)) ### Axiom % 24.24/24.45 113. ((cC34 (iV16459)) <=> ((cC30xcomp (iV16459)) /\ (cC32xcomp (iV16459)))) (-. (cC34 (iV16459))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) ### Equiv 111 112 % 24.24/24.45 114. (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (cC34 (iV16459))) ### All 113 % 24.24/24.45 115. (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y, (ra_Px22 (iV16459) Y))) ### Axiom % 24.24/24.45 116. (-. (cC64xcomp (iV16459))) (Ex Y, (ra_Px22 (iV16459) Y)) ### Definition-Pseudo(cC64xcomp) 115 % 24.24/24.45 117. (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y0, (ra_Px23 (iV16459) Y0)) ### Axiom % 24.24/24.45 118. (-. (-. (Ex Y0, (ra_Px23 (iV16459) Y0)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) ### NotNot 117 % 24.24/24.45 119. (-. (cC66xcomp (iV16459))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) ### Definition-Pseudo(cC66xcomp) 118 % 24.24/24.45 120. (-. ((cC64xcomp (iV16459)) /\ (cC66xcomp (iV16459)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) ### NotAnd 116 119 % 24.24/24.45 121. (-. (cC68 (iV16459))) (cC68 (iV16459)) ### Axiom % 24.24/24.45 122. ((cC68 (iV16459)) <=> ((cC64xcomp (iV16459)) /\ (cC66xcomp (iV16459)))) (-. (cC68 (iV16459))) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) ### Equiv 120 121 % 24.24/24.45 123. (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (cC68 (iV16459))) ### All 122 % 24.24/24.45 124. (cowlThing (iV16459)) (-. (cowlThing (iV16459))) ### Axiom % 24.24/24.45 125. (rR1 (iV16455) (iV16460)) (-. (rR1 (iV16455) (iV16460))) ### Axiom % 24.24/24.45 126. (-. (cC38 (iV16460))) (cC38 (iV16460)) ### Axiom % 24.24/24.45 127. ((rR1 (iV16455) (iV16460)) => (cC38 (iV16460))) (-. (cC38 (iV16460))) (rR1 (iV16455) (iV16460)) ### Imply 125 126 % 24.24/24.45 128. (All X, ((rR1 (iV16455) X) => (cC38 X))) (rR1 (iV16455) (iV16460)) (-. (cC38 (iV16460))) ### All 127 % 24.24/24.45 129. (cowlThing (iV16460)) (-. (cowlThing (iV16460))) ### Axiom % 24.24/24.45 130. (rR1 (iV16461) (iV16462)) (-. (rR1 (iV16461) (iV16462))) ### Axiom % 24.24/24.45 131. (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (Ex Y0, (ra_Px9 (iV16462) Y0)) ### Axiom % 24.24/24.45 132. (-. (-. (Ex Y0, (ra_Px9 (iV16462) Y0)))) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) ### NotNot 131 % 24.24/24.45 133. (-. (cC8xcomp (iV16462))) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) ### Definition-Pseudo(cC8xcomp) 132 % 24.24/24.45 134. (-. ((rR1 (iV16461) (iV16462)) /\ (cC8xcomp (iV16462)))) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) ### NotAnd 130 133 % 24.24/24.45 135. (-. (Ex Y, ((rR1 (iV16461) Y) /\ (cC8xcomp Y)))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) ### NotExists 134 % 24.24/24.45 136. (-. (cC42 (iV16461))) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) ### Definition-Pseudo(cC42) 135 % 24.24/24.45 137. (rR1 (iV16453) (iV16461)) (-. (rR1 (iV16453) (iV16461))) ### Axiom % 24.24/24.45 138. (-. (cC56 (iV16461))) (cC56 (iV16461)) ### Axiom % 24.24/24.45 139. ((rR1 (iV16453) (iV16461)) => (cC56 (iV16461))) (-. (cC56 (iV16461))) (rR1 (iV16453) (iV16461)) ### Imply 137 138 % 24.24/24.45 140. (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16453) (iV16461)) (-. (cC56 (iV16461))) ### All 139 % 24.24/24.45 141. (Ex Y, (ra_Px10 (iV16461) Y)) (-. (Ex Y, (ra_Px10 (iV16461) Y))) ### Axiom % 24.24/24.45 142. (-. (cC40xcomp (iV16461))) (Ex Y, (ra_Px10 (iV16461) Y)) ### Definition-Pseudo(cC40xcomp) 141 % 24.24/24.45 143. (-. ((cC40xcomp (iV16461)) /\ (cC42 (iV16461)))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (Ex Y, (ra_Px10 (iV16461) Y)) ### NotAnd 142 136 % 24.24/24.45 144. (-. (cC44 (iV16461))) (Ex Y, (ra_Px10 (iV16461) Y)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) ### Definition-Pseudo(cC44) 143 % 24.24/24.45 145. (cowlThing (iV16461)) (-. (cowlThing (iV16461))) ### Axiom % 24.24/24.45 146. (rR1 (iV16461) (iV16462)) (-. (rR1 (iV16461) (iV16462))) ### Axiom % 24.24/24.45 147. (-. (cC38 (iV16462))) (cC38 (iV16462)) ### Axiom % 24.24/24.45 148. ((rR1 (iV16461) (iV16462)) => (cC38 (iV16462))) (-. (cC38 (iV16462))) (rR1 (iV16461) (iV16462)) ### Imply 146 147 % 24.24/24.45 149. (All X, ((rR1 (iV16461) X) => (cC38 X))) (rR1 (iV16461) (iV16462)) (-. (cC38 (iV16462))) ### All 148 % 24.24/24.45 150. (cowlThing (iV16462)) (-. (cowlThing (iV16462))) ### Axiom % 24.24/24.45 151. (rR1 (iV16440) (iV16463)) (-. (rR1 (iV16440) (iV16463))) ### Axiom % 24.24/24.45 152. (-. (cC76 (iV16463))) (cC76 (iV16463)) ### Axiom % 24.24/24.45 153. ((rR1 (iV16440) (iV16463)) => (cC76 (iV16463))) (-. (cC76 (iV16463))) (rR1 (iV16440) (iV16463)) ### Imply 151 152 % 24.24/24.45 154. (All X, ((rR1 (iV16440) X) => (cC76 X))) (rR1 (iV16440) (iV16463)) (-. (cC76 (iV16463))) ### All 153 % 24.24/24.46 155. (rR1 (iV16463) (iV16464)) (-. (rR1 (iV16463) (iV16464))) ### Axiom % 24.24/24.46 156. (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (Ex Y0, (ra_Px18 (iV16464) Y0)) ### Axiom % 24.24/24.46 157. (-. (-. (Ex Y0, (ra_Px18 (iV16464) Y0)))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) ### NotNot 156 % 24.24/24.46 158. (-. (cC12xcomp (iV16464))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) ### Definition-Pseudo(cC12xcomp) 157 % 24.24/24.46 159. (-. ((rR1 (iV16463) (iV16464)) /\ (cC12xcomp (iV16464)))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) ### NotAnd 155 158 % 24.24/24.46 160. (-. (Ex Y, ((rR1 (iV16463) Y) /\ (cC12xcomp Y)))) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) ### NotExists 159 % 24.24/24.46 161. (-. (cC60 (iV16463))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) ### Definition-Pseudo(cC60) 160 % 24.24/24.46 162. (Ex Y, (ra_Px19 (iV16463) Y)) (-. (Ex Y, (ra_Px19 (iV16463) Y))) ### Axiom % 24.24/24.46 163. (-. (cC58xcomp (iV16463))) (Ex Y, (ra_Px19 (iV16463) Y)) ### Definition-Pseudo(cC58xcomp) 162 % 24.24/24.46 164. (-. ((cC60 (iV16463)) /\ (cC58xcomp (iV16463)))) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) ### NotAnd 161 163 % 24.24/24.46 165. (-. (cC62 (iV16463))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) ### Definition-Pseudo(cC62) 164 % 24.24/24.46 166. (cowlThing (iV16463)) (-. (cowlThing (iV16463))) ### Axiom % 24.24/24.46 167. (rR1 (iV16463) (iV16464)) (-. (rR1 (iV16463) (iV16464))) ### Axiom % 24.24/24.46 168. (-. (cC56 (iV16464))) (cC56 (iV16464)) ### Axiom % 24.24/24.46 169. ((rR1 (iV16463) (iV16464)) => (cC56 (iV16464))) (-. (cC56 (iV16464))) (rR1 (iV16463) (iV16464)) ### Imply 167 168 % 24.24/24.46 170. (All X, ((rR1 (iV16463) X) => (cC56 X))) (rR1 (iV16463) (iV16464)) (-. (cC56 (iV16464))) ### All 169 % 24.24/24.46 171. (rR1 (iV16464) (iV16465)) (-. (rR1 (iV16464) (iV16465))) ### Axiom % 24.24/24.46 172. (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (Ex Y0, (ra_Px9 (iV16465) Y0)) ### Axiom % 24.24/24.46 173. (-. (-. (Ex Y0, (ra_Px9 (iV16465) Y0)))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) ### NotNot 172 % 24.24/24.46 174. (-. (cC8xcomp (iV16465))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) ### Definition-Pseudo(cC8xcomp) 173 % 24.24/24.46 175. (-. ((rR1 (iV16464) (iV16465)) /\ (cC8xcomp (iV16465)))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) ### NotAnd 171 174 % 24.24/24.46 176. (-. (Ex Y, ((rR1 (iV16464) Y) /\ (cC8xcomp Y)))) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) ### NotExists 175 % 24.24/24.46 177. (-. (cC42 (iV16464))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) ### Definition-Pseudo(cC42) 176 % 24.24/24.46 178. (Ex Y, (ra_Px10 (iV16464) Y)) (-. (Ex Y, (ra_Px10 (iV16464) Y))) ### Axiom % 24.24/24.46 179. (-. (cC40xcomp (iV16464))) (Ex Y, (ra_Px10 (iV16464) Y)) ### Definition-Pseudo(cC40xcomp) 178 % 24.24/24.46 180. (-. ((cC40xcomp (iV16464)) /\ (cC42 (iV16464)))) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (Ex Y, (ra_Px10 (iV16464) Y)) ### NotAnd 179 177 % 24.24/24.46 181. (-. (cC44 (iV16464))) (Ex Y, (ra_Px10 (iV16464) Y)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) ### Definition-Pseudo(cC44) 180 % 24.24/24.46 182. (cowlThing (iV16464)) (-. (cowlThing (iV16464))) ### Axiom % 24.24/24.46 183. (rR1 (iV16464) (iV16465)) (-. (rR1 (iV16464) (iV16465))) ### Axiom % 24.24/24.46 184. (-. (cC38 (iV16465))) (cC38 (iV16465)) ### Axiom % 24.24/24.46 185. ((rR1 (iV16464) (iV16465)) => (cC38 (iV16465))) (-. (cC38 (iV16465))) (rR1 (iV16464) (iV16465)) ### Imply 183 184 % 24.24/24.46 186. (All X, ((rR1 (iV16464) X) => (cC38 X))) (rR1 (iV16464) (iV16465)) (-. (cC38 (iV16465))) ### All 185 % 24.24/24.46 187. (cowlThing (iV16465)) (-. (cowlThing (iV16465))) ### Axiom % 24.24/24.46 188. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC102xcomp Y))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC128 Y))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 1 8 10 12 14 16 18 19 23 30 34 35 42 43 60 56 61 52 78 74 72 79 86 87 96 105 114 123 124 128 129 136 140 144 145 149 150 154 165 166 161 170 177 181 182 186 187 % 24.24/24.46 189. (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC102xcomp Y))) ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cC130) 188 % 24.24/24.46 190. (cC104 (iV16439)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### Definition-Pseudo(cC104) 189 % 24.24/24.46 191. (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) ((cC104 (iV16439)) /\ (cC100xcomp (iV16439))) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### And 190 % 24.24/24.46 192. (cC106 (iV16439)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (Ex Y, ((rR1 (iV16439) Y) /\ (cC26 Y))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### Definition-Pseudo(cC106) 191 % 24.24/24.46 193. (cC28 (iV16439)) (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC106 (iV16439)) ### Definition-Pseudo(cC28) 192 % 24.24/24.46 194. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) ((cC28 (iV16439)) /\ (cC106 (iV16439))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cC130 (iV16439)) ### And 193 % 24.24/24.46 195. (cC108 (iV16439)) (cC130 (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cC108) 194 % 24.24/24.46 196. ((cC108 (iV16439)) /\ (cC130 (iV16439))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (Ex Y, (ra_Px28 (iV16440) Y)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### And 195 % 24.24/24.46 197. (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (Ex Y, (ra_Px28 (iV16440) Y)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (Ex Y, (ra_Px7 (iV16448) Y)) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) ### Definition-Pseudo(cTEST) 196 % 24.24/24.46 198. (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (Ex Y, (ra_Px25 (iV16453) Y)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (Ex Y, (ra_Px7 (iV16448) Y)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) ### Definition-Pseudo(cC78xcomp) 197 % 24.24/24.46 199. (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (Ex Y, (ra_Px19 (iV16453) Y)) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (Ex Y, (ra_Px25 (iV16453) Y)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) ### Definition-Pseudo(cC36xcomp) 198 % 24.24/24.46 200. (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (Ex Y, (ra_Px10 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (Ex Y, (ra_Px19 (iV16453) Y)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) ### Definition-Pseudo(cC74xcomp) 199 % 24.24/24.46 201. (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (Ex Y, (ra_Px10 (iV16455) Y)) (Ex Y, (ra_Px16 (iV16455) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) ### Definition-Pseudo(cC58xcomp) 200 % 24.24/24.46 202. (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (Ex Y, (ra_Px7 (iV16457) Y)) (cowlThing (iV16455)) (Ex Y, (ra_Px16 (iV16455) Y)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) ### Definition-Pseudo(cC40xcomp) 201 % 24.24/24.46 203. (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (cowlThing (iV16455)) (Ex Y, (ra_Px7 (iV16457) Y)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (Ex Y, (ra_Px4 (iV16459) Y)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) ### Definition-Pseudo(cC54xcomp) 202 % 24.24/24.46 204. (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (Ex Y, (ra_Px4 (iV16459) Y)) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (Ex Y, (ra_Px31 (iV16459) Y)) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) ### Definition-Pseudo(cC36xcomp) 203 % 24.24/24.46 205. (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (Ex Y, (ra_Px13 (iV16459) Y)) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (Ex Y, (ra_Px31 (iV16459) Y)) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) ### Definition-Pseudo(cC30xcomp) 204 % 24.24/24.46 206. (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (Ex Y, (ra_Px22 (iV16459) Y)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (Ex Y, (ra_Px13 (iV16459) Y)) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) ### Definition-Pseudo(cC84xcomp) 205 % 24.24/24.46 207. (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (Ex Y, (ra_Px22 (iV16459) Y)) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) ### Definition-Pseudo(cC46xcomp) 206 % 24.24/24.46 208. (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px32 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) ### Definition-Pseudo(cC64xcomp) 207 % 24.24/24.46 209. (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (-. (Ex Y0, (ra_Px5 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) ### Definition-Pseudo(cC86xcomp) 208 % 24.24/24.46 210. (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (-. (Ex Y0, (ra_Px14 (iV16459) Y0))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) ### Definition-Pseudo(cC32xcomp) 209 % 24.24/24.46 211. (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (-. (Ex Y0, (ra_Px23 (iV16459) Y0))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) ### Definition-Pseudo(cC48xcomp) 210 % 24.24/24.46 212. (cC66xcomp (iV16459)) (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (Ex Y, (ra_Px10 (iV16461) Y)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (-. (Ex Y0, (ra_Px9 (iV16460) Y0))) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) (cC48xcomp (iV16459)) ### Definition-Pseudo(cC66xcomp) 211 % 24.24/24.46 213. (cC8xcomp (iV16460)) (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (Ex Y, (ra_Px10 (iV16461) Y)) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) (cC66xcomp (iV16459)) ### Definition-Pseudo(cC8xcomp) 212 % 24.24/24.46 214. (cC40xcomp (iV16461)) (cC66xcomp (iV16459)) (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (-. (Ex Y0, (ra_Px18 (iV16461) Y0))) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) (cC48xcomp (iV16459)) (cC8xcomp (iV16460)) ### Definition-Pseudo(cC40xcomp) 213 % 24.24/24.46 215. (cC12xcomp (iV16461)) (cC8xcomp (iV16460)) (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (-. (Ex Y0, (ra_Px9 (iV16462) Y0))) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) (cC66xcomp (iV16459)) (cC40xcomp (iV16461)) ### Definition-Pseudo(cC12xcomp) 214 % 24.24/24.46 216. (cC8xcomp (iV16462)) (cC40xcomp (iV16461)) (cC66xcomp (iV16459)) (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (Ex Y, (ra_Px19 (iV16463) Y)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (-. (Ex Y0, (ra_Px27 (iV16463) Y0))) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) (cC48xcomp (iV16459)) (cC8xcomp (iV16460)) (cC12xcomp (iV16461)) ### Definition-Pseudo(cC8xcomp) 215 % 24.24/24.46 217. (cC16xcomp (iV16463)) (cC12xcomp (iV16461)) (cC8xcomp (iV16460)) (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (Ex Y, (ra_Px19 (iV16463) Y)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (Ex Y, (ra_Px10 (iV16464) Y)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) (cC66xcomp (iV16459)) (cC40xcomp (iV16461)) (cC8xcomp (iV16462)) ### Definition-Pseudo(cC16xcomp) 216 % 24.24/24.46 218. (cC58xcomp (iV16463)) (cC8xcomp (iV16462)) (cC40xcomp (iV16461)) (cC66xcomp (iV16459)) (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (Ex Y, (ra_Px10 (iV16464) Y)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (rR1 (iV16463) (iV16464)) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) (cC48xcomp (iV16459)) (cC8xcomp (iV16460)) (cC12xcomp (iV16461)) (cC16xcomp (iV16463)) ### Definition-Pseudo(cC58xcomp) 217 % 24.24/24.46 219. (cC40xcomp (iV16464)) (cC16xcomp (iV16463)) (cC12xcomp (iV16461)) (cC8xcomp (iV16460)) (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (-. (Ex Y0, (ra_Px18 (iV16464) Y0))) (rR1 (iV16463) (iV16464)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) (cC66xcomp (iV16459)) (cC40xcomp (iV16461)) (cC8xcomp (iV16462)) (cC58xcomp (iV16463)) ### Definition-Pseudo(cC40xcomp) 218 % 24.24/24.46 220. (cC12xcomp (iV16464)) (cC58xcomp (iV16463)) (cC8xcomp (iV16462)) (cC40xcomp (iV16461)) (cC66xcomp (iV16459)) (cC32xcomp (iV16459)) (cC64xcomp (iV16459)) (cC84xcomp (iV16459)) (cC36xcomp (iV16457)) (cC40xcomp (iV16455)) (cC74xcomp (iV16453)) (cC78xcomp (iV16440)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV16465)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16464)) (rR1 (iV16464) (iV16465)) (-. (Ex Y0, (ra_Px9 (iV16465) Y0))) (All X, ((rR1 (iV16463) X) => (cC56 X))) (cowlThing (iV16463)) (rR1 (iV16463) (iV16464)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (rR1 (iV16461) (iV16462)) (cowlThing (iV16460)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16459)) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (cowlThing (iV16457)) (cTOP (iV16457)) (cowlThing (iV16455)) (rR1 (iV16455) (iV16460)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (cowlThing (iV16453)) (rR1 (iV16453) (iV16461)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (cowlThing (iV16448)) (cTOP (iV16448)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cowlThing (iV16440)) (rR1 (iV16440) (iV16463)) (rR1 (iV16439) (iV16440)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (cowlThing (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cTEST (iV16439)) (cC36xcomp (iV16448)) (cC58xcomp (iV16453)) (cC54xcomp (iV16455)) (cC30xcomp (iV16459)) (cC46xcomp (iV16459)) (cC86xcomp (iV16459)) (cC48xcomp (iV16459)) (cC8xcomp (iV16460)) (cC12xcomp (iV16461)) (cC16xcomp (iV16463)) (cC40xcomp (iV16464)) ### Definition-Pseudo(cC12xcomp) 219 % 24.30/24.47 221. (cC8xcomp (iV16465)) (cC40xcomp (iV16464)) (cC16xcomp (iV16463)) (cC12xcomp (iV16461)) (cC8xcomp (iV16460)) (cC48xcomp (iV16459)) (cC86xcomp (iV16459)) (cC46xcomp (iV16459)) (cC30xcomp (iV16459)) (cC54xcomp (iV16455)) (cC58xcomp (iV16453)) (cC36xcomp (iV16448)) (cTEST (iV16439)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV16439)) (All X, ((rR1 (iV16439) X) => (cC98 X))) (rR1 (iV16439) (iV16440)) (rR1 (iV16440) (iV16463)) (cowlThing (iV16440)) (All X, ((cC38 X) <=> ((cTOP X) /\ (cC36xcomp X)))) (cTOP (iV16448)) (cowlThing (iV16448)) (All X, ((cC76 X) <=> ((cC74xcomp X) /\ (cC62 X)))) (rR1 (iV16453) (iV16461)) (cowlThing (iV16453)) (All X, ((cC56 X) <=> ((cC54xcomp X) /\ (cC44 X)))) (rR1 (iV16455) (iV16460)) (cowlThing (iV16455)) (cTOP (iV16457)) (cowlThing (iV16457)) (All X, ((cC50 X) <=> ((cC46xcomp X) /\ (cC48xcomp X)))) (All X, ((cC88 X) <=> ((cC84xcomp X) /\ (cC86xcomp X)))) (All X, ((cC34 X) <=> ((cC30xcomp X) /\ (cC32xcomp X)))) (All X, ((cC68 X) <=> ((cC64xcomp X) /\ (cC66xcomp X)))) (cowlThing (iV16459)) (All X, ((rR1 (iV16455) X) => (cC38 X))) (cowlThing (iV16460)) (rR1 (iV16461) (iV16462)) (All X, ((rR1 (iV16453) X) => (cC56 X))) (cowlThing (iV16461)) (All X, ((rR1 (iV16461) X) => (cC38 X))) (cowlThing (iV16462)) (All X, ((rR1 (iV16440) X) => (cC76 X))) (rR1 (iV16463) (iV16464)) (cowlThing (iV16463)) (All X, ((rR1 (iV16463) X) => (cC56 X))) (rR1 (iV16464) (iV16465)) (cowlThing (iV16464)) (All X, ((rR1 (iV16464) X) => (cC38 X))) (cowlThing (iV16465)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cC130 (iV16439)) /\ ((cC108 (iV16439)) /\ ((cC104 (iV16439)) /\ ((cC106 (iV16439)) /\ ((cC28 (iV16439)) /\ ((cowlThing (iV16439)) /\ ((cC98 (iV16440)) /\ ((cC80 (iV16440)) /\ ((cC82 (iV16440)) /\ ((cowlThing (iV16440)) /\ ((cC38 (iV16448)) /\ ((cowlThing (iV16448)) /\ ((cC76 (iV16453)) /\ ((cC62 (iV16453)) /\ ((cowlThing (iV16453)) /\ ((cC60 (iV16453)) /\ ((cC56 (iV16455)) /\ ((cC44 (iV16455)) /\ ((cC42 (iV16455)) /\ ((cowlThing (iV16455)) /\ ((cC38 (iV16457)) /\ ((cowlThing (iV16457)) /\ ((cC50 (iV16459)) /\ ((cC88 (iV16459)) /\ ((cC34 (iV16459)) /\ ((cC68 (iV16459)) /\ ((cowlThing (iV16459)) /\ ((cC38 (iV16460)) /\ ((cowlThing (iV16460)) /\ ((cC42 (iV16461)) /\ ((cC56 (iV16461)) /\ ((cC44 (iV16461)) /\ ((cowlThing (iV16461)) /\ ((cC38 (iV16462)) /\ ((cowlThing (iV16462)) /\ ((cC76 (iV16463)) /\ ((cC62 (iV16463)) /\ ((cowlThing (iV16463)) /\ ((cC60 (iV16463)) /\ ((cC56 (iV16464)) /\ ((cC42 (iV16464)) /\ ((cC44 (iV16464)) /\ ((cowlThing (iV16464)) /\ ((cC38 (iV16465)) /\ (cowlThing (iV16465))))))))))))))))))))))))))))))))))))))))))))))))) (cC78xcomp (iV16440)) (cC74xcomp (iV16453)) (cC40xcomp (iV16455)) (cC36xcomp (iV16457)) (cC84xcomp (iV16459)) (cC64xcomp (iV16459)) (cC32xcomp (iV16459)) (cC66xcomp (iV16459)) (cC40xcomp (iV16461)) (cC8xcomp (iV16462)) (cC58xcomp (iV16463)) (cC12xcomp (iV16464)) ### Definition-Pseudo(cC8xcomp) 220 % 24.30/24.47 % SZS output end Proof % 24.30/24.47 (* END-PROOF *) %------------------------------------------------------------------------------