%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS154+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:43 PM UTC 2025 % Result : Theorem 19.89s 20.16s % Output : Proof 20.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.15 % Problem : KRS154+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.17 % Command : duper %s % 0.14/0.40 % Computer : n007.cluster.edu % 0.14/0.40 % Model : x86_64 x86_64 % 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.40 % Memory : 8042.1875MB % 0.14/0.40 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.40 % CPULimit : 300 % 0.14/0.40 % WCLimit : 300 % 0.14/0.40 % DateTime : Thu Oct 2 10:20:38 EDT 2025 % 0.14/0.40 % CPUTime : % 19.89/20.16 SZS status Theorem for theBenchmark.p % 19.89/20.16 SZS output start Proof for theBenchmark.p % 19.89/20.16 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 19.89/20.16 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 19.89/20.16 Clause #15 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC110 X) (And (cC102xcomp X) (cC108xcomp X))) True % 19.89/20.16 Clause #21 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC114 X) (And (cC112xcomp X) (cC96xcomp X))) True % 19.89/20.16 Clause #22 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC116 X) (And (cC114 X) (cC80 X))) True % 19.89/20.16 Clause #42 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC136 X) (And (cC134xcomp X) (cC116 X))) True % 19.89/20.16 Clause #93 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC56 X) (And (cC4 X) (cC10xcomp X))) True % 19.89/20.16 Clause #94 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC58 X) (And (cC34 X) (cC56 X))) True % 19.89/20.16 Clause #117 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC80 X) (And (cC78xcomp X) (cC76xcomp X))) True % 19.89/20.16 Clause #136 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC94 X) (And (cC86xcomp X) (cC92xcomp X))) True % 19.89/20.16 Clause #147 (by assumption #[]): Eq (cC102xcomp iV822576) True % 19.89/20.16 Clause #148 (by assumption #[]): Eq (cC108xcomp iV822576) True % 19.89/20.16 Clause #149 (by assumption #[]): Eq (cC4 iV822576) True % 19.89/20.16 Clause #151 (by assumption #[]): Eq (cC112xcomp iV822576) True % 19.89/20.16 Clause #152 (by assumption #[]): Eq (cC76xcomp iV822576) True % 19.89/20.16 Clause #153 (by assumption #[]): Eq (cC96xcomp iV822576) True % 19.89/20.16 Clause #158 (by assumption #[]): Eq (cC78xcomp iV822576) True % 19.89/20.16 Clause #160 (by assumption #[]): Eq (cC134xcomp iV822576) True % 19.89/20.16 Clause #161 (by assumption #[]): Eq (cC86xcomp iV822576) True % 19.89/20.16 Clause #162 (by assumption #[]): Eq (cC34 iV822576) True % 19.89/20.16 Clause #167 (by assumption #[]): Eq (cC10xcomp iV822576) True % 19.89/20.16 Clause #168 (by assumption #[]): Eq (cC92xcomp iV822576) True % 19.89/20.16 Clause #169 (by assumption #[]): Eq % 19.89/20.16 (Not % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And % 19.89/20.16 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 19.89/20.16 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 19.89/20.16 (cC58 iV822576)) % 19.89/20.16 (cC116 iV822576)) % 19.89/20.16 (cC114 iV822576)) % 19.89/20.16 (cowlThing iV822576)) % 19.89/20.16 (cC94 iV822576)) % 19.89/20.16 (cC80 iV822576)) % 19.89/20.16 (cC110 iV822576)) % 19.89/20.16 (cC136 iV822576)) % 19.89/20.16 (cC56 iV822576))) % 19.89/20.16 True % 19.89/20.16 Clause #170 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 19.89/20.16 Clause #171 (by clausification #[170]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 19.89/20.16 Clause #172 (by clausification #[170]): ∀ (a : Iota), Eq (cowlThing a) True % 19.89/20.16 Clause #173 (by clausification #[171]): ∀ (a : Iota), Eq (cowlNothing a) False % 19.89/20.16 Clause #174 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 19.89/20.16 Clause #175 (by clausification #[174]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 19.89/20.16 Clause #176 (by clausification #[174]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 19.89/20.16 Clause #177 (by clausification #[175]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 19.89/20.16 Clause #196 (by clausification #[176]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 19.89/20.16 Clause #223 (by clausification #[15]): ∀ (a : Iota), Eq (Iff (cC110 a) (And (cC102xcomp a) (cC108xcomp a))) True % 19.89/20.16 Clause #224 (by clausification #[223]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Eq (And (cC102xcomp a) (cC108xcomp a)) False) % 19.89/20.16 Clause #226 (by clausification #[224]): ∀ (a : Iota), Or (Eq (cC110 a) True) (Or (Eq (cC102xcomp a) False) (Eq (cC108xcomp a) False)) % 19.89/20.16 Clause #227 (by superposition #[226, 147]): Or (Eq (cC110 iV822576) True) (Or (Eq (cC108xcomp iV822576) False) (Eq False True)) % 19.89/20.16 Clause #228 (by clausification #[227]): Or (Eq (cC110 iV822576) True) (Eq (cC108xcomp iV822576) False) % 19.89/20.16 Clause #229 (by superposition #[228, 148]): Or (Eq (cC110 iV822576) True) (Eq False True) % 19.99/20.19 Clause #236 (by clausification #[229]): Eq (cC110 iV822576) True % 19.99/20.19 Clause #419 (by clausification #[21]): ∀ (a : Iota), Eq (Iff (cC114 a) (And (cC112xcomp a) (cC96xcomp a))) True % 19.99/20.19 Clause #420 (by clausification #[419]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Eq (And (cC112xcomp a) (cC96xcomp a)) False) % 19.99/20.19 Clause #422 (by clausification #[420]): ∀ (a : Iota), Or (Eq (cC114 a) True) (Or (Eq (cC112xcomp a) False) (Eq (cC96xcomp a) False)) % 19.99/20.19 Clause #423 (by superposition #[422, 151]): Or (Eq (cC114 iV822576) True) (Or (Eq (cC96xcomp iV822576) False) (Eq False True)) % 19.99/20.19 Clause #425 (by clausification #[423]): Or (Eq (cC114 iV822576) True) (Eq (cC96xcomp iV822576) False) % 19.99/20.19 Clause #426 (by superposition #[425, 153]): Or (Eq (cC114 iV822576) True) (Eq False True) % 19.99/20.19 Clause #427 (by clausification #[426]): Eq (cC114 iV822576) True % 19.99/20.19 Clause #432 (by clausification #[22]): ∀ (a : Iota), Eq (Iff (cC116 a) (And (cC114 a) (cC80 a))) True % 19.99/20.19 Clause #433 (by clausification #[432]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Eq (And (cC114 a) (cC80 a)) False) % 19.99/20.19 Clause #435 (by clausification #[433]): ∀ (a : Iota), Or (Eq (cC116 a) True) (Or (Eq (cC114 a) False) (Eq (cC80 a) False)) % 19.99/20.19 Clause #436 (by superposition #[435, 427]): Or (Eq (cC116 iV822576) True) (Or (Eq (cC80 iV822576) False) (Eq False True)) % 19.99/20.19 Clause #438 (by clausification #[436]): Or (Eq (cC116 iV822576) True) (Eq (cC80 iV822576) False) % 19.99/20.19 Clause #473 (by clausification #[117]): ∀ (a : Iota), Eq (Iff (cC80 a) (And (cC78xcomp a) (cC76xcomp a))) True % 19.99/20.19 Clause #474 (by clausification #[473]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Eq (And (cC78xcomp a) (cC76xcomp a)) False) % 19.99/20.19 Clause #476 (by clausification #[474]): ∀ (a : Iota), Or (Eq (cC80 a) True) (Or (Eq (cC78xcomp a) False) (Eq (cC76xcomp a) False)) % 19.99/20.19 Clause #477 (by superposition #[476, 158]): Or (Eq (cC80 iV822576) True) (Or (Eq (cC76xcomp iV822576) False) (Eq False True)) % 19.99/20.19 Clause #478 (by clausification #[477]): Or (Eq (cC80 iV822576) True) (Eq (cC76xcomp iV822576) False) % 19.99/20.19 Clause #479 (by superposition #[478, 152]): Or (Eq (cC80 iV822576) True) (Eq False True) % 19.99/20.19 Clause #480 (by clausification #[479]): Eq (cC80 iV822576) True % 19.99/20.19 Clause #481 (by backward demodulation #[480, 438]): Or (Eq (cC116 iV822576) True) (Eq True False) % 19.99/20.19 Clause #490 (by clausification #[481]): Eq (cC116 iV822576) True % 19.99/20.19 Clause #670 (by clausification #[94]): ∀ (a : Iota), Eq (Iff (cC58 a) (And (cC34 a) (cC56 a))) True % 19.99/20.19 Clause #671 (by clausification #[670]): ∀ (a : Iota), Or (Eq (cC58 a) True) (Eq (And (cC34 a) (cC56 a)) False) % 19.99/20.19 Clause #673 (by clausification #[671]): ∀ (a : Iota), Or (Eq (cC58 a) True) (Or (Eq (cC34 a) False) (Eq (cC56 a) False)) % 19.99/20.19 Clause #674 (by superposition #[673, 162]): Or (Eq (cC58 iV822576) True) (Or (Eq (cC56 iV822576) False) (Eq False True)) % 19.99/20.19 Clause #675 (by clausification #[674]): Or (Eq (cC58 iV822576) True) (Eq (cC56 iV822576) False) % 19.99/20.19 Clause #712 (by clausification #[42]): ∀ (a : Iota), Eq (Iff (cC136 a) (And (cC134xcomp a) (cC116 a))) True % 19.99/20.19 Clause #713 (by clausification #[712]): ∀ (a : Iota), Or (Eq (cC136 a) True) (Eq (And (cC134xcomp a) (cC116 a)) False) % 19.99/20.19 Clause #715 (by clausification #[713]): ∀ (a : Iota), Or (Eq (cC136 a) True) (Or (Eq (cC134xcomp a) False) (Eq (cC116 a) False)) % 19.99/20.19 Clause #716 (by superposition #[715, 160]): Or (Eq (cC136 iV822576) True) (Or (Eq (cC116 iV822576) False) (Eq False True)) % 19.99/20.19 Clause #719 (by clausification #[716]): Or (Eq (cC136 iV822576) True) (Eq (cC116 iV822576) False) % 19.99/20.19 Clause #720 (by forward demodulation #[719, 490]): Or (Eq (cC136 iV822576) True) (Eq True False) % 19.99/20.19 Clause #721 (by clausification #[720]): Eq (cC136 iV822576) True % 19.99/20.19 Clause #869 (by clausification #[93]): ∀ (a : Iota), Eq (Iff (cC56 a) (And (cC4 a) (cC10xcomp a))) True % 19.99/20.19 Clause #870 (by clausification #[869]): ∀ (a : Iota), Or (Eq (cC56 a) True) (Eq (And (cC4 a) (cC10xcomp a)) False) % 19.99/20.19 Clause #872 (by clausification #[870]): ∀ (a : Iota), Or (Eq (cC56 a) True) (Or (Eq (cC4 a) False) (Eq (cC10xcomp a) False)) % 19.99/20.19 Clause #873 (by superposition #[872, 149]): Or (Eq (cC56 iV822576) True) (Or (Eq (cC10xcomp iV822576) False) (Eq False True)) % 19.99/20.19 Clause #874 (by clausification #[873]): Or (Eq (cC56 iV822576) True) (Eq (cC10xcomp iV822576) False) % 20.01/20.21 Clause #875 (by forward demodulation #[874, 167]): Or (Eq (cC56 iV822576) True) (Eq True False) % 20.01/20.21 Clause #876 (by clausification #[875]): Eq (cC56 iV822576) True % 20.01/20.21 Clause #877 (by superposition #[876, 675]): Or (Eq (cC58 iV822576) True) (Eq True False) % 20.01/20.21 Clause #878 (by clausification #[877]): Eq (cC58 iV822576) True % 20.01/20.21 Clause #1230 (by clausification #[136]): ∀ (a : Iota), Eq (Iff (cC94 a) (And (cC86xcomp a) (cC92xcomp a))) True % 20.01/20.21 Clause #1231 (by clausification #[1230]): ∀ (a : Iota), Or (Eq (cC94 a) True) (Eq (And (cC86xcomp a) (cC92xcomp a)) False) % 20.01/20.21 Clause #1233 (by clausification #[1231]): ∀ (a : Iota), Or (Eq (cC94 a) True) (Or (Eq (cC86xcomp a) False) (Eq (cC92xcomp a) False)) % 20.01/20.21 Clause #1234 (by superposition #[1233, 161]): Or (Eq (cC94 iV822576) True) (Or (Eq (cC92xcomp iV822576) False) (Eq False True)) % 20.01/20.21 Clause #1235 (by clausification #[1234]): Or (Eq (cC94 iV822576) True) (Eq (cC92xcomp iV822576) False) % 20.01/20.21 Clause #1236 (by forward demodulation #[1235, 168]): Or (Eq (cC94 iV822576) True) (Eq True False) % 20.01/20.21 Clause #1237 (by clausification #[1236]): Eq (cC94 iV822576) True % 20.01/20.21 Clause #1723 (by clausification #[169]): Eq % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.01/20.21 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.01/20.21 (cC58 iV822576)) % 20.01/20.21 (cC116 iV822576)) % 20.01/20.21 (cC114 iV822576)) % 20.01/20.21 (cowlThing iV822576)) % 20.01/20.21 (cC94 iV822576)) % 20.01/20.21 (cC80 iV822576)) % 20.01/20.21 (cC110 iV822576)) % 20.01/20.21 (cC136 iV822576)) % 20.01/20.21 (cC56 iV822576)) % 20.01/20.21 False % 20.01/20.21 Clause #1724 (by clausification #[1723]): Or % 20.01/20.21 (Eq % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.01/20.21 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.01/20.21 (cC58 iV822576)) % 20.01/20.21 (cC116 iV822576)) % 20.01/20.21 (cC114 iV822576)) % 20.01/20.21 (cowlThing iV822576)) % 20.01/20.21 (cC94 iV822576)) % 20.01/20.21 (cC80 iV822576)) % 20.01/20.21 (cC110 iV822576)) % 20.01/20.21 (cC136 iV822576)) % 20.01/20.21 False) % 20.01/20.21 (Eq (cC56 iV822576) False) % 20.01/20.21 Clause #1725 (by clausification #[1724]): Or (Eq (cC56 iV822576) False) % 20.01/20.21 (Or % 20.01/20.21 (Eq % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.01/20.21 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.01/20.21 (cC58 iV822576)) % 20.01/20.21 (cC116 iV822576)) % 20.01/20.21 (cC114 iV822576)) % 20.01/20.21 (cowlThing iV822576)) % 20.01/20.21 (cC94 iV822576)) % 20.01/20.21 (cC80 iV822576)) % 20.01/20.21 (cC110 iV822576)) % 20.01/20.21 False) % 20.01/20.21 (Eq (cC136 iV822576) False)) % 20.01/20.21 Clause #1726 (by clausification #[1725]): Or (Eq (cC56 iV822576) False) % 20.01/20.21 (Or (Eq (cC136 iV822576) False) % 20.01/20.21 (Or % 20.01/20.21 (Eq % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.01/20.21 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.01/20.21 (cC58 iV822576)) % 20.01/20.21 (cC116 iV822576)) % 20.01/20.21 (cC114 iV822576)) % 20.01/20.21 (cowlThing iV822576)) % 20.01/20.21 (cC94 iV822576)) % 20.01/20.21 (cC80 iV822576)) % 20.01/20.21 False) % 20.01/20.21 (Eq (cC110 iV822576) False))) % 20.01/20.21 Clause #1727 (by clausification #[1726]): Or (Eq (cC56 iV822576) False) % 20.01/20.21 (Or (Eq (cC136 iV822576) False) % 20.01/20.21 (Or (Eq (cC110 iV822576) False) % 20.01/20.21 (Or % 20.01/20.21 (Eq % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And % 20.01/20.21 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.01/20.21 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 (cC58 iV822576)) % 20.03/20.23 (cC116 iV822576)) % 20.03/20.23 (cC114 iV822576)) % 20.03/20.23 (cowlThing iV822576)) % 20.03/20.23 (cC94 iV822576)) % 20.03/20.23 False) % 20.03/20.23 (Eq (cC80 iV822576) False)))) % 20.03/20.23 Clause #1728 (by clausification #[1727]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or % 20.03/20.23 (Eq % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.03/20.23 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 (cC58 iV822576)) % 20.03/20.23 (cC116 iV822576)) % 20.03/20.23 (cC114 iV822576)) % 20.03/20.23 (cowlThing iV822576)) % 20.03/20.23 False) % 20.03/20.23 (Eq (cC94 iV822576) False))))) % 20.03/20.23 Clause #1729 (by clausification #[1728]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or (Eq (cC94 iV822576) False) % 20.03/20.23 (Or % 20.03/20.23 (Eq % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.03/20.23 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 (cC58 iV822576)) % 20.03/20.23 (cC116 iV822576)) % 20.03/20.23 (cC114 iV822576)) % 20.03/20.23 False) % 20.03/20.23 (Eq (cowlThing iV822576) False)))))) % 20.03/20.23 Clause #1730 (by clausification #[1729]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or (Eq (cC94 iV822576) False) % 20.03/20.23 (Or (Eq (cowlThing iV822576) False) % 20.03/20.23 (Or % 20.03/20.23 (Eq % 20.03/20.23 (And % 20.03/20.23 (And % 20.03/20.23 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.03/20.23 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 (cC58 iV822576)) % 20.03/20.23 (cC116 iV822576)) % 20.03/20.23 False) % 20.03/20.23 (Eq (cC114 iV822576) False))))))) % 20.03/20.23 Clause #1731 (by clausification #[1730]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or (Eq (cC94 iV822576) False) % 20.03/20.23 (Or (Eq (cowlThing iV822576) False) % 20.03/20.23 (Or (Eq (cC114 iV822576) False) % 20.03/20.23 (Or % 20.03/20.23 (Eq % 20.03/20.23 (And % 20.03/20.23 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.03/20.23 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 (cC58 iV822576)) % 20.03/20.23 False) % 20.03/20.23 (Eq (cC116 iV822576) False)))))))) % 20.03/20.23 Clause #1732 (by clausification #[1731]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or (Eq (cC94 iV822576) False) % 20.03/20.23 (Or (Eq (cowlThing iV822576) False) % 20.03/20.23 (Or (Eq (cC114 iV822576) False) % 20.03/20.23 (Or (Eq (cC116 iV822576) False) % 20.03/20.23 (Or % 20.03/20.23 (Eq % 20.03/20.23 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 20.03/20.23 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 20.03/20.23 False) % 20.03/20.23 (Eq (cC58 iV822576) False))))))))) % 20.03/20.23 Clause #1733 (by clausification #[1732]): Or (Eq (cC56 iV822576) False) % 20.03/20.23 (Or (Eq (cC136 iV822576) False) % 20.03/20.23 (Or (Eq (cC110 iV822576) False) % 20.03/20.23 (Or (Eq (cC80 iV822576) False) % 20.03/20.23 (Or (Eq (cC94 iV822576) False) % 20.03/20.23 (Or (Eq (cowlThing iV822576) False) % 20.03/20.23 (Or (Eq (cC114 iV822576) False) % 20.03/20.23 (Or (Eq (cC116 iV822576) False) % 20.03/20.23 (Or (Eq (cC58 iV822576) False) % 20.03/20.23 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 20.03/20.23 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)))))))))) % 20.03/20.26 Clause #1734 (by clausification #[1733]): ∀ (a : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 20.03/20.26 (Eq (Not (And (cowlThing (skS.0 78 a)) (Not (cowlNothing (skS.0 78 a))))) True)))))))))) % 20.03/20.26 Clause #1735 (by clausification #[1734]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (Not (And (cowlThing (skS.0 78 a)) (Not (cowlNothing (skS.0 78 a))))) True) % 20.03/20.26 (Eq (Not (Iff (xsd_string (skS.0 79 a_1)) (Not (xsd_integer (skS.0 79 a_1))))) True)))))))))) % 20.03/20.26 Clause #1736 (by clausification #[1735]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (Not (Iff (xsd_string (skS.0 79 a)) (Not (xsd_integer (skS.0 79 a))))) True) % 20.03/20.26 (Eq (And (cowlThing (skS.0 78 a_1)) (Not (cowlNothing (skS.0 78 a_1)))) False)))))))))) % 20.03/20.26 Clause #1737 (by clausification #[1736]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (And (cowlThing (skS.0 78 a)) (Not (cowlNothing (skS.0 78 a)))) False) % 20.03/20.26 (Eq (Iff (xsd_string (skS.0 79 a_1)) (Not (xsd_integer (skS.0 79 a_1)))) False)))))))))) % 20.03/20.26 Clause #1738 (by clausification #[1737]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (Iff (xsd_string (skS.0 79 a)) (Not (xsd_integer (skS.0 79 a)))) False) % 20.03/20.26 (Or (Eq (cowlThing (skS.0 78 a_1)) False) (Eq (Not (cowlNothing (skS.0 78 a_1))) False))))))))))) % 20.03/20.26 Clause #1739 (by clausification #[1738]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.26 (Or (Eq (cC110 iV822576) False) % 20.03/20.26 (Or (Eq (cC80 iV822576) False) % 20.03/20.26 (Or (Eq (cC94 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing iV822576) False) % 20.03/20.26 (Or (Eq (cC114 iV822576) False) % 20.03/20.26 (Or (Eq (cC116 iV822576) False) % 20.03/20.26 (Or (Eq (cC58 iV822576) False) % 20.03/20.26 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.26 (Or (Eq (Not (cowlNothing (skS.0 78 a))) False) % 20.03/20.26 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.26 (Eq (Not (xsd_integer (skS.0 79 a_1))) False)))))))))))) % 20.03/20.26 Clause #1740 (by clausification #[1738]): ∀ (a a_1 : Iota), % 20.03/20.26 Or (Eq (cC56 iV822576) False) % 20.03/20.26 (Or (Eq (cC136 iV822576) False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (Not (cowlNothing (skS.0 78 a))) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.03/20.28 (Eq (Not (xsd_integer (skS.0 79 a_1))) True)))))))))))) % 20.03/20.28 Clause #1741 (by clausification #[1739]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq (cC56 iV822576) False) % 20.03/20.28 (Or (Eq (cC136 iV822576) False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.28 (Or (Eq (Not (xsd_integer (skS.0 79 a_1))) False) % 20.03/20.28 (Eq (cowlNothing (skS.0 78 a)) True)))))))))))) % 20.03/20.28 Clause #1742 (by clausification #[1741]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq (cC56 iV822576) False) % 20.03/20.28 (Or (Eq (cC136 iV822576) False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.28 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))))))) % 20.03/20.28 Clause #1743 (by forward demodulation #[1742, 876]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq True False) % 20.03/20.28 (Or (Eq (cC136 iV822576) False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.28 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))))))) % 20.03/20.28 Clause #1744 (by clausification #[1743]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq (cC136 iV822576) False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.28 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))))))) % 20.03/20.28 Clause #1745 (by forward demodulation #[1744, 721]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq True False) % 20.03/20.28 (Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.28 (Or (Eq (cC114 iV822576) False) % 20.03/20.28 (Or (Eq (cC116 iV822576) False) % 20.03/20.28 (Or (Eq (cC58 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.28 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.28 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))))))) % 20.03/20.28 Clause #1746 (by clausification #[1745]): ∀ (a a_1 : Iota), % 20.03/20.28 Or (Eq (cC110 iV822576) False) % 20.03/20.28 (Or (Eq (cC80 iV822576) False) % 20.03/20.28 (Or (Eq (cC94 iV822576) False) % 20.03/20.28 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))))) % 20.03/20.30 Clause #1747 (by forward demodulation #[1746, 236]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq True False) % 20.03/20.30 (Or (Eq (cC80 iV822576) False) % 20.03/20.30 (Or (Eq (cC94 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))))) % 20.03/20.30 Clause #1748 (by clausification #[1747]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq (cC80 iV822576) False) % 20.03/20.30 (Or (Eq (cC94 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))))) % 20.03/20.30 Clause #1749 (by forward demodulation #[1748, 480]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq True False) % 20.03/20.30 (Or (Eq (cC94 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))))) % 20.03/20.30 Clause #1750 (by clausification #[1749]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq (cC94 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))) % 20.03/20.30 Clause #1751 (by forward demodulation #[1750, 1237]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq True False) % 20.03/20.30 (Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))))) % 20.03/20.30 Clause #1752 (by clausification #[1751]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq (cowlThing iV822576) False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))) % 20.03/20.30 Clause #1753 (by forward demodulation #[1752, 172]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq True False) % 20.03/20.30 (Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))))) % 20.03/20.30 Clause #1754 (by clausification #[1753]): ∀ (a a_1 : Iota), % 20.03/20.30 Or (Eq (cC114 iV822576) False) % 20.03/20.30 (Or (Eq (cC116 iV822576) False) % 20.03/20.30 (Or (Eq (cC58 iV822576) False) % 20.03/20.30 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.03/20.30 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.03/20.30 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))) % 20.12/20.33 Clause #1755 (by forward demodulation #[1754, 427]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq True False) % 20.12/20.33 (Or (Eq (cC116 iV822576) False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))))) % 20.12/20.33 Clause #1756 (by clausification #[1755]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (cC116 iV822576) False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))) % 20.12/20.33 Clause #1757 (by forward demodulation #[1756, 490]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq True False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))))) % 20.12/20.33 Clause #1758 (by clausification #[1757]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))) % 20.12/20.33 Clause #1759 (by forward demodulation #[1758, 878]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq True False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)))) % 20.12/20.33 Clause #1760 (by clausification #[1759]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True))) % 20.12/20.33 Clause #1761 (by forward demodulation #[1760, 172]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq True False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Eq (xsd_integer (skS.0 79 a)) True))) % 20.12/20.33 Clause #1762 (by clausification #[1761]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (xsd_string (skS.0 79 a)) False) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Eq (xsd_integer (skS.0 79 a)) True)) % 20.12/20.33 Clause #2288 (by clausification #[1740]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (cC56 iV822576) False) % 20.12/20.33 (Or (Eq (cC136 iV822576) False) % 20.12/20.33 (Or (Eq (cC110 iV822576) False) % 20.12/20.33 (Or (Eq (cC80 iV822576) False) % 20.12/20.33 (Or (Eq (cC94 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing iV822576) False) % 20.12/20.33 (Or (Eq (cC114 iV822576) False) % 20.12/20.33 (Or (Eq (cC116 iV822576) False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.33 (Or (Eq (Not (xsd_integer (skS.0 79 a_1))) True) (Eq (cowlNothing (skS.0 78 a)) True)))))))))))) % 20.12/20.33 Clause #2289 (by clausification #[2288]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq (cC56 iV822576) False) % 20.12/20.33 (Or (Eq (cC136 iV822576) False) % 20.12/20.33 (Or (Eq (cC110 iV822576) False) % 20.12/20.33 (Or (Eq (cC80 iV822576) False) % 20.12/20.33 (Or (Eq (cC94 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing iV822576) False) % 20.12/20.33 (Or (Eq (cC114 iV822576) False) % 20.12/20.33 (Or (Eq (cC116 iV822576) False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.33 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.33 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))))))) % 20.12/20.33 Clause #2290 (by forward demodulation #[2289, 876]): ∀ (a a_1 : Iota), % 20.12/20.33 Or (Eq True False) % 20.12/20.33 (Or (Eq (cC136 iV822576) False) % 20.12/20.33 (Or (Eq (cC110 iV822576) False) % 20.12/20.33 (Or (Eq (cC80 iV822576) False) % 20.12/20.33 (Or (Eq (cC94 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing iV822576) False) % 20.12/20.33 (Or (Eq (cC114 iV822576) False) % 20.12/20.33 (Or (Eq (cC116 iV822576) False) % 20.12/20.33 (Or (Eq (cC58 iV822576) False) % 20.12/20.33 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))))))) % 20.12/20.36 Clause #2291 (by clausification #[2290]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq (cC136 iV822576) False) % 20.12/20.36 (Or (Eq (cC110 iV822576) False) % 20.12/20.36 (Or (Eq (cC80 iV822576) False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))))))) % 20.12/20.36 Clause #2292 (by forward demodulation #[2291, 721]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq True False) % 20.12/20.36 (Or (Eq (cC110 iV822576) False) % 20.12/20.36 (Or (Eq (cC80 iV822576) False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))))))) % 20.12/20.36 Clause #2293 (by clausification #[2292]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq (cC110 iV822576) False) % 20.12/20.36 (Or (Eq (cC80 iV822576) False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))))) % 20.12/20.36 Clause #2294 (by forward demodulation #[2293, 236]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq True False) % 20.12/20.36 (Or (Eq (cC80 iV822576) False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))))) % 20.12/20.36 Clause #2295 (by clausification #[2294]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq (cC80 iV822576) False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))))) % 20.12/20.36 Clause #2296 (by forward demodulation #[2295, 480]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq True False) % 20.12/20.36 (Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))))) % 20.12/20.36 Clause #2297 (by clausification #[2296]): ∀ (a a_1 : Iota), % 20.12/20.36 Or (Eq (cC94 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing iV822576) False) % 20.12/20.36 (Or (Eq (cC114 iV822576) False) % 20.12/20.36 (Or (Eq (cC116 iV822576) False) % 20.12/20.36 (Or (Eq (cC58 iV822576) False) % 20.12/20.36 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.36 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.36 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))) % 20.12/20.36 Clause #2298 (by forward demodulation #[2297, 1237]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (cowlThing iV822576) False) % 20.12/20.38 (Or (Eq (cC114 iV822576) False) % 20.12/20.38 (Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))))) % 20.12/20.38 Clause #2299 (by clausification #[2298]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (cowlThing iV822576) False) % 20.12/20.38 (Or (Eq (cC114 iV822576) False) % 20.12/20.38 (Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))) % 20.12/20.38 Clause #2300 (by forward demodulation #[2299, 172]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (cC114 iV822576) False) % 20.12/20.38 (Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))))) % 20.12/20.38 Clause #2301 (by clausification #[2300]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (cC114 iV822576) False) % 20.12/20.38 (Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))) % 20.12/20.38 Clause #2302 (by forward demodulation #[2301, 427]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))))) % 20.12/20.38 Clause #2303 (by clausification #[2302]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (cC116 iV822576) False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))) % 20.12/20.38 Clause #2304 (by forward demodulation #[2303, 490]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))))) % 20.12/20.38 Clause #2305 (by clausification #[2304]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (cC58 iV822576) False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))) % 20.12/20.38 Clause #2306 (by forward demodulation #[2305, 878]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False)))) % 20.12/20.38 Clause #2307 (by clausification #[2306]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (cowlThing (skS.0 78 a)) False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a_1)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) False))) % 20.12/20.38 Clause #2308 (by forward demodulation #[2307, 172]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq True False) % 20.12/20.38 (Or (Eq (xsd_string (skS.0 79 a)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Eq (xsd_integer (skS.0 79 a)) False))) % 20.12/20.38 Clause #2309 (by clausification #[2308]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (xsd_string (skS.0 79 a)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Eq (xsd_integer (skS.0 79 a)) False)) % 20.12/20.38 Clause #2310 (by superposition #[2309, 177]): ∀ (a a_1 : Iota), % 20.12/20.38 Or (Eq (xsd_string (skS.0 79 a)) True) % 20.12/20.38 (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Or (Eq (xsd_string (skS.0 79 a)) True) (Eq False True))) % 20.12/20.38 Clause #3089 (by clausification #[2310]): ∀ (a a_1 : Iota), % 20.20/20.40 Or (Eq (xsd_string (skS.0 79 a)) True) (Or (Eq (cowlNothing (skS.0 78 a_1)) True) (Eq (xsd_string (skS.0 79 a)) True)) % 20.20/20.40 Clause #3090 (by eliminate duplicate literals #[3089]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 79 a)) True) (Eq (cowlNothing (skS.0 78 a_1)) True) % 20.20/20.40 Clause #3093 (by superposition #[3090, 173]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 79 a)) True) (Eq True False) % 20.20/20.40 Clause #3094 (by clausification #[3093]): ∀ (a : Iota), Eq (xsd_string (skS.0 79 a)) True % 20.20/20.40 Clause #3095 (by backward demodulation #[3094, 1762]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True)) % 20.20/20.40 Clause #3096 (by superposition #[3094, 196]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 79 a)) False) % 20.20/20.40 Clause #3097 (by clausification #[3096]): ∀ (a : Iota), Eq (xsd_integer (skS.0 79 a)) False % 20.20/20.40 Clause #3099 (by clausification #[3095]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq (xsd_integer (skS.0 79 a_1)) True) % 20.20/20.40 Clause #3101 (by superposition #[3099, 3097]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 78 a)) True) (Eq True False) % 20.20/20.40 Clause #3102 (by clausification #[3101]): ∀ (a : Iota), Eq (cowlNothing (skS.0 78 a)) True % 20.20/20.40 Clause #3103 (by superposition #[3102, 173]): Eq True False % 20.20/20.40 Clause #3106 (by clausification #[3103]): False % 20.20/20.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------