%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS165+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:44 PM UTC 2025 % Result : Theorem 7.58s 7.75s % Output : Proof 7.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : KRS165+1 : TPTP v9.2.0. Released v3.1.0. % 0.11/0.13 % Command : duper %s % 0.14/0.34 % Computer : n002.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 10:18:53 EDT 2025 % 0.14/0.34 % CPUTime : % 7.58/7.75 SZS status Theorem for theBenchmark.p % 7.58/7.75 SZS output start Proof for theBenchmark.p % 7.58/7.75 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 7.58/7.75 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 7.58/7.75 Clause #2 (by assumption #[]): Eq (∀ (X : Iota), Iff (cCar X) (cAutomobile X)) True % 7.58/7.75 Clause #3 (by assumption #[]): Eq % 7.58/7.75 (Not % 7.58/7.75 (And % 7.58/7.75 (And % 7.58/7.75 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 7.58/7.75 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 7.58/7.75 (∀ (X : Iota), cAutomobile X → cCar X)) % 7.58/7.75 (∀ (X : Iota), cCar X → cAutomobile X))) % 7.58/7.75 True % 7.58/7.75 Clause #4 (by clausification #[2]): ∀ (a : Iota), Eq (Iff (cCar a) (cAutomobile a)) True % 7.58/7.75 Clause #5 (by clausification #[4]): ∀ (a : Iota), Or (Eq (cCar a) True) (Eq (cAutomobile a) False) % 7.58/7.75 Clause #6 (by clausification #[4]): ∀ (a : Iota), Or (Eq (cCar a) False) (Eq (cAutomobile a) True) % 7.58/7.75 Clause #7 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 7.58/7.75 Clause #8 (by clausification #[7]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 7.58/7.75 Clause #9 (by clausification #[7]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 7.58/7.75 Clause #10 (by clausification #[8]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 7.58/7.75 Clause #11 (by clausification #[9]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 7.58/7.75 Clause #13 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 7.58/7.75 Clause #14 (by clausification #[13]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 7.58/7.75 Clause #15 (by clausification #[13]): ∀ (a : Iota), Eq (cowlThing a) True % 7.58/7.75 Clause #16 (by clausification #[14]): ∀ (a : Iota), Eq (cowlNothing a) False % 7.58/7.75 Clause #17 (by clausification #[3]): Eq % 7.58/7.75 (And % 7.58/7.75 (And % 7.58/7.75 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 7.58/7.75 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 7.58/7.75 (∀ (X : Iota), cAutomobile X → cCar X)) % 7.58/7.75 (∀ (X : Iota), cCar X → cAutomobile X)) % 7.58/7.75 False % 7.58/7.75 Clause #18 (by clausification #[17]): Or % 7.58/7.75 (Eq % 7.58/7.75 (And % 7.58/7.75 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 7.58/7.75 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 7.58/7.75 (∀ (X : Iota), cAutomobile X → cCar X)) % 7.58/7.75 False) % 7.58/7.75 (Eq (∀ (X : Iota), cCar X → cAutomobile X) False) % 7.58/7.75 Clause #19 (by clausification #[18]): Or (Eq (∀ (X : Iota), cCar X → cAutomobile X) False) % 7.58/7.75 (Or % 7.58/7.75 (Eq % 7.58/7.75 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 7.58/7.75 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 7.58/7.75 False) % 7.58/7.75 (Eq (∀ (X : Iota), cAutomobile X → cCar X) False)) % 7.58/7.75 Clause #20 (by clausification #[19]): ∀ (a : Iota), % 7.58/7.75 Or % 7.58/7.75 (Eq % 7.58/7.75 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 7.58/7.75 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 7.58/7.75 False) % 7.58/7.75 (Or (Eq (∀ (X : Iota), cAutomobile X → cCar X) False) (Eq (Not (cCar (skS.0 0 a) → cAutomobile (skS.0 0 a))) True)) % 7.58/7.75 Clause #21 (by clausification #[20]): ∀ (a : Iota), % 7.58/7.75 Or (Eq (∀ (X : Iota), cAutomobile X → cCar X) False) % 7.58/7.75 (Or (Eq (Not (cCar (skS.0 0 a) → cAutomobile (skS.0 0 a))) True) % 7.58/7.75 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 7.58/7.75 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False))) % 7.58/7.75 Clause #22 (by clausification #[21]): ∀ (a a_1 : Iota), % 7.58/7.75 Or (Eq (Not (cCar (skS.0 0 a) → cAutomobile (skS.0 0 a))) True) % 7.58/7.75 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 7.58/7.75 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 7.58/7.75 (Eq (Not (cAutomobile (skS.0 1 a_1) → cCar (skS.0 1 a_1))) True))) % 7.58/7.75 Clause #23 (by clausification #[22]): ∀ (a a_1 : Iota), % 7.58/7.75 Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 7.58/7.75 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 7.58/7.75 (Or (Eq (Not (cAutomobile (skS.0 1 a) → cCar (skS.0 1 a))) True) % 7.58/7.78 (Eq (cCar (skS.0 0 a_1) → cAutomobile (skS.0 0 a_1)) False))) % 7.58/7.78 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 : Iota), % 7.58/7.78 Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 7.58/7.78 (Or (Eq (Not (cAutomobile (skS.0 1 a) → cCar (skS.0 1 a))) True) % 7.58/7.78 (Or (Eq (cCar (skS.0 0 a_1) → cAutomobile (skS.0 0 a_1)) False) % 7.58/7.78 (Eq (Not (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2))))) True))) % 7.58/7.78 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (Not (cAutomobile (skS.0 1 a) → cCar (skS.0 1 a))) True) % 7.58/7.78 (Or (Eq (cCar (skS.0 0 a_1) → cAutomobile (skS.0 0 a_1)) False) % 7.58/7.78 (Or (Eq (Not (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2))))) True) % 7.58/7.78 (Eq (Not (Iff (xsd_string (skS.0 3 a_3)) (Not (xsd_integer (skS.0 3 a_3))))) True))) % 7.58/7.78 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a) → cAutomobile (skS.0 0 a)) False) % 7.58/7.78 (Or (Eq (Not (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1))))) True) % 7.58/7.78 (Or (Eq (Not (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2))))) True) % 7.58/7.78 (Eq (cAutomobile (skS.0 1 a_3) → cCar (skS.0 1 a_3)) False))) % 7.58/7.78 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (Not (And (cowlThing (skS.0 2 a)) (Not (cowlNothing (skS.0 2 a))))) True) % 7.58/7.78 (Or (Eq (Not (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1))))) True) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_2) → cCar (skS.0 1 a_2)) False) (Eq (cCar (skS.0 0 a_3)) True))) % 7.58/7.78 Clause #28 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (Not (And (cowlThing (skS.0 2 a)) (Not (cowlNothing (skS.0 2 a))))) True) % 7.58/7.78 (Or (Eq (Not (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1))))) True) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_2) → cCar (skS.0 1 a_2)) False) (Eq (cAutomobile (skS.0 0 a_3)) False))) % 7.58/7.78 Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (Not (Iff (xsd_string (skS.0 3 a)) (Not (xsd_integer (skS.0 3 a))))) True) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_1) → cCar (skS.0 1 a_1)) False) % 7.58/7.78 (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq (And (cowlThing (skS.0 2 a_3)) (Not (cowlNothing (skS.0 2 a_3)))) False))) % 7.58/7.78 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cAutomobile (skS.0 1 a) → cCar (skS.0 1 a)) False) % 7.58/7.78 (Or (Eq (cCar (skS.0 0 a_1)) True) % 7.58/7.78 (Or (Eq (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2)))) False) % 7.58/7.78 (Eq (Iff (xsd_string (skS.0 3 a_3)) (Not (xsd_integer (skS.0 3 a_3)))) False))) % 7.58/7.78 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a)) True) % 7.58/7.78 (Or (Eq (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1)))) False) % 7.58/7.78 (Or (Eq (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2)))) False) % 7.58/7.78 (Eq (cAutomobile (skS.0 1 a_3)) True))) % 7.58/7.78 Clause #32 (by clausification #[30]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a)) True) % 7.58/7.78 (Or (Eq (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1)))) False) % 7.58/7.78 (Or (Eq (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2)))) False) % 7.58/7.78 (Eq (cCar (skS.0 1 a_3)) False))) % 7.58/7.78 Clause #33 (by clausification #[31]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a)) True) % 7.58/7.78 (Or (Eq (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1)))) False) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.58/7.78 (Or (Eq (cowlThing (skS.0 2 a_3)) False) (Eq (Not (cowlNothing (skS.0 2 a_3))) False)))) % 7.58/7.78 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a)) True) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.58/7.78 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.58/7.78 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.58/7.78 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (Not (xsd_integer (skS.0 3 a_3))) False))))) % 7.58/7.78 Clause #35 (by clausification #[33]): ∀ (a a_1 a_2 a_3 : Iota), % 7.58/7.78 Or (Eq (cCar (skS.0 0 a)) True) % 7.58/7.78 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.58/7.78 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.80 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (Not (xsd_integer (skS.0 3 a_3))) True))))) % 7.65/7.80 Clause #36 (by clausification #[34]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.80 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) False) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.65/7.80 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.80 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.80 Clause #38 (by forward demodulation #[37, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.80 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.65/7.80 Clause #40 (by superposition #[15, 39]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_2)) False) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq False True)))) % 7.65/7.80 Clause #42 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (xsd_string (skS.0 3 a_2)) False) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 7.65/7.80 Clause #43 (by superposition #[42, 10]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 7.65/7.80 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.80 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 7.65/7.80 Clause #45 (by eliminate duplicate literals #[44]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) True)) % 7.65/7.80 Clause #47 (by superposition #[45, 5]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.80 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq True False))) % 7.65/7.80 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (cCar (skS.0 1 a_2)) True)) % 7.65/7.80 Clause #49 (by superposition #[48, 6]): ∀ (a a_1 a_2 : Iota), % 7.65/7.80 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.65/7.80 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 0 a_2)) True))) % 7.65/7.80 Clause #51 (by clausification #[28]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (Not (Iff (xsd_string (skS.0 3 a)) (Not (xsd_integer (skS.0 3 a))))) True) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 1 a_1) → cCar (skS.0 1 a_1)) False) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 0 a_2)) False) % 7.65/7.80 (Eq (And (cowlThing (skS.0 2 a_3)) (Not (cowlNothing (skS.0 2 a_3)))) False))) % 7.65/7.80 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cAutomobile (skS.0 1 a) → cCar (skS.0 1 a)) False) % 7.65/7.80 (Or (Eq (cAutomobile (skS.0 0 a_1)) False) % 7.65/7.80 (Or (Eq (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2)))) False) % 7.65/7.80 (Eq (Iff (xsd_string (skS.0 3 a_3)) (Not (xsd_integer (skS.0 3 a_3)))) False))) % 7.65/7.80 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.80 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.80 (Or (Eq (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1)))) False) % 7.65/7.80 (Or (Eq (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2)))) False) % 7.65/7.83 (Eq (cAutomobile (skS.0 1 a_3)) True))) % 7.65/7.83 Clause #54 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1)))) False) % 7.65/7.83 (Or (Eq (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2)))) False) % 7.65/7.83 (Eq (cCar (skS.0 1 a_3)) False))) % 7.65/7.83 Clause #55 (by clausification #[53]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1)))) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_3)) False) (Eq (Not (cowlNothing (skS.0 2 a_3))) False)))) % 7.65/7.83 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (Not (xsd_integer (skS.0 3 a_3))) False))))) % 7.65/7.83 Clause #57 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (Not (xsd_integer (skS.0 3 a_3))) True))))) % 7.65/7.83 Clause #58 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.83 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) False) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.65/7.83 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.83 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.83 Clause #60 (by forward demodulation #[59, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.83 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.65/7.83 Clause #63 (by clausification #[49]): ∀ (a a_1 a_2 : Iota), % 7.65/7.83 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq (cAutomobile (skS.0 0 a_2)) True)) % 7.65/7.83 Clause #65 (by superposition #[63, 61]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.65/7.83 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.65/7.83 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.65/7.83 (Or (Eq True False) % 7.65/7.83 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_3)) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_4)) True)))))) % 7.65/7.83 Clause #73 (by clausification #[32]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.83 (Or (Eq (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1)))) False) % 7.65/7.83 (Or (Eq (cCar (skS.0 1 a_2)) False) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_3)) False) (Eq (Not (cowlNothing (skS.0 2 a_3))) False)))) % 7.65/7.83 Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.83 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.83 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.83 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.83 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.65/7.83 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (Not (xsd_integer (skS.0 3 a_3))) False))))) % 7.65/7.83 Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (Not (xsd_integer (skS.0 3 a_3))) True))))) % 7.65/7.86 Clause #76 (by clausification #[74]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.86 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) False) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.65/7.86 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.65/7.86 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.86 Clause #78 (by forward demodulation #[77, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.65/7.86 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.65/7.86 Clause #81 (by superposition #[79, 63]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 7.65/7.86 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (cAutomobile (skS.0 0 a_4)) True)))))) % 7.65/7.86 Clause #84 (by clausification #[35]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.65/7.86 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) True) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.65/7.86 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.65/7.86 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.65/7.86 Clause #86 (by forward demodulation #[85, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.65/7.86 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False)))) % 7.65/7.86 Clause #88 (by superposition #[87, 15]): ∀ (a a_1 a_2 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) False) (Eq False True)))) % 7.65/7.86 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False))) % 7.65/7.86 Clause #90 (by superposition #[89, 45]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.65/7.86 (Or (Eq (xsd_string (skS.0 3 a_2)) True) % 7.65/7.86 (Or (Eq (cCar (skS.0 0 a_3)) True) (Or (Eq (cAutomobile (skS.0 1 a_4)) True) (Eq False True))))) % 7.65/7.86 Clause #94 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.65/7.86 Or (Eq (cCar (skS.0 0 a)) True) % 7.65/7.86 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_2)) True) % 7.72/7.89 (Or (Eq (cCar (skS.0 0 a_3)) True) (Eq (cAutomobile (skS.0 1 a_4)) True)))) % 7.72/7.89 Clause #101 (by equality factoring #[94]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cCar (skS.0 0 a)) True) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 7.72/7.89 (Or (Eq (cCar (skS.0 0 a_2)) True) (Or (Ne True True) (Eq (cAutomobile (skS.0 1 a_3)) True)))) % 7.72/7.89 Clause #102 (by clausification #[54]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1)))) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_2)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_3)) False) (Eq (Not (cowlNothing (skS.0 2 a_3))) False)))) % 7.72/7.89 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (Not (xsd_integer (skS.0 3 a_3))) False))))) % 7.72/7.89 Clause #104 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (Not (xsd_integer (skS.0 3 a_3))) True))))) % 7.72/7.89 Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.72/7.89 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) False) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.72/7.89 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 7.72/7.89 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.72/7.89 Clause #107 (by forward demodulation #[106, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.72/7.89 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.72/7.89 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.72/7.89 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.72/7.89 Clause #111 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cCar (skS.0 0 a)) True) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 7.72/7.89 (Or (Eq (cCar (skS.0 0 a_2)) True) % 7.72/7.89 (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Or (Eq True False) (Eq True False))))) % 7.72/7.89 Clause #113 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cCar (skS.0 0 a)) True) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 7.72/7.89 (Or (Eq (cCar (skS.0 0 a_2)) True) (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Eq True False)))) % 7.72/7.89 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 : Iota), % 7.72/7.89 Or (Eq (cCar (skS.0 0 a)) True) % 7.72/7.89 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq (cAutomobile (skS.0 1 a_3)) True))) % 7.72/7.89 Clause #119 (by equality factoring #[114]): ∀ (a a_1 a_2 : Iota), % 7.72/7.89 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.72/7.89 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (cCar (skS.0 0 a_2)) True))) % 7.72/7.89 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), % 7.72/7.89 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.72/7.89 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.72/7.89 Clause #122 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), % 7.72/7.89 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.72/7.89 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq True False))) % 7.75/7.91 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Eq (cCar (skS.0 0 a_2)) True)) % 7.75/7.91 Clause #124 (by superposition #[123, 11]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.75/7.91 (Or (Eq (cCar (skS.0 0 a_1)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_2)) False))) % 7.75/7.91 Clause #126 (by superposition #[123, 6]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 0 a_2)) True))) % 7.75/7.91 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Eq (cAutomobile (skS.0 0 a_2)) True)) % 7.75/7.91 Clause #129 (by superposition #[127, 5]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq True False))) % 7.75/7.91 Clause #132 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Eq (cCar (skS.0 1 a_2)) True)) % 7.75/7.91 Clause #134 (by superposition #[132, 61]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.75/7.91 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.75/7.91 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq True False) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_3)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_4)) True)))))) % 7.75/7.91 Clause #140 (by clausification #[57]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.75/7.91 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) True) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.75/7.91 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.75/7.91 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.75/7.91 Clause #142 (by forward demodulation #[141, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.75/7.91 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False)))) % 7.75/7.91 Clause #165 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.75/7.91 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.75/7.91 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.75/7.91 (Or (Eq (cowlThing (skS.0 2 a_3)) False) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_4)) True))))) % 7.75/7.91 Clause #166 (by superposition #[165, 15]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.75/7.91 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.75/7.91 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.75/7.91 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq False True))))) % 7.75/7.91 Clause #173 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) False)) % 7.75/7.91 Clause #176 (by superposition #[173, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.75/7.91 (Or (Eq (cCar (skS.0 0 a_1)) True) % 7.75/7.91 (Or (Eq False True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq (cAutomobile (skS.0 0 a_3)) True)))) % 7.75/7.91 Clause #181 (by clausification #[176]): ∀ (a a_1 a_2 a_3 : Iota), % 7.75/7.91 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 0 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq (cAutomobile (skS.0 0 a_3)) True))) % 7.78/7.94 Clause #189 (by superposition #[181, 5]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 0 a_1)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_2)) True) (Or (Eq (cCar (skS.0 0 a_3)) True) (Eq True False)))) % 7.78/7.94 Clause #190 (by clausification #[189]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 0 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq (cCar (skS.0 0 a_3)) True))) % 7.78/7.94 Clause #196 (by equality factoring #[190]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (cCar (skS.0 0 a_2)) True))) % 7.78/7.94 Clause #197 (by clausification #[196]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.78/7.94 Clause #199 (by clausification #[197]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq True False))) % 7.78/7.94 Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq (cCar (skS.0 0 a_2)) True)) % 7.78/7.94 Clause #204 (by superposition #[200, 6]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 0 a_2)) True))) % 7.78/7.94 Clause #205 (by clausification #[204]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq (cAutomobile (skS.0 0 a_2)) True)) % 7.78/7.94 Clause #208 (by superposition #[205, 6]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 1 a_2)) True))) % 7.78/7.94 Clause #212 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.94 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Eq (cAutomobile (skS.0 1 a_2)) True)) % 7.78/7.94 Clause #219 (by equality factoring #[212]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Ne True True) (Eq (cAutomobile (skS.0 1 a_1)) True)) % 7.78/7.94 Clause #220 (by clausification #[75]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.94 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.94 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.78/7.94 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) True) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.78/7.94 Clause #221 (by clausification #[220]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.94 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.94 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.78/7.94 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.78/7.94 Clause #222 (by forward demodulation #[221, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.94 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.94 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.78/7.94 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.94 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.94 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.94 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.94 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False)))) % 7.78/7.94 Clause #230 (by clausification #[219]): ∀ (a a_1 : Iota), % 7.78/7.94 Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.78/7.94 Clause #232 (by clausification #[230]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Eq True False)) % 7.78/7.94 Clause #233 (by clausification #[232]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/7.94 Clause #236 (by superposition #[233, 143]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.97 (Or (Eq True False) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.78/7.97 Clause #261 (by clausification #[81]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq (cAutomobile (skS.0 0 a_4)) True))))) % 7.78/7.97 Clause #262 (by superposition #[261, 15]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq (cAutomobile (skS.0 0 a_3)) True) (Eq False True))))) % 7.78/7.97 Clause #302 (by clausification #[236]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False)))) % 7.78/7.97 Clause #303 (by superposition #[302, 15]): ∀ (a a_1 a_2 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) False) (Eq False True)))) % 7.78/7.97 Clause #304 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False))) % 7.78/7.97 Clause #309 (by clausification #[104]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.78/7.97 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.78/7.97 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) True) (Eq (cowlNothing (skS.0 2 a_2)) True))))) % 7.78/7.97 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.78/7.97 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 7.78/7.97 (Or (Eq (cowlNothing (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.78/7.97 Clause #311 (by forward demodulation #[310, 16]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.78/7.97 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) False))))) % 7.78/7.97 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cAutomobile (skS.0 0 a)) False) % 7.78/7.97 (Or (Eq (cCar (skS.0 1 a_1)) False) % 7.78/7.97 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) False)))) % 7.78/7.97 Clause #329 (by clausification #[262]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (cAutomobile (skS.0 0 a_3)) True)))) % 7.78/7.97 Clause #330 (by superposition #[329, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 0 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_1)) True))))) % 7.78/7.97 Clause #331 (by clausification #[330]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 7.78/7.97 (Or (Eq (cAutomobile (skS.0 0 a_3)) True) (Eq (xsd_integer (skS.0 3 a_1)) True)))) % 7.78/7.97 Clause #332 (by eliminate duplicate literals #[331]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/7.97 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) % 7.78/7.97 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (cAutomobile (skS.0 0 a_3)) True))) % 7.78/8.00 Clause #340 (by equality factoring #[332]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 7.78/8.00 Clause #341 (by clausification #[340]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) % 7.78/8.00 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.78/8.00 Clause #343 (by clausification #[341]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq True False))) % 7.78/8.00 Clause #344 (by clausification #[343]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (cAutomobile (skS.0 0 a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) True)) % 7.78/8.00 Clause #350 (by superposition #[344, 5]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) % 7.78/8.00 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq True False))) % 7.78/8.00 Clause #353 (by clausification #[350]): ∀ (a a_1 a_2 : Iota), % 7.78/8.00 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (cCar (skS.0 0 a_2)) True)) % 7.78/8.00 Clause #357 (by equality factoring #[353]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Ne True True) (Eq (cCar (skS.0 0 a_1)) True)) % 7.78/8.00 Clause #358 (by clausification #[357]): ∀ (a a_1 : Iota), % 7.78/8.00 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 0 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.78/8.00 Clause #360 (by clausification #[358]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 0 a_1)) True) (Eq True False)) % 7.78/8.00 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (cCar (skS.0 0 a_1)) True) % 7.78/8.00 Clause #363 (by superposition #[361, 6]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 0 a_1)) True)) % 7.78/8.00 Clause #364 (by clausification #[363]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (cAutomobile (skS.0 0 a_1)) True) % 7.78/8.00 Clause #385 (by clausification #[134]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.00 (Or (Eq (cowlThing (skS.0 2 a_3)) False) % 7.78/8.00 (Or (Eq (xsd_string (skS.0 3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_4)) True))))) % 7.78/8.00 Clause #386 (by superposition #[385, 15]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.00 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq False True))))) % 7.78/8.00 Clause #387 (by clausification #[386]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.00 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.78/8.00 Clause #388 (by superposition #[387, 10]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.00 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_3)) True))))) % 7.78/8.00 Clause #389 (by clausification #[388]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.00 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.78/8.00 Clause #390 (by eliminate duplicate literals #[389]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (cAutomobile (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 3 a_3)) True))) % 7.78/8.00 Clause #399 (by superposition #[390, 5]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.00 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.78/8.00 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq (cCar (skS.0 1 a_3)) True) (Eq True False)))) % 7.78/8.03 Clause #401 (by clausification #[399]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (cCar (skS.0 1 a_3)) True))) % 7.78/8.03 Clause #418 (by equality factoring #[401]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Ne True True) (Eq (cCar (skS.0 1 a_2)) True))) % 7.78/8.03 Clause #419 (by clausification #[418]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.78/8.03 Clause #421 (by clausification #[419]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq True False))) % 7.78/8.03 Clause #422 (by clausification #[421]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (cCar (skS.0 1 a_2)) True)) % 7.78/8.03 Clause #431 (by superposition #[422, 6]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 1 a_2)) True))) % 7.78/8.03 Clause #432 (by clausification #[431]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (cAutomobile (skS.0 1 a_2)) True)) % 7.78/8.03 Clause #434 (by superposition #[432, 304]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Or (Eq (xsd_string (skS.0 3 a_4)) True) (Eq True False))))) % 7.78/8.03 Clause #459 (by clausification #[434]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Eq (xsd_string (skS.0 3 a_4)) True)))) % 7.78/8.03 Clause #464 (by equality factoring #[459]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Or (Ne True True) (Eq (cAutomobile (skS.0 1 a_3)) True)))) % 7.78/8.03 Clause #465 (by clausification #[464]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_2)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Or (Eq True False) (Eq True False))))) % 7.78/8.03 Clause #467 (by clausification #[465]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Or (Eq (cAutomobile (skS.0 1 a_3)) True) (Eq True False)))) % 7.78/8.03 Clause #468 (by clausification #[467]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (cAutomobile (skS.0 1 a_3)) True))) % 7.78/8.03 Clause #474 (by equality factoring #[468]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Ne True True) (Eq (cAutomobile (skS.0 1 a_2)) True))) % 7.78/8.03 Clause #475 (by clausification #[474]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 7.78/8.03 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.78/8.03 Clause #477 (by clausification #[475]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) % 7.78/8.03 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq (cAutomobile (skS.0 1 a_2)) True) (Eq True False))) % 7.78/8.03 Clause #478 (by clausification #[477]): ∀ (a a_1 a_2 : Iota), % 7.78/8.03 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq (cAutomobile (skS.0 1 a_2)) True)) % 7.78/8.03 Clause #481 (by equality factoring #[478]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Ne True True) (Eq (xsd_string (skS.0 3 a_1)) True)) % 7.88/8.05 Clause #482 (by clausification #[481]): ∀ (a a_1 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.88/8.05 Clause #484 (by clausification #[482]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq True False)) % 7.88/8.05 Clause #485 (by clausification #[484]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Eq (xsd_string (skS.0 3 a_1)) True) % 7.88/8.05 Clause #486 (by superposition #[485, 5]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq True False)) % 7.88/8.05 Clause #493 (by clausification #[486]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (cCar (skS.0 1 a_1)) True) % 7.88/8.05 Clause #494 (by superposition #[493, 11]): ∀ (a a_1 : Iota), Or (Eq (cCar (skS.0 1 a)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_1)) False)) % 7.88/8.05 Clause #501 (by clausification #[494]): ∀ (a a_1 : Iota), Or (Eq (cCar (skS.0 1 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) False) % 7.88/8.05 Clause #513 (by clausification #[166]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.88/8.05 (Or (Eq (xsd_string (skS.0 3 a_3)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)))) % 7.88/8.05 Clause #515 (by superposition #[513, 493]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.88/8.05 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Or (Eq False True) (Eq (cCar (skS.0 1 a_4)) True))))) % 7.88/8.05 Clause #529 (by clausification #[515]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_2)) True) % 7.88/8.05 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq (cCar (skS.0 1 a_4)) True)))) % 7.88/8.05 Clause #546 (by equality factoring #[529]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Ne True True) (Eq (cCar (skS.0 1 a_3)) True)))) % 7.88/8.05 Clause #547 (by clausification #[546]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_3)) True) (Or (Eq True False) (Eq True False))))) % 7.88/8.05 Clause #549 (by clausification #[547]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.88/8.05 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq (cCar (skS.0 1 a_3)) True) (Eq True False)))) % 7.88/8.05 Clause #550 (by clausification #[549]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.05 Or (Eq (xsd_integer (skS.0 3 a)) True) % 7.88/8.05 (Or (Eq (cAutomobile (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (cCar (skS.0 1 a_3)) True))) % 7.88/8.05 Clause #561 (by equality factoring #[550]): ∀ (a a_1 a_2 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 7.88/8.05 Clause #562 (by clausification #[561]): ∀ (a a_1 a_2 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq True False) (Eq True False)))) % 7.88/8.05 Clause #564 (by clausification #[562]): ∀ (a a_1 a_2 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq True False))) % 7.88/8.05 Clause #565 (by clausification #[564]): ∀ (a a_1 a_2 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) True)) % 7.88/8.05 Clause #573 (by superposition #[565, 501]): ∀ (a a_1 a_2 : Iota), % 7.88/8.05 Or (Eq (cAutomobile (skS.0 1 a)) True) % 7.88/8.05 (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq (cCar (skS.0 1 a_2)) True) (Eq True False))) % 7.88/8.05 Clause #575 (by clausification #[573]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq (cCar (skS.0 1 a_2)) True)) % 7.88/8.08 Clause #582 (by equality factoring #[575]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Ne True True) (Eq (cCar (skS.0 1 a_1)) True)) % 7.88/8.08 Clause #583 (by clausification #[582]): ∀ (a a_1 : Iota), % 7.88/8.08 Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.88/8.08 Clause #585 (by clausification #[583]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq (cCar (skS.0 1 a_1)) True) (Eq True False)) % 7.88/8.08 Clause #586 (by clausification #[585]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Eq (cCar (skS.0 1 a_1)) True) % 7.88/8.08 Clause #592 (by superposition #[586, 6]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 1 a_1)) True)) % 7.88/8.08 Clause #593 (by clausification #[592]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Eq (cAutomobile (skS.0 1 a_1)) True) % 7.88/8.08 Clause #594 (by equality factoring #[593]): ∀ (a : Iota), Or (Ne True True) (Eq (cAutomobile (skS.0 1 a)) True) % 7.88/8.08 Clause #595 (by clausification #[594]): ∀ (a : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Or (Eq True False) (Eq True False)) % 7.88/8.08 Clause #597 (by clausification #[595]): ∀ (a : Iota), Or (Eq (cAutomobile (skS.0 1 a)) True) (Eq True False) % 7.88/8.08 Clause #598 (by clausification #[597]): ∀ (a : Iota), Eq (cAutomobile (skS.0 1 a)) True % 7.88/8.08 Clause #599 (by superposition #[598, 5]): ∀ (a : Iota), Or (Eq (cCar (skS.0 1 a)) True) (Eq True False) % 7.88/8.08 Clause #600 (by clausification #[599]): ∀ (a : Iota), Eq (cCar (skS.0 1 a)) True % 7.88/8.08 Clause #601 (by superposition #[600, 223]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) % 7.88/8.08 (Or (Eq True False) % 7.88/8.08 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.88/8.08 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False)))) % 7.88/8.08 Clause #612 (by clausification #[601]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) % 7.88/8.08 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.88/8.08 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False))) % 7.88/8.08 Clause #613 (by superposition #[612, 15]): ∀ (a a_1 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) % 7.88/8.08 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq False True))) % 7.88/8.08 Clause #614 (by clausification #[613]): ∀ (a a_1 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq (xsd_integer (skS.0 3 a_1)) False)) % 7.88/8.08 Clause #616 (by superposition #[614, 364]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) % 7.88/8.08 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq False True) (Eq (cAutomobile (skS.0 0 a_2)) True))) % 7.88/8.08 Clause #617 (by clausification #[616]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq (cAutomobile (skS.0 0 a_2)) True)) % 7.88/8.08 Clause #622 (by superposition #[617, 5]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) % 7.88/8.08 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq (cCar (skS.0 0 a_2)) True) (Eq True False))) % 7.88/8.08 Clause #623 (by clausification #[622]): ∀ (a a_1 a_2 : Iota), % 7.88/8.08 Or (Eq (cCar (skS.0 0 a)) True) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq (cCar (skS.0 0 a_2)) True)) % 7.88/8.08 Clause #627 (by equality factoring #[623]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Ne True True) (Eq (cCar (skS.0 0 a_1)) True)) % 7.88/8.08 Clause #628 (by clausification #[627]): ∀ (a a_1 : Iota), % 7.88/8.08 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 0 a_1)) True) (Or (Eq True False) (Eq True False))) % 7.88/8.08 Clause #630 (by clausification #[628]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (cCar (skS.0 0 a_1)) True) (Eq True False)) % 7.88/8.08 Clause #631 (by clausification #[630]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (cCar (skS.0 0 a_1)) True) % 7.88/8.08 Clause #633 (by superposition #[631, 6]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq True False) (Eq (cAutomobile (skS.0 0 a_1)) True)) % 7.88/8.08 Clause #635 (by clausification #[633]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (cAutomobile (skS.0 0 a_1)) True) % 7.95/8.11 Clause #636 (by superposition #[635, 11]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_1)) False)) % 7.95/8.11 Clause #639 (by clausification #[636]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) False) % 7.95/8.11 Clause #641 (by superposition #[639, 364]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Eq False True) (Eq (cAutomobile (skS.0 0 a_1)) True)) % 7.95/8.11 Clause #642 (by clausification #[641]): ∀ (a a_1 : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Eq (cAutomobile (skS.0 0 a_1)) True) % 7.95/8.11 Clause #646 (by equality factoring #[642]): ∀ (a : Iota), Or (Ne True True) (Eq (cAutomobile (skS.0 0 a)) True) % 7.95/8.11 Clause #647 (by clausification #[646]): ∀ (a : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Or (Eq True False) (Eq True False)) % 7.95/8.11 Clause #649 (by clausification #[647]): ∀ (a : Iota), Or (Eq (cAutomobile (skS.0 0 a)) True) (Eq True False) % 7.95/8.11 Clause #650 (by clausification #[649]): ∀ (a : Iota), Eq (cAutomobile (skS.0 0 a)) True % 7.95/8.11 Clause #651 (by superposition #[650, 108]): ∀ (a a_1 a_2 : Iota), % 7.95/8.11 Or (Eq True False) % 7.95/8.11 (Or (Eq (cCar (skS.0 1 a)) False) % 7.95/8.11 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_2)) False) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 7.95/8.11 Clause #652 (by superposition #[650, 312]): ∀ (a a_1 a_2 : Iota), % 7.95/8.11 Or (Eq True False) % 7.95/8.11 (Or (Eq (cCar (skS.0 1 a)) False) % 7.95/8.11 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False)))) % 7.95/8.11 Clause #672 (by clausification #[652]): ∀ (a a_1 a_2 : Iota), % 7.95/8.11 Or (Eq (cCar (skS.0 1 a)) False) % 7.95/8.11 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_2)) True) (Eq (xsd_integer (skS.0 3 a_2)) False))) % 7.95/8.11 Clause #673 (by superposition #[672, 600]): ∀ (a a_1 : Iota), % 7.95/8.11 Or (Eq (cowlThing (skS.0 2 a)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq False True))) % 7.95/8.11 Clause #674 (by clausification #[673]): ∀ (a a_1 : Iota), % 7.95/8.11 Or (Eq (cowlThing (skS.0 2 a)) False) (Or (Eq (xsd_string (skS.0 3 a_1)) True) (Eq (xsd_integer (skS.0 3 a_1)) False)) % 7.95/8.11 Clause #675 (by superposition #[674, 15]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (xsd_integer (skS.0 3 a)) False) (Eq False True)) % 7.95/8.11 Clause #676 (by clausification #[675]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (xsd_integer (skS.0 3 a)) False) % 7.95/8.11 Clause #685 (by clausification #[651]): ∀ (a a_1 a_2 : Iota), % 7.95/8.11 Or (Eq (cCar (skS.0 1 a)) False) % 7.95/8.11 (Or (Eq (cowlThing (skS.0 2 a_1)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_2)) False) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 7.95/8.11 Clause #686 (by superposition #[685, 600]): ∀ (a a_1 : Iota), % 7.95/8.11 Or (Eq (cowlThing (skS.0 2 a)) False) % 7.95/8.11 (Or (Eq (xsd_string (skS.0 3 a_1)) False) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq False True))) % 7.95/8.11 Clause #688 (by clausification #[686]): ∀ (a a_1 : Iota), % 7.95/8.11 Or (Eq (cowlThing (skS.0 2 a)) False) (Or (Eq (xsd_string (skS.0 3 a_1)) False) (Eq (xsd_integer (skS.0 3 a_1)) True)) % 7.95/8.11 Clause #689 (by superposition #[688, 15]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) False) (Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq False True)) % 7.95/8.11 Clause #690 (by clausification #[689]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) False) (Eq (xsd_integer (skS.0 3 a)) True) % 7.95/8.11 Clause #691 (by superposition #[690, 10]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a)) True)) % 7.95/8.11 Clause #692 (by clausification #[691]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (xsd_integer (skS.0 3 a)) True) % 7.95/8.11 Clause #693 (by eliminate duplicate literals #[692]): ∀ (a : Iota), Eq (xsd_integer (skS.0 3 a)) True % 7.95/8.11 Clause #694 (by backward demodulation #[693, 676]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq True False) % 7.95/8.11 Clause #696 (by clausification #[694]): ∀ (a : Iota), Eq (xsd_string (skS.0 3 a)) True % 7.95/8.11 Clause #697 (by superposition #[696, 11]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 3 a)) False) % 7.95/8.11 Clause #700 (by clausification #[697]): ∀ (a : Iota), Eq (xsd_integer (skS.0 3 a)) False % 7.95/8.11 Clause #701 (by superposition #[700, 693]): Eq False True % 7.95/8.11 Clause #702 (by clausification #[701]): False % 7.95/8.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------