%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS174+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.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 5.05s 5.25s % Output : Proof 5.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : KRS174+1 : TPTP v9.2.0. Released v3.1.0. % 0.07/0.15 % Command : duper %s % 0.14/0.37 % Computer : n017.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Thu Oct 2 10:18:08 EDT 2025 % 0.14/0.37 % CPUTime : % 5.05/5.25 SZS status Theorem for theBenchmark.p % 5.05/5.25 SZS output start Proof for theBenchmark.p % 5.05/5.25 Clause #7 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 5.05/5.25 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 5.05/5.25 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), Iff (cA X) (Eq X ia)) True % 5.05/5.25 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (Eq X ib) (Eq X ia))) True % 5.05/5.25 Clause #11 (by assumption #[]): Eq (∀ (X : Iota), Iff (cB X) (Eq X ib)) True % 5.05/5.25 Clause #14 (by assumption #[]): Eq % 5.05/5.25 (Not % 5.05/5.25 (And % 5.05/5.25 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 5.05/5.25 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 5.05/5.25 (∀ (X : Iota), Iff (cA_and_B X) (Or (cB X) (cA X))))) % 5.05/5.25 True % 5.05/5.25 Clause #57 (by clausification #[7]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 5.05/5.25 Clause #58 (by clausification #[57]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 5.05/5.25 Clause #59 (by clausification #[57]): ∀ (a : Iota), Eq (cowlThing a) True % 5.05/5.25 Clause #60 (by clausification #[58]): ∀ (a : Iota), Eq (cowlNothing a) False % 5.05/5.25 Clause #61 (by clausification #[8]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 5.05/5.25 Clause #62 (by clausification #[61]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 5.05/5.25 Clause #63 (by clausification #[61]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 5.05/5.25 Clause #64 (by clausification #[62]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 5.05/5.25 Clause #65 (by clausification #[63]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 5.05/5.25 Clause #68 (by clausification #[11]): ∀ (a : Iota), Eq (Iff (cB a) (Eq a ib)) True % 5.05/5.25 Clause #69 (by clausification #[68]): ∀ (a : Iota), Or (Eq (cB a) True) (Eq (Eq a ib) False) % 5.05/5.25 Clause #70 (by clausification #[68]): ∀ (a : Iota), Or (Eq (cB a) False) (Eq (Eq a ib) True) % 5.05/5.25 Clause #71 (by clausification #[69]): ∀ (a : Iota), Or (Eq (cB a) True) (Ne a ib) % 5.05/5.25 Clause #72 (by destructive equality resolution #[71]): Eq (cB ib) True % 5.05/5.25 Clause #73 (by clausification #[70]): ∀ (a : Iota), Or (Eq (cB a) False) (Eq a ib) % 5.05/5.25 Clause #76 (by clausification #[9]): ∀ (a : Iota), Eq (Iff (cA a) (Eq a ia)) True % 5.05/5.25 Clause #77 (by clausification #[76]): ∀ (a : Iota), Or (Eq (cA a) True) (Eq (Eq a ia) False) % 5.05/5.25 Clause #78 (by clausification #[76]): ∀ (a : Iota), Or (Eq (cA a) False) (Eq (Eq a ia) True) % 5.05/5.25 Clause #79 (by clausification #[77]): ∀ (a : Iota), Or (Eq (cA a) True) (Ne a ia) % 5.05/5.25 Clause #80 (by destructive equality resolution #[79]): Eq (cA ia) True % 5.05/5.25 Clause #81 (by clausification #[78]): ∀ (a : Iota), Or (Eq (cA a) False) (Eq a ia) % 5.05/5.25 Clause #84 (by clausification #[10]): ∀ (a : Iota), Eq (Iff (cA_and_B a) (Or (Eq a ib) (Eq a ia))) True % 5.05/5.25 Clause #85 (by clausification #[84]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (Or (Eq a ib) (Eq a ia)) False) % 5.05/5.25 Clause #86 (by clausification #[84]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Eq (Or (Eq a ib) (Eq a ia)) True) % 5.05/5.25 Clause #87 (by clausification #[85]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (Eq a ia) False) % 5.05/5.25 Clause #88 (by clausification #[85]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Eq (Eq a ib) False) % 5.05/5.25 Clause #89 (by clausification #[87]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Ne a ia) % 5.05/5.25 Clause #90 (by destructive equality resolution #[89]): Eq (cA_and_B ia) True % 5.05/5.25 Clause #91 (by clausification #[88]): ∀ (a : Iota), Or (Eq (cA_and_B a) True) (Ne a ib) % 5.05/5.25 Clause #92 (by destructive equality resolution #[91]): Eq (cA_and_B ib) True % 5.05/5.25 Clause #93 (by clausification #[86]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Or (Eq (Eq a ib) True) (Eq (Eq a ia) True)) % 5.05/5.25 Clause #94 (by clausification #[93]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Or (Eq (Eq a ia) True) (Eq a ib)) % 5.05/5.25 Clause #95 (by clausification #[94]): ∀ (a : Iota), Or (Eq (cA_and_B a) False) (Or (Eq a ib) (Eq a ia)) % 5.05/5.25 Clause #98 (by clausification #[14]): Eq % 5.05/5.25 (And % 5.05/5.25 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 5.05/5.25 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 5.11/5.28 (∀ (X : Iota), Iff (cA_and_B X) (Or (cB X) (cA X)))) % 5.11/5.28 False % 5.11/5.28 Clause #99 (by clausification #[98]): Or % 5.11/5.28 (Eq % 5.11/5.28 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 5.11/5.28 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 5.11/5.28 False) % 5.11/5.28 (Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (cB X) (cA X))) False) % 5.11/5.28 Clause #100 (by clausification #[99]): Or (Eq (∀ (X : Iota), Iff (cA_and_B X) (Or (cB X) (cA X))) False) % 5.11/5.28 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 5.11/5.28 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)) % 5.11/5.28 Clause #101 (by clausification #[100]): ∀ (a : Iota), % 5.11/5.28 Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 5.11/5.28 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 5.11/5.28 (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))))) True)) % 5.11/5.28 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), % 5.11/5.28 Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 5.11/5.28 (Or (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))))) True) % 5.11/5.28 (Eq (Not (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1))))) True)) % 5.11/5.28 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (Not (Iff (cA_and_B (skS.0 0 a)) (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))))) True) % 5.11/5.28 (Or (Eq (Not (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1))))) True) % 5.11/5.28 (Eq (Not (Iff (xsd_string (skS.0 2 a_2)) (Not (xsd_integer (skS.0 2 a_2))))) True)) % 5.11/5.28 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (Not (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a))))) True) % 5.11/5.28 (Or (Eq (Not (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1))))) True) % 5.11/5.28 (Eq (Iff (cA_and_B (skS.0 0 a_2)) (Or (cB (skS.0 0 a_2)) (cA (skS.0 0 a_2)))) False)) % 5.11/5.28 Clause #105 (by clausification #[104]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (Not (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a))))) True) % 5.11/5.28 (Or (Eq (Iff (cA_and_B (skS.0 0 a_1)) (Or (cB (skS.0 0 a_1)) (cA (skS.0 0 a_1)))) False) % 5.11/5.28 (Eq (And (cowlThing (skS.0 1 a_2)) (Not (cowlNothing (skS.0 1 a_2)))) False)) % 5.11/5.28 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (Iff (cA_and_B (skS.0 0 a)) (Or (cB (skS.0 0 a)) (cA (skS.0 0 a)))) False) % 5.11/5.28 (Or (Eq (And (cowlThing (skS.0 1 a_1)) (Not (cowlNothing (skS.0 1 a_1)))) False) % 5.11/5.28 (Eq (Iff (xsd_string (skS.0 2 a_2)) (Not (xsd_integer (skS.0 2 a_2)))) False)) % 5.11/5.28 Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a)))) False) % 5.11/5.28 (Or (Eq (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1)))) False) % 5.11/5.28 (Or (Eq (cA_and_B (skS.0 0 a_2)) False) (Eq (Or (cB (skS.0 0 a_2)) (cA (skS.0 0 a_2))) False))) % 5.11/5.28 Clause #108 (by clausification #[106]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (And (cowlThing (skS.0 1 a)) (Not (cowlNothing (skS.0 1 a)))) False) % 5.11/5.28 (Or (Eq (Iff (xsd_string (skS.0 2 a_1)) (Not (xsd_integer (skS.0 2 a_1)))) False) % 5.11/5.28 (Or (Eq (cA_and_B (skS.0 0 a_2)) True) (Eq (Or (cB (skS.0 0 a_2)) (cA (skS.0 0 a_2))) True))) % 5.11/5.28 Clause #109 (by clausification #[107]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a)))) False) % 5.11/5.28 (Or (Eq (cA_and_B (skS.0 0 a_1)) False) % 5.11/5.28 (Or (Eq (Or (cB (skS.0 0 a_1)) (cA (skS.0 0 a_1))) False) % 5.11/5.28 (Or (Eq (cowlThing (skS.0 1 a_2)) False) (Eq (Not (cowlNothing (skS.0 1 a_2))) False)))) % 5.11/5.28 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.28 (Or (Eq (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))) False) % 5.11/5.28 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.28 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.28 (Or (Eq (xsd_string (skS.0 2 a_2)) False) (Eq (Not (xsd_integer (skS.0 2 a_2))) False))))) % 5.11/5.28 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 : Iota), % 5.11/5.28 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.28 (Or (Eq (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))) False) % 5.11/5.28 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) True) (Eq (Not (xsd_integer (skS.0 2 a_2))) True))))) % 5.11/5.31 Clause #112 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) (Eq (cA (skS.0 0 a)) False))))) % 5.11/5.31 Clause #113 (by clausification #[110]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) (Eq (cB (skS.0 0 a)) False))))) % 5.11/5.31 Clause #114 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 5.11/5.31 (Or (Eq (cA (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))) % 5.11/5.31 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (cA (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 5.11/5.31 Clause #116 (by forward demodulation #[115, 59]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq True False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.11/5.31 (Or (Eq (cA (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))))) % 5.11/5.31 Clause #117 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.11/5.31 (Or (Eq (cA (skS.0 0 a)) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 5.11/5.31 Clause #120 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 5.11/5.31 (Or (Eq (cB (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))) % 5.11/5.31 Clause #121 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.31 (Or (Eq (cB (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 5.11/5.31 Clause #122 (by forward demodulation #[121, 59]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq True False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.11/5.31 (Or (Eq (cB (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))))) % 5.11/5.31 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.11/5.31 (Or (Eq (cB (skS.0 0 a)) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 5.11/5.31 Clause #124 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) (Eq (cA (skS.0 0 a)) False))))) % 5.11/5.31 Clause #125 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 5.11/5.31 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.31 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.31 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.31 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.31 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) (Eq (cB (skS.0 0 a)) False))))) % 5.11/5.31 Clause #126 (by clausification #[124]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.34 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 5.11/5.34 (Or (Eq (cA (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))) % 5.11/5.34 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.34 (Or (Eq (cA (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False))))) % 5.11/5.34 Clause #128 (by forward demodulation #[127, 59]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq True False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.11/5.34 (Or (Eq (cA (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False))))) % 5.11/5.34 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.11/5.34 (Or (Eq (cA (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False)))) % 5.11/5.34 Clause #130 (by clausification #[125]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.34 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 5.11/5.34 (Or (Eq (cB (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_1)) True))))) % 5.11/5.34 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.11/5.34 (Or (Eq (cB (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False))))) % 5.11/5.34 Clause #132 (by forward demodulation #[131, 59]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq True False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.11/5.34 (Or (Eq (cB (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False))))) % 5.11/5.34 Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.11/5.34 (Or (Eq (cB (skS.0 0 a)) False) % 5.11/5.34 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False)))) % 5.11/5.34 Clause #134 (by clausification #[108]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (Iff (xsd_string (skS.0 2 a)) (Not (xsd_integer (skS.0 2 a)))) False) % 5.11/5.34 (Or (Eq (cA_and_B (skS.0 0 a_1)) True) % 5.11/5.34 (Or (Eq (Or (cB (skS.0 0 a_1)) (cA (skS.0 0 a_1))) True) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_2)) False) (Eq (Not (cowlNothing (skS.0 1 a_2))) False)))) % 5.11/5.34 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.11/5.34 (Or (Eq (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))) True) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) False) (Eq (Not (xsd_integer (skS.0 2 a_2))) False))))) % 5.11/5.34 Clause #136 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.11/5.34 (Or (Eq (Or (cB (skS.0 0 a)) (cA (skS.0 0 a))) True) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) True) (Eq (Not (xsd_integer (skS.0 2 a_2))) True))))) % 5.11/5.34 Clause #137 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.11/5.34 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 5.11/5.34 (Or (Eq (cB (skS.0 0 a)) True) (Eq (cA (skS.0 0 a)) True)))))) % 5.11/5.34 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 5.11/5.34 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.11/5.34 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.11/5.34 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.18/5.36 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) False) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (cA (skS.0 0 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True)))))) % 5.18/5.36 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.18/5.36 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))) % 5.18/5.36 Clause #140 (by forward demodulation #[139, 59]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq True False) % 5.18/5.36 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))))) % 5.18/5.36 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))))) % 5.18/5.36 Clause #142 (by superposition #[141, 64]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.18/5.36 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))) % 5.18/5.36 Clause #143 (by clausification #[142]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.18/5.36 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 5.18/5.36 Clause #144 (by eliminate duplicate literals #[143]): ∀ (a a_1 a_2 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))) % 5.18/5.36 Clause #146 (by superposition #[144, 60]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cA (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Eq True False)))) % 5.18/5.36 Clause #147 (by clausification #[146]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (cA (skS.0 0 a)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))) % 5.18/5.36 Clause #148 (by superposition #[147, 81]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq True False) (Eq (skS.0 0 a) ia)))) % 5.18/5.36 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Eq (skS.0 0 a) ia))) % 5.18/5.36 Clause #154 (by superposition #[149, 95]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) % 5.18/5.36 (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))))) % 5.18/5.36 Clause #155 (by clausification #[154]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cB (skS.0 0 a)) True) % 5.18/5.36 (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ia) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) % 5.18/5.36 Clause #156 (by eliminate duplicate literals #[155]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (xsd_integer (skS.0 2 a_1)) True) (Or (Eq (skS.0 0 a) ia) (Eq (skS.0 0 a) ib))) % 5.18/5.36 Clause #157 (by superposition #[156, 73]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.18/5.36 (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (skS.0 0 a_1) ib) (Or (Eq True False) (Eq (skS.0 0 a_1) ib)))) % 5.18/5.36 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), % 5.18/5.36 Or (Eq (xsd_integer (skS.0 2 a)) True) (Or (Eq (skS.0 0 a_1) ia) (Or (Eq (skS.0 0 a_1) ib) (Eq (skS.0 0 a_1) ib))) % 5.18/5.36 Clause #159 (by eliminate duplicate literals #[158]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 2 a)) True) (Or (Eq (skS.0 0 a_1) ia) (Eq (skS.0 0 a_1) ib)) % 5.19/5.39 Clause #161 (by superposition #[159, 123]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (cA_and_B ib) False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.19/5.39 (Or (Eq (cB ib) False) (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))) % 5.19/5.39 Clause #167 (by clausification #[136]): ∀ (a a_1 a_2 : Iota), % 5.19/5.39 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.19/5.39 (Or (Eq (Not (cowlNothing (skS.0 1 a_1))) False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.19/5.39 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) (Or (Eq (cB (skS.0 0 a)) True) (Eq (cA (skS.0 0 a)) True)))))) % 5.19/5.39 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 : Iota), % 5.19/5.39 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.19/5.39 (Or (Eq (Not (xsd_integer (skS.0 2 a_2))) True) % 5.19/5.39 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (cA (skS.0 0 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True)))))) % 5.19/5.39 Clause #169 (by clausification #[168]): ∀ (a a_1 a_2 : Iota), % 5.19/5.39 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlThing (skS.0 1 a_1)) False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) True) % 5.19/5.39 (Or (Eq (cB (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cA (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) False)))))) % 5.19/5.39 Clause #170 (by forward demodulation #[169, 59]): ∀ (a a_1 a_2 : Iota), % 5.19/5.39 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq True False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.19/5.39 (Or (Eq (cB (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cA (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False)))))) % 5.19/5.39 Clause #171 (by clausification #[170]): ∀ (a a_1 a_2 : Iota), % 5.19/5.39 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.19/5.39 (Or (Eq (cB (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cA (skS.0 0 a)) True) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) False))))) % 5.19/5.39 Clause #188 (by forward demodulation #[161, 92]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq True False) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.19/5.39 (Or (Eq (cB ib) False) (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))))) % 5.19/5.39 Clause #189 (by clausification #[188]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.19/5.39 (Or (Eq (cB ib) False) (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 5.19/5.39 Clause #190 (by forward demodulation #[189, 72]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.19/5.39 (Or (Eq True False) (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))))) % 5.19/5.39 Clause #191 (by clausification #[190]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (xsd_string (skS.0 2 a_2)) False) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_3)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)))) % 5.19/5.39 Clause #192 (by superposition #[191, 64]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 5.19/5.39 (Or (Eq (xsd_integer (skS.0 2 a_3)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_3)) True))))) % 5.19/5.39 Clause #193 (by clausification #[192]): ∀ (a a_1 a_2 a_3 : Iota), % 5.19/5.39 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.19/5.39 (Or (Eq (skS.0 0 a_1) ia) % 5.19/5.39 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) % 5.19/5.39 (Or (Eq (xsd_integer (skS.0 2 a_3)) True) (Eq (xsd_integer (skS.0 2 a_3)) True)))) % 5.19/5.39 Clause #194 (by eliminate duplicate literals #[193]): ∀ (a a_1 a_2 a_3 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (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))) % 5.24/5.41 Clause #205 (by equality factoring #[194]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (skS.0 0 a) ia) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 2 a_2)) True))) % 5.24/5.41 Clause #206 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (skS.0 0 a) ia) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.24/5.41 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq True False) (Eq True False)))) % 5.24/5.41 Clause #208 (by clausification #[206]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (skS.0 0 a) ia) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq True False))) % 5.24/5.41 Clause #209 (by clausification #[208]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 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)) % 5.24/5.41 Clause #215 (by superposition #[209, 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)) % 5.24/5.41 Clause #217 (by clausification #[215]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) True) % 5.24/5.41 Clause #218 (by superposition #[217, 117]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (cA_and_B ia) False) % 5.24/5.41 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.24/5.41 (Or (Eq (cA ia) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))))) % 5.24/5.41 Clause #238 (by forward demodulation #[218, 90]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq True False) % 5.24/5.41 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.24/5.41 (Or (Eq (cA ia) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))))) % 5.24/5.41 Clause #239 (by clausification #[238]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.24/5.41 (Or (Eq (cA ia) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 5.24/5.41 Clause #240 (by forward demodulation #[239, 80]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.24/5.41 (Or (Eq True False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True)))) % 5.24/5.41 Clause #241 (by clausification #[240]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (xsd_string (skS.0 2 a_1)) False) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq (xsd_integer (skS.0 2 a_1)) True))) % 5.24/5.41 Clause #242 (by superposition #[241, 64]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.24/5.41 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 2 a_2)) True)))) % 5.24/5.41 Clause #243 (by clausification #[242]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.24/5.41 (Or (Eq (xsd_integer (skS.0 2 a_2)) True) (Eq (xsd_integer (skS.0 2 a_2)) True))) % 5.24/5.41 Clause #244 (by eliminate duplicate literals #[243]): ∀ (a a_1 a_2 : Iota), % 5.24/5.41 Or (Eq (xsd_integer (skS.0 2 a)) True) % 5.24/5.41 (Or (Eq (cowlNothing (skS.0 1 a_1)) True) (Eq (xsd_integer (skS.0 2 a_2)) True)) % 5.24/5.41 Clause #250 (by equality factoring #[244]): ∀ (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)) % 5.24/5.41 Clause #251 (by clausification #[250]): ∀ (a a_1 : Iota), % 5.24/5.41 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))) % 5.24/5.41 Clause #253 (by clausification #[251]): ∀ (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)) % 5.24/5.41 Clause #254 (by clausification #[253]): ∀ (a a_1 : Iota), Or (Eq (cowlNothing (skS.0 1 a)) True) (Eq (xsd_integer (skS.0 2 a_1)) True) % 5.24/5.41 Clause #255 (by superposition #[254, 60]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 2 a)) True) (Eq True False) % 5.24/5.45 Clause #258 (by clausification #[255]): ∀ (a : Iota), Eq (xsd_integer (skS.0 2 a)) True % 5.24/5.45 Clause #259 (by backward demodulation #[258, 129]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.24/5.45 (Or (Eq (cA (skS.0 0 a)) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq True False)))) % 5.24/5.45 Clause #260 (by backward demodulation #[258, 133]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) False) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq True False)))) % 5.24/5.45 Clause #261 (by backward demodulation #[258, 171]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (cA (skS.0 0 a)) True) (Or (Eq (cowlNothing (skS.0 1 a_2)) True) (Eq True False))))) % 5.24/5.45 Clause #263 (by clausification #[260]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.24/5.45 Clause #264 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) False) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cA (skS.0 0 a)) False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.24/5.45 Clause #274 (by clausification #[261]): ∀ (a a_1 a_2 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (cA (skS.0 0 a)) True) (Eq (cowlNothing (skS.0 1 a_2)) True)))) % 5.24/5.45 Clause #277 (by superposition #[274, 60]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (cA (skS.0 0 a)) True) (Eq True False)))) % 5.24/5.45 Clause #279 (by clausification #[277]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB (skS.0 0 a)) True) (Eq (cA (skS.0 0 a)) True))) % 5.24/5.45 Clause #281 (by superposition #[279, 81]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq True False) (Eq (skS.0 0 a) ia)))) % 5.24/5.45 Clause #282 (by clausification #[281]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB (skS.0 0 a)) True) (Eq (skS.0 0 a) ia))) % 5.24/5.45 Clause #286 (by superposition #[282, 65]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Eq (xsd_integer (skS.0 2 a_1)) False)))) % 5.24/5.45 Clause #287 (by clausification #[286]): ∀ (a a_1 : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) False))) % 5.24/5.45 Clause #288 (by superposition #[287, 258]): ∀ (a : Iota), % 5.24/5.45 Or (Eq (cA_and_B (skS.0 0 a)) True) (Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ia) (Eq False True))) % 5.24/5.45 Clause #289 (by clausification #[288]): ∀ (a : Iota), Or (Eq (cA_and_B (skS.0 0 a)) True) (Or (Eq (cB (skS.0 0 a)) True) (Eq (skS.0 0 a) ia)) % 5.24/5.45 Clause #292 (by superposition #[289, 95]): ∀ (a : Iota), % 5.24/5.45 Or (Eq (cB (skS.0 0 a)) True) % 5.24/5.45 (Or (Eq (skS.0 0 a) ia) (Or (Eq True False) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia)))) % 5.24/5.45 Clause #293 (by clausification #[292]): ∀ (a : Iota), Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ia) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ia))) % 5.24/5.45 Clause #294 (by eliminate duplicate literals #[293]): ∀ (a : Iota), Or (Eq (cB (skS.0 0 a)) True) (Or (Eq (skS.0 0 a) ia) (Eq (skS.0 0 a) ib)) % 5.24/5.45 Clause #295 (by superposition #[294, 73]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ia) (Or (Eq (skS.0 0 a) ib) (Or (Eq True False) (Eq (skS.0 0 a) ib))) % 5.24/5.45 Clause #297 (by clausification #[295]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ia) (Or (Eq (skS.0 0 a) ib) (Eq (skS.0 0 a) ib)) % 5.24/5.45 Clause #298 (by eliminate duplicate literals #[297]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ia) (Eq (skS.0 0 a) ib) % 5.24/5.45 Clause #299 (by superposition #[298, 263]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (skS.0 0 a) ia) % 5.28/5.47 (Or (Eq (cA_and_B ib) False) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB ib) False) (Eq (cowlNothing (skS.0 1 a_2)) True)))) % 5.28/5.47 Clause #309 (by forward demodulation #[299, 92]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (skS.0 0 a) ia) % 5.28/5.47 (Or (Eq True False) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB ib) False) (Eq (cowlNothing (skS.0 1 a_2)) True)))) % 5.28/5.47 Clause #310 (by clausification #[309]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (skS.0 0 a) ia) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq (cB ib) False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.28/5.47 Clause #311 (by forward demodulation #[310, 72]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (skS.0 0 a) ia) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a_1)) True) (Or (Eq True False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.28/5.47 Clause #312 (by clausification #[311]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 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)) % 5.28/5.47 Clause #317 (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)) % 5.28/5.47 Clause #318 (by clausification #[317]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_string (skS.0 2 a_1)) True) % 5.28/5.47 Clause #322 (by superposition #[318, 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)) % 5.28/5.47 Clause #323 (by clausification #[322]): ∀ (a a_1 : Iota), Or (Eq (skS.0 0 a) ia) (Eq (xsd_integer (skS.0 2 a_1)) False) % 5.28/5.47 Clause #324 (by superposition #[323, 258]): ∀ (a : Iota), Or (Eq (skS.0 0 a) ia) (Eq False True) % 5.28/5.47 Clause #325 (by clausification #[324]): ∀ (a : Iota), Eq (skS.0 0 a) ia % 5.28/5.47 Clause #327 (by backward demodulation #[325, 264]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (cA_and_B ia) False) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a)) True) (Or (Eq (cA (skS.0 0 a_1)) False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.28/5.47 Clause #344 (by forward demodulation #[327, 90]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq True False) % 5.28/5.47 (Or (Eq (xsd_string (skS.0 2 a)) True) (Or (Eq (cA (skS.0 0 a_1)) False) (Eq (cowlNothing (skS.0 1 a_2)) True))) % 5.28/5.47 Clause #345 (by clausification #[344]): ∀ (a a_1 a_2 : Iota), % 5.28/5.47 Or (Eq (xsd_string (skS.0 2 a)) True) (Or (Eq (cA (skS.0 0 a_1)) False) (Eq (cowlNothing (skS.0 1 a_2)) True)) % 5.28/5.47 Clause #346 (by forward demodulation #[345, 325]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Or (Eq (cA ia) False) (Eq (cowlNothing (skS.0 1 a_1)) True)) % 5.28/5.47 Clause #347 (by forward demodulation #[346, 80]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Or (Eq True False) (Eq (cowlNothing (skS.0 1 a_1)) True)) % 5.28/5.47 Clause #348 (by clausification #[347]): ∀ (a a_1 : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Eq (cowlNothing (skS.0 1 a_1)) True) % 5.28/5.47 Clause #350 (by superposition #[348, 60]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 2 a)) True) (Eq True False) % 5.28/5.47 Clause #351 (by clausification #[350]): ∀ (a : Iota), Eq (xsd_string (skS.0 2 a)) True % 5.28/5.47 Clause #352 (by superposition #[351, 65]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 2 a)) False) % 5.28/5.47 Clause #353 (by clausification #[352]): ∀ (a : Iota), Eq (xsd_integer (skS.0 2 a)) False % 5.28/5.47 Clause #354 (by superposition #[353, 258]): Eq False True % 5.28/5.47 Clause #355 (by clausification #[354]): False % 5.28/5.47 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------