%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS146+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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 : 300s % DateTime : Fri Oct 3 07:52:42 PM UTC 2025 % Result : Theorem 11.98s 12.17s % Output : Proof 12.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : KRS146+1 : TPTP v9.2.0. Released v3.1.0. % 0.06/0.13 % Command : duper %s % 0.13/0.33 % Computer : n021.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Oct 2 10:12:38 EDT 2025 % 0.13/0.34 % CPUTime : % 11.98/12.17 SZS status Theorem for theBenchmark.p % 11.98/12.17 SZS output start Proof for theBenchmark.p % 11.98/12.17 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 11.98/12.17 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 11.98/12.17 Clause #7 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC110 X) (And (Not (cC102 X)) (Not (cC108 X)))) True % 11.98/12.17 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC114 X) (And (Not (cC96 X)) (Not (cC112 X)))) True % 11.98/12.17 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC116 X) (And (cC114 X) (cC80 X))) True % 11.98/12.17 Clause #21 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC136 X) (And (cC116 X) (Not (cC134 X)))) True % 11.98/12.17 Clause #43 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC56 X) (And (cC4 X) (Not (cC10 X)))) True % 11.98/12.17 Clause #44 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC58 X) (And (cC34 X) (cC56 X))) True % 11.98/12.17 Clause #57 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC80 X) (And (Not (cC78 X)) (Not (cC76 X)))) True % 11.98/12.17 Clause #65 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC96 X) (And (Not (cC94 X)) (cC2 X))) True % 11.98/12.17 Clause #70 (by assumption #[]): Eq (Not (cC102 iV822576)) True % 11.98/12.17 Clause #71 (by assumption #[]): Eq (Not (cC134 iV822576)) True % 11.98/12.17 Clause #74 (by assumption #[]): Eq (cC34 iV822576) True % 11.98/12.17 Clause #75 (by assumption #[]): Eq (cC4 iV822576) True % 11.98/12.17 Clause #76 (by assumption #[]): Eq (Not (cC96 iV822576)) True % 11.98/12.17 Clause #79 (by assumption #[]): Eq (Not (cC108 iV822576)) True % 11.98/12.17 Clause #84 (by assumption #[]): Eq (Not (cC10 iV822576)) True % 11.98/12.17 Clause #86 (by assumption #[]): Eq (Not (cC76 iV822576)) True % 11.98/12.17 Clause #87 (by assumption #[]): Eq (Not (cC112 iV822576)) True % 11.98/12.17 Clause #88 (by assumption #[]): Eq (Not (cC78 iV822576)) True % 11.98/12.17 Clause #89 (by assumption #[]): Eq (cC2 iV822576) True % 11.98/12.17 Clause #91 (by assumption #[]): Eq % 11.98/12.17 (Not % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And % 11.98/12.17 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 11.98/12.17 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 11.98/12.17 (cC94 iV822576)) % 11.98/12.17 (cowlThing iV822576)) % 11.98/12.17 (cC58 iV822576)) % 11.98/12.17 (cC116 iV822576)) % 11.98/12.17 (cC56 iV822576)) % 11.98/12.17 (cC110 iV822576)) % 11.98/12.17 (cC114 iV822576)) % 11.98/12.17 (cC136 iV822576)) % 11.98/12.17 (cC80 iV822576))) % 11.98/12.17 True % 11.98/12.17 Clause #92 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 11.98/12.17 Clause #93 (by clausification #[92]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 11.98/12.17 Clause #94 (by clausification #[92]): ∀ (a : Iota), Eq (cowlThing a) True % 11.98/12.17 Clause #95 (by clausification #[93]): ∀ (a : Iota), Eq (cowlNothing a) False % 11.98/12.17 Clause #96 (by clausification #[88]): Eq (cC78 iV822576) False % 11.98/12.17 Clause #97 (by clausification #[79]): Eq (cC108 iV822576) False % 11.98/12.17 Clause #100 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 11.98/12.17 Clause #101 (by clausification #[100]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 11.98/12.17 Clause #102 (by clausification #[100]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 11.98/12.17 Clause #103 (by clausification #[101]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 11.98/12.17 Clause #104 (by clausification #[76]): Eq (cC96 iV822576) False % 11.98/12.17 Clause #105 (by clausification #[71]): Eq (cC134 iV822576) False % 11.98/12.17 Clause #106 (by clausification #[70]): Eq (cC102 iV822576) False % 11.98/12.17 Clause #107 (by clausification #[87]): Eq (cC112 iV822576) False % 11.98/12.17 Clause #117 (by clausification #[84]): Eq (cC10 iV822576) False % 11.98/12.17 Clause #118 (by clausification #[86]): Eq (cC76 iV822576) False % 11.98/12.17 Clause #134 (by clausification #[102]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 11.98/12.17 Clause #175 (by clausification #[7]): ∀ (a : Iota), Eq (Iff (cC110 a) (And (Not (cC102 a)) (Not (cC108 a)))) True % 11.98/12.17 Clause #176 (by clausification #[175]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Eq (And (Not (cC102 a)) (Not (cC108 a))) False) % 11.98/12.17 Clause #178 (by clausification #[176]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Or (Eq (Not (cC102 a)) False) (Eq (Not (cC108 a)) False)) % 12.05/12.22 Clause #179 (by clausification #[178]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Or (Eq (Not (cC108 a)) False) (Eq (cC102 a) True)) % 12.05/12.22 Clause #180 (by clausification #[179]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Or (Eq (cC102 a) True) (Eq (cC108 a) True)) % 12.05/12.22 Clause #181 (by superposition #[180, 106]): Or (Eq (cC110 iV822576) True) (Or (Eq (cC108 iV822576) True) (Eq True False)) % 12.05/12.22 Clause #185 (by clausification #[181]): Or (Eq (cC110 iV822576) True) (Eq (cC108 iV822576) True) % 12.05/12.22 Clause #186 (by forward demodulation #[185, 97]): Or (Eq (cC110 iV822576) True) (Eq False True) % 12.05/12.22 Clause #187 (by clausification #[186]): Eq (cC110 iV822576) True % 12.05/12.22 Clause #213 (by clausification #[9]): ∀ (a : Iota), Eq (Iff (cC114 a) (And (Not (cC96 a)) (Not (cC112 a)))) True % 12.05/12.22 Clause #214 (by clausification #[213]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Eq (And (Not (cC96 a)) (Not (cC112 a))) False) % 12.05/12.22 Clause #216 (by clausification #[214]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Or (Eq (Not (cC96 a)) False) (Eq (Not (cC112 a)) False)) % 12.05/12.22 Clause #217 (by clausification #[216]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Or (Eq (Not (cC112 a)) False) (Eq (cC96 a) True)) % 12.05/12.22 Clause #218 (by clausification #[217]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Or (Eq (cC96 a) True) (Eq (cC112 a) True)) % 12.05/12.22 Clause #219 (by superposition #[218, 104]): Or (Eq (cC114 iV822576) True) (Or (Eq (cC112 iV822576) True) (Eq True False)) % 12.05/12.22 Clause #220 (by clausification #[219]): Or (Eq (cC114 iV822576) True) (Eq (cC112 iV822576) True) % 12.05/12.22 Clause #221 (by superposition #[220, 107]): Or (Eq (cC114 iV822576) True) (Eq True False) % 12.05/12.22 Clause #224 (by clausification #[221]): Eq (cC114 iV822576) True % 12.05/12.22 Clause #229 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (cC116 a) (And (cC114 a) (cC80 a))) True % 12.05/12.22 Clause #230 (by clausification #[229]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Eq (And (cC114 a) (cC80 a)) False) % 12.05/12.22 Clause #232 (by clausification #[230]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Or (Eq (cC114 a) False) (Eq (cC80 a) False)) % 12.05/12.22 Clause #233 (by superposition #[232, 224]): Or (Eq (cC116 iV822576) True) (Or (Eq (cC80 iV822576) False) (Eq False True)) % 12.05/12.22 Clause #234 (by clausification #[233]): Or (Eq (cC116 iV822576) True) (Eq (cC80 iV822576) False) % 12.05/12.22 Clause #263 (by clausification #[44]): ∀ (a : Iota), Eq (Iff (cC58 a) (And (cC34 a) (cC56 a))) True % 12.05/12.22 Clause #264 (by clausification #[263]): ∀ (a : Iota), Or (Eq (cC58 a) True) (Eq (And (cC34 a) (cC56 a)) False) % 12.05/12.22 Clause #266 (by clausification #[264]): ∀ (a : Iota), Or (Eq (cC58 a) True) (Or (Eq (cC34 a) False) (Eq (cC56 a) False)) % 12.05/12.22 Clause #267 (by superposition #[266, 74]): Or (Eq (cC58 iV822576) True) (Or (Eq (cC56 iV822576) False) (Eq False True)) % 12.05/12.22 Clause #268 (by clausification #[267]): Or (Eq (cC58 iV822576) True) (Eq (cC56 iV822576) False) % 12.05/12.22 Clause #374 (by clausification #[21]): ∀ (a : Iota), Eq (Iff (cC136 a) (And (cC116 a) (Not (cC134 a)))) True % 12.05/12.22 Clause #375 (by clausification #[374]): ∀ (a : Iota), Or (Eq (cC136 a) True) (Eq (And (cC116 a) (Not (cC134 a))) False) % 12.05/12.22 Clause #377 (by clausification #[375]): ∀ (a : Iota), Or (Eq (cC136 a) True) (Or (Eq (cC116 a) False) (Eq (Not (cC134 a)) False)) % 12.05/12.22 Clause #378 (by clausification #[377]): ∀ (a : Iota), Or (Eq (cC136 a) True) (Or (Eq (cC116 a) False) (Eq (cC134 a) True)) % 12.05/12.22 Clause #576 (by clausification #[43]): ∀ (a : Iota), Eq (Iff (cC56 a) (And (cC4 a) (Not (cC10 a)))) True % 12.05/12.22 Clause #577 (by clausification #[576]): ∀ (a : Iota), Or (Eq (cC56 a) True) (Eq (And (cC4 a) (Not (cC10 a))) False) % 12.05/12.22 Clause #579 (by clausification #[577]): ∀ (a : Iota), Or (Eq (cC56 a) True) (Or (Eq (cC4 a) False) (Eq (Not (cC10 a)) False)) % 12.05/12.22 Clause #580 (by clausification #[579]): ∀ (a : Iota), Or (Eq (cC56 a) True) (Or (Eq (cC4 a) False) (Eq (cC10 a) True)) % 12.05/12.22 Clause #581 (by superposition #[580, 75]): Or (Eq (cC56 iV822576) True) (Or (Eq (cC10 iV822576) True) (Eq False True)) % 12.05/12.22 Clause #583 (by clausification #[581]): Or (Eq (cC56 iV822576) True) (Eq (cC10 iV822576) True) % 12.05/12.22 Clause #584 (by forward demodulation #[583, 117]): Or (Eq (cC56 iV822576) True) (Eq False True) % 12.06/12.27 Clause #585 (by clausification #[584]): Eq (cC56 iV822576) True % 12.06/12.27 Clause #586 (by backward demodulation #[585, 268]): Or (Eq (cC58 iV822576) True) (Eq True False) % 12.06/12.27 Clause #587 (by clausification #[586]): Eq (cC58 iV822576) True % 12.06/12.27 Clause #609 (by clausification #[65]): ∀ (a : Iota), Eq (Iff (cC96 a) (And (Not (cC94 a)) (cC2 a))) True % 12.06/12.27 Clause #610 (by clausification #[609]): ∀ (a : Iota), Or (Eq (cC96 a) True) (Eq (And (Not (cC94 a)) (cC2 a)) False) % 12.06/12.27 Clause #612 (by clausification #[610]): ∀ (a : Iota), Or (Eq (cC96 a) True) (Or (Eq (Not (cC94 a)) False) (Eq (cC2 a) False)) % 12.06/12.27 Clause #613 (by clausification #[612]): ∀ (a : Iota), Or (Eq (cC96 a) True) (Or (Eq (cC2 a) False) (Eq (cC94 a) True)) % 12.06/12.27 Clause #614 (by superposition #[613, 89]): Or (Eq (cC96 iV822576) True) (Or (Eq (cC94 iV822576) True) (Eq False True)) % 12.06/12.27 Clause #615 (by clausification #[614]): Or (Eq (cC96 iV822576) True) (Eq (cC94 iV822576) True) % 12.06/12.27 Clause #616 (by superposition #[615, 104]): Or (Eq (cC94 iV822576) True) (Eq True False) % 12.06/12.27 Clause #617 (by clausification #[616]): Eq (cC94 iV822576) True % 12.06/12.27 Clause #746 (by clausification #[57]): ∀ (a : Iota), Eq (Iff (cC80 a) (And (Not (cC78 a)) (Not (cC76 a)))) True % 12.06/12.27 Clause #747 (by clausification #[746]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Eq (And (Not (cC78 a)) (Not (cC76 a))) False) % 12.06/12.27 Clause #749 (by clausification #[747]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Or (Eq (Not (cC78 a)) False) (Eq (Not (cC76 a)) False)) % 12.06/12.27 Clause #750 (by clausification #[749]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Or (Eq (Not (cC76 a)) False) (Eq (cC78 a) True)) % 12.06/12.27 Clause #751 (by clausification #[750]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Or (Eq (cC78 a) True) (Eq (cC76 a) True)) % 12.06/12.27 Clause #752 (by superposition #[751, 118]): Or (Eq (cC80 iV822576) True) (Or (Eq (cC78 iV822576) True) (Eq True False)) % 12.06/12.27 Clause #755 (by clausification #[752]): Or (Eq (cC80 iV822576) True) (Eq (cC78 iV822576) True) % 12.06/12.27 Clause #756 (by superposition #[755, 96]): Or (Eq (cC80 iV822576) True) (Eq True False) % 12.06/12.27 Clause #759 (by clausification #[756]): Eq (cC80 iV822576) True % 12.06/12.27 Clause #760 (by backward demodulation #[759, 234]): Or (Eq (cC116 iV822576) True) (Eq True False) % 12.06/12.27 Clause #762 (by clausification #[760]): Eq (cC116 iV822576) True % 12.06/12.27 Clause #765 (by superposition #[762, 378]): Or (Eq (cC136 iV822576) True) (Or (Eq True False) (Eq (cC134 iV822576) True)) % 12.06/12.27 Clause #771 (by clausification #[765]): Or (Eq (cC136 iV822576) True) (Eq (cC134 iV822576) True) % 12.06/12.27 Clause #772 (by forward demodulation #[771, 105]): Or (Eq (cC136 iV822576) True) (Eq False True) % 12.06/12.27 Clause #773 (by clausification #[772]): Eq (cC136 iV822576) True % 12.06/12.27 Clause #808 (by clausification #[91]): Eq % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.06/12.27 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.06/12.27 (cC94 iV822576)) % 12.06/12.27 (cowlThing iV822576)) % 12.06/12.27 (cC58 iV822576)) % 12.06/12.27 (cC116 iV822576)) % 12.06/12.27 (cC56 iV822576)) % 12.06/12.27 (cC110 iV822576)) % 12.06/12.27 (cC114 iV822576)) % 12.06/12.27 (cC136 iV822576)) % 12.06/12.27 (cC80 iV822576)) % 12.06/12.27 False % 12.06/12.27 Clause #809 (by clausification #[808]): Or % 12.06/12.27 (Eq % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.06/12.27 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.06/12.27 (cC94 iV822576)) % 12.06/12.27 (cowlThing iV822576)) % 12.06/12.27 (cC58 iV822576)) % 12.06/12.27 (cC116 iV822576)) % 12.06/12.27 (cC56 iV822576)) % 12.06/12.27 (cC110 iV822576)) % 12.06/12.27 (cC114 iV822576)) % 12.06/12.27 (cC136 iV822576)) % 12.06/12.27 False) % 12.06/12.27 (Eq (cC80 iV822576) False) % 12.06/12.27 Clause #810 (by clausification #[809]): Or (Eq (cC80 iV822576) False) % 12.06/12.27 (Or % 12.06/12.27 (Eq % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.06/12.27 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 (cC58 iV822576)) % 12.14/12.31 (cC116 iV822576)) % 12.14/12.31 (cC56 iV822576)) % 12.14/12.31 (cC110 iV822576)) % 12.14/12.31 (cC114 iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC136 iV822576) False)) % 12.14/12.31 Clause #811 (by clausification #[810]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 (cC58 iV822576)) % 12.14/12.31 (cC116 iV822576)) % 12.14/12.31 (cC56 iV822576)) % 12.14/12.31 (cC110 iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC114 iV822576) False))) % 12.14/12.31 Clause #812 (by clausification #[811]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or (Eq (cC114 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 (cC58 iV822576)) % 12.14/12.31 (cC116 iV822576)) % 12.14/12.31 (cC56 iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC110 iV822576) False)))) % 12.14/12.31 Clause #813 (by clausification #[812]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or (Eq (cC114 iV822576) False) % 12.14/12.31 (Or (Eq (cC110 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 (cC58 iV822576)) % 12.14/12.31 (cC116 iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC56 iV822576) False))))) % 12.14/12.31 Clause #814 (by clausification #[813]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or (Eq (cC114 iV822576) False) % 12.14/12.31 (Or (Eq (cC110 iV822576) False) % 12.14/12.31 (Or (Eq (cC56 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 (cC58 iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC116 iV822576) False)))))) % 12.14/12.31 Clause #815 (by clausification #[814]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or (Eq (cC114 iV822576) False) % 12.14/12.31 (Or (Eq (cC110 iV822576) False) % 12.14/12.31 (Or (Eq (cC56 iV822576) False) % 12.14/12.31 (Or (Eq (cC116 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.14/12.31 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.14/12.31 (cC94 iV822576)) % 12.14/12.31 (cowlThing iV822576)) % 12.14/12.31 False) % 12.14/12.31 (Eq (cC58 iV822576) False))))))) % 12.14/12.31 Clause #816 (by clausification #[815]): Or (Eq (cC80 iV822576) False) % 12.14/12.31 (Or (Eq (cC136 iV822576) False) % 12.14/12.31 (Or (Eq (cC114 iV822576) False) % 12.14/12.31 (Or (Eq (cC110 iV822576) False) % 12.14/12.31 (Or (Eq (cC56 iV822576) False) % 12.14/12.31 (Or (Eq (cC116 iV822576) False) % 12.14/12.31 (Or (Eq (cC58 iV822576) False) % 12.14/12.31 (Or % 12.14/12.31 (Eq % 12.14/12.31 (And % 12.14/12.31 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.19/12.37 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.19/12.37 (cC94 iV822576)) % 12.19/12.37 False) % 12.19/12.37 (Eq (cowlThing iV822576) False)))))))) % 12.19/12.37 Clause #817 (by clausification #[816]): Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or % 12.19/12.37 (Eq % 12.19/12.37 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 12.19/12.37 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 12.19/12.37 False) % 12.19/12.37 (Eq (cC94 iV822576) False))))))))) % 12.19/12.37 Clause #818 (by clausification #[817]): Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or (Eq (cC94 iV822576) False) % 12.19/12.37 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 12.19/12.37 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)))))))))) % 12.19/12.37 Clause #819 (by clausification #[818]): ∀ (a : Iota), % 12.19/12.37 Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or (Eq (cC94 iV822576) False) % 12.19/12.37 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 12.19/12.37 (Eq (Not (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a))))) True)))))))))) % 12.19/12.37 Clause #820 (by clausification #[819]): ∀ (a a_1 : Iota), % 12.19/12.37 Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or (Eq (cC94 iV822576) False) % 12.19/12.37 (Or (Eq (Not (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a))))) True) % 12.19/12.37 (Eq (Not (Iff (xsd_string (skS.0 1 a_1)) (Not (xsd_integer (skS.0 1 a_1))))) True)))))))))) % 12.19/12.37 Clause #821 (by clausification #[820]): ∀ (a a_1 : Iota), % 12.19/12.37 Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or (Eq (cC94 iV822576) False) % 12.19/12.37 (Or (Eq (Not (Iff (xsd_string (skS.0 1 a)) (Not (xsd_integer (skS.0 1 a))))) True) % 12.19/12.37 (Eq (And (cowlThing (skS.0 0 a_1)) (Not (cowlNothing (skS.0 0 a_1)))) False)))))))))) % 12.19/12.37 Clause #822 (by clausification #[821]): ∀ (a a_1 : Iota), % 12.19/12.37 Or (Eq (cC80 iV822576) False) % 12.19/12.37 (Or (Eq (cC136 iV822576) False) % 12.19/12.37 (Or (Eq (cC114 iV822576) False) % 12.19/12.37 (Or (Eq (cC110 iV822576) False) % 12.19/12.37 (Or (Eq (cC56 iV822576) False) % 12.19/12.37 (Or (Eq (cC116 iV822576) False) % 12.19/12.37 (Or (Eq (cC58 iV822576) False) % 12.19/12.37 (Or (Eq (cowlThing iV822576) False) % 12.19/12.37 (Or (Eq (cC94 iV822576) False) % 12.19/12.37 (Or (Eq (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a)))) False) % 12.19/12.37 (Eq (Iff (xsd_string (skS.0 1 a_1)) (Not (xsd_integer (skS.0 1 a_1)))) False)))))))))) % 12.19/12.37 Clause #823 (by clausification #[822]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq (cC80 iV822576) False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (Iff (xsd_string (skS.0 1 a)) (Not (xsd_integer (skS.0 1 a)))) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a_1)) False) (Eq (Not (cowlNothing (skS.0 0 a_1))) False))))))))))) % 12.19/12.42 Clause #824 (by clausification #[823]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq (cC80 iV822576) False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.19/12.42 (Or (Eq (Not (cowlNothing (skS.0 0 a))) False) % 12.19/12.42 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.19/12.42 (Eq (Not (xsd_integer (skS.0 1 a_1))) False)))))))))))) % 12.19/12.42 Clause #825 (by clausification #[823]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq (cC80 iV822576) False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.19/12.42 (Or (Eq (Not (cowlNothing (skS.0 0 a))) False) % 12.19/12.42 (Or (Eq (xsd_string (skS.0 1 a_1)) True) (Eq (Not (xsd_integer (skS.0 1 a_1))) True)))))))))))) % 12.19/12.42 Clause #826 (by clausification #[824]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq (cC80 iV822576) False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.19/12.42 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.19/12.42 (Or (Eq (Not (xsd_integer (skS.0 1 a_1))) False) (Eq (cowlNothing (skS.0 0 a)) True)))))))))))) % 12.19/12.42 Clause #827 (by clausification #[826]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq (cC80 iV822576) False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.19/12.42 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.19/12.42 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))))) % 12.19/12.42 Clause #828 (by forward demodulation #[827, 759]): ∀ (a a_1 : Iota), % 12.19/12.42 Or (Eq True False) % 12.19/12.42 (Or (Eq (cC136 iV822576) False) % 12.19/12.42 (Or (Eq (cC114 iV822576) False) % 12.19/12.42 (Or (Eq (cC110 iV822576) False) % 12.19/12.42 (Or (Eq (cC56 iV822576) False) % 12.19/12.42 (Or (Eq (cC116 iV822576) False) % 12.19/12.42 (Or (Eq (cC58 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing iV822576) False) % 12.19/12.42 (Or (Eq (cC94 iV822576) False) % 12.19/12.42 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.19/12.42 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.19/12.42 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))))) % 12.19/12.42 Clause #829 (by clausification #[828]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq (cC136 iV822576) False) % 12.29/12.47 (Or (Eq (cC114 iV822576) False) % 12.29/12.47 (Or (Eq (cC110 iV822576) False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))))) % 12.29/12.47 Clause #830 (by forward demodulation #[829, 773]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq True False) % 12.29/12.47 (Or (Eq (cC114 iV822576) False) % 12.29/12.47 (Or (Eq (cC110 iV822576) False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))))) % 12.29/12.47 Clause #831 (by clausification #[830]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq (cC114 iV822576) False) % 12.29/12.47 (Or (Eq (cC110 iV822576) False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))) % 12.29/12.47 Clause #832 (by forward demodulation #[831, 224]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq True False) % 12.29/12.47 (Or (Eq (cC110 iV822576) False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))) % 12.29/12.47 Clause #833 (by clausification #[832]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq (cC110 iV822576) False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))) % 12.29/12.47 Clause #834 (by forward demodulation #[833, 187]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq True False) % 12.29/12.47 (Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))) % 12.29/12.47 Clause #835 (by clausification #[834]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq (cC56 iV822576) False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.29/12.47 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))) % 12.29/12.47 Clause #836 (by forward demodulation #[835, 585]): ∀ (a a_1 : Iota), % 12.29/12.47 Or (Eq True False) % 12.29/12.47 (Or (Eq (cC116 iV822576) False) % 12.29/12.47 (Or (Eq (cC58 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing iV822576) False) % 12.29/12.47 (Or (Eq (cC94 iV822576) False) % 12.29/12.47 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.29/12.47 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))) % 12.32/12.53 Clause #837 (by clausification #[836]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cC116 iV822576) False) % 12.32/12.53 (Or (Eq (cC58 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))) % 12.32/12.53 Clause #838 (by forward demodulation #[837, 762]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq True False) % 12.32/12.53 (Or (Eq (cC58 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))) % 12.32/12.53 Clause #839 (by clausification #[838]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cC58 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))) % 12.32/12.53 Clause #840 (by forward demodulation #[839, 587]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq True False) % 12.32/12.53 (Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))) % 12.32/12.53 Clause #841 (by clausification #[840]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))) % 12.32/12.53 Clause #842 (by forward demodulation #[841, 94]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq True False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))) % 12.32/12.53 Clause #843 (by clausification #[842]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))) % 12.32/12.53 Clause #844 (by forward demodulation #[843, 617]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq True False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))) % 12.32/12.53 Clause #845 (by clausification #[844]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))) % 12.32/12.53 Clause #846 (by forward demodulation #[845, 94]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq True False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a)) False) % 12.32/12.53 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) True))) % 12.32/12.53 Clause #847 (by clausification #[846]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (xsd_string (skS.0 1 a)) False) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) True)) % 12.32/12.53 Clause #993 (by clausification #[825]): ∀ (a a_1 : Iota), % 12.32/12.53 Or (Eq (cC80 iV822576) False) % 12.32/12.53 (Or (Eq (cC136 iV822576) False) % 12.32/12.53 (Or (Eq (cC114 iV822576) False) % 12.32/12.53 (Or (Eq (cC110 iV822576) False) % 12.32/12.53 (Or (Eq (cC56 iV822576) False) % 12.32/12.53 (Or (Eq (cC116 iV822576) False) % 12.32/12.53 (Or (Eq (cC58 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing iV822576) False) % 12.32/12.53 (Or (Eq (cC94 iV822576) False) % 12.32/12.53 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.32/12.53 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.32/12.53 (Or (Eq (Not (xsd_integer (skS.0 1 a_1))) True) (Eq (cowlNothing (skS.0 0 a)) True)))))))))))) % 12.36/12.58 Clause #994 (by clausification #[993]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq (cC80 iV822576) False) % 12.36/12.58 (Or (Eq (cC136 iV822576) False) % 12.36/12.58 (Or (Eq (cC114 iV822576) False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))))) % 12.36/12.58 Clause #995 (by forward demodulation #[994, 759]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq True False) % 12.36/12.58 (Or (Eq (cC136 iV822576) False) % 12.36/12.58 (Or (Eq (cC114 iV822576) False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))))) % 12.36/12.58 Clause #996 (by clausification #[995]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq (cC136 iV822576) False) % 12.36/12.58 (Or (Eq (cC114 iV822576) False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))))) % 12.36/12.58 Clause #997 (by forward demodulation #[996, 773]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq True False) % 12.36/12.58 (Or (Eq (cC114 iV822576) False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))))) % 12.36/12.58 Clause #998 (by clausification #[997]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq (cC114 iV822576) False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))) % 12.36/12.58 Clause #999 (by forward demodulation #[998, 224]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq True False) % 12.36/12.58 (Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.36/12.58 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.36/12.58 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))) % 12.36/12.58 Clause #1000 (by clausification #[999]): ∀ (a a_1 : Iota), % 12.36/12.58 Or (Eq (cC110 iV822576) False) % 12.36/12.58 (Or (Eq (cC56 iV822576) False) % 12.36/12.58 (Or (Eq (cC116 iV822576) False) % 12.36/12.58 (Or (Eq (cC58 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing iV822576) False) % 12.36/12.58 (Or (Eq (cC94 iV822576) False) % 12.36/12.58 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))) % 12.46/12.64 Clause #1001 (by forward demodulation #[1000, 187]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq True False) % 12.46/12.64 (Or (Eq (cC56 iV822576) False) % 12.46/12.64 (Or (Eq (cC116 iV822576) False) % 12.46/12.64 (Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))) % 12.46/12.64 Clause #1002 (by clausification #[1001]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq (cC56 iV822576) False) % 12.46/12.64 (Or (Eq (cC116 iV822576) False) % 12.46/12.64 (Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))) % 12.46/12.64 Clause #1003 (by forward demodulation #[1002, 585]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq True False) % 12.46/12.64 (Or (Eq (cC116 iV822576) False) % 12.46/12.64 (Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))) % 12.46/12.64 Clause #1004 (by clausification #[1003]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq (cC116 iV822576) False) % 12.46/12.64 (Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))) % 12.46/12.64 Clause #1005 (by forward demodulation #[1004, 762]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq True False) % 12.46/12.64 (Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))) % 12.46/12.64 Clause #1006 (by clausification #[1005]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq (cC58 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))) % 12.46/12.64 Clause #1007 (by forward demodulation #[1006, 587]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq True False) % 12.46/12.64 (Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))) % 12.46/12.64 Clause #1008 (by clausification #[1007]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq (cowlThing iV822576) False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))) % 12.46/12.64 Clause #1009 (by forward demodulation #[1008, 94]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq True False) % 12.46/12.64 (Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))) % 12.46/12.64 Clause #1010 (by clausification #[1009]): ∀ (a a_1 : Iota), % 12.46/12.64 Or (Eq (cC94 iV822576) False) % 12.46/12.64 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.64 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.64 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))) % 12.46/12.64 Clause #1011 (by forward demodulation #[1010, 617]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq True False) % 12.46/12.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))) % 12.46/12.68 Clause #1012 (by clausification #[1011]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq (cowlThing (skS.0 0 a)) False) % 12.46/12.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 12.46/12.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))) % 12.46/12.68 Clause #1013 (by forward demodulation #[1012, 94]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq True False) % 12.46/12.68 (Or (Eq (xsd_string (skS.0 1 a)) True) % 12.46/12.68 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) False))) % 12.46/12.68 Clause #1014 (by clausification #[1013]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq (xsd_string (skS.0 1 a)) True) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) False)) % 12.46/12.68 Clause #1015 (by superposition #[1014, 103]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq (xsd_string (skS.0 1 a)) True) % 12.46/12.68 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_string (skS.0 1 a)) True) (Eq False True))) % 12.46/12.68 Clause #1134 (by clausification #[1015]): ∀ (a a_1 : Iota), % 12.46/12.68 Or (Eq (xsd_string (skS.0 1 a)) True) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_string (skS.0 1 a)) True)) % 12.46/12.68 Clause #1135 (by eliminate duplicate literals #[1134]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 1 a)) True) (Eq (cowlNothing (skS.0 0 a_1)) True) % 12.46/12.68 Clause #1138 (by superposition #[1135, 95]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 1 a)) True) (Eq True False) % 12.46/12.68 Clause #1139 (by clausification #[1138]): ∀ (a : Iota), Eq (xsd_string (skS.0 1 a)) True % 12.46/12.68 Clause #1140 (by backward demodulation #[1139, 847]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)) % 12.46/12.68 Clause #1141 (by superposition #[1139, 134]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 1 a)) False) % 12.46/12.68 Clause #1142 (by clausification #[1141]): ∀ (a : Iota), Eq (xsd_integer (skS.0 1 a)) False % 12.46/12.68 Clause #1259 (by clausification #[1140]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True) % 12.46/12.68 Clause #1261 (by superposition #[1259, 1142]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq True False) % 12.46/12.68 Clause #1262 (by clausification #[1261]): ∀ (a : Iota), Eq (cowlNothing (skS.0 0 a)) True % 12.46/12.68 Clause #1263 (by superposition #[1262, 95]): Eq True False % 12.46/12.68 Clause #1264 (by clausification #[1263]): False % 12.46/12.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------