%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS150+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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 4.33s 4.53s % Output : Proof 4.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : KRS150+1 : TPTP v9.2.0. Released v3.1.0. % 0.03/0.13 % Command : duper %s % 0.13/0.33 % Computer : n028.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Thu Oct 2 10:09:53 EDT 2025 % 0.13/0.34 % CPUTime : % 4.33/4.53 SZS status Theorem for theBenchmark.p % 4.33/4.53 SZS output start Proof for theBenchmark.p % 4.33/4.53 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 4.33/4.53 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 4.33/4.53 Clause #3 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC12 X) (And (Not (cC2 X)) (Not (cC10 X)))) True % 4.33/4.53 Clause #5 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC16 X) (And (cC14 X) (cC8 X))) True % 4.33/4.53 Clause #6 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC18 X) (And (cTOP X) (cC16 X))) True % 4.33/4.53 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), Iff (cC6 X) (And (Not (cC2 X)) (Not (cC4 X)))) True % 4.33/4.53 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (cTEST X) (And (cC18 X) (cTOP X))) True % 4.33/4.53 Clause #12 (by assumption #[]): Eq (cTEST iV16560) True % 4.33/4.53 Clause #16 (by assumption #[]): Eq (Not (cC4 iV16561)) True % 4.33/4.53 Clause #19 (by assumption #[]): Eq (Not (cC2 iV16561)) True % 4.33/4.53 Clause #20 (by assumption #[]): Eq (Not (cC10 iV16562)) True % 4.33/4.53 Clause #21 (by assumption #[]): Eq (Not (cC2 iV16562)) True % 4.33/4.53 Clause #24 (by assumption #[]): Eq % 4.33/4.53 (Not % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And % 4.33/4.53 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.33/4.53 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.33/4.53 (cC18 iV16560)) % 4.33/4.53 (cC16 iV16560)) % 4.33/4.53 (cowlThing iV16560)) % 4.33/4.53 (cC14 iV16560)) % 4.33/4.53 (cC8 iV16560)) % 4.33/4.53 (cowlThing iV16561)) % 4.33/4.53 (cC6 iV16561)) % 4.33/4.53 (cowlThing iV16562)) % 4.33/4.53 (cC12 iV16562))) % 4.33/4.53 True % 4.33/4.53 Clause #25 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 4.33/4.53 Clause #26 (by clausification #[25]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 4.33/4.53 Clause #27 (by clausification #[25]): ∀ (a : Iota), Eq (cowlThing a) True % 4.33/4.53 Clause #28 (by clausification #[26]): ∀ (a : Iota), Eq (cowlNothing a) False % 4.33/4.53 Clause #29 (by clausification #[16]): Eq (cC4 iV16561) False % 4.33/4.53 Clause #30 (by clausification #[21]): Eq (cC2 iV16562) False % 4.33/4.53 Clause #31 (by clausification #[20]): Eq (cC10 iV16562) False % 4.33/4.53 Clause #32 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 4.33/4.53 Clause #33 (by clausification #[32]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 4.33/4.53 Clause #34 (by clausification #[32]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 4.33/4.53 Clause #35 (by clausification #[33]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 4.33/4.53 Clause #36 (by clausification #[19]): Eq (cC2 iV16561) False % 4.33/4.53 Clause #41 (by clausification #[34]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 4.33/4.53 Clause #54 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (cTEST a) (And (cC18 a) (cTOP a))) True % 4.33/4.53 Clause #56 (by clausification #[54]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (And (cC18 a) (cTOP a)) True) % 4.33/4.53 Clause #59 (by clausification #[56]): ∀ (a : Iota), Or (Eq (cTEST a) False) (Eq (cC18 a) True) % 4.33/4.53 Clause #61 (by clausification #[3]): ∀ (a : Iota), Eq (Iff (cC12 a) (And (Not (cC2 a)) (Not (cC10 a)))) True % 4.33/4.53 Clause #62 (by clausification #[61]): ∀ (a : Iota), Or (Eq (cC12 a) True) (Eq (And (Not (cC2 a)) (Not (cC10 a))) False) % 4.33/4.53 Clause #64 (by clausification #[62]): ∀ (a : Iota), Or (Eq (cC12 a) True) (Or (Eq (Not (cC2 a)) False) (Eq (Not (cC10 a)) False)) % 4.33/4.53 Clause #65 (by clausification #[64]): ∀ (a : Iota), Or (Eq (cC12 a) True) (Or (Eq (Not (cC10 a)) False) (Eq (cC2 a) True)) % 4.33/4.53 Clause #66 (by clausification #[65]): ∀ (a : Iota), Or (Eq (cC12 a) True) (Or (Eq (cC2 a) True) (Eq (cC10 a) True)) % 4.33/4.53 Clause #67 (by superposition #[59, 12]): Or (Eq (cC18 iV16560) True) (Eq False True) % 4.33/4.53 Clause #68 (by clausification #[67]): Eq (cC18 iV16560) True % 4.33/4.53 Clause #72 (by clausification #[6]): ∀ (a : Iota), Eq (Iff (cC18 a) (And (cTOP a) (cC16 a))) True % 4.33/4.53 Clause #74 (by clausification #[72]): ∀ (a : Iota), Or (Eq (cC18 a) False) (Eq (And (cTOP a) (cC16 a)) True) % 4.40/4.55 Clause #89 (by clausification #[74]): ∀ (a : Iota), Or (Eq (cC18 a) False) (Eq (cC16 a) True) % 4.40/4.55 Clause #91 (by superposition #[89, 68]): Or (Eq (cC16 iV16560) True) (Eq False True) % 4.40/4.55 Clause #92 (by clausification #[91]): Eq (cC16 iV16560) True % 4.40/4.55 Clause #93 (by clausification #[5]): ∀ (a : Iota), Eq (Iff (cC16 a) (And (cC14 a) (cC8 a))) True % 4.40/4.55 Clause #95 (by clausification #[93]): ∀ (a : Iota), Or (Eq (cC16 a) False) (Eq (And (cC14 a) (cC8 a)) True) % 4.40/4.55 Clause #97 (by clausification #[95]): ∀ (a : Iota), Or (Eq (cC16 a) False) (Eq (cC8 a) True) % 4.40/4.55 Clause #98 (by clausification #[95]): ∀ (a : Iota), Or (Eq (cC16 a) False) (Eq (cC14 a) True) % 4.40/4.55 Clause #99 (by superposition #[97, 92]): Or (Eq (cC8 iV16560) True) (Eq False True) % 4.40/4.55 Clause #100 (by clausification #[99]): Eq (cC8 iV16560) True % 4.40/4.55 Clause #101 (by superposition #[98, 92]): Or (Eq (cC14 iV16560) True) (Eq False True) % 4.40/4.55 Clause #102 (by clausification #[101]): Eq (cC14 iV16560) True % 4.40/4.55 Clause #128 (by clausification #[8]): ∀ (a : Iota), Eq (Iff (cC6 a) (And (Not (cC2 a)) (Not (cC4 a)))) True % 4.40/4.55 Clause #129 (by clausification #[128]): ∀ (a : Iota), Or (Eq (cC6 a) True) (Eq (And (Not (cC2 a)) (Not (cC4 a))) False) % 4.40/4.55 Clause #131 (by clausification #[129]): ∀ (a : Iota), Or (Eq (cC6 a) True) (Or (Eq (Not (cC2 a)) False) (Eq (Not (cC4 a)) False)) % 4.40/4.55 Clause #132 (by clausification #[131]): ∀ (a : Iota), Or (Eq (cC6 a) True) (Or (Eq (Not (cC4 a)) False) (Eq (cC2 a) True)) % 4.40/4.55 Clause #133 (by clausification #[132]): ∀ (a : Iota), Or (Eq (cC6 a) True) (Or (Eq (cC2 a) True) (Eq (cC4 a) True)) % 4.40/4.55 Clause #134 (by superposition #[133, 29]): Or (Eq (cC6 iV16561) True) (Or (Eq (cC2 iV16561) True) (Eq True False)) % 4.40/4.55 Clause #137 (by clausification #[134]): Or (Eq (cC6 iV16561) True) (Eq (cC2 iV16561) True) % 4.40/4.55 Clause #138 (by forward demodulation #[137, 36]): Or (Eq (cC6 iV16561) True) (Eq False True) % 4.40/4.55 Clause #139 (by clausification #[138]): Eq (cC6 iV16561) True % 4.40/4.55 Clause #158 (by clausification #[24]): Eq % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.55 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.55 (cC18 iV16560)) % 4.40/4.55 (cC16 iV16560)) % 4.40/4.55 (cowlThing iV16560)) % 4.40/4.55 (cC14 iV16560)) % 4.40/4.55 (cC8 iV16560)) % 4.40/4.55 (cowlThing iV16561)) % 4.40/4.55 (cC6 iV16561)) % 4.40/4.55 (cowlThing iV16562)) % 4.40/4.55 (cC12 iV16562)) % 4.40/4.55 False % 4.40/4.55 Clause #159 (by clausification #[158]): Or % 4.40/4.55 (Eq % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.55 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.55 (cC18 iV16560)) % 4.40/4.55 (cC16 iV16560)) % 4.40/4.55 (cowlThing iV16560)) % 4.40/4.55 (cC14 iV16560)) % 4.40/4.55 (cC8 iV16560)) % 4.40/4.55 (cowlThing iV16561)) % 4.40/4.55 (cC6 iV16561)) % 4.40/4.55 (cowlThing iV16562)) % 4.40/4.55 False) % 4.40/4.55 (Eq (cC12 iV16562) False) % 4.40/4.55 Clause #160 (by clausification #[159]): Or (Eq (cC12 iV16562) False) % 4.40/4.55 (Or % 4.40/4.55 (Eq % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.55 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.55 (cC18 iV16560)) % 4.40/4.55 (cC16 iV16560)) % 4.40/4.55 (cowlThing iV16560)) % 4.40/4.55 (cC14 iV16560)) % 4.40/4.55 (cC8 iV16560)) % 4.40/4.55 (cowlThing iV16561)) % 4.40/4.55 (cC6 iV16561)) % 4.40/4.55 False) % 4.40/4.55 (Eq (cowlThing iV16562) False)) % 4.40/4.55 Clause #161 (by clausification #[160]): Or (Eq (cC12 iV16562) False) % 4.40/4.55 (Or (Eq (cowlThing iV16562) False) % 4.40/4.55 (Or % 4.40/4.55 (Eq % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And % 4.40/4.55 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 (cC16 iV16560)) % 4.40/4.56 (cowlThing iV16560)) % 4.40/4.56 (cC14 iV16560)) % 4.40/4.56 (cC8 iV16560)) % 4.40/4.56 (cowlThing iV16561)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cC6 iV16561) False))) % 4.40/4.56 Clause #162 (by clausification #[161]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 (cC16 iV16560)) % 4.40/4.56 (cowlThing iV16560)) % 4.40/4.56 (cC14 iV16560)) % 4.40/4.56 (cC8 iV16560)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cowlThing iV16561) False)))) % 4.40/4.56 Clause #163 (by clausification #[162]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or (Eq (cowlThing iV16561) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 (cC16 iV16560)) % 4.40/4.56 (cowlThing iV16560)) % 4.40/4.56 (cC14 iV16560)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cC8 iV16560) False))))) % 4.40/4.56 Clause #164 (by clausification #[163]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or (Eq (cowlThing iV16561) False) % 4.40/4.56 (Or (Eq (cC8 iV16560) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 (cC16 iV16560)) % 4.40/4.56 (cowlThing iV16560)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cC14 iV16560) False)))))) % 4.40/4.56 Clause #165 (by clausification #[164]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or (Eq (cowlThing iV16561) False) % 4.40/4.56 (Or (Eq (cC8 iV16560) False) % 4.40/4.56 (Or (Eq (cC14 iV16560) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And % 4.40/4.56 (And % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 (cC16 iV16560)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cowlThing iV16560) False))))))) % 4.40/4.56 Clause #166 (by clausification #[165]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or (Eq (cowlThing iV16561) False) % 4.40/4.56 (Or (Eq (cC8 iV16560) False) % 4.40/4.56 (Or (Eq (cC14 iV16560) False) % 4.40/4.56 (Or (Eq (cowlThing iV16560) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.56 (cC18 iV16560)) % 4.40/4.56 False) % 4.40/4.56 (Eq (cC16 iV16560) False)))))))) % 4.40/4.56 Clause #167 (by clausification #[166]): Or (Eq (cC12 iV16562) False) % 4.40/4.56 (Or (Eq (cowlThing iV16562) False) % 4.40/4.56 (Or (Eq (cC6 iV16561) False) % 4.40/4.56 (Or (Eq (cowlThing iV16561) False) % 4.40/4.56 (Or (Eq (cC8 iV16560) False) % 4.40/4.56 (Or (Eq (cC14 iV16560) False) % 4.40/4.56 (Or (Eq (cowlThing iV16560) False) % 4.40/4.56 (Or (Eq (cC16 iV16560) False) % 4.40/4.56 (Or % 4.40/4.56 (Eq % 4.40/4.56 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 4.40/4.56 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 4.40/4.59 False) % 4.40/4.59 (Eq (cC18 iV16560) False))))))))) % 4.40/4.59 Clause #168 (by clausification #[167]): Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 4.40/4.59 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)))))))))) % 4.40/4.59 Clause #169 (by clausification #[168]): ∀ (a : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 4.40/4.59 (Eq (Not (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a))))) True)))))))))) % 4.40/4.59 Clause #170 (by clausification #[169]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (Not (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a))))) True) % 4.40/4.59 (Eq (Not (Iff (xsd_string (skS.0 1 a_1)) (Not (xsd_integer (skS.0 1 a_1))))) True)))))))))) % 4.40/4.59 Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (Not (Iff (xsd_string (skS.0 1 a)) (Not (xsd_integer (skS.0 1 a))))) True) % 4.40/4.59 (Eq (And (cowlThing (skS.0 0 a_1)) (Not (cowlNothing (skS.0 0 a_1)))) False)))))))))) % 4.40/4.59 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (And (cowlThing (skS.0 0 a)) (Not (cowlNothing (skS.0 0 a)))) False) % 4.40/4.59 (Eq (Iff (xsd_string (skS.0 1 a_1)) (Not (xsd_integer (skS.0 1 a_1)))) False)))))))))) % 4.40/4.59 Clause #173 (by clausification #[172]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.59 (Or (Eq (cC8 iV16560) False) % 4.40/4.59 (Or (Eq (cC14 iV16560) False) % 4.40/4.59 (Or (Eq (cowlThing iV16560) False) % 4.40/4.59 (Or (Eq (cC16 iV16560) False) % 4.40/4.59 (Or (Eq (cC18 iV16560) False) % 4.40/4.59 (Or (Eq (Iff (xsd_string (skS.0 1 a)) (Not (xsd_integer (skS.0 1 a)))) False) % 4.40/4.59 (Or (Eq (cowlThing (skS.0 0 a_1)) False) (Eq (Not (cowlNothing (skS.0 0 a_1))) False))))))))))) % 4.40/4.59 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), % 4.40/4.59 Or (Eq (cC12 iV16562) False) % 4.40/4.59 (Or (Eq (cowlThing iV16562) False) % 4.40/4.59 (Or (Eq (cC6 iV16561) False) % 4.40/4.59 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (Not (cowlNothing (skS.0 0 a))) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.40/4.61 (Eq (Not (xsd_integer (skS.0 1 a_1))) False)))))))))))) % 4.40/4.61 Clause #175 (by clausification #[173]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq (cowlThing iV16562) False) % 4.40/4.61 (Or (Eq (cC6 iV16561) False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (Not (cowlNothing (skS.0 0 a))) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) True) (Eq (Not (xsd_integer (skS.0 1 a_1))) True)))))))))))) % 4.40/4.61 Clause #176 (by clausification #[174]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq (cowlThing iV16562) False) % 4.40/4.61 (Or (Eq (cC6 iV16561) False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.40/4.61 (Or (Eq (Not (xsd_integer (skS.0 1 a_1))) False) (Eq (cowlNothing (skS.0 0 a)) True)))))))))))) % 4.40/4.61 Clause #177 (by clausification #[176]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq (cowlThing iV16562) False) % 4.40/4.61 (Or (Eq (cC6 iV16561) False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.40/4.61 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))))) % 4.40/4.61 Clause #178 (by forward demodulation #[177, 27]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq True False) % 4.40/4.61 (Or (Eq (cC6 iV16561) False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.40/4.61 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))))) % 4.40/4.61 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq (cC6 iV16561) False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.40/4.61 (Or (Eq (cC16 iV16560) False) % 4.40/4.61 (Or (Eq (cC18 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.40/4.61 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.40/4.61 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))))) % 4.40/4.61 Clause #180 (by forward demodulation #[179, 139]): ∀ (a a_1 : Iota), % 4.40/4.61 Or (Eq (cC12 iV16562) False) % 4.40/4.61 (Or (Eq True False) % 4.40/4.61 (Or (Eq (cowlThing iV16561) False) % 4.40/4.61 (Or (Eq (cC8 iV16560) False) % 4.40/4.61 (Or (Eq (cC14 iV16560) False) % 4.40/4.61 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))))) % 4.47/4.63 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq (cowlThing iV16561) False) % 4.47/4.63 (Or (Eq (cC8 iV16560) False) % 4.47/4.63 (Or (Eq (cC14 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))) % 4.47/4.63 Clause #182 (by forward demodulation #[181, 27]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq True False) % 4.47/4.63 (Or (Eq (cC8 iV16560) False) % 4.47/4.63 (Or (Eq (cC14 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))))) % 4.47/4.63 Clause #183 (by clausification #[182]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq (cC8 iV16560) False) % 4.47/4.63 (Or (Eq (cC14 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))) % 4.47/4.63 Clause #184 (by forward demodulation #[183, 100]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq True False) % 4.47/4.63 (Or (Eq (cC14 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))))) % 4.47/4.63 Clause #185 (by clausification #[184]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq (cC14 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))) % 4.47/4.63 Clause #186 (by forward demodulation #[185, 102]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq True False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))))) % 4.47/4.63 Clause #187 (by clausification #[186]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq (cowlThing iV16560) False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))) % 4.47/4.63 Clause #188 (by forward demodulation #[187, 27]): ∀ (a a_1 : Iota), % 4.47/4.63 Or (Eq (cC12 iV16562) False) % 4.47/4.63 (Or (Eq True False) % 4.47/4.63 (Or (Eq (cC16 iV16560) False) % 4.47/4.63 (Or (Eq (cC18 iV16560) False) % 4.47/4.63 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.63 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.63 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))))) % 4.47/4.66 Clause #189 (by clausification #[188]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (cC16 iV16560) False) % 4.47/4.66 (Or (Eq (cC18 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))) % 4.47/4.66 Clause #190 (by forward demodulation #[189, 92]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq True False) % 4.47/4.66 (Or (Eq (cC18 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))))) % 4.47/4.66 Clause #191 (by clausification #[190]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (cC18 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))) % 4.47/4.66 Clause #192 (by forward demodulation #[191, 68]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq True False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True))))) % 4.47/4.66 Clause #193 (by clausification #[192]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)))) % 4.47/4.66 Clause #194 (by forward demodulation #[193, 27]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq True False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) True)))) % 4.47/4.66 Clause #195 (by clausification #[194]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) True))) % 4.47/4.66 Clause #196 (by superposition #[195, 66]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (xsd_string (skS.0 1 a)) False) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.47/4.66 (Or (Eq (xsd_integer (skS.0 1 a)) True) % 4.47/4.66 (Or (Eq False True) (Or (Eq (cC2 iV16562) True) (Eq (cC10 iV16562) True))))) % 4.47/4.66 Clause #243 (by clausification #[175]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (cowlThing iV16562) False) % 4.47/4.66 (Or (Eq (cC6 iV16561) False) % 4.47/4.66 (Or (Eq (cowlThing iV16561) False) % 4.47/4.66 (Or (Eq (cC8 iV16560) False) % 4.47/4.66 (Or (Eq (cC14 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing iV16560) False) % 4.47/4.66 (Or (Eq (cC16 iV16560) False) % 4.47/4.66 (Or (Eq (cC18 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.47/4.66 (Or (Eq (Not (xsd_integer (skS.0 1 a_1))) True) (Eq (cowlNothing (skS.0 0 a)) True)))))))))))) % 4.47/4.66 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq (cowlThing iV16562) False) % 4.47/4.66 (Or (Eq (cC6 iV16561) False) % 4.47/4.66 (Or (Eq (cowlThing iV16561) False) % 4.47/4.66 (Or (Eq (cC8 iV16560) False) % 4.47/4.66 (Or (Eq (cC14 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing iV16560) False) % 4.47/4.66 (Or (Eq (cC16 iV16560) False) % 4.47/4.66 (Or (Eq (cC18 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.47/4.66 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.47/4.66 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))))) % 4.47/4.66 Clause #245 (by forward demodulation #[244, 27]): ∀ (a a_1 : Iota), % 4.47/4.66 Or (Eq (cC12 iV16562) False) % 4.47/4.66 (Or (Eq True False) % 4.47/4.66 (Or (Eq (cC6 iV16561) False) % 4.47/4.66 (Or (Eq (cowlThing iV16561) False) % 4.47/4.66 (Or (Eq (cC8 iV16560) False) % 4.47/4.66 (Or (Eq (cC14 iV16560) False) % 4.47/4.66 (Or (Eq (cowlThing iV16560) False) % 4.47/4.66 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))))) % 4.52/4.68 Clause #246 (by clausification #[245]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq (cC6 iV16561) False) % 4.52/4.68 (Or (Eq (cowlThing iV16561) False) % 4.52/4.68 (Or (Eq (cC8 iV16560) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))))) % 4.52/4.68 Clause #247 (by forward demodulation #[246, 139]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq True False) % 4.52/4.68 (Or (Eq (cowlThing iV16561) False) % 4.52/4.68 (Or (Eq (cC8 iV16560) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))))) % 4.52/4.68 Clause #248 (by clausification #[247]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq (cowlThing iV16561) False) % 4.52/4.68 (Or (Eq (cC8 iV16560) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))) % 4.52/4.68 Clause #249 (by forward demodulation #[248, 27]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq True False) % 4.52/4.68 (Or (Eq (cC8 iV16560) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))))) % 4.52/4.68 Clause #250 (by clausification #[249]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq (cC8 iV16560) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))) % 4.52/4.68 Clause #251 (by forward demodulation #[250, 100]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq True False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))))) % 4.52/4.68 Clause #252 (by clausification #[251]): ∀ (a a_1 : Iota), % 4.52/4.68 Or (Eq (cC12 iV16562) False) % 4.52/4.68 (Or (Eq (cC14 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing iV16560) False) % 4.52/4.68 (Or (Eq (cC16 iV16560) False) % 4.52/4.68 (Or (Eq (cC18 iV16560) False) % 4.52/4.68 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.68 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.68 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))) % 4.52/4.70 Clause #253 (by forward demodulation #[252, 102]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq True False) % 4.52/4.70 (Or (Eq (cowlThing iV16560) False) % 4.52/4.70 (Or (Eq (cC16 iV16560) False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))))) % 4.52/4.70 Clause #254 (by clausification #[253]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq (cowlThing iV16560) False) % 4.52/4.70 (Or (Eq (cC16 iV16560) False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))) % 4.52/4.70 Clause #255 (by forward demodulation #[254, 27]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq True False) % 4.52/4.70 (Or (Eq (cC16 iV16560) False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))))) % 4.52/4.70 Clause #256 (by clausification #[255]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq (cC16 iV16560) False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))) % 4.52/4.70 Clause #257 (by forward demodulation #[256, 92]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq True False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))))) % 4.52/4.70 Clause #258 (by clausification #[257]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq (cC18 iV16560) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))) % 4.52/4.70 Clause #259 (by forward demodulation #[258, 68]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq True False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False))))) % 4.52/4.70 Clause #260 (by clausification #[259]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq (cowlThing (skS.0 0 a)) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a_1)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) False)))) % 4.52/4.70 Clause #261 (by forward demodulation #[260, 27]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq True False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) False)))) % 4.52/4.70 Clause #262 (by clausification #[261]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (cC12 iV16562) False) % 4.52/4.70 (Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) False))) % 4.52/4.70 Clause #263 (by superposition #[262, 66]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.70 (Or (Eq (xsd_integer (skS.0 1 a)) False) % 4.52/4.70 (Or (Eq False True) (Or (Eq (cC2 iV16562) True) (Eq (cC10 iV16562) True))))) % 4.52/4.70 Clause #279 (by clausification #[196]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (xsd_string (skS.0 1 a)) False) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.70 (Or (Eq (xsd_integer (skS.0 1 a)) True) (Or (Eq (cC2 iV16562) True) (Eq (cC10 iV16562) True)))) % 4.52/4.70 Clause #280 (by forward demodulation #[279, 30]): ∀ (a a_1 : Iota), % 4.52/4.70 Or (Eq (xsd_string (skS.0 1 a)) False) % 4.52/4.70 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.70 (Or (Eq (xsd_integer (skS.0 1 a)) True) (Or (Eq False True) (Eq (cC10 iV16562) True)))) % 4.52/4.72 Clause #281 (by clausification #[280]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) False) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_integer (skS.0 1 a)) True) (Eq (cC10 iV16562) True))) % 4.52/4.72 Clause #282 (by forward demodulation #[281, 31]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) False) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_integer (skS.0 1 a)) True) (Eq False True))) % 4.52/4.72 Clause #283 (by clausification #[282]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) False) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) True)) % 4.52/4.72 Clause #317 (by clausification #[263]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.72 (Or (Eq (xsd_integer (skS.0 1 a)) False) (Or (Eq (cC2 iV16562) True) (Eq (cC10 iV16562) True)))) % 4.52/4.72 Clause #318 (by forward demodulation #[317, 30]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.72 (Or (Eq (xsd_integer (skS.0 1 a)) False) (Or (Eq False True) (Eq (cC10 iV16562) True)))) % 4.52/4.72 Clause #319 (by clausification #[318]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_integer (skS.0 1 a)) False) (Eq (cC10 iV16562) True))) % 4.52/4.72 Clause #320 (by forward demodulation #[319, 31]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_integer (skS.0 1 a)) False) (Eq False True))) % 4.52/4.72 Clause #321 (by clausification #[320]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 1 a)) False)) % 4.52/4.72 Clause #322 (by superposition #[321, 35]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) % 4.52/4.72 (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Or (Eq (xsd_string (skS.0 1 a)) True) (Eq False True))) % 4.52/4.72 Clause #345 (by clausification #[322]): ∀ (a a_1 : Iota), % 4.52/4.72 Or (Eq (xsd_string (skS.0 1 a)) True) (Or (Eq (cowlNothing (skS.0 0 a_1)) True) (Eq (xsd_string (skS.0 1 a)) True)) % 4.52/4.72 Clause #346 (by eliminate duplicate literals #[345]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 1 a)) True) (Eq (cowlNothing (skS.0 0 a_1)) True) % 4.52/4.72 Clause #349 (by superposition #[346, 28]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 1 a)) True) (Eq True False) % 4.52/4.72 Clause #350 (by clausification #[349]): ∀ (a : Iota), Eq (xsd_string (skS.0 1 a)) True % 4.52/4.72 Clause #351 (by backward demodulation #[350, 283]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True)) % 4.52/4.72 Clause #352 (by superposition #[350, 41]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 1 a)) False) % 4.52/4.72 Clause #353 (by clausification #[352]): ∀ (a : Iota), Eq (xsd_integer (skS.0 1 a)) False % 4.52/4.72 Clause #372 (by clausification #[351]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 1 a_1)) True) % 4.52/4.72 Clause #374 (by superposition #[372, 353]): ∀ (a : Iota), Or (Eq (cowlNothing (skS.0 0 a)) True) (Eq True False) % 4.52/4.72 Clause #376 (by clausification #[374]): ∀ (a : Iota), Eq (cowlNothing (skS.0 0 a)) True % 4.52/4.72 Clause #377 (by superposition #[376, 28]): Eq True False % 4.52/4.72 Clause #378 (by clausification #[377]): False % 4.52/4.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------