%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS151+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 : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sun Jul 17 03:32:03 EDT 2022 % Result : Theorem 0.19s 0.44s % Output : Proof 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS151+1 : TPTP v8.1.0. Released v3.1.0. % 0.03/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.33 % Computer : n023.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 600 % 0.14/0.33 % DateTime : Tue Jun 7 14:51:38 EDT 2022 % 0.14/0.33 % CPUTime : % 0.19/0.44 % SZS status Theorem % 0.19/0.44 (* PROOF-FOUND *) % 0.19/0.44 (* BEGIN-PROOF *) % 0.19/0.44 % SZS output start Proof % 0.19/0.44 1. (-. (cC2 (iV21027))) (cC2 (iV21027)) ### Axiom % 0.19/0.44 2. (-. (cC12 (iV21029))) (cC12 (iV21029)) ### Axiom % 0.19/0.44 3. (-. (cC12 (iV21029))) (cC12 (iV21029)) ### Axiom % 0.19/0.44 4. (-. (cC18 (iV21030))) (cC18 (iV21030)) ### Axiom % 0.19/0.44 5. (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (All X, ((cowlThing X) /\ (-. (cowlNothing X))))) ### Axiom % 0.19/0.44 6. (-. (xsd_integer T_0)) (xsd_integer T_0) ### Axiom % 0.19/0.44 7. (-. (xsd_string T_0)) (-. (xsd_integer T_0)) ### Extension/test/not_axiom_1 6 % 0.19/0.44 8. (-. (-. (xsd_integer T_0))) (-. (xsd_integer T_0)) ### Axiom % 0.19/0.44 9. (xsd_string T_0) (-. (-. (xsd_integer T_0))) ### Extension/test/axiom_1 8 % 0.19/0.44 10. (-. ((xsd_string T_0) <=> (-. (xsd_integer T_0)))) ### NotEquiv 7 9 % 0.19/0.44 11. (-. (All X, ((xsd_string X) <=> (-. (xsd_integer X))))) ### NotAllEx 10 % 0.19/0.44 12. (cowlThing (iV21026)) (-. (cowlThing (iV21026))) ### Axiom % 0.19/0.44 13. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 14. (-. (cC84 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_79 13 % 0.19/0.44 15. (cC16 (iV21026)) (-. (cC16 (iV21026))) ### Axiom % 0.19/0.44 16. (cC36 (iV21026)) (-. (cC36 (iV21026))) ### Axiom % 0.19/0.44 17. (cC42 (iV21026)) (-. (cC42 (iV21026))) ### Axiom % 0.19/0.44 18. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 19. (-. (cC88 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_81 18 % 0.19/0.44 20. (cC86 (iV21026)) (-. (cC86 (iV21026))) ### Axiom % 0.19/0.44 21. (cC174 (iV21026)) (-. (cC174 (iV21026))) ### Axiom % 0.19/0.44 22. (cC20 (iV21026)) (-. (cC20 (iV21026))) ### Axiom % 0.19/0.44 23. (cC156 (iV21026)) (-. (cC156 (iV21026))) ### Axiom % 0.19/0.44 24. (cC60 (iV21026)) (-. (cC60 (iV21026))) ### Axiom % 0.19/0.44 25. (cC38 (iV21026)) (-. (cC38 (iV21026))) ### Axiom % 0.19/0.44 26. (cC158 (iV21026)) (-. (cC158 (iV21026))) ### Axiom % 0.19/0.44 27. (cC10 (iV21026)) (-. (cC10 (iV21026))) ### Axiom % 0.19/0.44 28. (cC134 (iV21026)) (-. (cC134 (iV21026))) ### Axiom % 0.19/0.44 29. (cC22 (iV21026)) (-. (cC22 (iV21026))) ### Axiom % 0.19/0.44 30. (cC168 (iV21026)) (-. (cC168 (iV21026))) ### Axiom % 0.19/0.44 31. (cC56 (iV21026)) (-. (cC56 (iV21026))) ### Axiom % 0.19/0.44 32. (cC78 (iV21026)) (-. (cC78 (iV21026))) ### Axiom % 0.19/0.44 33. (cC58 (iV21026)) (-. (cC58 (iV21026))) ### Axiom % 0.19/0.44 34. (cC152 (iV21026)) (-. (cC152 (iV21026))) ### Axiom % 0.19/0.44 35. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 36. (-. (cC40 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_56 35 % 0.19/0.44 37. (cC132 (iV21026)) (-. (cC132 (iV21026))) ### Axiom % 0.19/0.44 38. (cC130 (iV21026)) (-. (cC130 (iV21026))) ### Axiom % 0.19/0.44 39. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 40. (-. (cC62 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_67 39 % 0.19/0.44 41. (cC154 (iV21026)) (-. (cC154 (iV21026))) ### Axiom % 0.19/0.44 42. (cC80 (iV21026)) (-. (cC80 (iV21026))) ### Axiom % 0.19/0.44 43. (cC8 (iV21026)) (-. (cC8 (iV21026))) ### Axiom % 0.19/0.44 44. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 45. (-. (cC136 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_20 44 % 0.19/0.44 46. (cC112 (iV21026)) (-. (cC112 (iV21026))) ### Axiom % 0.19/0.44 47. (cC180 (iV21026)) (-. (cC180 (iV21026))) ### Axiom % 0.19/0.44 48. (cTOP (iV21026)) (-. (cTOP (iV21026))) ### Axiom % 0.19/0.44 49. (-. (cC114 (iV21026))) (cTOP (iV21026)) ### Extension/test/not_axiom_9 48 % 0.19/0.44 50. (cC64 (iV21026)) (-. (cC64 (iV21026))) ### Axiom % 0.19/0.44 51. (cC110 (iV21026)) (-. (cC110 (iV21026))) ### Axiom % 0.19/0.44 52. (cC116 (iV21026)) (-. (cC116 (iV21026))) ### Axiom % 0.19/0.44 53. (cC82 (iV21026)) (-. (cC82 (iV21026))) ### Axiom % 0.19/0.44 54. (cC138 (iV21026)) (-. (cC138 (iV21026))) ### Axiom % 0.19/0.44 55. (cC4 (iV21026)) (-. (cC4 (iV21026))) ### Axiom % 0.19/0.44 56. (cC108 (iV21026)) (-. (cC108 (iV21026))) ### Axiom % 0.19/0.44 57. (cC14 (iV21026)) (-. (cC14 (iV21026))) ### Axiom % 0.19/0.44 58. (cC90 (iV21026)) (-. (cC90 (iV21026))) ### Axiom % 0.19/0.44 59. (cowlThing (iV21027)) (-. (cowlThing (iV21027))) ### Axiom % 0.19/0.44 60. (cC30 (iV21027)) (-. (cC30 (iV21027))) ### Axiom % 0.19/0.44 61. (cC24 (iV21027)) (-. (cC24 (iV21027))) ### Axiom % 0.19/0.44 62. (cowlThing (iV21029)) (-. (cowlThing (iV21029))) ### Axiom % 0.19/0.44 63. (cC50 (iV21029)) (-. (cC50 (iV21029))) ### Axiom % 0.19/0.44 64. (cC44 (iV21029)) (-. (cC44 (iV21029))) ### Axiom % 0.19/0.44 65. (cowlThing (iV21030)) (-. (cowlThing (iV21030))) ### Axiom % 0.19/0.44 66. (cC66 (iV21030)) (-. (cC66 (iV21030))) ### Axiom % 0.19/0.44 67. (cC72 (iV21030)) (-. (cC72 (iV21030))) ### Axiom % 0.19/0.44 68. (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cC72 (iV21030)) (cC66 (iV21030)) (cowlThing (iV21030)) (cC44 (iV21029)) (cC50 (iV21029)) (cowlThing (iV21029)) (cC24 (iV21027)) (cC30 (iV21027)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC14 (iV21026)) (cC108 (iV21026)) (cC4 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC8 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC168 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC10 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC174 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) ### DisjTree 5 11 12 14 15 16 17 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 36 37 38 40 41 42 43 45 46 47 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 % 0.19/0.44 69. (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC16 (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC174 (iV21026)) (cC20 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC10 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC168 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC8 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC4 (iV21026)) (cC108 (iV21026)) (cC14 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cC30 (iV21027)) (cC24 (iV21027)) (cowlThing (iV21029)) (cC50 (iV21029)) (cC44 (iV21029)) (cowlThing (iV21030)) (cC66 (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) ### Extension/test/not_axiom_73 4 68 % 0.19/0.44 70. (-. (cC18 (iV21030))) (cC18 (iV21030)) ### Axiom % 0.19/0.44 71. (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cC44 (iV21029)) (cC50 (iV21029)) (cowlThing (iV21029)) (cC24 (iV21027)) (cC30 (iV21027)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC14 (iV21026)) (cC108 (iV21026)) (cC4 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC8 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC168 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC10 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC174 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) ### Extension/test/not_axiom_70 69 70 % 0.19/0.44 72. (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC16 (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC174 (iV21026)) (cC20 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC10 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC168 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC8 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC4 (iV21026)) (cC108 (iV21026)) (cC14 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cC30 (iV21027)) (cC24 (iV21027)) (cowlThing (iV21029)) (cC44 (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC12 (iV21029))) ### Extension/test/not_axiom_62 3 71 % 0.19/0.44 73. (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cC24 (iV21027)) (cC30 (iV21027)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC14 (iV21026)) (cC108 (iV21026)) (cC4 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC8 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC168 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC10 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC174 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) ### Extension/test/not_axiom_59 2 72 % 0.19/0.44 74. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC16 (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC174 (iV21026)) (cC20 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC10 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC168 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC8 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC4 (iV21026)) (cC108 (iV21026)) (cC14 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cC24 (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) ### Extension/test/not_axiom_51 1 73 % 0.19/0.44 75. (-. (cC2 (iV21027))) (cC2 (iV21027)) ### Axiom % 0.19/0.44 76. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC14 (iV21026)) (cC108 (iV21026)) (cC4 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC8 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC168 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC10 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC174 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/not_axiom_48 74 75 % 0.19/0.44 77. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC16 (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC174 (iV21026)) (cC20 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC10 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC8 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC4 (iV21026)) (cC108 (iV21026)) (cC14 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_41 76 % 0.19/0.44 78. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC14 (iV21026)) (cC108 (iV21026)) (cC4 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC8 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC10 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_44 77 % 0.19/0.44 79. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC16 (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC20 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC10 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC108 (iV21026)) (cC14 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_2 78 % 0.19/0.44 80. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC108 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC20 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cC16 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_33 79 % 0.19/0.44 81. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC36 (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC108 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_46 80 % 0.19/0.44 82. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC38 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cC36 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_7 81 % 0.19/0.44 83. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC38 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC56 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_54 82 % 0.19/0.44 84. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC58 (iV21026)) (cC78 (iV21026)) (cC56 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC86 (iV21026)) (cC42 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_57 83 % 0.19/0.44 85. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC42 (iV21026)) (cC86 (iV21026)) (cC156 (iV21026)) (cC60 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC78 (iV21026)) (cC58 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_65 84 % 0.19/0.44 86. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC78 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC60 (iV21026)) (cC156 (iV21026)) (cC86 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_66 85 % 0.19/0.44 87. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC86 (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC78 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC80 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC64 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_68 86 % 0.19/0.44 88. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC138 (iV21026)) (cC82 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC64 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC80 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cC86 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_77 87 % 0.19/0.44 89. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC86 (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC82 (iV21026)) (cC138 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_78 88 % 0.19/0.44 90. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC90 (iV21026)) (cC138 (iV21026)) (cC116 (iV21026)) (cC110 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cC86 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_80 89 % 0.19/0.44 91. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC112 (iV21026)) (cC180 (iV21026)) (cC110 (iV21026)) (cC116 (iV21026)) (cC138 (iV21026)) (cC90 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_82 90 % 0.19/0.44 92. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC138 (iV21026)) (cC116 (iV21026)) (cC180 (iV21026)) (cC112 (iV21026)) (cC154 (iV21026)) (cC130 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_8 91 % 0.19/0.44 93. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC152 (iV21026)) (cC132 (iV21026)) (cC130 (iV21026)) (cC154 (iV21026)) (cC180 (iV21026)) (cC116 (iV21026)) (cC138 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_10 92 % 0.19/0.44 94. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC138 (iV21026)) (cC116 (iV21026)) (cC180 (iV21026)) (cC154 (iV21026)) (cC132 (iV21026)) (cC152 (iV21026)) (cC22 (iV21026)) (cC134 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_18 93 % 0.19/0.44 95. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC134 (iV21026)) (cC22 (iV21026)) (cC152 (iV21026)) (cC154 (iV21026)) (cC180 (iV21026)) (cC138 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_19 94 % 0.19/0.45 96. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC138 (iV21026)) (cC180 (iV21026)) (cC154 (iV21026)) (cC152 (iV21026)) (cC22 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_21 95 % 0.19/0.45 97. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC156 (iV21026)) (cC158 (iV21026)) (cC22 (iV21026)) (cC154 (iV21026)) (cC180 (iV21026)) (cC138 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_30 96 % 0.19/0.45 98. (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cC180 (iV21026)) (cC22 (iV21026)) (cC158 (iV21026)) (cC156 (iV21026)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_31 97 % 0.19/0.45 99. (-. (cC32 (iV21027))) (-. (cC12 (iV21029))) (-. (cC52 (iV21029))) (-. (cC74 (iV21030))) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (cowlThing (iV21026)) (cTOP (iV21026)) (cC158 (iV21026)) (cC180 (iV21026)) (cowlThing (iV21027)) (cowlThing (iV21029)) (cowlThing (iV21030)) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (-. (cC18 (iV21030))) (-. (cC68 (iV21030))) (-. (cC46 (iV21029))) (-. (cC2 (iV21027))) (-. (cC26 (iV21027))) ### Extension/test/axiom_32 98 % 0.19/0.45 100. (cTEST (iV21026)) (-. (cC26 (iV21027))) (-. (cC2 (iV21027))) (-. (cC46 (iV21029))) (-. (cC68 (iV21030))) (-. (cC18 (iV21030))) (-. ((All X, ((cowlThing X) /\ (-. (cowlNothing X)))) /\ ((All X, ((xsd_string X) <=> (-. (xsd_integer X)))) /\ ((cowlThing (iV21026)) /\ ((cC84 (iV21026)) /\ ((cC16 (iV21026)) /\ ((cC36 (iV21026)) /\ ((cC42 (iV21026)) /\ ((cC88 (iV21026)) /\ ((cC86 (iV21026)) /\ ((cC174 (iV21026)) /\ ((cC20 (iV21026)) /\ ((cC156 (iV21026)) /\ ((cC60 (iV21026)) /\ ((cC38 (iV21026)) /\ ((cC158 (iV21026)) /\ ((cC10 (iV21026)) /\ ((cC134 (iV21026)) /\ ((cC22 (iV21026)) /\ ((cC168 (iV21026)) /\ ((cC56 (iV21026)) /\ ((cC78 (iV21026)) /\ ((cC58 (iV21026)) /\ ((cC152 (iV21026)) /\ ((cC40 (iV21026)) /\ ((cC132 (iV21026)) /\ ((cC130 (iV21026)) /\ ((cC62 (iV21026)) /\ ((cC154 (iV21026)) /\ ((cC80 (iV21026)) /\ ((cC8 (iV21026)) /\ ((cC136 (iV21026)) /\ ((cC112 (iV21026)) /\ ((cC180 (iV21026)) /\ ((cC114 (iV21026)) /\ ((cC64 (iV21026)) /\ ((cC110 (iV21026)) /\ ((cC116 (iV21026)) /\ ((cC82 (iV21026)) /\ ((cC138 (iV21026)) /\ ((cC4 (iV21026)) /\ ((cC108 (iV21026)) /\ ((cC14 (iV21026)) /\ ((cC90 (iV21026)) /\ ((cowlThing (iV21027)) /\ ((cC30 (iV21027)) /\ ((cC24 (iV21027)) /\ ((cowlThing (iV21029)) /\ ((cC50 (iV21029)) /\ ((cC44 (iV21029)) /\ ((cowlThing (iV21030)) /\ ((cC66 (iV21030)) /\ (cC72 (iV21030)))))))))))))))))))))))))))))))))))))))))))))))))))))) (cowlThing (iV21030)) (cowlThing (iV21029)) (cowlThing (iV21027)) (cTOP (iV21026)) (cowlThing (iV21026)) (All X, ((cowlThing X) /\ (-. (cowlNothing X)))) (-. (cC74 (iV21030))) (-. (cC52 (iV21029))) (-. (cC12 (iV21029))) (-. (cC32 (iV21027))) ### Extension/test/axiom_86 99 % 0.19/0.45 % SZS output end Proof % 0.19/0.45 (* END-PROOF *) %------------------------------------------------------------------------------