%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS175+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:52:45 PM UTC 2025 % Result : Theorem 8.42s 8.62s % Output : Proof 8.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.13 % Problem : KRS175+1 : TPTP v9.2.0. Released v3.1.0. % 0.09/0.14 % Command : duper %s % 0.11/0.35 % Computer : n021.cluster.edu % 0.11/0.35 % Model : x86_64 x86_64 % 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.35 % Memory : 8042.1875MB % 0.11/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.35 % CPULimit : 300 % 0.11/0.35 % WCLimit : 300 % 0.11/0.35 % DateTime : Thu Oct 2 10:20:08 EDT 2025 % 0.11/0.36 % CPUTime : % 8.42/8.62 SZS status Theorem for theBenchmark.p % 8.42/8.62 SZS output start Proof for theBenchmark.p % 8.42/8.62 Clause #7 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 8.42/8.62 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 8.42/8.62 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), Iff (cA X) (Eq X ia)) True % 8.42/8.62 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (cA X) (cB X))) True % 8.42/8.62 Clause #11 (by assumption #[]): Eq (∀ (X : Iota), Iff (cB X) (Eq X ib)) True % 8.42/8.62 Clause #14 (by assumption #[]): Eq % 8.42/8.62 (Not % 8.42/8.62 (And % 8.42/8.62 (And % 8.42/8.62 (And % 8.42/8.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.42/8.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.42/8.62 (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia)))) % 8.42/8.62 (cowlThing ia)) % 8.42/8.62 (cowlThing ib))) % 8.42/8.62 True % 8.42/8.62 Clause #57 (by clausification #[7]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 8.42/8.62 Clause #58 (by clausification #[57]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 8.42/8.62 Clause #59 (by clausification #[57]): ∀ (a : Iota), Eq (cowlThing a) True % 8.42/8.62 Clause #60 (by clausification #[58]): ∀ (a : Iota), Eq (cowlNothing a) False % 8.42/8.62 Clause #61 (by clausification #[8]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 8.42/8.62 Clause #62 (by clausification #[61]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 8.42/8.62 Clause #63 (by clausification #[61]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 8.42/8.62 Clause #64 (by clausification #[62]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 8.42/8.62 Clause #65 (by clausification #[63]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 8.42/8.62 Clause #68 (by clausification #[11]): ∀ (a : Iota), Eq (Iff (cB a) (Eq a ib)) True % 8.42/8.62 Clause #69 (by clausification #[68]): ∀ (a : Iota), Or (Eq (cB a) True) (Eq (Eq a ib) False) % 8.42/8.62 Clause #70 (by clausification #[68]): ∀ (a : Iota), Or (Eq (cB a) False) (Eq (Eq a ib) True) % 8.42/8.62 Clause #71 (by clausification #[69]): ∀ (a : Iota), Or (Eq (cB a) True) (Ne a ib) % 8.42/8.62 Clause #72 (by destructive equality resolution #[71]): Eq (cB ib) True % 8.42/8.62 Clause #73 (by clausification #[70]): ∀ (a : Iota), Or (Eq (cB a) False) (Eq a ib) % 8.42/8.62 Clause #76 (by clausification #[9]): ∀ (a : Iota), Eq (Iff (cA a) (Eq a ia)) True % 8.42/8.62 Clause #77 (by clausification #[76]): ∀ (a : Iota), Or (Eq (cA a) True) (Eq (Eq a ia) False) % 8.42/8.62 Clause #78 (by clausification #[76]): ∀ (a : Iota), Or (Eq (cA a) False) (Eq (Eq a ia) True) % 8.42/8.62 Clause #79 (by clausification #[77]): ∀ (a : Iota), Or (Eq (cA a) True) (Ne a ia) % 8.42/8.62 Clause #80 (by destructive equality resolution #[79]): Eq (cA ia) True % 8.42/8.62 Clause #81 (by clausification #[78]): ∀ (a : Iota), Or (Eq (cA a) False) (Eq a ia) % 8.42/8.62 Clause #84 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (cA_and_B a) (Or (cA a) (cB a))) True % 8.42/8.62 Clause #85 (by clausification #[84]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (Or (cA a) (cB a)) False) % 8.42/8.62 Clause #86 (by clausification #[84]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Eq (Or (cA a) (cB a)) True) % 8.42/8.62 Clause #87 (by clausification #[85]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (cB a) False) % 8.42/8.62 Clause #88 (by clausification #[85]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (cA a) False) % 8.42/8.62 Clause #89 (by superposition #[87, 72]): Or (Eq (cA_and_B ib) True) (Eq False True) % 8.42/8.62 Clause #90 (by clausification #[89]): Eq (cA_and_B ib) True % 8.42/8.62 Clause #91 (by superposition #[88, 80]): Or (Eq (cA_and_B ia) True) (Eq False True) % 8.42/8.62 Clause #92 (by clausification #[14]): Eq % 8.42/8.62 (And % 8.42/8.62 (And % 8.42/8.62 (And % 8.42/8.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.42/8.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.42/8.62 (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia)))) % 8.42/8.62 (cowlThing ia)) % 8.42/8.62 (cowlThing ib)) % 8.42/8.62 False % 8.42/8.62 Clause #93 (by clausification #[92]): Or % 8.42/8.62 (Eq % 8.42/8.62 (And % 8.42/8.62 (And % 8.42/8.62 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.42/8.62 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.42/8.62 (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia)))) % 8.44/8.65 (cowlThing ia)) % 8.44/8.65 False) % 8.44/8.65 (Eq (cowlThing ib) False) % 8.44/8.65 Clause #94 (by clausification #[93]): Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or % 8.44/8.65 (Eq % 8.44/8.65 (And % 8.44/8.65 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.44/8.65 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.44/8.65 (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia)))) % 8.44/8.65 False) % 8.44/8.65 (Eq (cowlThing ia) False)) % 8.44/8.65 Clause #95 (by clausification #[94]): Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or % 8.44/8.65 (Eq % 8.44/8.65 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.44/8.65 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.44/8.65 False) % 8.44/8.65 (Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia))) False))) % 8.44/8.65 Clause #96 (by clausification #[95]): Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia))) False) % 8.44/8.65 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 8.44/8.65 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)))) % 8.44/8.65 Clause #97 (by clausification #[96]): ∀ (a : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 8.44/8.65 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 8.44/8.65 (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) True)))) % 8.44/8.65 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 8.44/8.65 (Or (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) True) % 8.44/8.65 (Eq (Not (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1))))) True)))) % 8.44/8.65 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) True) % 8.44/8.65 (Or (Eq (Not (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1))))) True) % 8.44/8.65 (Eq (Not (Iff (xsd_string (skS.0 2 a_2)) (Not (xsd_integer (skS.0 2 a_2))))) True)))) % 8.44/8.65 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (Not (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a))))) True) % 8.44/8.65 (Or (Eq (Not (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1))))) True) % 8.44/8.65 (Eq (Iff (cA_and_B (skS.0 0 a_2)) (Or (Eq (skS.0 0 a_2) ib) (Eq (skS.0 0 a_2) ia))) False)))) % 8.44/8.65 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (Not (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a))))) True) % 8.44/8.65 (Or (Eq (Iff (cA_and_B (skS.0 0 a_1)) (Or (Eq (skS.0 0 a_1) ib) (Eq (skS.0 0 a_1) ia))) False) % 8.44/8.65 (Eq (And (cowlThing (skS.0 1 a_2)) (Not (cowlNothing (skS.0 1 a_2)))) False)))) % 8.44/8.65 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (Iff (cA_and_B (skS.0 0 a)) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))) False) % 8.44/8.65 (Or (Eq (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1)))) False) % 8.44/8.65 (Eq (Iff (xsd_string (skS.0 2 a_2)) (Not (xsd_integer (skS.0 2 a_2)))) False)))) % 8.44/8.65 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.65 (Or (Eq (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a)))) False) % 8.44/8.65 (Or (Eq (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1)))) False) % 8.44/8.65 (Or (Eq (cA_and_B (skS.0 0 a_2)) False) (Eq (Or (Eq (skS.0 0 a_2) ib) (Eq (skS.0 0 a_2) ia)) False))))) % 8.44/8.65 Clause #104 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 8.44/8.65 Or (Eq (cowlThing ib) False) % 8.44/8.65 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a)))) False) % 8.44/8.68 (Or (Eq (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1)))) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a_2)) True) (Eq (Or (Eq (skS.0 0 a_2) ib) (Eq (skS.0 0 a_2) ia)) True))))) % 8.44/8.68 Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a)))) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a_1)) False) % 8.44/8.68 (Or (Eq (Or (Eq (skS.0 0 a_1) ib) (Eq (skS.0 0 a_1) ia)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_2)) False) (Eq (Not (cowlNothing (skS.0 1 a_2))) False)))))) % 8.44/8.68 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) (Eq (Not (xsd_integer (skS.0 2 a_2))) False))))))) % 8.44/8.68 Clause #107 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) True) (Eq (Not (xsd_integer (skS.0 2 a_2))) True))))))) % 8.44/8.68 Clause #108 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) (Eq (Eq (skS.0 0 a) ia) False))))))) % 8.44/8.68 Clause #109 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) (Eq (Eq (skS.0 0 a) ib) False))))))) % 8.44/8.68 Clause #110 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 8.44/8.68 (Or (Eq (Eq (skS.0 0 a) ia) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))))) % 8.44/8.68 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (Eq (skS.0 0 a) ia) False) % 8.44/8.68 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))))) % 8.44/8.68 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq (cowlThing ib) False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.44/8.68 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ia))))))) % 8.44/8.68 Clause #113 (by forward demodulation #[112, 59]): ∀ (a a_1 a_2 : Iota), % 8.44/8.68 Or (Eq True False) % 8.44/8.68 (Or (Eq (cowlThing ia) False) % 8.44/8.68 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.44/8.68 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.44/8.68 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.44/8.68 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.52/8.72 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ia))))))) % 8.52/8.72 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ia)))))) % 8.52/8.72 Clause #115 (by forward demodulation #[114, 59]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq True False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ia)))))) % 8.52/8.72 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ia))))) % 8.52/8.72 Clause #117 (by forward demodulation #[116, 59]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq True False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Ne (skS.0 0 a) ia))))) % 8.52/8.72 Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Ne (skS.0 0 a) ia)))) % 8.52/8.72 Clause #119 (by clausification #[91]): Eq (cA_and_B ia) True % 8.52/8.72 Clause #120 (by clausification #[86]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Or (Eq (cA a) True) (Eq (cB a) True)) % 8.52/8.72 Clause #126 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cowlThing ib) False) % 8.52/8.72 (Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 8.52/8.72 (Or (Eq (Eq (skS.0 0 a) ib) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))))) % 8.52/8.72 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cowlThing ib) False) % 8.52/8.72 (Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (Eq (skS.0 0 a) ib) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))))) % 8.52/8.72 Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cowlThing ib) False) % 8.52/8.72 (Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.52/8.72 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ib))))))) % 8.52/8.72 Clause #129 (by forward demodulation #[128, 59]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq True False) % 8.52/8.72 (Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.52/8.72 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ib))))))) % 8.52/8.72 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq (cowlThing ia) False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.72 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ib)))))) % 8.52/8.72 Clause #131 (by forward demodulation #[130, 59]): ∀ (a a_1 a_2 : Iota), % 8.52/8.72 Or (Eq True False) % 8.52/8.72 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.72 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.72 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ib)))))) % 8.52/8.75 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne (skS.0 0 a) ib))))) % 8.52/8.75 Clause #133 (by forward demodulation #[132, 59]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.75 (Or (Eq True False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.52/8.75 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Ne (skS.0 0 a) ib))))) % 8.52/8.75 Clause #134 (by clausification #[133]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.52/8.75 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Ne (skS.0 0 a) ib)))) % 8.52/8.75 Clause #135 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a)))) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a_1)) True) % 8.52/8.75 (Or (Eq (Or (Eq (skS.0 0 a_1) ib) (Eq (skS.0 0 a_1) ia)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_2)) False) (Eq (Not (cowlNothing (skS.0 1 a_2))) False)))))) % 8.52/8.75 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) (Eq (Not (xsd_integer (skS.0 2 a_2))) False))))))) % 8.52/8.75 Clause #137 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) True) (Eq (Not (xsd_integer (skS.0 2 a_2))) True))))))) % 8.52/8.75 Clause #138 (by clausification #[136]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ib) True) (Eq (Eq (skS.0 0 a) ia) True)))))))) % 8.52/8.75 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ib) True) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ia) True) (Eq (cowlNothing (skS.0 1 a_1)) True)))))))) % 8.52/8.75 Clause #140 (by clausification #[139]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ib) True) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ia) True) % 8.52/8.75 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))))) % 8.52/8.75 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), % 8.52/8.75 Or (Eq (cowlThing ib) False) % 8.52/8.75 (Or (Eq (cowlThing ia) False) % 8.52/8.75 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.52/8.75 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.52/8.75 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.52/8.75 (Or (Eq (Eq (skS.0 0 a) ia) True) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq (skS.0 0 a) ib)))))))) % 8.59/8.79 Clause #142 (by clausification #[141]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cowlThing ib) False) % 8.59/8.79 (Or (Eq (cowlThing ia) False) % 8.59/8.79 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))))) % 8.59/8.79 Clause #143 (by forward demodulation #[142, 59]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq True False) % 8.59/8.79 (Or (Eq (cowlThing ia) False) % 8.59/8.79 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))))) % 8.59/8.79 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cowlThing ia) False) % 8.59/8.79 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))))) % 8.59/8.79 Clause #145 (by forward demodulation #[144, 59]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq True False) % 8.59/8.79 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))))) % 8.59/8.79 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))) % 8.59/8.79 Clause #147 (by forward demodulation #[146, 59]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq True False) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))) % 8.59/8.79 Clause #148 (by clausification #[147]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))) % 8.59/8.79 Clause #149 (by superposition #[148, 64]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) % 8.59/8.79 (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))) % 8.59/8.79 Clause #150 (by clausification #[149]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) % 8.59/8.79 (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 8.59/8.79 Clause #151 (by eliminate duplicate literals #[150]): ∀ (a a_1 a_2 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) % 8.59/8.79 Clause #155 (by superposition #[151, 60]): ∀ (a a_1 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq True False)))) % 8.59/8.79 Clause #156 (by clausification #[155]): ∀ (a a_1 : Iota), % 8.59/8.79 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.59/8.79 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))) % 8.59/8.79 Clause #159 (by superposition #[156, 120]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ia) (Or (Eq True False) (Or (Eq (cA (skS.0 0 a_1)) True) (Eq (cB (skS.0 0 a_1)) True))))) % 8.59/8.82 Clause #160 (by clausification #[159]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (cA (skS.0 0 a_1)) True) (Eq (cB (skS.0 0 a_1)) True)))) % 8.59/8.82 Clause #161 (by superposition #[160, 81]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (cB (skS.0 0 a_1)) True) (Or (Eq True False) (Eq (skS.0 0 a_1) ia))))) % 8.59/8.82 Clause #163 (by clausification #[161]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (cB (skS.0 0 a_1)) True) (Eq (skS.0 0 a_1) ia)))) % 8.59/8.82 Clause #164 (by eliminate duplicate literals #[163]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) (Or (Eq (skS.0 0 a_1) ia) (Eq (cB (skS.0 0 a_1)) True))) % 8.59/8.82 Clause #165 (by superposition #[164, 73]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ib) (Or (Eq (skS.0 0 a_1) ia) (Or (Eq True False) (Eq (skS.0 0 a_1) ib)))) % 8.59/8.82 Clause #167 (by clausification #[165]): ∀ (a a_1 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) (Or (Eq (skS.0 0 a_1) ib) (Or (Eq (skS.0 0 a_1) ia) (Eq (skS.0 0 a_1) ib))) % 8.59/8.82 Clause #168 (by eliminate duplicate literals #[167]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 2 a)) True) (Or (Eq (skS.0 0 a_1) ib) (Eq (skS.0 0 a_1) ia)) % 8.59/8.82 Clause #170 (by superposition #[168, 134]): ∀ (a a_1 a_2 a_3 : Iota), % 8.59/8.82 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.59/8.82 (Or (Eq (skS.0 0 a_1) ia) % 8.59/8.82 (Or (Eq (cA_and_B ib) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.59/8.82 (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Ne ib ib)))))) % 8.59/8.82 Clause #172 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 8.59/8.82 Or (Eq (cowlThing ib) False) % 8.59/8.82 (Or (Eq (cowlThing ia) False) % 8.59/8.82 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.59/8.82 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.82 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.59/8.82 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) (Eq (Eq (skS.0 0 a) ia) False))))))) % 8.59/8.82 Clause #173 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 8.59/8.82 Or (Eq (cowlThing ib) False) % 8.59/8.82 (Or (Eq (cowlThing ia) False) % 8.59/8.82 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.59/8.82 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.82 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.59/8.82 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) (Eq (Eq (skS.0 0 a) ib) False))))))) % 8.59/8.82 Clause #174 (by clausification #[172]): ∀ (a a_1 a_2 : Iota), % 8.59/8.82 Or (Eq (cowlThing ib) False) % 8.59/8.82 (Or (Eq (cowlThing ia) False) % 8.59/8.82 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.59/8.82 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.59/8.82 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 8.59/8.82 (Or (Eq (Eq (skS.0 0 a) ia) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))))) % 8.59/8.82 Clause #175 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 8.59/8.82 Or (Eq (cowlThing ib) False) % 8.59/8.82 (Or (Eq (cowlThing ia) False) % 8.59/8.82 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.59/8.82 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.59/8.82 (Or (Eq (Eq (skS.0 0 a) ia) False) % 8.59/8.82 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False))))))) % 8.59/8.82 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 : Iota), % 8.59/8.82 Or (Eq (cowlThing ib) False) % 8.59/8.82 (Or (Eq (cowlThing ia) False) % 8.59/8.82 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.59/8.82 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.59/8.82 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.59/8.82 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.59/8.82 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ia))))))) % 8.67/8.87 Clause #177 (by forward demodulation #[176, 59]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq True False) % 8.67/8.87 (Or (Eq (cowlThing ia) False) % 8.67/8.87 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.67/8.87 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ia))))))) % 8.67/8.87 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (cowlThing ia) False) % 8.67/8.87 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ia)))))) % 8.67/8.87 Clause #179 (by forward demodulation #[178, 59]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq True False) % 8.67/8.87 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ia)))))) % 8.67/8.87 Clause #180 (by clausification #[179]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ia))))) % 8.67/8.87 Clause #181 (by forward demodulation #[180, 59]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq True False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Ne (skS.0 0 a) ia))))) % 8.67/8.87 Clause #182 (by clausification #[181]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Ne (skS.0 0 a) ia)))) % 8.67/8.87 Clause #186 (by eliminate resolved literals #[170]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) % 8.67/8.87 (Or (Eq (cA_and_B ib) False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 8.67/8.87 Clause #187 (by forward demodulation #[186, 90]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) % 8.67/8.87 (Or (Eq True False) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 8.67/8.87 Clause #188 (by clausification #[187]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) % 8.67/8.87 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))) % 8.67/8.87 Clause #189 (by superposition #[188, 64]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.67/8.87 (Or (Eq (xsd_integer (skS.0 2 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_3)) True))))) % 8.67/8.87 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.67/8.87 (Or (Eq (xsd_integer (skS.0 2 a_3)) True) (Eq (xsd_integer (skS.0 2 a_3)) True)))) % 8.67/8.87 Clause #191 (by eliminate duplicate literals #[190]): ∀ (a a_1 a_2 a_3 : Iota), % 8.67/8.87 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.67/8.87 (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_3)) True))) % 8.67/8.87 Clause #196 (by equality factoring #[191]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (skS.0 0 a) ia) % 8.67/8.87 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 2 a_2)) True))) % 8.67/8.87 Clause #197 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 8.67/8.87 Or (Eq (cowlThing ib) False) % 8.67/8.87 (Or (Eq (cowlThing ia) False) % 8.67/8.87 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ib) True) (Eq (Eq (skS.0 0 a) ia) True)))))))) % 8.72/8.93 Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cowlThing ib) False) % 8.72/8.93 (Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ib) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ia) True) (Eq (cowlNothing (skS.0 1 a_1)) True)))))))) % 8.72/8.93 Clause #199 (by clausification #[198]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cowlThing ib) False) % 8.72/8.93 (Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ib) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ia) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False)))))))) % 8.72/8.93 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cowlThing ib) False) % 8.72/8.93 (Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (Eq (skS.0 0 a) ia) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Eq (skS.0 0 a) ib)))))))) % 8.72/8.93 Clause #201 (by clausification #[200]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cowlThing ib) False) % 8.72/8.93 (Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))))) % 8.72/8.93 Clause #202 (by forward demodulation #[201, 59]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq True False) % 8.72/8.93 (Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))))) % 8.72/8.93 Clause #203 (by clausification #[202]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cowlThing ia) False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))))) % 8.72/8.93 Clause #204 (by forward demodulation #[203, 59]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq True False) % 8.72/8.93 (Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))))) % 8.72/8.93 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))) % 8.72/8.93 Clause #206 (by forward demodulation #[205, 59]): ∀ (a a_1 a_2 : Iota), % 8.72/8.93 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.72/8.93 (Or (Eq True False) % 8.72/8.93 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.72/8.93 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.72/8.93 (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))))) % 8.72/8.93 Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 8.74/8.99 (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))) % 8.74/8.99 Clause #211 (by clausification #[196]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (skS.0 0 a) ia) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.74/8.99 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq True False) (Eq True False)))) % 8.74/8.99 Clause #213 (by clausification #[211]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (skS.0 0 a) ia) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq True False))) % 8.74/8.99 Clause #214 (by clausification #[213]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (skS.0 0 a) ia) (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)) % 8.74/8.99 Clause #215 (by backward contextual literal cutting #[214, 118]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))) % 8.74/8.99 Clause #218 (by superposition #[214, 60]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Eq True False)) % 8.74/8.99 Clause #220 (by clausification #[218]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) True) % 8.74/8.99 Clause #225 (by superposition #[215, 220]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq (cA_and_B ia) False) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 8.74/8.99 Clause #227 (by forward demodulation #[225, 119]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq True False) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 8.74/8.99 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))) % 8.74/8.99 Clause #229 (by superposition #[228, 64]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.74/8.99 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_2)) True)))) % 8.74/8.99 Clause #230 (by clausification #[229]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.74/8.99 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))) % 8.74/8.99 Clause #231 (by eliminate duplicate literals #[230]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (xsd_integer (skS.0 2 a)) True) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)) % 8.74/8.99 Clause #235 (by equality factoring #[231]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 1 a)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 2 a_1)) True)) % 8.74/8.99 Clause #236 (by clausification #[235]): ∀ (a a_1 : Iota), % 8.74/8.99 Or (Eq (cowlNothing (skS.0 1 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq True False) (Eq True False))) % 8.74/8.99 Clause #238 (by clausification #[236]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 1 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Eq True False)) % 8.74/8.99 Clause #239 (by clausification #[238]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 1 a)) True) (Eq (xsd_integer (skS.0 2 a_1)) True) % 8.74/8.99 Clause #240 (by superposition #[239, 60]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 2 a)) True) (Eq True False) % 8.74/8.99 Clause #242 (by clausification #[240]): ∀ (a : Iota), Eq (xsd_integer (skS.0 2 a)) True % 8.74/8.99 Clause #243 (by backward demodulation #[242, 182]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.74/8.99 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq True False) (Ne (skS.0 0 a) ia)))) % 8.74/8.99 Clause #244 (by backward demodulation #[242, 207]): ∀ (a a_1 a_2 : Iota), % 8.74/8.99 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.74/8.99 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.82/9.05 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq True False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))) % 8.82/9.05 Clause #247 (by clausification #[243]): ∀ (a a_1 a_2 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Ne (skS.0 0 a) ia))) % 8.82/9.05 Clause #256 (by clausification #[244]): ∀ (a a_1 a_2 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.82/9.05 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) % 8.82/9.05 Clause #260 (by superposition #[256, 60]): ∀ (a a_1 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq True False)))) % 8.82/9.05 Clause #262 (by clausification #[260]): ∀ (a a_1 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))) % 8.82/9.05 Clause #265 (by superposition #[262, 65]): ∀ (a a_1 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.82/9.05 (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Eq (xsd_integer (skS.0 2 a_1)) False)))) % 8.82/9.05 Clause #266 (by clausification #[265]): ∀ (a a_1 : Iota), % 8.82/9.05 Or (Eq (cA_and_B (skS.0 0 a)) True) % 8.82/9.05 (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) False))) % 8.82/9.05 Clause #267 (by superposition #[266, 242]): ∀ (a : Iota), Or (Eq (cA_and_B (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq False True))) % 8.82/9.05 Clause #268 (by clausification #[267]): ∀ (a : Iota), Or (Eq (cA_and_B (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)) % 8.82/9.05 Clause #270 (by superposition #[268, 120]): ∀ (a : Iota), % 8.82/9.05 Or (Eq (skS.0 0 a) ib) % 8.82/9.05 (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Or (Eq (cA (skS.0 0 a)) True) (Eq (cB (skS.0 0 a)) True)))) % 8.82/9.05 Clause #271 (by clausification #[270]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Or (Eq (cA (skS.0 0 a)) True) (Eq (cB (skS.0 0 a)) True))) % 8.82/9.05 Clause #272 (by superposition #[271, 81]): ∀ (a : Iota), % 8.82/9.05 Or (Eq (skS.0 0 a) ib) % 8.82/9.05 (Or (Eq (skS.0 0 a) ia) (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq True False) (Eq (skS.0 0 a) ia)))) % 8.82/9.05 Clause #274 (by clausification #[272]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Or (Eq (cB (skS.0 0 a)) True) (Eq (skS.0 0 a) ia))) % 8.82/9.05 Clause #275 (by eliminate duplicate literals #[274]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq (cB (skS.0 0 a)) True)) % 8.82/9.05 Clause #276 (by superposition #[275, 73]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Eq (skS.0 0 a) ib))) % 8.82/9.05 Clause #279 (by clausification #[276]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Or (Eq (skS.0 0 a) ia) (Eq (skS.0 0 a) ib)) % 8.82/9.05 Clause #280 (by eliminate duplicate literals #[279]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia) % 8.82/9.05 Clause #298 (by clausification #[173]): ∀ (a a_1 a_2 : Iota), % 8.82/9.05 Or (Eq (cowlThing ib) False) % 8.82/9.05 (Or (Eq (cowlThing ia) False) % 8.82/9.05 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.82/9.05 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.82/9.05 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 8.82/9.05 (Or (Eq (Eq (skS.0 0 a) ib) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))))) % 8.82/9.05 Clause #299 (by clausification #[298]): ∀ (a a_1 a_2 : Iota), % 8.82/9.05 Or (Eq (cowlThing ib) False) % 8.82/9.05 (Or (Eq (cowlThing ia) False) % 8.82/9.05 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.82/9.05 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.82/9.05 (Or (Eq (Eq (skS.0 0 a) ib) False) % 8.82/9.05 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False))))))) % 8.82/9.05 Clause #300 (by clausification #[299]): ∀ (a a_1 a_2 : Iota), % 8.82/9.05 Or (Eq (cowlThing ib) False) % 8.82/9.05 (Or (Eq (cowlThing ia) False) % 8.82/9.05 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.82/9.05 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.82/9.05 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.82/9.05 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.90/9.11 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ib))))))) % 8.90/9.11 Clause #301 (by forward demodulation #[300, 59]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq True False) % 8.90/9.11 (Or (Eq (cowlThing ia) False) % 8.90/9.11 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.90/9.11 (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ib))))))) % 8.90/9.11 Clause #302 (by clausification #[301]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cowlThing ia) False) % 8.90/9.11 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ib)))))) % 8.90/9.11 Clause #303 (by forward demodulation #[302, 59]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq True False) % 8.90/9.11 (Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ib)))))) % 8.90/9.11 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) False) (Ne (skS.0 0 a) ib))))) % 8.90/9.11 Clause #305 (by forward demodulation #[304, 59]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq True False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Ne (skS.0 0 a) ib))))) % 8.90/9.11 Clause #306 (by clausification #[305]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) False) (Ne (skS.0 0 a) ib)))) % 8.90/9.11 Clause #307 (by forward demodulation #[306, 242]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 8.90/9.11 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Or (Eq True False) (Ne (skS.0 0 a) ib)))) % 8.90/9.11 Clause #308 (by clausification #[307]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Ne (skS.0 0 a) ib))) % 8.90/9.11 Clause #309 (by superposition #[308, 280]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (skS.0 0 a) ia) % 8.90/9.11 (Or (Eq (cA_and_B ib) False) % 8.90/9.11 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Ne ib ib)))) % 8.90/9.11 Clause #310 (by eliminate resolved literals #[309]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (skS.0 0 a) ia) % 8.90/9.11 (Or (Eq (cA_and_B ib) False) (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 8.90/9.11 Clause #311 (by forward demodulation #[310, 90]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (skS.0 0 a) ia) % 8.90/9.11 (Or (Eq True False) (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 8.90/9.11 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (skS.0 0 a) ia) (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Eq (cowlNothing (skS.0 1 a_2)) True)) % 8.90/9.11 Clause #313 (by backward contextual literal cutting #[312, 247]): ∀ (a a_1 a_2 : Iota), % 8.90/9.11 Or (Eq (cA_and_B (skS.0 0 a)) False) (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Eq (cowlNothing (skS.0 1 a_2)) True)) % 8.90/9.11 Clause #316 (by superposition #[312, 60]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Eq True False)) % 8.90/9.11 Clause #317 (by clausification #[316]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_string (skS.0 2 a_1)) True) % 8.90/9.11 Clause #319 (by superposition #[317, 65]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Eq (xsd_integer (skS.0 2 a_1)) False)) % 8.90/9.11 Clause #320 (by clausification #[319]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) False) % 8.90/9.13 Clause #321 (by superposition #[320, 242]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ia) (Eq False True) % 8.90/9.13 Clause #322 (by clausification #[321]): ∀ (a : Iota), Eq (skS.0 0 a) ia % 8.90/9.13 Clause #329 (by forward demodulation #[313, 322]): ∀ (a a_1 : Iota), % 8.90/9.13 Or (Eq (cA_and_B ia) False) (Or (Eq (xsd_string (skS.0 2 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True)) % 8.90/9.13 Clause #330 (by forward demodulation #[329, 119]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (xsd_string (skS.0 2 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True)) % 8.90/9.13 Clause #331 (by clausification #[330]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True) % 8.90/9.13 Clause #333 (by superposition #[331, 60]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Eq True False) % 8.90/9.13 Clause #334 (by clausification #[333]): ∀ (a : Iota), Eq (xsd_string (skS.0 2 a)) True % 8.90/9.13 Clause #335 (by superposition #[334, 65]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 2 a)) False) % 8.90/9.13 Clause #336 (by clausification #[335]): ∀ (a : Iota), Eq (xsd_integer (skS.0 2 a)) False % 8.90/9.13 Clause #337 (by superposition #[336, 242]): Eq False True % 8.90/9.13 Clause #338 (by clausification #[337]): False % 8.90/9.13 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------