%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS167+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 8.12s 8.38s % Output : Proof 8.62s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : KRS167+1 : TPTP v9.2.0. Released v3.1.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n002.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Oct 2 10:21:53 EDT 2025 % 0.12/0.34 % CPUTime : % 8.12/8.38 SZS status Theorem for theBenchmark.p % 8.12/8.38 SZS output start Proof for theBenchmark.p % 8.12/8.38 Clause #8 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 8.12/8.38 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 8.12/8.38 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), Iff (cc1 X) (And (Exists fun Y0 => rp X Y0) (∀ (Y0 Y1 : Iota), And (rp X Y0) (rp X Y1) → Eq Y0 Y1))) % 8.12/8.38 True % 8.12/8.38 Clause #11 (by assumption #[]): Eq (∀ (X : Iota), Iff (cc2 X) (And (Exists fun Y0 => rp X Y0) (∀ (Y0 Y1 : Iota), And (rp X Y0) (rp X Y1) → Eq Y0 Y1))) % 8.12/8.38 True % 8.12/8.38 Clause #12 (by assumption #[]): Eq % 8.12/8.38 (Not % 8.12/8.38 (And % 8.12/8.38 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.12/8.38 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.12/8.38 (∀ (X : Iota), Iff (cc1 X) (cc2 X)))) % 8.12/8.38 True % 8.12/8.38 Clause #62 (by clausification #[9]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 8.12/8.38 Clause #63 (by clausification #[62]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 8.12/8.38 Clause #64 (by clausification #[62]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 8.12/8.38 Clause #65 (by clausification #[63]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 8.12/8.38 Clause #66 (by clausification #[64]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 8.12/8.38 Clause #67 (by clausification #[8]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 8.12/8.38 Clause #68 (by clausification #[67]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 8.12/8.38 Clause #69 (by clausification #[67]): ∀ (a : Iota), Eq (cowlThing a) True % 8.12/8.38 Clause #70 (by clausification #[68]): ∀ (a : Iota), Eq (cowlNothing a) False % 8.12/8.38 Clause #71 (by betaEtaReduce #[10]): Eq (∀ (X : Iota), Iff (cc1 X) (And (Exists (rp X)) (∀ (Y0 Y1 : Iota), And (rp X Y0) (rp X Y1) → Eq Y0 Y1))) True % 8.12/8.38 Clause #72 (by clausification #[71]): ∀ (a : Iota), Eq (Iff (cc1 a) (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1))) True % 8.12/8.38 Clause #73 (by clausification #[72]): ∀ (a : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) (Eq (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1)) False) % 8.12/8.38 Clause #74 (by clausification #[72]): ∀ (a : Iota), % 8.12/8.38 Or (Eq (cc1 a) False) (Eq (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1)) True) % 8.12/8.38 Clause #75 (by clausification #[73]): ∀ (a : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) (Or (Eq (Exists (rp a)) False) (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) False)) % 8.12/8.38 Clause #76 (by clausification #[75]): ∀ (a a_1 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) (Or (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) False) (Eq (rp a a_1) False)) % 8.12/8.38 Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) % 8.12/8.38 (Or (Eq (rp a a_1) False) % 8.12/8.38 (Eq (Not (∀ (Y1 : Iota), And (rp a (skS.0 0 a a_2)) (rp a Y1) → Eq (skS.0 0 a a_2) Y1)) True)) % 8.12/8.38 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) % 8.12/8.38 (Or (Eq (rp a a_1) False) (Eq (∀ (Y1 : Iota), And (rp a (skS.0 0 a a_2)) (rp a Y1) → Eq (skS.0 0 a a_2) Y1) False)) % 8.12/8.38 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) % 8.12/8.38 (Or (Eq (rp a a_1) False) % 8.12/8.38 (Eq (Not (And (rp a (skS.0 0 a a_2)) (rp a (skS.0 1 a a_2 a_3)) → Eq (skS.0 0 a a_2) (skS.0 1 a a_2 a_3))) True)) % 8.12/8.38 Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) % 8.12/8.38 (Or (Eq (rp a a_1) False) % 8.12/8.38 (Eq (And (rp a (skS.0 0 a a_2)) (rp a (skS.0 1 a a_2 a_3)) → Eq (skS.0 0 a a_2) (skS.0 1 a a_2 a_3)) False)) % 8.12/8.38 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) (Or (Eq (rp a a_1) False) (Eq (And (rp a (skS.0 0 a a_2)) (rp a (skS.0 1 a a_2 a_3))) True)) % 8.12/8.38 Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 a_3 : Iota), % 8.12/8.38 Or (Eq (cc1 a) True) (Or (Eq (rp a a_1) False) (Eq (Eq (skS.0 0 a a_2) (skS.0 1 a a_2 a_3)) False)) % 8.12/8.38 Clause #83 (by clausification #[81]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc1 a) True) (Or (Eq (rp a a_1) False) (Eq (rp a (skS.0 1 a a_2 a_3)) True)) % 8.23/8.45 Clause #84 (by clausification #[81]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 a) True) (Or (Eq (rp a a_1) False) (Eq (rp a (skS.0 0 a a_2)) True)) % 8.23/8.45 Clause #85 (by clausification #[74]): ∀ (a : Iota), Or (Eq (cc1 a) False) (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) True) % 8.23/8.45 Clause #86 (by clausification #[74]): ∀ (a : Iota), Or (Eq (cc1 a) False) (Eq (Exists (rp a)) True) % 8.23/8.45 Clause #87 (by clausification #[85]): ∀ (a a_1 : Iota), Or (Eq (cc1 a) False) (Eq (∀ (Y1 : Iota), And (rp a a_1) (rp a Y1) → Eq a_1 Y1) True) % 8.23/8.45 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 a) False) (Eq (And (rp a a_1) (rp a a_2) → Eq a_1 a_2) True) % 8.23/8.45 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 a) False) (Or (Eq (And (rp a a_1) (rp a a_2)) False) (Eq (Eq a_1 a_2) True)) % 8.23/8.45 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 a) False) (Or (Eq (Eq a_1 a_2) True) (Or (Eq (rp a a_1) False) (Eq (rp a a_2) False))) % 8.23/8.45 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 a) False) (Or (Eq (rp a a_1) False) (Or (Eq (rp a a_2) False) (Eq a_1 a_2))) % 8.23/8.45 Clause #92 (by clausification #[86]): ∀ (a a_1 : Iota), Or (Eq (cc1 a) False) (Eq (rp a (skS.0 2 a a_1)) True) % 8.23/8.45 Clause #93 (by betaEtaReduce #[11]): Eq (∀ (X : Iota), Iff (cc2 X) (And (Exists (rp X)) (∀ (Y0 Y1 : Iota), And (rp X Y0) (rp X Y1) → Eq Y0 Y1))) True % 8.23/8.45 Clause #94 (by clausification #[93]): ∀ (a : Iota), Eq (Iff (cc2 a) (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1))) True % 8.23/8.45 Clause #95 (by clausification #[94]): ∀ (a : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) (Eq (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1)) False) % 8.23/8.45 Clause #96 (by clausification #[94]): ∀ (a : Iota), % 8.23/8.45 Or (Eq (cc2 a) False) (Eq (And (Exists (rp a)) (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1)) True) % 8.23/8.45 Clause #97 (by clausification #[95]): ∀ (a : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) (Or (Eq (Exists (rp a)) False) (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) False)) % 8.23/8.45 Clause #98 (by clausification #[97]): ∀ (a a_1 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) (Or (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) False) (Eq (rp a a_1) False)) % 8.23/8.45 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) % 8.23/8.45 (Or (Eq (rp a a_1) False) % 8.23/8.45 (Eq (Not (∀ (Y1 : Iota), And (rp a (skS.0 3 a a_2)) (rp a Y1) → Eq (skS.0 3 a a_2) Y1)) True)) % 8.23/8.45 Clause #100 (by clausification #[99]): ∀ (a a_1 a_2 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) % 8.23/8.45 (Or (Eq (rp a a_1) False) (Eq (∀ (Y1 : Iota), And (rp a (skS.0 3 a a_2)) (rp a Y1) → Eq (skS.0 3 a a_2) Y1) False)) % 8.23/8.45 Clause #101 (by clausification #[100]): ∀ (a a_1 a_2 a_3 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) % 8.23/8.45 (Or (Eq (rp a a_1) False) % 8.23/8.45 (Eq (Not (And (rp a (skS.0 3 a a_2)) (rp a (skS.0 4 a a_2 a_3)) → Eq (skS.0 3 a a_2) (skS.0 4 a a_2 a_3))) True)) % 8.23/8.45 Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 a_3 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) % 8.23/8.45 (Or (Eq (rp a a_1) False) % 8.23/8.45 (Eq (And (rp a (skS.0 3 a a_2)) (rp a (skS.0 4 a a_2 a_3)) → Eq (skS.0 3 a a_2) (skS.0 4 a a_2 a_3)) False)) % 8.23/8.45 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) (Or (Eq (rp a a_1) False) (Eq (And (rp a (skS.0 3 a a_2)) (rp a (skS.0 4 a a_2 a_3))) True)) % 8.23/8.45 Clause #104 (by clausification #[102]): ∀ (a a_1 a_2 a_3 : Iota), % 8.23/8.45 Or (Eq (cc2 a) True) (Or (Eq (rp a a_1) False) (Eq (Eq (skS.0 3 a a_2) (skS.0 4 a a_2 a_3)) False)) % 8.23/8.45 Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc2 a) True) (Or (Eq (rp a a_1) False) (Eq (rp a (skS.0 4 a a_2 a_3)) True)) % 8.23/8.45 Clause #106 (by clausification #[103]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 a) True) (Or (Eq (rp a a_1) False) (Eq (rp a (skS.0 3 a a_2)) True)) % 8.23/8.45 Clause #107 (by clausification #[12]): Eq % 8.23/8.45 (And % 8.23/8.45 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.23/8.45 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.23/8.45 (∀ (X : Iota), Iff (cc1 X) (cc2 X))) % 8.32/8.51 False % 8.32/8.51 Clause #108 (by clausification #[107]): Or % 8.32/8.51 (Eq % 8.32/8.51 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 8.32/8.51 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 8.32/8.51 False) % 8.32/8.51 (Eq (∀ (X : Iota), Iff (cc1 X) (cc2 X)) False) % 8.32/8.51 Clause #109 (by clausification #[108]): Or (Eq (∀ (X : Iota), Iff (cc1 X) (cc2 X)) False) % 8.32/8.51 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 8.32/8.51 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False)) % 8.32/8.51 Clause #110 (by clausification #[109]): ∀ (a : Iota), % 8.32/8.51 Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 8.32/8.51 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 8.32/8.51 (Eq (Not (Iff (cc1 (skS.0 5 a)) (cc2 (skS.0 5 a)))) True)) % 8.32/8.51 Clause #111 (by clausification #[110]): ∀ (a a_1 : Iota), % 8.32/8.51 Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 8.32/8.51 (Or (Eq (Not (Iff (cc1 (skS.0 5 a)) (cc2 (skS.0 5 a)))) True) % 8.32/8.51 (Eq (Not (And (cowlThing (skS.0 6 a_1)) (Not (cowlNothing (skS.0 6 a_1))))) True)) % 8.32/8.51 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (Not (Iff (cc1 (skS.0 5 a)) (cc2 (skS.0 5 a)))) True) % 8.32/8.51 (Or (Eq (Not (And (cowlThing (skS.0 6 a_1)) (Not (cowlNothing (skS.0 6 a_1))))) True) % 8.32/8.51 (Eq (Not (Iff (xsd_string (skS.0 7 a_2)) (Not (xsd_integer (skS.0 7 a_2))))) True)) % 8.32/8.51 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (Not (And (cowlThing (skS.0 6 a)) (Not (cowlNothing (skS.0 6 a))))) True) % 8.32/8.51 (Or (Eq (Not (Iff (xsd_string (skS.0 7 a_1)) (Not (xsd_integer (skS.0 7 a_1))))) True) % 8.32/8.51 (Eq (Iff (cc1 (skS.0 5 a_2)) (cc2 (skS.0 5 a_2))) False)) % 8.32/8.51 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (Not (Iff (xsd_string (skS.0 7 a)) (Not (xsd_integer (skS.0 7 a))))) True) % 8.32/8.51 (Or (Eq (Iff (cc1 (skS.0 5 a_1)) (cc2 (skS.0 5 a_1))) False) % 8.32/8.51 (Eq (And (cowlThing (skS.0 6 a_2)) (Not (cowlNothing (skS.0 6 a_2)))) False)) % 8.32/8.51 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (Iff (cc1 (skS.0 5 a)) (cc2 (skS.0 5 a))) False) % 8.32/8.51 (Or (Eq (And (cowlThing (skS.0 6 a_1)) (Not (cowlNothing (skS.0 6 a_1)))) False) % 8.32/8.51 (Eq (Iff (xsd_string (skS.0 7 a_2)) (Not (xsd_integer (skS.0 7 a_2)))) False)) % 8.32/8.51 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (And (cowlThing (skS.0 6 a)) (Not (cowlNothing (skS.0 6 a)))) False) % 8.32/8.51 (Or (Eq (Iff (xsd_string (skS.0 7 a_1)) (Not (xsd_integer (skS.0 7 a_1)))) False) % 8.32/8.51 (Or (Eq (cc1 (skS.0 5 a_2)) False) (Eq (cc2 (skS.0 5 a_2)) False))) % 8.32/8.51 Clause #117 (by clausification #[115]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (And (cowlThing (skS.0 6 a)) (Not (cowlNothing (skS.0 6 a)))) False) % 8.32/8.51 (Or (Eq (Iff (xsd_string (skS.0 7 a_1)) (Not (xsd_integer (skS.0 7 a_1)))) False) % 8.32/8.51 (Or (Eq (cc1 (skS.0 5 a_2)) True) (Eq (cc2 (skS.0 5 a_2)) True))) % 8.32/8.51 Clause #118 (by clausification #[116]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (Iff (xsd_string (skS.0 7 a)) (Not (xsd_integer (skS.0 7 a)))) False) % 8.32/8.51 (Or (Eq (cc1 (skS.0 5 a_1)) False) % 8.32/8.51 (Or (Eq (cc2 (skS.0 5 a_1)) False) % 8.32/8.51 (Or (Eq (cowlThing (skS.0 6 a_2)) False) (Eq (Not (cowlNothing (skS.0 6 a_2))) False)))) % 8.32/8.51 Clause #119 (by clausification #[118]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.51 (Or (Eq (Not (cowlNothing (skS.0 6 a_1))) False) % 8.32/8.51 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (Not (xsd_integer (skS.0 7 a_2))) False))))) % 8.32/8.51 Clause #120 (by clausification #[118]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.51 (Or (Eq (Not (cowlNothing (skS.0 6 a_1))) False) % 8.32/8.51 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (Not (xsd_integer (skS.0 7 a_2))) True))))) % 8.32/8.51 Clause #121 (by clausification #[119]): ∀ (a a_1 a_2 : Iota), % 8.32/8.51 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.51 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.51 (Or (Eq (xsd_string (skS.0 7 a_2)) False) % 8.32/8.51 (Or (Eq (Not (xsd_integer (skS.0 7 a_2))) False) (Eq (cowlNothing (skS.0 6 a_1)) True))))) % 8.32/8.58 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) % 8.32/8.58 (Or (Eq (cowlNothing (skS.0 6 a_1)) True) (Eq (xsd_integer (skS.0 7 a_2)) True))))) % 8.32/8.58 Clause #123 (by forward demodulation #[122, 70]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 7 a_2)) True))))) % 8.32/8.58 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (xsd_integer (skS.0 7 a_2)) True)))) % 8.32/8.58 Clause #125 (by clausification #[96]): ∀ (a : Iota), Or (Eq (cc2 a) False) (Eq (∀ (Y0 Y1 : Iota), And (rp a Y0) (rp a Y1) → Eq Y0 Y1) True) % 8.32/8.58 Clause #126 (by clausification #[96]): ∀ (a : Iota), Or (Eq (cc2 a) False) (Eq (Exists (rp a)) True) % 8.32/8.58 Clause #127 (by clausification #[125]): ∀ (a a_1 : Iota), Or (Eq (cc2 a) False) (Eq (∀ (Y1 : Iota), And (rp a a_1) (rp a Y1) → Eq a_1 Y1) True) % 8.32/8.58 Clause #128 (by clausification #[127]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 a) False) (Eq (And (rp a a_1) (rp a a_2) → Eq a_1 a_2) True) % 8.32/8.58 Clause #129 (by clausification #[128]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 a) False) (Or (Eq (And (rp a a_1) (rp a a_2)) False) (Eq (Eq a_1 a_2) True)) % 8.32/8.58 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 a) False) (Or (Eq (Eq a_1 a_2) True) (Or (Eq (rp a a_1) False) (Eq (rp a a_2) False))) % 8.32/8.58 Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 a) False) (Or (Eq (rp a a_1) False) (Or (Eq (rp a a_2) False) (Eq a_1 a_2))) % 8.32/8.58 Clause #132 (by clausification #[126]): ∀ (a a_1 : Iota), Or (Eq (cc2 a) False) (Eq (rp a (skS.0 8 a a_1)) True) % 8.32/8.58 Clause #133 (by clausification #[104]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc2 a) True) (Or (Eq (rp a a_1) False) (Ne (skS.0 3 a a_2) (skS.0 4 a a_2 a_3))) % 8.32/8.58 Clause #134 (by clausification #[82]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc1 a) True) (Or (Eq (rp a a_1) False) (Ne (skS.0 0 a a_2) (skS.0 1 a a_2 a_3))) % 8.32/8.58 Clause #135 (by clausification #[117]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (Iff (xsd_string (skS.0 7 a)) (Not (xsd_integer (skS.0 7 a)))) False) % 8.32/8.58 (Or (Eq (cc1 (skS.0 5 a_1)) True) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a_1)) True) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_2)) False) (Eq (Not (cowlNothing (skS.0 6 a_2))) False)))) % 8.32/8.58 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (Not (cowlNothing (skS.0 6 a_1))) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (Not (xsd_integer (skS.0 7 a_2))) False))))) % 8.32/8.58 Clause #137 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (Not (cowlNothing (skS.0 6 a_1))) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (Not (xsd_integer (skS.0 7 a_2))) True))))) % 8.32/8.58 Clause #138 (by clausification #[136]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) % 8.32/8.58 (Or (Eq (Not (xsd_integer (skS.0 7 a_2))) False) (Eq (cowlNothing (skS.0 6 a_1)) True))))) % 8.32/8.58 Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), % 8.32/8.58 Or (Eq (cc1 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.32/8.58 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.32/8.58 (Or (Eq (xsd_string (skS.0 7 a_2)) False) % 8.32/8.58 (Or (Eq (cowlNothing (skS.0 6 a_1)) True) (Eq (xsd_integer (skS.0 7 a_2)) True))))) % 8.32/8.58 Clause #140 (by forward demodulation #[139, 70]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Or (Eq False True) (Eq (xsd_integer (skS.0 7 a_2)) True))))) % 8.41/8.64 Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (xsd_integer (skS.0 7 a_2)) True)))) % 8.41/8.64 Clause #142 (by superposition #[141, 69]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_1)) False) (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Eq False True)))) % 8.41/8.64 Clause #143 (by clausification #[142]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq (xsd_string (skS.0 7 a_1)) False) (Eq (xsd_integer (skS.0 7 a_1)) True))) % 8.41/8.64 Clause #144 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) True) % 8.41/8.64 (Or (Eq (Not (xsd_integer (skS.0 7 a_2))) True) (Eq (cowlNothing (skS.0 6 a_1)) True))))) % 8.41/8.64 Clause #145 (by clausification #[144]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) True) % 8.41/8.64 (Or (Eq (cowlNothing (skS.0 6 a_1)) True) (Eq (xsd_integer (skS.0 7 a_2)) False))))) % 8.41/8.64 Clause #146 (by forward demodulation #[145, 70]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 7 a_2)) False))))) % 8.41/8.64 Clause #147 (by clausification #[146]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (xsd_integer (skS.0 7 a_2)) False)))) % 8.41/8.64 Clause #148 (by superposition #[147, 69]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Or (Eq (xsd_integer (skS.0 7 a_1)) False) (Eq False True)))) % 8.41/8.64 Clause #149 (by clausification #[148]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Eq (xsd_integer (skS.0 7 a_1)) False))) % 8.41/8.64 Clause #150 (by superposition #[149, 65]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Eq False True)))) % 8.41/8.64 Clause #151 (by clausification #[150]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Eq (xsd_string (skS.0 7 a_1)) True))) % 8.41/8.64 Clause #152 (by eliminate duplicate literals #[151]): ∀ (a a_1 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Eq (xsd_string (skS.0 7 a_1)) True)) % 8.41/8.64 Clause #155 (by superposition #[152, 143]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc1 (skS.0 5 a_1)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a_1)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 7 a_2)) True))))) % 8.41/8.64 Clause #156 (by superposition #[152, 66]): ∀ (a a_1 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) True) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 7 a_1)) False))) % 8.41/8.64 Clause #157 (by clausification #[156]): ∀ (a a_1 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Eq (xsd_integer (skS.0 7 a_1)) False)) % 8.41/8.64 Clause #159 (by clausification #[120]): ∀ (a a_1 a_2 : Iota), % 8.41/8.64 Or (Eq (cc1 (skS.0 5 a)) False) % 8.41/8.64 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.41/8.64 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.51/8.70 (Or (Eq (xsd_string (skS.0 7 a_2)) True) % 8.51/8.70 (Or (Eq (Not (xsd_integer (skS.0 7 a_2))) True) (Eq (cowlNothing (skS.0 6 a_1)) True))))) % 8.51/8.70 Clause #160 (by clausification #[159]): ∀ (a a_1 a_2 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.51/8.70 (Or (Eq (xsd_string (skS.0 7 a_2)) True) % 8.51/8.70 (Or (Eq (cowlNothing (skS.0 6 a_1)) True) (Eq (xsd_integer (skS.0 7 a_2)) False))))) % 8.51/8.70 Clause #161 (by forward demodulation #[160, 70]): ∀ (a a_1 a_2 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.51/8.70 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Or (Eq False True) (Eq (xsd_integer (skS.0 7 a_2)) False))))) % 8.51/8.70 Clause #162 (by clausification #[161]): ∀ (a a_1 a_2 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.51/8.70 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.51/8.70 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (xsd_integer (skS.0 7 a_2)) False)))) % 8.51/8.70 Clause #177 (by clausification #[155]): ∀ (a a_1 a_2 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a_1)) True) (Or (Eq (cc2 (skS.0 5 a_1)) True) (Eq (xsd_integer (skS.0 7 a_2)) True)))) % 8.51/8.70 Clause #184 (by equality factoring #[177]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Or (Ne True True) (Eq (cc2 (skS.0 5 a)) True)))) % 8.51/8.70 Clause #185 (by clausification #[184]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Eq True False))))) % 8.51/8.70 Clause #187 (by clausification #[185]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Eq True False)))) % 8.51/8.70 Clause #188 (by clausification #[187]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Eq (cc2 (skS.0 5 a)) True))) % 8.51/8.70 Clause #189 (by eliminate duplicate literals #[188]): ∀ (a a_1 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (xsd_integer (skS.0 7 a_1)) True) (Eq (cc2 (skS.0 5 a)) True)) % 8.51/8.70 Clause #190 (by superposition #[189, 157]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a_1)) True) (Or (Eq (cc2 (skS.0 5 a_1)) True) (Eq True False)))) % 8.51/8.70 Clause #194 (by clausification #[190]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq (cc1 (skS.0 5 a_1)) True) (Eq (cc2 (skS.0 5 a_1)) True))) % 8.51/8.70 Clause #199 (by equality factoring #[194]): ∀ (a : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Ne True True) (Eq (cc2 (skS.0 5 a)) True))) % 8.51/8.70 Clause #200 (by clausification #[199]): ∀ (a : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Eq True False)))) % 8.51/8.70 Clause #202 (by clausification #[200]): ∀ (a : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc2 (skS.0 5 a)) True) (Eq True False))) % 8.51/8.70 Clause #203 (by clausification #[202]): ∀ (a : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc1 (skS.0 5 a)) True) (Eq (cc2 (skS.0 5 a)) True)) % 8.51/8.70 Clause #204 (by eliminate duplicate literals #[203]): ∀ (a : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Eq (cc2 (skS.0 5 a)) True) % 8.51/8.70 Clause #205 (by superposition #[204, 131]): ∀ (a a_1 a_2 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) % 8.51/8.70 (Or (Eq True False) (Or (Eq (rp (skS.0 5 a) a_1) False) (Or (Eq (rp (skS.0 5 a) a_2) False) (Eq a_1 a_2)))) % 8.51/8.70 Clause #206 (by superposition #[204, 132]): ∀ (a a_1 : Iota), % 8.51/8.70 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 8 (skS.0 5 a) a_1)) True)) % 8.51/8.70 Clause #207 (by clausification #[205]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (rp (skS.0 5 a) a_1) False) (Or (Eq (rp (skS.0 5 a) a_2) False) (Eq a_1 a_2))) % 8.53/8.76 Clause #211 (by clausification #[206]): ∀ (a a_1 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 8 (skS.0 5 a) a_1)) True) % 8.53/8.76 Clause #213 (by superposition #[211, 83]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 1 (skS.0 5 a) a_1 a_2)) True))) % 8.53/8.76 Clause #214 (by superposition #[211, 84]): ∀ (a a_1 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 0 (skS.0 5 a) a_1)) True))) % 8.53/8.76 Clause #218 (by superposition #[211, 134]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq True False) (Ne (skS.0 0 (skS.0 5 a) a_1) (skS.0 1 (skS.0 5 a) a_1 a_2)))) % 8.53/8.76 Clause #225 (by clausification #[214]): ∀ (a a_1 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (cc1 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 0 (skS.0 5 a) a_1)) True)) % 8.53/8.76 Clause #226 (by eliminate duplicate literals #[225]): ∀ (a a_1 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 0 (skS.0 5 a) a_1)) True) % 8.53/8.76 Clause #230 (by clausification #[213]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 1 (skS.0 5 a) a_1 a_2)) True)) % 8.53/8.76 Clause #231 (by eliminate duplicate literals #[230]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 1 (skS.0 5 a) a_1 a_2)) True) % 8.53/8.76 Clause #232 (by superposition #[231, 207]): ∀ (a a_1 a_2 a_3 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq True False) (Or (Eq (rp (skS.0 5 a) a_1) False) (Eq (skS.0 1 (skS.0 5 a) a_2 a_3) a_1)))) % 8.53/8.76 Clause #246 (by clausification #[232]): ∀ (a a_1 a_2 a_3 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (rp (skS.0 5 a) a_1) False) (Eq (skS.0 1 (skS.0 5 a) a_2 a_3) a_1))) % 8.53/8.76 Clause #247 (by eliminate duplicate literals #[246]): ∀ (a a_1 a_2 a_3 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) (Or (Eq (rp (skS.0 5 a) a_1) False) (Eq (skS.0 1 (skS.0 5 a) a_2 a_3) a_1)) % 8.53/8.76 Clause #249 (by superposition #[247, 226]): ∀ (a a_1 a_2 a_3 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (skS.0 1 (skS.0 5 a) a_1 a_2) (skS.0 0 (skS.0 5 a) a_3)) (Or (Eq (cc1 (skS.0 5 a)) True) (Eq False True))) % 8.53/8.76 Clause #269 (by clausification #[218]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (cc1 (skS.0 5 a)) True) (Ne (skS.0 0 (skS.0 5 a) a_1) (skS.0 1 (skS.0 5 a) a_1 a_2))) % 8.53/8.76 Clause #270 (by eliminate duplicate literals #[269]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Ne (skS.0 0 (skS.0 5 a) a_1) (skS.0 1 (skS.0 5 a) a_1 a_2)) % 8.53/8.76 Clause #271 (by clausification #[249]): ∀ (a a_1 a_2 a_3 : Iota), % 8.53/8.76 Or (Eq (cc1 (skS.0 5 a)) True) % 8.53/8.76 (Or (Eq (skS.0 1 (skS.0 5 a) a_1 a_2) (skS.0 0 (skS.0 5 a) a_3)) (Eq (cc1 (skS.0 5 a)) True)) % 8.53/8.76 Clause #272 (by eliminate duplicate literals #[271]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc1 (skS.0 5 a)) True) (Eq (skS.0 1 (skS.0 5 a) a_1 a_2) (skS.0 0 (skS.0 5 a) a_3)) % 8.53/8.76 Clause #273 (by backward contextual literal cutting #[272, 270]): ∀ (a : Iota), Eq (cc1 (skS.0 5 a)) True % 8.53/8.76 Clause #278 (by backward demodulation #[273, 124]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq True False) % 8.53/8.76 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.53/8.76 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.53/8.76 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (xsd_integer (skS.0 7 a_2)) True)))) % 8.53/8.76 Clause #279 (by backward demodulation #[273, 162]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq True False) % 8.53/8.76 (Or (Eq (cc2 (skS.0 5 a)) False) % 8.53/8.76 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.53/8.76 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (xsd_integer (skS.0 7 a_2)) False)))) % 8.53/8.76 Clause #292 (by superposition #[273, 91]): ∀ (a a_1 a_2 : Iota), % 8.53/8.76 Or (Eq True False) (Or (Eq (rp (skS.0 5 a) a_1) False) (Or (Eq (rp (skS.0 5 a) a_2) False) (Eq a_1 a_2))) % 8.53/8.76 Clause #293 (by superposition #[273, 92]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 2 (skS.0 5 a) a_1)) True) % 8.62/8.82 Clause #296 (by clausification #[292]): ∀ (a a_1 a_2 : Iota), Or (Eq (rp (skS.0 5 a) a_1) False) (Or (Eq (rp (skS.0 5 a) a_2) False) (Eq a_1 a_2)) % 8.62/8.82 Clause #299 (by clausification #[293]): ∀ (a a_1 : Iota), Eq (rp (skS.0 5 a) (skS.0 2 (skS.0 5 a) a_1)) True % 8.62/8.82 Clause #303 (by superposition #[299, 105]): ∀ (a a_1 a_2 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 4 (skS.0 5 a) a_1 a_2)) True)) % 8.62/8.82 Clause #304 (by superposition #[299, 106]): ∀ (a a_1 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Eq (rp (skS.0 5 a) (skS.0 3 (skS.0 5 a) a_1)) True)) % 8.62/8.82 Clause #305 (by superposition #[299, 133]): ∀ (a a_1 a_2 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq True False) (Ne (skS.0 3 (skS.0 5 a) a_1) (skS.0 4 (skS.0 5 a) a_1 a_2))) % 8.62/8.82 Clause #315 (by clausification #[304]): ∀ (a a_1 : Iota), Or (Eq (cc2 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 3 (skS.0 5 a) a_1)) True) % 8.62/8.82 Clause #324 (by clausification #[303]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 (skS.0 5 a)) True) (Eq (rp (skS.0 5 a) (skS.0 4 (skS.0 5 a) a_1 a_2)) True) % 8.62/8.82 Clause #325 (by superposition #[324, 296]): ∀ (a a_1 a_2 a_3 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) % 8.62/8.82 (Or (Eq True False) (Or (Eq (rp (skS.0 5 a) a_1) False) (Eq (skS.0 4 (skS.0 5 a) a_2 a_3) a_1))) % 8.62/8.82 Clause #333 (by clausification #[278]): ∀ (a a_1 a_2 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) False) % 8.62/8.82 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.62/8.82 (Or (Eq (xsd_string (skS.0 7 a_2)) False) (Eq (xsd_integer (skS.0 7 a_2)) True))) % 8.62/8.82 Clause #334 (by clausification #[279]): ∀ (a a_1 a_2 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) False) % 8.62/8.82 (Or (Eq (cowlThing (skS.0 6 a_1)) False) % 8.62/8.82 (Or (Eq (xsd_string (skS.0 7 a_2)) True) (Eq (xsd_integer (skS.0 7 a_2)) False))) % 8.62/8.82 Clause #335 (by clausification #[325]): ∀ (a a_1 a_2 a_3 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) (Or (Eq (rp (skS.0 5 a) a_1) False) (Eq (skS.0 4 (skS.0 5 a) a_2 a_3) a_1)) % 8.62/8.82 Clause #337 (by superposition #[335, 315]): ∀ (a a_1 a_2 a_3 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) % 8.62/8.82 (Or (Eq (skS.0 4 (skS.0 5 a) a_1 a_2) (skS.0 3 (skS.0 5 a) a_3)) (Or (Eq (cc2 (skS.0 5 a)) True) (Eq False True))) % 8.62/8.82 Clause #352 (by clausification #[305]): ∀ (a a_1 a_2 : Iota), Or (Eq (cc2 (skS.0 5 a)) True) (Ne (skS.0 3 (skS.0 5 a) a_1) (skS.0 4 (skS.0 5 a) a_1 a_2)) % 8.62/8.82 Clause #372 (by clausification #[337]): ∀ (a a_1 a_2 a_3 : Iota), % 8.62/8.82 Or (Eq (cc2 (skS.0 5 a)) True) % 8.62/8.82 (Or (Eq (skS.0 4 (skS.0 5 a) a_1 a_2) (skS.0 3 (skS.0 5 a) a_3)) (Eq (cc2 (skS.0 5 a)) True)) % 8.62/8.82 Clause #373 (by eliminate duplicate literals #[372]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (cc2 (skS.0 5 a)) True) (Eq (skS.0 4 (skS.0 5 a) a_1 a_2) (skS.0 3 (skS.0 5 a) a_3)) % 8.62/8.82 Clause #374 (by backward contextual literal cutting #[373, 352]): ∀ (a : Iota), Eq (cc2 (skS.0 5 a)) True % 8.62/8.82 Clause #385 (by superposition #[374, 333]): ∀ (a a_1 : Iota), % 8.62/8.82 Or (Eq True False) % 8.62/8.82 (Or (Eq (cowlThing (skS.0 6 a)) False) % 8.62/8.82 (Or (Eq (xsd_string (skS.0 7 a_1)) False) (Eq (xsd_integer (skS.0 7 a_1)) True))) % 8.62/8.82 Clause #386 (by superposition #[374, 334]): ∀ (a a_1 : Iota), % 8.62/8.82 Or (Eq True False) % 8.62/8.82 (Or (Eq (cowlThing (skS.0 6 a)) False) % 8.62/8.82 (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Eq (xsd_integer (skS.0 7 a_1)) False))) % 8.62/8.82 Clause #396 (by clausification #[385]): ∀ (a a_1 : Iota), % 8.62/8.82 Or (Eq (cowlThing (skS.0 6 a)) False) (Or (Eq (xsd_string (skS.0 7 a_1)) False) (Eq (xsd_integer (skS.0 7 a_1)) True)) % 8.62/8.82 Clause #397 (by superposition #[396, 69]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) False) (Or (Eq (xsd_integer (skS.0 7 a)) True) (Eq False True)) % 8.62/8.82 Clause #398 (by clausification #[397]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) False) (Eq (xsd_integer (skS.0 7 a)) True) % 8.62/8.82 Clause #399 (by clausification #[386]): ∀ (a a_1 : Iota), % 8.62/8.82 Or (Eq (cowlThing (skS.0 6 a)) False) (Or (Eq (xsd_string (skS.0 7 a_1)) True) (Eq (xsd_integer (skS.0 7 a_1)) False)) % 8.62/8.82 Clause #400 (by superposition #[399, 69]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) True) (Or (Eq (xsd_integer (skS.0 7 a)) False) (Eq False True)) % 8.62/8.84 Clause #401 (by clausification #[400]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) True) (Eq (xsd_integer (skS.0 7 a)) False) % 8.62/8.84 Clause #402 (by superposition #[401, 65]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) True) (Or (Eq (xsd_string (skS.0 7 a)) True) (Eq False True)) % 8.62/8.84 Clause #403 (by clausification #[402]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 7 a)) True) (Eq (xsd_string (skS.0 7 a)) True) % 8.62/8.84 Clause #404 (by eliminate duplicate literals #[403]): ∀ (a : Iota), Eq (xsd_string (skS.0 7 a)) True % 8.62/8.84 Clause #405 (by backward demodulation #[404, 398]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 7 a)) True) % 8.62/8.84 Clause #407 (by superposition #[404, 66]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 7 a)) False) % 8.62/8.84 Clause #408 (by clausification #[407]): ∀ (a : Iota), Eq (xsd_integer (skS.0 7 a)) False % 8.62/8.84 Clause #410 (by clausification #[405]): ∀ (a : Iota), Eq (xsd_integer (skS.0 7 a)) True % 8.62/8.84 Clause #411 (by superposition #[410, 408]): Eq True False % 8.62/8.84 Clause #415 (by clausification #[411]): False % 8.62/8.84 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------