%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS157+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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 54.62s 54.79s % Output : Proof 54.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : KRS157+1 : TPTP v9.2.0. Released v3.1.0. % 0.10/0.13 % Command : duper %s % 0.14/0.34 % Computer : n020.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 10:16:38 EDT 2025 % 0.14/0.34 % CPUTime : % 54.62/54.79 SZS status Theorem for theBenchmark.p % 54.62/54.79 SZS output start Proof for theBenchmark.p % 54.62/54.79 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 54.62/54.79 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 54.62/54.79 Clause #44 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC14 X) (And (cC2xcomp X) (cC12xcomp X))) True % 54.62/54.79 Clause #121 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC216 X) (And (cC64 X) (cC214xcomp X))) True % 54.62/54.79 Clause #132 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC30 X) (And (cC28 X) (cC14 X))) True % 54.62/54.79 Clause #147 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC44 X) (And (cC42xcomp X) (cC32xcomp X))) True % 54.62/54.79 Clause #148 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC46 X) (And (cC30 X) (cC44 X))) True % 54.62/54.79 Clause #201 (by assumption #[]): Eq (∀ (X : Iota), Iff (cTEST X) (And (cC216 X) (cC46 X))) True % 54.62/54.79 Clause #202 (by assumption #[]): Eq (cTEST iV3102) True % 54.62/54.79 Clause #203 (by assumption #[]): Eq (cC2xcomp iV3102) True % 54.62/54.79 Clause #207 (by assumption #[]): Eq (cC32xcomp iV3102) True % 54.62/54.79 Clause #211 (by assumption #[]): Eq (cC42xcomp iV3102) True % 54.62/54.79 Clause #215 (by assumption #[]): Eq (cC12xcomp iV3102) True % 54.62/54.79 Clause #219 (by assumption #[]): Eq % 54.62/54.79 (Not % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And % 54.62/54.79 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.62/54.79 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.62/54.79 (cC14 iV3102)) % 54.62/54.79 (cC44 iV3102)) % 54.62/54.79 (cC216 iV3102)) % 54.62/54.79 (cC64 iV3102)) % 54.62/54.79 (cC46 iV3102)) % 54.62/54.79 (cC28 iV3102)) % 54.62/54.79 (cowlThing iV3102)) % 54.62/54.79 (cC30 iV3102))) % 54.62/54.79 True % 54.62/54.79 Clause #220 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 54.62/54.79 Clause #221 (by clausification #[220]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 54.62/54.79 Clause #222 (by clausification #[220]): ∀ (a : Iota), Eq (cowlThing a) True % 54.62/54.79 Clause #223 (by clausification #[221]): ∀ (a : Iota), Eq (cowlNothing a) False % 54.62/54.79 Clause #224 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 54.62/54.79 Clause #225 (by clausification #[224]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 54.62/54.79 Clause #226 (by clausification #[224]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 54.62/54.79 Clause #227 (by clausification #[225]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 54.62/54.79 Clause #243 (by clausification #[226]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 54.62/54.79 Clause #253 (by clausification #[201]): ∀ (a : Iota), Eq (Iff (cTEST a) (And (cC216 a) (cC46 a))) True % 54.62/54.79 Clause #255 (by clausification #[253]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (And (cC216 a) (cC46 a)) True) % 54.62/54.79 Clause #257 (by clausification #[255]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC46 a) True) % 54.62/54.79 Clause #258 (by clausification #[255]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC216 a) True) % 54.62/54.79 Clause #259 (by superposition #[257, 202]): Or (Eq (cC46 iV3102) True) (Eq False True) % 54.62/54.79 Clause #267 (by clausification #[259]): Eq (cC46 iV3102) True % 54.62/54.79 Clause #268 (by superposition #[258, 202]): Or (Eq (cC216 iV3102) True) (Eq False True) % 54.62/54.79 Clause #269 (by clausification #[268]): Eq (cC216 iV3102) True % 54.62/54.79 Clause #326 (by clausification #[44]): ∀ (a : Iota), Eq (Iff (cC14 a) (And (cC2xcomp a) (cC12xcomp a))) True % 54.62/54.79 Clause #327 (by clausification #[326]): ∀ (a : Iota), Or (Eq (cC14 a) True) (Eq (And (cC2xcomp a) (cC12xcomp a)) False) % 54.62/54.79 Clause #329 (by clausification #[327]): ∀ (a : Iota), Or (Eq (cC14 a) True) (Or (Eq (cC2xcomp a) False) (Eq (cC12xcomp a) False)) % 54.62/54.79 Clause #330 (by superposition #[329, 203]): Or (Eq (cC14 iV3102) True) (Or (Eq (cC12xcomp iV3102) False) (Eq False True)) % 54.62/54.79 Clause #331 (by clausification #[330]): Or (Eq (cC14 iV3102) True) (Eq (cC12xcomp iV3102) False) % 54.62/54.79 Clause #332 (by superposition #[331, 215]): Or (Eq (cC14 iV3102) True) (Eq False True) % 54.62/54.79 Clause #333 (by clausification #[332]): Eq (cC14 iV3102) True % 54.66/54.81 Clause #499 (by clausification #[121]): ∀ (a : Iota), Eq (Iff (cC216 a) (And (cC64 a) (cC214xcomp a))) True % 54.66/54.81 Clause #501 (by clausification #[499]): ∀ (a : Iota), Or (Eq (cC216 a) False) (Eq (And (cC64 a) (cC214xcomp a)) True) % 54.66/54.81 Clause #504 (by clausification #[501]): ∀ (a : Iota), Or (Eq (cC216 a) False) (Eq (cC64 a) True) % 54.66/54.81 Clause #512 (by superposition #[504, 269]): Or (Eq (cC64 iV3102) True) (Eq False True) % 54.66/54.81 Clause #513 (by clausification #[512]): Eq (cC64 iV3102) True % 54.66/54.81 Clause #950 (by clausification #[132]): ∀ (a : Iota), Eq (Iff (cC30 a) (And (cC28 a) (cC14 a))) True % 54.66/54.81 Clause #952 (by clausification #[950]): ∀ (a : Iota), Or (Eq (cC30 a) False) (Eq (And (cC28 a) (cC14 a)) True) % 54.66/54.81 Clause #980 (by clausification #[952]): ∀ (a : Iota), Or (Eq (cC30 a) False) (Eq (cC28 a) True) % 54.66/54.81 Clause #1000 (by clausification #[147]): ∀ (a : Iota), Eq (Iff (cC44 a) (And (cC42xcomp a) (cC32xcomp a))) True % 54.66/54.81 Clause #1001 (by clausification #[1000]): ∀ (a : Iota), Or (Eq (cC44 a) True) (Eq (And (cC42xcomp a) (cC32xcomp a)) False) % 54.66/54.81 Clause #1003 (by clausification #[1001]): ∀ (a : Iota), Or (Eq (cC44 a) True) (Or (Eq (cC42xcomp a) False) (Eq (cC32xcomp a) False)) % 54.66/54.81 Clause #1004 (by superposition #[1003, 211]): Or (Eq (cC44 iV3102) True) (Or (Eq (cC32xcomp iV3102) False) (Eq False True)) % 54.66/54.81 Clause #1005 (by clausification #[1004]): Or (Eq (cC44 iV3102) True) (Eq (cC32xcomp iV3102) False) % 54.66/54.81 Clause #1006 (by forward demodulation #[1005, 207]): Or (Eq (cC44 iV3102) True) (Eq True False) % 54.66/54.81 Clause #1007 (by clausification #[1006]): Eq (cC44 iV3102) True % 54.66/54.81 Clause #1021 (by clausification #[148]): ∀ (a : Iota), Eq (Iff (cC46 a) (And (cC30 a) (cC44 a))) True % 54.66/54.81 Clause #1023 (by clausification #[1021]): ∀ (a : Iota), Or (Eq (cC46 a) False) (Eq (And (cC30 a) (cC44 a)) True) % 54.66/54.81 Clause #1031 (by clausification #[1023]): ∀ (a : Iota), Or (Eq (cC46 a) False) (Eq (cC30 a) True) % 54.66/54.81 Clause #1033 (by superposition #[1031, 267]): Or (Eq (cC30 iV3102) True) (Eq False True) % 54.66/54.81 Clause #1034 (by clausification #[1033]): Eq (cC30 iV3102) True % 54.66/54.81 Clause #1036 (by superposition #[1034, 980]): Or (Eq True False) (Eq (cC28 iV3102) True) % 54.66/54.81 Clause #1038 (by clausification #[1036]): Eq (cC28 iV3102) True % 54.66/54.81 Clause #2095 (by clausification #[219]): Eq % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.66/54.81 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.66/54.81 (cC14 iV3102)) % 54.66/54.81 (cC44 iV3102)) % 54.66/54.81 (cC216 iV3102)) % 54.66/54.81 (cC64 iV3102)) % 54.66/54.81 (cC46 iV3102)) % 54.66/54.81 (cC28 iV3102)) % 54.66/54.81 (cowlThing iV3102)) % 54.66/54.81 (cC30 iV3102)) % 54.66/54.81 False % 54.66/54.81 Clause #2096 (by clausification #[2095]): Or % 54.66/54.81 (Eq % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.66/54.81 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.66/54.81 (cC14 iV3102)) % 54.66/54.81 (cC44 iV3102)) % 54.66/54.81 (cC216 iV3102)) % 54.66/54.81 (cC64 iV3102)) % 54.66/54.81 (cC46 iV3102)) % 54.66/54.81 (cC28 iV3102)) % 54.66/54.81 (cowlThing iV3102)) % 54.66/54.81 False) % 54.66/54.81 (Eq (cC30 iV3102) False) % 54.66/54.81 Clause #2097 (by clausification #[2096]): Or (Eq (cC30 iV3102) False) % 54.66/54.81 (Or % 54.66/54.81 (Eq % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.66/54.81 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.66/54.81 (cC14 iV3102)) % 54.66/54.81 (cC44 iV3102)) % 54.66/54.81 (cC216 iV3102)) % 54.66/54.81 (cC64 iV3102)) % 54.66/54.81 (cC46 iV3102)) % 54.66/54.81 (cC28 iV3102)) % 54.66/54.81 False) % 54.66/54.81 (Eq (cowlThing iV3102) False)) % 54.66/54.81 Clause #2098 (by clausification #[2097]): Or (Eq (cC30 iV3102) False) % 54.66/54.81 (Or (Eq (cowlThing iV3102) False) % 54.66/54.81 (Or % 54.66/54.81 (Eq % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And % 54.66/54.81 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 (cC14 iV3102)) % 54.68/54.84 (cC44 iV3102)) % 54.68/54.84 (cC216 iV3102)) % 54.68/54.84 (cC64 iV3102)) % 54.68/54.84 (cC46 iV3102)) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC28 iV3102) False))) % 54.68/54.84 Clause #2099 (by clausification #[2098]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or % 54.68/54.84 (Eq % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 (cC14 iV3102)) % 54.68/54.84 (cC44 iV3102)) % 54.68/54.84 (cC216 iV3102)) % 54.68/54.84 (cC64 iV3102)) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC46 iV3102) False)))) % 54.68/54.84 Clause #2100 (by clausification #[2099]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or % 54.68/54.84 (Eq % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 (cC14 iV3102)) % 54.68/54.84 (cC44 iV3102)) % 54.68/54.84 (cC216 iV3102)) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC64 iV3102) False))))) % 54.68/54.84 Clause #2101 (by clausification #[2100]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or (Eq (cC64 iV3102) False) % 54.68/54.84 (Or % 54.68/54.84 (Eq % 54.68/54.84 (And % 54.68/54.84 (And % 54.68/54.84 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 (cC14 iV3102)) % 54.68/54.84 (cC44 iV3102)) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC216 iV3102) False)))))) % 54.68/54.84 Clause #2102 (by clausification #[2101]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or (Eq (cC64 iV3102) False) % 54.68/54.84 (Or (Eq (cC216 iV3102) False) % 54.68/54.84 (Or % 54.68/54.84 (Eq % 54.68/54.84 (And % 54.68/54.84 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 (cC14 iV3102)) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC44 iV3102) False))))))) % 54.68/54.84 Clause #2103 (by clausification #[2102]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or (Eq (cC64 iV3102) False) % 54.68/54.84 (Or (Eq (cC216 iV3102) False) % 54.68/54.84 (Or (Eq (cC44 iV3102) False) % 54.68/54.84 (Or % 54.68/54.84 (Eq % 54.68/54.84 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 54.68/54.84 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 54.68/54.84 False) % 54.68/54.84 (Eq (cC14 iV3102) False)))))))) % 54.68/54.84 Clause #2104 (by clausification #[2103]): Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or (Eq (cC64 iV3102) False) % 54.68/54.84 (Or (Eq (cC216 iV3102) False) % 54.68/54.84 (Or (Eq (cC44 iV3102) False) % 54.68/54.84 (Or (Eq (cC14 iV3102) False) % 54.68/54.84 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 54.68/54.84 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False))))))))) % 54.68/54.84 Clause #2105 (by clausification #[2104]): ∀ (a : Iota), % 54.68/54.84 Or (Eq (cC30 iV3102) False) % 54.68/54.84 (Or (Eq (cowlThing iV3102) False) % 54.68/54.84 (Or (Eq (cC28 iV3102) False) % 54.68/54.84 (Or (Eq (cC46 iV3102) False) % 54.68/54.84 (Or (Eq (cC64 iV3102) False) % 54.68/54.84 (Or (Eq (cC216 iV3102) False) % 54.68/54.84 (Or (Eq (cC44 iV3102) False) % 54.68/54.84 (Or (Eq (cC14 iV3102) False) % 54.68/54.84 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 54.68/54.86 (Eq (Not (And (cowlThing (skS.0 142 a)) (Not (cowlNothing (skS.0 142 a))))) True))))))))) % 54.68/54.86 Clause #2106 (by clausification #[2105]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (Not (And (cowlThing (skS.0 142 a)) (Not (cowlNothing (skS.0 142 a))))) True) % 54.68/54.86 (Eq (Not (Iff (xsd_string (skS.0 143 a_1)) (Not (xsd_integer (skS.0 143 a_1))))) True))))))))) % 54.68/54.86 Clause #2107 (by clausification #[2106]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (Not (Iff (xsd_string (skS.0 143 a)) (Not (xsd_integer (skS.0 143 a))))) True) % 54.68/54.86 (Eq (And (cowlThing (skS.0 142 a_1)) (Not (cowlNothing (skS.0 142 a_1)))) False))))))))) % 54.68/54.86 Clause #2108 (by clausification #[2107]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (And (cowlThing (skS.0 142 a)) (Not (cowlNothing (skS.0 142 a)))) False) % 54.68/54.86 (Eq (Iff (xsd_string (skS.0 143 a_1)) (Not (xsd_integer (skS.0 143 a_1)))) False))))))))) % 54.68/54.86 Clause #2109 (by clausification #[2108]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (Iff (xsd_string (skS.0 143 a)) (Not (xsd_integer (skS.0 143 a)))) False) % 54.68/54.86 (Or (Eq (cowlThing (skS.0 142 a_1)) False) (Eq (Not (cowlNothing (skS.0 142 a_1))) False)))))))))) % 54.68/54.86 Clause #2110 (by clausification #[2109]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.86 (Or (Eq (Not (cowlNothing (skS.0 142 a))) False) % 54.68/54.86 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.86 (Eq (Not (xsd_integer (skS.0 143 a_1))) False))))))))))) % 54.68/54.86 Clause #2111 (by clausification #[2109]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.86 (Or (Eq (Not (cowlNothing (skS.0 142 a))) False) % 54.68/54.86 (Or (Eq (xsd_string (skS.0 143 a_1)) True) (Eq (Not (xsd_integer (skS.0 143 a_1))) True))))))))))) % 54.68/54.86 Clause #2112 (by clausification #[2110]): ∀ (a a_1 : Iota), % 54.68/54.86 Or (Eq (cC30 iV3102) False) % 54.68/54.86 (Or (Eq (cowlThing iV3102) False) % 54.68/54.86 (Or (Eq (cC28 iV3102) False) % 54.68/54.86 (Or (Eq (cC46 iV3102) False) % 54.68/54.86 (Or (Eq (cC64 iV3102) False) % 54.68/54.86 (Or (Eq (cC216 iV3102) False) % 54.68/54.86 (Or (Eq (cC44 iV3102) False) % 54.68/54.86 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (Not (xsd_integer (skS.0 143 a_1))) False) (Eq (cowlNothing (skS.0 142 a)) True))))))))))) % 54.68/54.89 Clause #2113 (by clausification #[2112]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq (cC30 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing iV3102) False) % 54.68/54.89 (Or (Eq (cC28 iV3102) False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))))))) % 54.68/54.89 Clause #2114 (by forward demodulation #[2113, 1034]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq True False) % 54.68/54.89 (Or (Eq (cowlThing iV3102) False) % 54.68/54.89 (Or (Eq (cC28 iV3102) False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))))))) % 54.68/54.89 Clause #2115 (by clausification #[2114]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq (cowlThing iV3102) False) % 54.68/54.89 (Or (Eq (cC28 iV3102) False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))))))) % 54.68/54.89 Clause #2116 (by forward demodulation #[2115, 222]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq True False) % 54.68/54.89 (Or (Eq (cC28 iV3102) False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))))))) % 54.68/54.89 Clause #2117 (by clausification #[2116]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq (cC28 iV3102) False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))))) % 54.68/54.89 Clause #2118 (by forward demodulation #[2117, 1038]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq True False) % 54.68/54.89 (Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))))) % 54.68/54.89 Clause #2119 (by clausification #[2118]): ∀ (a a_1 : Iota), % 54.68/54.89 Or (Eq (cC46 iV3102) False) % 54.68/54.89 (Or (Eq (cC64 iV3102) False) % 54.68/54.89 (Or (Eq (cC216 iV3102) False) % 54.68/54.89 (Or (Eq (cC44 iV3102) False) % 54.68/54.89 (Or (Eq (cC14 iV3102) False) % 54.68/54.89 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.68/54.89 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.68/54.89 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))))) % 54.68/54.89 Clause #2120 (by forward demodulation #[2119, 267]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (cC64 iV3102) False) % 54.76/54.92 (Or (Eq (cC216 iV3102) False) % 54.76/54.92 (Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))))) % 54.76/54.92 Clause #2121 (by clausification #[2120]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cC64 iV3102) False) % 54.76/54.92 (Or (Eq (cC216 iV3102) False) % 54.76/54.92 (Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))) % 54.76/54.92 Clause #2122 (by forward demodulation #[2121, 513]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (cC216 iV3102) False) % 54.76/54.92 (Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))))) % 54.76/54.92 Clause #2123 (by clausification #[2122]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cC216 iV3102) False) % 54.76/54.92 (Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))) % 54.76/54.92 Clause #2124 (by forward demodulation #[2123, 269]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))))) % 54.76/54.92 Clause #2125 (by clausification #[2124]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cC44 iV3102) False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))) % 54.76/54.92 Clause #2126 (by forward demodulation #[2125, 1007]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))))) % 54.76/54.92 Clause #2127 (by clausification #[2126]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cC14 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))) % 54.76/54.92 Clause #2128 (by forward demodulation #[2127, 333]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)))) % 54.76/54.92 Clause #2129 (by clausification #[2128]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a_1)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True))) % 54.76/54.92 Clause #2130 (by forward demodulation #[2129, 222]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq True False) % 54.76/54.92 (Or (Eq (xsd_string (skS.0 143 a)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Eq (xsd_integer (skS.0 143 a)) True))) % 54.76/54.92 Clause #2131 (by clausification #[2130]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (xsd_string (skS.0 143 a)) False) % 54.76/54.92 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Eq (xsd_integer (skS.0 143 a)) True)) % 54.76/54.92 Clause #2800 (by clausification #[2111]): ∀ (a a_1 : Iota), % 54.76/54.92 Or (Eq (cC30 iV3102) False) % 54.76/54.92 (Or (Eq (cowlThing iV3102) False) % 54.76/54.92 (Or (Eq (cC28 iV3102) False) % 54.76/54.92 (Or (Eq (cC46 iV3102) False) % 54.76/54.92 (Or (Eq (cC64 iV3102) False) % 54.76/54.92 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (Not (xsd_integer (skS.0 143 a_1))) True) (Eq (cowlNothing (skS.0 142 a)) True))))))))))) % 54.76/54.95 Clause #2801 (by clausification #[2800]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq (cC30 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing iV3102) False) % 54.76/54.95 (Or (Eq (cC28 iV3102) False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))))))) % 54.76/54.95 Clause #2802 (by forward demodulation #[2801, 1034]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq True False) % 54.76/54.95 (Or (Eq (cowlThing iV3102) False) % 54.76/54.95 (Or (Eq (cC28 iV3102) False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))))))) % 54.76/54.95 Clause #2803 (by clausification #[2802]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq (cowlThing iV3102) False) % 54.76/54.95 (Or (Eq (cC28 iV3102) False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))))))) % 54.76/54.95 Clause #2804 (by forward demodulation #[2803, 222]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq True False) % 54.76/54.95 (Or (Eq (cC28 iV3102) False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))))))) % 54.76/54.95 Clause #2805 (by clausification #[2804]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq (cC28 iV3102) False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))))) % 54.76/54.95 Clause #2806 (by forward demodulation #[2805, 1038]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq True False) % 54.76/54.95 (Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))))) % 54.76/54.95 Clause #2807 (by clausification #[2806]): ∀ (a a_1 : Iota), % 54.76/54.95 Or (Eq (cC46 iV3102) False) % 54.76/54.95 (Or (Eq (cC64 iV3102) False) % 54.76/54.95 (Or (Eq (cC216 iV3102) False) % 54.76/54.95 (Or (Eq (cC44 iV3102) False) % 54.76/54.95 (Or (Eq (cC14 iV3102) False) % 54.76/54.95 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.95 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.95 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))))) % 54.76/54.98 Clause #2808 (by forward demodulation #[2807, 267]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (cC64 iV3102) False) % 54.76/54.98 (Or (Eq (cC216 iV3102) False) % 54.76/54.98 (Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))))) % 54.76/54.98 Clause #2809 (by clausification #[2808]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (cC64 iV3102) False) % 54.76/54.98 (Or (Eq (cC216 iV3102) False) % 54.76/54.98 (Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))) % 54.76/54.98 Clause #2810 (by forward demodulation #[2809, 513]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (cC216 iV3102) False) % 54.76/54.98 (Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))))) % 54.76/54.98 Clause #2811 (by clausification #[2810]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (cC216 iV3102) False) % 54.76/54.98 (Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))) % 54.76/54.98 Clause #2812 (by forward demodulation #[2811, 269]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))))) % 54.76/54.98 Clause #2813 (by clausification #[2812]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (cC44 iV3102) False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))) % 54.76/54.98 Clause #2814 (by forward demodulation #[2813, 1007]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))))) % 54.76/54.98 Clause #2815 (by clausification #[2814]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (cC14 iV3102) False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))) % 54.76/54.98 Clause #2816 (by forward demodulation #[2815, 333]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False)))) % 54.76/54.98 Clause #2817 (by clausification #[2816]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (cowlThing (skS.0 142 a)) False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a_1)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) False))) % 54.76/54.98 Clause #2818 (by forward demodulation #[2817, 222]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq True False) % 54.76/54.98 (Or (Eq (xsd_string (skS.0 143 a)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Eq (xsd_integer (skS.0 143 a)) False))) % 54.76/54.98 Clause #2819 (by clausification #[2818]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (xsd_string (skS.0 143 a)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Eq (xsd_integer (skS.0 143 a)) False)) % 54.76/54.98 Clause #2820 (by superposition #[2819, 227]): ∀ (a a_1 : Iota), % 54.76/54.98 Or (Eq (xsd_string (skS.0 143 a)) True) % 54.76/54.98 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Or (Eq (xsd_string (skS.0 143 a)) True) (Eq False True))) % 54.83/55.03 Clause #10746 (by clausification #[2820]): ∀ (a a_1 : Iota), % 54.83/55.03 Or (Eq (xsd_string (skS.0 143 a)) True) % 54.83/55.03 (Or (Eq (cowlNothing (skS.0 142 a_1)) True) (Eq (xsd_string (skS.0 143 a)) True)) % 54.83/55.03 Clause #10747 (by eliminate duplicate literals #[10746]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 143 a)) True) (Eq (cowlNothing (skS.0 142 a_1)) True) % 54.83/55.03 Clause #10750 (by superposition #[10747, 223]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 143 a)) True) (Eq True False) % 54.83/55.03 Clause #10751 (by clausification #[10750]): ∀ (a : Iota), Eq (xsd_string (skS.0 143 a)) True % 54.83/55.03 Clause #10752 (by backward demodulation #[10751, 2131]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True)) % 54.83/55.03 Clause #10753 (by superposition #[10751, 243]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 143 a)) False) % 54.83/55.03 Clause #10754 (by clausification #[10753]): ∀ (a : Iota), Eq (xsd_integer (skS.0 143 a)) False % 54.83/55.03 Clause #10765 (by clausification #[10752]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq (xsd_integer (skS.0 143 a_1)) True) % 54.83/55.03 Clause #10767 (by superposition #[10765, 10754]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 142 a)) True) (Eq True False) % 54.83/55.03 Clause #10768 (by clausification #[10767]): ∀ (a : Iota), Eq (cowlNothing (skS.0 142 a)) True % 54.83/55.03 Clause #10769 (by superposition #[10768, 223]): Eq True False % 54.83/55.03 Clause #10770 (by clausification #[10769]): False % 54.83/55.03 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------