%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS149+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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 51.83s 52.04s % Output : Proof 52.03s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : KRS149+1 : TPTP v9.2.0. Released v3.1.0. % 0.13/0.13 % Command : duper %s % 0.13/0.34 % Computer : n008.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 10:19:08 EDT 2025 % 0.13/0.35 % CPUTime : % 51.83/52.04 SZS status Theorem for theBenchmark.p % 51.83/52.04 SZS output start Proof for theBenchmark.p % 51.83/52.04 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 51.83/52.04 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 51.83/52.04 Clause #70 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC30 X) (And (cC14 X) (cC28 X))) True % 51.83/52.04 Clause #78 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC46 X) (And (cC30 X) (cC44 X))) True % 51.83/52.04 Clause #88 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC64 X) (And (Not (cC62 X)) (cTOP X))) True % 51.83/52.04 Clause #107 (by assumption #[]): Eq (∀ (X : Iota), Iff (cTEST X) (And (cC216 X) (cC46 X))) True % 51.83/52.04 Clause #108 (by assumption #[]): Eq (cTEST iV3102) True % 51.83/52.04 Clause #112 (by assumption #[]): Eq (cTOP iV3102) True % 51.83/52.04 Clause #119 (by assumption #[]): Eq (Not (cC62 iV3102)) True % 51.83/52.04 Clause #125 (by assumption #[]): Eq % 51.83/52.04 (Not % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And % 51.83/52.04 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.04 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.04 (cC216 iV3102)) % 51.83/52.04 (cC46 iV3102)) % 51.83/52.04 (cC30 iV3102)) % 51.83/52.04 (cC44 iV3102)) % 51.83/52.04 (cC28 iV3102)) % 51.83/52.04 (cC64 iV3102)) % 51.83/52.04 (cC14 iV3102)) % 51.83/52.04 (cowlThing iV3102))) % 51.83/52.04 True % 51.83/52.04 Clause #128 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 51.83/52.04 Clause #129 (by clausification #[128]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 51.83/52.04 Clause #130 (by clausification #[128]): ∀ (a : Iota), Eq (cowlThing a) True % 51.83/52.04 Clause #131 (by clausification #[129]): ∀ (a : Iota), Eq (cowlNothing a) False % 51.83/52.04 Clause #133 (by clausification #[119]): Eq (cC62 iV3102) False % 51.83/52.04 Clause #136 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 51.83/52.04 Clause #137 (by clausification #[136]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 51.83/52.04 Clause #138 (by clausification #[136]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 51.83/52.04 Clause #139 (by clausification #[137]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 51.83/52.04 Clause #163 (by clausification #[138]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 51.83/52.04 Clause #176 (by clausification #[107]): ∀ (a : Iota), Eq (Iff (cTEST a) (And (cC216 a) (cC46 a))) True % 51.83/52.04 Clause #178 (by clausification #[176]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (And (cC216 a) (cC46 a)) True) % 51.83/52.04 Clause #180 (by clausification #[178]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC46 a) True) % 51.83/52.04 Clause #181 (by clausification #[178]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC216 a) True) % 51.83/52.04 Clause #182 (by superposition #[180, 108]): Or (Eq (cC46 iV3102) True) (Eq False True) % 51.83/52.04 Clause #183 (by clausification #[182]): Eq (cC46 iV3102) True % 51.83/52.04 Clause #190 (by superposition #[181, 108]): Or (Eq (cC216 iV3102) True) (Eq False True) % 51.83/52.04 Clause #191 (by clausification #[190]): Eq (cC216 iV3102) True % 51.83/52.04 Clause #316 (by clausification #[78]): ∀ (a : Iota), Eq (Iff (cC46 a) (And (cC30 a) (cC44 a))) True % 51.83/52.04 Clause #318 (by clausification #[316]): ∀ (a : Iota), Or (Eq (cC46 a) False) (Eq (And (cC30 a) (cC44 a)) True) % 51.83/52.04 Clause #320 (by clausification #[318]): ∀ (a : Iota), Or (Eq (cC46 a) False) (Eq (cC44 a) True) % 51.83/52.04 Clause #321 (by clausification #[318]): ∀ (a : Iota), Or (Eq (cC46 a) False) (Eq (cC30 a) True) % 51.83/52.04 Clause #322 (by superposition #[320, 183]): Or (Eq (cC44 iV3102) True) (Eq False True) % 51.83/52.04 Clause #323 (by clausification #[322]): Eq (cC44 iV3102) True % 51.83/52.04 Clause #330 (by superposition #[321, 183]): Or (Eq (cC30 iV3102) True) (Eq False True) % 51.83/52.04 Clause #331 (by clausification #[330]): Eq (cC30 iV3102) True % 51.83/52.04 Clause #352 (by clausification #[70]): ∀ (a : Iota), Eq (Iff (cC30 a) (And (cC14 a) (cC28 a))) True % 51.83/52.04 Clause #354 (by clausification #[352]): ∀ (a : Iota), Or (Eq (cC30 a) False) (Eq (And (cC14 a) (cC28 a)) True) % 51.83/52.04 Clause #362 (by clausification #[354]): ∀ (a : Iota), Or (Eq (cC30 a) False) (Eq (cC28 a) True) % 51.83/52.06 Clause #363 (by clausification #[354]): ∀ (a : Iota), Or (Eq (cC30 a) False) (Eq (cC14 a) True) % 51.83/52.06 Clause #364 (by superposition #[362, 331]): Or (Eq (cC28 iV3102) True) (Eq False True) % 51.83/52.06 Clause #365 (by clausification #[364]): Eq (cC28 iV3102) True % 51.83/52.06 Clause #366 (by superposition #[363, 331]): Or (Eq (cC14 iV3102) True) (Eq False True) % 51.83/52.06 Clause #367 (by clausification #[366]): Eq (cC14 iV3102) True % 51.83/52.06 Clause #382 (by clausification #[88]): ∀ (a : Iota), Eq (Iff (cC64 a) (And (Not (cC62 a)) (cTOP a))) True % 51.83/52.06 Clause #383 (by clausification #[382]): ∀ (a : Iota), Or (Eq (cC64 a) True) (Eq (And (Not (cC62 a)) (cTOP a)) False) % 51.83/52.06 Clause #385 (by clausification #[383]): ∀ (a : Iota), Or (Eq (cC64 a) True) (Or (Eq (Not (cC62 a)) False) (Eq (cTOP a) False)) % 51.83/52.06 Clause #386 (by clausification #[385]): ∀ (a : Iota), Or (Eq (cC64 a) True) (Or (Eq (cTOP a) False) (Eq (cC62 a) True)) % 51.83/52.06 Clause #387 (by superposition #[386, 112]): Or (Eq (cC64 iV3102) True) (Or (Eq (cC62 iV3102) True) (Eq False True)) % 51.83/52.06 Clause #388 (by clausification #[387]): Or (Eq (cC64 iV3102) True) (Eq (cC62 iV3102) True) % 51.83/52.06 Clause #389 (by superposition #[388, 133]): Or (Eq (cC64 iV3102) True) (Eq True False) % 51.83/52.06 Clause #395 (by clausification #[389]): Eq (cC64 iV3102) True % 51.83/52.06 Clause #1146 (by clausification #[125]): Eq % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.06 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.06 (cC216 iV3102)) % 51.83/52.06 (cC46 iV3102)) % 51.83/52.06 (cC30 iV3102)) % 51.83/52.06 (cC44 iV3102)) % 51.83/52.06 (cC28 iV3102)) % 51.83/52.06 (cC64 iV3102)) % 51.83/52.06 (cC14 iV3102)) % 51.83/52.06 (cowlThing iV3102)) % 51.83/52.06 False % 51.83/52.06 Clause #1147 (by clausification #[1146]): Or % 51.83/52.06 (Eq % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.06 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.06 (cC216 iV3102)) % 51.83/52.06 (cC46 iV3102)) % 51.83/52.06 (cC30 iV3102)) % 51.83/52.06 (cC44 iV3102)) % 51.83/52.06 (cC28 iV3102)) % 51.83/52.06 (cC64 iV3102)) % 51.83/52.06 (cC14 iV3102)) % 51.83/52.06 False) % 51.83/52.06 (Eq (cowlThing iV3102) False) % 51.83/52.06 Clause #1148 (by clausification #[1147]): Or (Eq (cowlThing iV3102) False) % 51.83/52.06 (Or % 51.83/52.06 (Eq % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.06 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.06 (cC216 iV3102)) % 51.83/52.06 (cC46 iV3102)) % 51.83/52.06 (cC30 iV3102)) % 51.83/52.06 (cC44 iV3102)) % 51.83/52.06 (cC28 iV3102)) % 51.83/52.06 (cC64 iV3102)) % 51.83/52.06 False) % 51.83/52.06 (Eq (cC14 iV3102) False)) % 51.83/52.06 Clause #1149 (by clausification #[1148]): Or (Eq (cowlThing iV3102) False) % 51.83/52.06 (Or (Eq (cC14 iV3102) False) % 51.83/52.06 (Or % 51.83/52.06 (Eq % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.06 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.06 (cC216 iV3102)) % 51.83/52.06 (cC46 iV3102)) % 51.83/52.06 (cC30 iV3102)) % 51.83/52.06 (cC44 iV3102)) % 51.83/52.06 (cC28 iV3102)) % 51.83/52.06 False) % 51.83/52.06 (Eq (cC64 iV3102) False))) % 51.83/52.06 Clause #1150 (by clausification #[1149]): Or (Eq (cowlThing iV3102) False) % 51.83/52.06 (Or (Eq (cC14 iV3102) False) % 51.83/52.06 (Or (Eq (cC64 iV3102) False) % 51.83/52.06 (Or % 51.83/52.06 (Eq % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And % 51.83/52.06 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.83/52.06 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.83/52.06 (cC216 iV3102)) % 51.83/52.06 (cC46 iV3102)) % 51.83/52.06 (cC30 iV3102)) % 51.83/52.06 (cC44 iV3102)) % 51.83/52.06 False) % 51.83/52.06 (Eq (cC28 iV3102) False)))) % 51.83/52.06 Clause #1151 (by clausification #[1150]): Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or % 51.89/52.09 (Eq % 51.89/52.09 (And % 51.89/52.09 (And % 51.89/52.09 (And % 51.89/52.09 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.89/52.09 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.89/52.09 (cC216 iV3102)) % 51.89/52.09 (cC46 iV3102)) % 51.89/52.09 (cC30 iV3102)) % 51.89/52.09 False) % 51.89/52.09 (Eq (cC44 iV3102) False))))) % 51.89/52.09 Clause #1152 (by clausification #[1151]): Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or % 51.89/52.09 (Eq % 51.89/52.09 (And % 51.89/52.09 (And % 51.89/52.09 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.89/52.09 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.89/52.09 (cC216 iV3102)) % 51.89/52.09 (cC46 iV3102)) % 51.89/52.09 False) % 51.89/52.09 (Eq (cC30 iV3102) False)))))) % 51.89/52.09 Clause #1153 (by clausification #[1152]): Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or (Eq (cC30 iV3102) False) % 51.89/52.09 (Or % 51.89/52.09 (Eq % 51.89/52.09 (And % 51.89/52.09 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.89/52.09 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.89/52.09 (cC216 iV3102)) % 51.89/52.09 False) % 51.89/52.09 (Eq (cC46 iV3102) False))))))) % 51.89/52.09 Clause #1154 (by clausification #[1153]): Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or (Eq (cC30 iV3102) False) % 51.89/52.09 (Or (Eq (cC46 iV3102) False) % 51.89/52.09 (Or % 51.89/52.09 (Eq % 51.89/52.09 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 51.89/52.09 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 51.89/52.09 False) % 51.89/52.09 (Eq (cC216 iV3102) False)))))))) % 51.89/52.09 Clause #1155 (by clausification #[1154]): Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or (Eq (cC30 iV3102) False) % 51.89/52.09 (Or (Eq (cC46 iV3102) False) % 51.89/52.09 (Or (Eq (cC216 iV3102) False) % 51.89/52.09 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 51.89/52.09 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False))))))))) % 51.89/52.09 Clause #1156 (by clausification #[1155]): ∀ (a : Iota), % 51.89/52.09 Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or (Eq (cC30 iV3102) False) % 51.89/52.09 (Or (Eq (cC46 iV3102) False) % 51.89/52.09 (Or (Eq (cC216 iV3102) False) % 51.89/52.09 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 51.89/52.09 (Eq (Not (And (cowlThing (skS.0 49 a)) (Not (cowlNothing (skS.0 49 a))))) True))))))))) % 51.89/52.09 Clause #1157 (by clausification #[1156]): ∀ (a a_1 : Iota), % 51.89/52.09 Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.09 (Or (Eq (cC30 iV3102) False) % 51.89/52.09 (Or (Eq (cC46 iV3102) False) % 51.89/52.09 (Or (Eq (cC216 iV3102) False) % 51.89/52.09 (Or (Eq (Not (And (cowlThing (skS.0 49 a)) (Not (cowlNothing (skS.0 49 a))))) True) % 51.89/52.09 (Eq (Not (Iff (xsd_string (skS.0 50 a_1)) (Not (xsd_integer (skS.0 50 a_1))))) True))))))))) % 51.89/52.09 Clause #1158 (by clausification #[1157]): ∀ (a a_1 : Iota), % 51.89/52.09 Or (Eq (cowlThing iV3102) False) % 51.89/52.09 (Or (Eq (cC14 iV3102) False) % 51.89/52.09 (Or (Eq (cC64 iV3102) False) % 51.89/52.09 (Or (Eq (cC28 iV3102) False) % 51.89/52.09 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (Not (Iff (xsd_string (skS.0 50 a)) (Not (xsd_integer (skS.0 50 a))))) True) % 51.89/52.11 (Eq (And (cowlThing (skS.0 49 a_1)) (Not (cowlNothing (skS.0 49 a_1)))) False))))))))) % 51.89/52.11 Clause #1159 (by clausification #[1158]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (And (cowlThing (skS.0 49 a)) (Not (cowlNothing (skS.0 49 a)))) False) % 51.89/52.11 (Eq (Iff (xsd_string (skS.0 50 a_1)) (Not (xsd_integer (skS.0 50 a_1)))) False))))))))) % 51.89/52.11 Clause #1160 (by clausification #[1159]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (Iff (xsd_string (skS.0 50 a)) (Not (xsd_integer (skS.0 50 a)))) False) % 51.89/52.11 (Or (Eq (cowlThing (skS.0 49 a_1)) False) (Eq (Not (cowlNothing (skS.0 49 a_1))) False)))))))))) % 51.89/52.11 Clause #1161 (by clausification #[1160]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.11 (Or (Eq (Not (cowlNothing (skS.0 49 a))) False) % 51.89/52.11 (Or (Eq (xsd_string (skS.0 50 a_1)) False) (Eq (Not (xsd_integer (skS.0 50 a_1))) False))))))))))) % 51.89/52.11 Clause #1162 (by clausification #[1160]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.11 (Or (Eq (Not (cowlNothing (skS.0 49 a))) False) % 51.89/52.11 (Or (Eq (xsd_string (skS.0 50 a_1)) True) (Eq (Not (xsd_integer (skS.0 50 a_1))) True))))))))))) % 51.89/52.11 Clause #1163 (by clausification #[1161]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.11 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.11 (Or (Eq (Not (xsd_integer (skS.0 50 a_1))) False) (Eq (cowlNothing (skS.0 49 a)) True))))))))))) % 51.89/52.11 Clause #1164 (by clausification #[1163]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq (cowlThing iV3102) False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.11 (Or (Eq (cC64 iV3102) False) % 51.89/52.11 (Or (Eq (cC28 iV3102) False) % 51.89/52.11 (Or (Eq (cC44 iV3102) False) % 51.89/52.11 (Or (Eq (cC30 iV3102) False) % 51.89/52.11 (Or (Eq (cC46 iV3102) False) % 51.89/52.11 (Or (Eq (cC216 iV3102) False) % 51.89/52.11 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.11 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.11 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))))))) % 51.89/52.11 Clause #1165 (by forward demodulation #[1164, 130]): ∀ (a a_1 : Iota), % 51.89/52.11 Or (Eq True False) % 51.89/52.11 (Or (Eq (cC14 iV3102) False) % 51.89/52.13 (Or (Eq (cC64 iV3102) False) % 51.89/52.13 (Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))))))) % 51.89/52.13 Clause #1166 (by clausification #[1165]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq (cC14 iV3102) False) % 51.89/52.13 (Or (Eq (cC64 iV3102) False) % 51.89/52.13 (Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))))))) % 51.89/52.13 Clause #1167 (by forward demodulation #[1166, 367]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq True False) % 51.89/52.13 (Or (Eq (cC64 iV3102) False) % 51.89/52.13 (Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))))))) % 51.89/52.13 Clause #1168 (by clausification #[1167]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq (cC64 iV3102) False) % 51.89/52.13 (Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))))) % 51.89/52.13 Clause #1169 (by forward demodulation #[1168, 395]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq True False) % 51.89/52.13 (Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))))) % 51.89/52.13 Clause #1170 (by clausification #[1169]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq (cC28 iV3102) False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))))) % 51.89/52.13 Clause #1171 (by forward demodulation #[1170, 365]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq True False) % 51.89/52.13 (Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))))) % 51.89/52.13 Clause #1172 (by clausification #[1171]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq (cC44 iV3102) False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.89/52.13 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.89/52.13 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))) % 51.89/52.13 Clause #1173 (by forward demodulation #[1172, 323]): ∀ (a a_1 : Iota), % 51.89/52.13 Or (Eq True False) % 51.89/52.13 (Or (Eq (cC30 iV3102) False) % 51.89/52.13 (Or (Eq (cC46 iV3102) False) % 51.89/52.13 (Or (Eq (cC216 iV3102) False) % 51.89/52.13 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))))) % 51.97/52.16 Clause #1174 (by clausification #[1173]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cC30 iV3102) False) % 51.97/52.16 (Or (Eq (cC46 iV3102) False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))) % 51.97/52.16 Clause #1175 (by forward demodulation #[1174, 331]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq True False) % 51.97/52.16 (Or (Eq (cC46 iV3102) False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))))) % 51.97/52.16 Clause #1176 (by clausification #[1175]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cC46 iV3102) False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))) % 51.97/52.16 Clause #1177 (by forward demodulation #[1176, 183]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq True False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))))) % 51.97/52.16 Clause #1178 (by clausification #[1177]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))) % 51.97/52.16 Clause #1179 (by forward demodulation #[1178, 191]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq True False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)))) % 51.97/52.16 Clause #1180 (by clausification #[1179]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True))) % 51.97/52.16 Clause #1181 (by forward demodulation #[1180, 130]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq True False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Eq (xsd_integer (skS.0 50 a)) True))) % 51.97/52.16 Clause #1182 (by clausification #[1181]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (xsd_string (skS.0 50 a)) False) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Eq (xsd_integer (skS.0 50 a)) True)) % 51.97/52.16 Clause #2146 (by clausification #[1162]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cowlThing iV3102) False) % 51.97/52.16 (Or (Eq (cC14 iV3102) False) % 51.97/52.16 (Or (Eq (cC64 iV3102) False) % 51.97/52.16 (Or (Eq (cC28 iV3102) False) % 51.97/52.16 (Or (Eq (cC44 iV3102) False) % 51.97/52.16 (Or (Eq (cC30 iV3102) False) % 51.97/52.16 (Or (Eq (cC46 iV3102) False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.97/52.16 (Or (Eq (Not (xsd_integer (skS.0 50 a_1))) True) (Eq (cowlNothing (skS.0 49 a)) True))))))))))) % 51.97/52.16 Clause #2147 (by clausification #[2146]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq (cowlThing iV3102) False) % 51.97/52.16 (Or (Eq (cC14 iV3102) False) % 51.97/52.16 (Or (Eq (cC64 iV3102) False) % 51.97/52.16 (Or (Eq (cC28 iV3102) False) % 51.97/52.16 (Or (Eq (cC44 iV3102) False) % 51.97/52.16 (Or (Eq (cC30 iV3102) False) % 51.97/52.16 (Or (Eq (cC46 iV3102) False) % 51.97/52.16 (Or (Eq (cC216 iV3102) False) % 51.97/52.16 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.97/52.16 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.97/52.16 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))))))) % 51.97/52.16 Clause #2148 (by forward demodulation #[2147, 130]): ∀ (a a_1 : Iota), % 51.97/52.16 Or (Eq True False) % 51.97/52.16 (Or (Eq (cC14 iV3102) False) % 51.99/52.18 (Or (Eq (cC64 iV3102) False) % 51.99/52.18 (Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))))))) % 51.99/52.18 Clause #2149 (by clausification #[2148]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq (cC14 iV3102) False) % 51.99/52.18 (Or (Eq (cC64 iV3102) False) % 51.99/52.18 (Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))))))) % 51.99/52.18 Clause #2150 (by forward demodulation #[2149, 367]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq True False) % 51.99/52.18 (Or (Eq (cC64 iV3102) False) % 51.99/52.18 (Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))))))) % 51.99/52.18 Clause #2151 (by clausification #[2150]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq (cC64 iV3102) False) % 51.99/52.18 (Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))))) % 51.99/52.18 Clause #2152 (by forward demodulation #[2151, 395]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq True False) % 51.99/52.18 (Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))))) % 51.99/52.18 Clause #2153 (by clausification #[2152]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq (cC28 iV3102) False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))))) % 51.99/52.18 Clause #2154 (by forward demodulation #[2153, 365]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq True False) % 51.99/52.18 (Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))))) % 51.99/52.18 Clause #2155 (by clausification #[2154]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq (cC44 iV3102) False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.18 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.18 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))) % 51.99/52.18 Clause #2156 (by forward demodulation #[2155, 323]): ∀ (a a_1 : Iota), % 51.99/52.18 Or (Eq True False) % 51.99/52.18 (Or (Eq (cC30 iV3102) False) % 51.99/52.18 (Or (Eq (cC46 iV3102) False) % 51.99/52.18 (Or (Eq (cC216 iV3102) False) % 51.99/52.18 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))))) % 51.99/52.21 Clause #2157 (by clausification #[2156]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (cC30 iV3102) False) % 51.99/52.21 (Or (Eq (cC46 iV3102) False) % 51.99/52.21 (Or (Eq (cC216 iV3102) False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))) % 51.99/52.21 Clause #2158 (by forward demodulation #[2157, 331]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq True False) % 51.99/52.21 (Or (Eq (cC46 iV3102) False) % 51.99/52.21 (Or (Eq (cC216 iV3102) False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))))) % 51.99/52.21 Clause #2159 (by clausification #[2158]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (cC46 iV3102) False) % 51.99/52.21 (Or (Eq (cC216 iV3102) False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))) % 51.99/52.21 Clause #2160 (by forward demodulation #[2159, 183]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq True False) % 51.99/52.21 (Or (Eq (cC216 iV3102) False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))))) % 51.99/52.21 Clause #2161 (by clausification #[2160]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (cC216 iV3102) False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))) % 51.99/52.21 Clause #2162 (by forward demodulation #[2161, 191]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq True False) % 51.99/52.21 (Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False)))) % 51.99/52.21 Clause #2163 (by clausification #[2162]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (cowlThing (skS.0 49 a)) False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a_1)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) False))) % 51.99/52.21 Clause #2164 (by forward demodulation #[2163, 130]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq True False) % 51.99/52.21 (Or (Eq (xsd_string (skS.0 50 a)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Eq (xsd_integer (skS.0 50 a)) False))) % 51.99/52.21 Clause #2165 (by clausification #[2164]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (xsd_string (skS.0 50 a)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Eq (xsd_integer (skS.0 50 a)) False)) % 51.99/52.21 Clause #2166 (by superposition #[2165, 139]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (xsd_string (skS.0 50 a)) True) % 51.99/52.21 (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Or (Eq (xsd_string (skS.0 50 a)) True) (Eq False True))) % 51.99/52.21 Clause #6196 (by clausification #[2166]): ∀ (a a_1 : Iota), % 51.99/52.21 Or (Eq (xsd_string (skS.0 50 a)) True) (Or (Eq (cowlNothing (skS.0 49 a_1)) True) (Eq (xsd_string (skS.0 50 a)) True)) % 51.99/52.21 Clause #6197 (by eliminate duplicate literals #[6196]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 50 a)) True) (Eq (cowlNothing (skS.0 49 a_1)) True) % 51.99/52.21 Clause #6200 (by superposition #[6197, 131]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 50 a)) True) (Eq True False) % 51.99/52.21 Clause #6201 (by clausification #[6200]): ∀ (a : Iota), Eq (xsd_string (skS.0 50 a)) True % 51.99/52.21 Clause #6202 (by backward demodulation #[6201, 1182]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True)) % 51.99/52.21 Clause #6203 (by superposition #[6201, 163]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 50 a)) False) % 51.99/52.21 Clause #6204 (by clausification #[6203]): ∀ (a : Iota), Eq (xsd_integer (skS.0 50 a)) False % 51.99/52.21 Clause #6206 (by clausification #[6202]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq (xsd_integer (skS.0 50 a_1)) True) % 51.99/52.21 Clause #6208 (by superposition #[6206, 6204]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 49 a)) True) (Eq True False) % 52.03/52.23 Clause #6209 (by clausification #[6208]): ∀ (a : Iota), Eq (cowlNothing (skS.0 49 a)) True % 52.03/52.23 Clause #6210 (by superposition #[6209, 131]): Eq True False % 52.03/52.23 Clause #6215 (by clausification #[6210]): False % 52.03/52.23 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------