%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : KRS170+1 : TPTP v9.2.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 6.55s 6.74s % Output : Proof 6.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : KRS170+1 : TPTP v9.2.0. Released v3.1.0. % 0.13/0.13 % Command : duper %s % 0.14/0.34 % Computer : n016.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:10:08 EDT 2025 % 0.14/0.35 % CPUTime : % 6.55/6.74 SZS status Theorem for theBenchmark.p % 6.55/6.74 SZS output start Proof for theBenchmark.p % 6.55/6.74 Clause #0 (by assumption #[]): Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) True % 6.55/6.74 Clause #1 (by assumption #[]): Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) True % 6.55/6.74 Clause #2 (by assumption #[]): Eq (∀ (X Y : Iota), Iff (rhasLeader X Y) (rhasHead X Y)) True % 6.55/6.74 Clause #3 (by assumption #[]): Eq % 6.55/6.74 (Not % 6.55/6.74 (And % 6.55/6.74 (And % 6.55/6.74 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 6.55/6.74 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 6.55/6.74 (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y)) % 6.55/6.74 (∀ (X Y : Iota), rhasHead X Y → rhasLeader X Y))) % 6.55/6.74 True % 6.55/6.74 Clause #4 (by clausification #[1]): ∀ (a : Iota), Eq (Iff (xsd_string a) (Not (xsd_integer a))) True % 6.55/6.74 Clause #5 (by clausification #[4]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (Not (xsd_integer a)) False) % 6.55/6.74 Clause #6 (by clausification #[4]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (Not (xsd_integer a)) True) % 6.55/6.74 Clause #7 (by clausification #[5]): ∀ (a : Iota), Or (Eq (xsd_string a) True) (Eq (xsd_integer a) True) % 6.55/6.74 Clause #8 (by clausification #[6]): ∀ (a : Iota), Or (Eq (xsd_string a) False) (Eq (xsd_integer a) False) % 6.55/6.74 Clause #11 (by clausification #[0]): ∀ (a : Iota), Eq (And (cowlThing a) (Not (cowlNothing a))) True % 6.55/6.74 Clause #12 (by clausification #[11]): ∀ (a : Iota), Eq (Not (cowlNothing a)) True % 6.55/6.74 Clause #13 (by clausification #[11]): ∀ (a : Iota), Eq (cowlThing a) True % 6.55/6.74 Clause #14 (by clausification #[12]): ∀ (a : Iota), Eq (cowlNothing a) False % 6.55/6.74 Clause #15 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (Y : Iota), Iff (rhasLeader a Y) (rhasHead a Y)) True % 6.55/6.74 Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota), Eq (Iff (rhasLeader a a_1) (rhasHead a a_1)) True % 6.55/6.74 Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota), Or (Eq (rhasLeader a a_1) True) (Eq (rhasHead a a_1) False) % 6.55/6.74 Clause #18 (by clausification #[16]): ∀ (a a_1 : Iota), Or (Eq (rhasLeader a a_1) False) (Eq (rhasHead a a_1) True) % 6.55/6.74 Clause #19 (by clausification #[3]): Eq % 6.55/6.74 (And % 6.55/6.74 (And % 6.55/6.74 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 6.55/6.74 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 6.55/6.74 (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y)) % 6.55/6.74 (∀ (X Y : Iota), rhasHead X Y → rhasLeader X Y)) % 6.55/6.74 False % 6.55/6.74 Clause #20 (by clausification #[19]): Or % 6.55/6.74 (Eq % 6.55/6.74 (And % 6.55/6.74 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 6.55/6.74 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 6.55/6.74 (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y)) % 6.55/6.74 False) % 6.55/6.74 (Eq (∀ (X Y : Iota), rhasHead X Y → rhasLeader X Y) False) % 6.55/6.74 Clause #21 (by clausification #[20]): Or (Eq (∀ (X Y : Iota), rhasHead X Y → rhasLeader X Y) False) % 6.55/6.74 (Or % 6.55/6.74 (Eq % 6.55/6.74 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 6.55/6.74 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 6.55/6.74 False) % 6.55/6.74 (Eq (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y) False)) % 6.55/6.74 Clause #22 (by clausification #[21]): ∀ (a : Iota), % 6.55/6.74 Or % 6.55/6.74 (Eq % 6.55/6.74 (And (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) % 6.55/6.74 (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X)))) % 6.55/6.74 False) % 6.55/6.74 (Or (Eq (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y) False) % 6.55/6.74 (Eq (Not (∀ (Y : Iota), rhasHead (skS.0 0 a) Y → rhasLeader (skS.0 0 a) Y)) True)) % 6.55/6.74 Clause #23 (by clausification #[22]): ∀ (a : Iota), % 6.55/6.74 Or (Eq (∀ (X Y : Iota), rhasLeader X Y → rhasHead X Y) False) % 6.55/6.74 (Or (Eq (Not (∀ (Y : Iota), rhasHead (skS.0 0 a) Y → rhasLeader (skS.0 0 a) Y)) True) % 6.55/6.74 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 6.55/6.74 (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False))) % 6.55/6.74 Clause #24 (by clausification #[23]): ∀ (a a_1 : Iota), % 6.55/6.74 Or (Eq (Not (∀ (Y : Iota), rhasHead (skS.0 0 a) Y → rhasLeader (skS.0 0 a) Y)) True) % 6.55/6.74 (Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 6.55/6.74 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 6.55/6.74 (Eq (Not (∀ (Y : Iota), rhasLeader (skS.0 1 a_1) Y → rhasHead (skS.0 1 a_1) Y)) True))) % 6.62/6.77 Clause #25 (by clausification #[24]): ∀ (a a_1 : Iota), % 6.62/6.77 Or (Eq (∀ (X : Iota), And (cowlThing X) (Not (cowlNothing X))) False) % 6.62/6.77 (Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 6.62/6.77 (Or (Eq (Not (∀ (Y : Iota), rhasLeader (skS.0 1 a) Y → rhasHead (skS.0 1 a) Y)) True) % 6.62/6.77 (Eq (∀ (Y : Iota), rhasHead (skS.0 0 a_1) Y → rhasLeader (skS.0 0 a_1) Y) False))) % 6.62/6.77 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 : Iota), % 6.62/6.77 Or (Eq (∀ (X : Iota), Iff (xsd_string X) (Not (xsd_integer X))) False) % 6.62/6.77 (Or (Eq (Not (∀ (Y : Iota), rhasLeader (skS.0 1 a) Y → rhasHead (skS.0 1 a) Y)) True) % 6.62/6.77 (Or (Eq (∀ (Y : Iota), rhasHead (skS.0 0 a_1) Y → rhasLeader (skS.0 0 a_1) Y) False) % 6.62/6.77 (Eq (Not (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2))))) True))) % 6.62/6.77 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 : Iota), % 6.62/6.77 Or (Eq (Not (∀ (Y : Iota), rhasLeader (skS.0 1 a) Y → rhasHead (skS.0 1 a) Y)) True) % 6.62/6.77 (Or (Eq (∀ (Y : Iota), rhasHead (skS.0 0 a_1) Y → rhasLeader (skS.0 0 a_1) Y) False) % 6.62/6.77 (Or (Eq (Not (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2))))) True) % 6.62/6.77 (Eq (Not (Iff (xsd_string (skS.0 3 a_3)) (Not (xsd_integer (skS.0 3 a_3))))) True))) % 6.62/6.77 Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : Iota), % 6.62/6.77 Or (Eq (∀ (Y : Iota), rhasHead (skS.0 0 a) Y → rhasLeader (skS.0 0 a) Y) False) % 6.62/6.77 (Or (Eq (Not (And (cowlThing (skS.0 2 a_1)) (Not (cowlNothing (skS.0 2 a_1))))) True) % 6.62/6.77 (Or (Eq (Not (Iff (xsd_string (skS.0 3 a_2)) (Not (xsd_integer (skS.0 3 a_2))))) True) % 6.62/6.77 (Eq (∀ (Y : Iota), rhasLeader (skS.0 1 a_3) Y → rhasHead (skS.0 1 a_3) Y) False))) % 6.62/6.77 Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.62/6.77 Or (Eq (Not (And (cowlThing (skS.0 2 a)) (Not (cowlNothing (skS.0 2 a))))) True) % 6.62/6.77 (Or (Eq (Not (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1))))) True) % 6.62/6.77 (Or (Eq (∀ (Y : Iota), rhasLeader (skS.0 1 a_2) Y → rhasHead (skS.0 1 a_2) Y) False) % 6.62/6.77 (Eq (Not (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4) → rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4))) True))) % 6.62/6.77 Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.62/6.77 Or (Eq (Not (Iff (xsd_string (skS.0 3 a)) (Not (xsd_integer (skS.0 3 a))))) True) % 6.62/6.77 (Or (Eq (∀ (Y : Iota), rhasLeader (skS.0 1 a_1) Y → rhasHead (skS.0 1 a_1) Y) False) % 6.62/6.77 (Or (Eq (Not (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3) → rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3))) True) % 6.62/6.77 (Eq (And (cowlThing (skS.0 2 a_4)) (Not (cowlNothing (skS.0 2 a_4)))) False))) % 6.62/6.77 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.62/6.77 Or (Eq (∀ (Y : Iota), rhasLeader (skS.0 1 a) Y → rhasHead (skS.0 1 a) Y) False) % 6.62/6.77 (Or (Eq (Not (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2) → rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2))) True) % 6.62/6.77 (Or (Eq (And (cowlThing (skS.0 2 a_3)) (Not (cowlNothing (skS.0 2 a_3)))) False) % 6.62/6.77 (Eq (Iff (xsd_string (skS.0 3 a_4)) (Not (xsd_integer (skS.0 3 a_4)))) False))) % 6.62/6.77 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.62/6.77 Or (Eq (Not (rhasHead (skS.0 0 a) (skS.0 4 a a_1) → rhasLeader (skS.0 0 a) (skS.0 4 a a_1))) True) % 6.62/6.77 (Or (Eq (And (cowlThing (skS.0 2 a_2)) (Not (cowlNothing (skS.0 2 a_2)))) False) % 6.62/6.77 (Or (Eq (Iff (xsd_string (skS.0 3 a_3)) (Not (xsd_integer (skS.0 3 a_3)))) False) % 6.62/6.77 (Eq (Not (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5) → rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5))) True))) % 6.62/6.77 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.62/6.77 Or (Eq (And (cowlThing (skS.0 2 a)) (Not (cowlNothing (skS.0 2 a)))) False) % 6.62/6.77 (Or (Eq (Iff (xsd_string (skS.0 3 a_1)) (Not (xsd_integer (skS.0 3 a_1)))) False) % 6.62/6.77 (Or (Eq (Not (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3))) True) % 6.62/6.77 (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5) → rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False))) % 6.62/6.77 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (Iff (xsd_string (skS.0 3 a)) (Not (xsd_integer (skS.0 3 a)))) False) % 6.64/6.80 (Or (Eq (Not (rhasLeader (skS.0 1 a_1) (skS.0 5 a_1 a_2) → rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2))) True) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4) → rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4)) False) % 6.64/6.80 (Or (Eq (cowlThing (skS.0 2 a_5)) False) (Eq (Not (cowlNothing (skS.0 2 a_5))) False)))) % 6.64/6.80 Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (Not (rhasLeader (skS.0 1 a) (skS.0 5 a a_1) → rhasHead (skS.0 1 a) (skS.0 5 a a_1))) True) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3) → rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.64/6.80 (Or (Eq (cowlThing (skS.0 2 a_4)) False) % 6.64/6.80 (Or (Eq (Not (cowlNothing (skS.0 2 a_4))) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_5)) False) (Eq (Not (xsd_integer (skS.0 3 a_5))) False))))) % 6.64/6.80 Clause #36 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (Not (rhasLeader (skS.0 1 a) (skS.0 5 a a_1) → rhasHead (skS.0 1 a) (skS.0 5 a a_1))) True) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3) → rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.64/6.80 (Or (Eq (cowlThing (skS.0 2 a_4)) False) % 6.64/6.80 (Or (Eq (Not (cowlNothing (skS.0 2 a_4))) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_5)) True) (Eq (Not (xsd_integer (skS.0 3 a_5))) True))))) % 6.64/6.80 Clause #37 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1) → rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.64/6.80 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 6.64/6.80 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_3)) False) % 6.64/6.80 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) False) % 6.64/6.80 (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5) → rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.64/6.80 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.64/6.80 (Or (Eq (Not (cowlNothing (skS.0 2 a))) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.64/6.80 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) False) % 6.64/6.80 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.64/6.80 (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True))))) % 6.64/6.80 Clause #39 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.64/6.80 (Or (Eq (Not (cowlNothing (skS.0 2 a))) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.64/6.80 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) False) % 6.64/6.80 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.64/6.80 (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False))))) % 6.64/6.80 Clause #40 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.64/6.80 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) False) % 6.64/6.80 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True) (Eq (cowlNothing (skS.0 2 a)) True))))) % 6.64/6.80 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.64/6.80 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True) % 6.64/6.80 (Or (Eq (cowlNothing (skS.0 2 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) True))))) % 6.64/6.80 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.64/6.80 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.64/6.80 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.64/6.80 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.64/6.80 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.64/6.80 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.64/6.80 Clause #43 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.67/6.82 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.67/6.82 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.67/6.82 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.67/6.82 Clause #44 (by forward demodulation #[42, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.67/6.82 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.67/6.82 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.67/6.82 (Or (Eq False True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.67/6.82 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.67/6.82 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.67/6.82 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True)))) % 6.67/6.82 Clause #46 (by superposition #[45, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.67/6.82 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq False True)))) % 6.67/6.82 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.67/6.82 Clause #48 (by superposition #[47, 7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.67/6.82 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) % 6.67/6.82 (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 6.67/6.82 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.67/6.82 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 6.67/6.82 Clause #50 (by eliminate duplicate literals #[49]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.67/6.82 Clause #52 (by superposition #[50, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.67/6.82 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.67/6.82 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.67/6.82 Clause #54 (by superposition #[53, 17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.67/6.82 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.67/6.82 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) % 6.67/6.82 (Or (Eq (rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True) (Eq True False))) % 6.67/6.82 Clause #56 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.67/6.82 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1) → rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.67/6.82 (Or (Eq (cowlThing (skS.0 2 a_2)) False) % 6.67/6.82 (Or (Eq (Not (cowlNothing (skS.0 2 a_2))) False) % 6.67/6.82 (Or (Eq (xsd_string (skS.0 3 a_3)) True) % 6.67/6.82 (Or (Eq (Not (xsd_integer (skS.0 3 a_3))) True) % 6.67/6.82 (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5) → rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.67/6.82 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.67/6.82 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.67/6.82 (Or (Eq (Not (cowlNothing (skS.0 2 a))) False) % 6.67/6.82 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.67/6.82 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) True) % 6.67/6.82 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.67/6.82 (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True))))) % 6.69/6.84 Clause #58 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.84 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.84 (Or (Eq (Not (cowlNothing (skS.0 2 a))) False) % 6.69/6.84 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.84 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) True) % 6.69/6.84 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.84 (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False))))) % 6.69/6.84 Clause #59 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.84 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.84 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.84 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) True) % 6.69/6.84 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.84 (Or (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True) (Eq (cowlNothing (skS.0 2 a)) True))))) % 6.69/6.84 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.84 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True) % 6.69/6.85 (Or (Eq (cowlNothing (skS.0 2 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) False))))) % 6.69/6.85 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.85 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.85 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.85 Clause #62 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.85 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.85 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.69/6.85 Clause #63 (by forward demodulation #[61, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.85 (Or (Eq False True) % 6.69/6.85 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.85 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.85 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True)))) % 6.69/6.85 Clause #65 (by superposition #[64, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.85 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.85 (Or (Eq (xsd_integer (skS.0 3 a)) False) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq False True)))) % 6.69/6.85 Clause #66 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.85 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.85 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) (Eq (rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True)) % 6.69/6.85 Clause #74 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.85 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) False) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False) (Eq (cowlNothing (skS.0 2 a)) True))))) % 6.69/6.85 Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.85 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.85 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.85 (Or (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False) % 6.69/6.87 (Or (Eq (cowlNothing (skS.0 2 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) True))))) % 6.69/6.87 Clause #76 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.87 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.87 Clause #77 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.87 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.69/6.87 Clause #78 (by forward demodulation #[76, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.87 (Or (Eq False True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.87 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True)))) % 6.69/6.87 Clause #80 (by superposition #[79, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq False True)))) % 6.69/6.87 Clause #83 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.69/6.87 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a)) False) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.69/6.87 Clause #88 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.69/6.87 Clause #89 (by superposition #[88, 7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) % 6.69/6.87 (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 6.69/6.87 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.87 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 6.69/6.87 Clause #91 (by eliminate duplicate literals #[90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.69/6.87 Clause #94 (by forward demodulation #[43, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.87 (Or (Eq False True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.69/6.87 Clause #95 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.87 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.87 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.69/6.87 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.87 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.69/6.87 Clause #96 (by superposition #[95, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.87 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.69/6.90 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.90 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq False True)))) % 6.69/6.90 Clause #97 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.69/6.90 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False))) % 6.69/6.90 Clause #98 (by superposition #[97, 7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.90 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) % 6.69/6.90 (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 6.69/6.90 Clause #99 (by clausification #[98]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.90 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 6.69/6.90 Clause #100 (by eliminate duplicate literals #[99]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False)) % 6.69/6.90 Clause #102 (by superposition #[100, 66]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) % 6.69/6.90 (Or (Eq False True) (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True)))) % 6.69/6.90 Clause #103 (by clausification #[102]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) True))) % 6.69/6.90 Clause #108 (by equality factoring #[103]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.90 (Or (Ne True True) (Eq (xsd_integer (skS.0 3 a_4)) True))) % 6.69/6.90 Clause #109 (by clausification #[108]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_4)) True) (Or (Eq True False) (Eq True False)))) % 6.69/6.90 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_4)) True) (Eq True False))) % 6.69/6.90 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) (Eq (xsd_integer (skS.0 3 a_4)) True)) % 6.69/6.90 Clause #115 (by superposition #[112, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq True False) (Eq (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True))) % 6.69/6.90 Clause #117 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.69/6.90 Or (Eq (rhasHead (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.69/6.90 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True)) % 6.69/6.90 Clause #121 (by equality factoring #[117]): ∀ (a a_1 a_2 : Iota), % 6.69/6.90 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Ne True True) (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True)) % 6.69/6.90 Clause #122 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.90 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.90 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.90 (Or (Eq (Not (xsd_integer (skS.0 3 a_1))) True) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.90 (Or (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False) (Eq (cowlNothing (skS.0 2 a)) True))))) % 6.69/6.90 Clause #123 (by clausification #[122]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.90 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3) → rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) False) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 0 a_4) (skS.0 4 a_4 a_5)) False) % 6.69/6.92 (Or (Eq (cowlNothing (skS.0 2 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) False))))) % 6.69/6.92 Clause #124 (by clausification #[123]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.92 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.92 Clause #125 (by clausification #[123]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.92 (Or (Eq (cowlNothing (skS.0 2 a)) True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.69/6.92 Clause #126 (by forward demodulation #[124, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.92 (Or (Eq False True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))))) % 6.69/6.92 Clause #127 (by clausification #[126]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True)))) % 6.69/6.92 Clause #129 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 6.69/6.92 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.92 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Or (Eq True False) (Eq True False))) % 6.69/6.92 Clause #131 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), % 6.69/6.92 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq True False)) % 6.69/6.92 Clause #132 (by clausification #[131]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.92 Clause #134 (by superposition #[132, 17]): ∀ (a a_1 a_2 : Iota), % 6.69/6.92 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq True False)) % 6.69/6.92 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.69/6.92 Clause #137 (by superposition #[135, 91]): ∀ (a a_1 a_2 a_3 : Iota), % 6.69/6.92 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.92 (Or (Eq True False) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True))) % 6.69/6.92 Clause #139 (by clausification #[137]): ∀ (a a_1 a_2 a_3 : Iota), % 6.69/6.92 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True)) % 6.69/6.92 Clause #142 (by equality factoring #[139]): ∀ (a a_1 a_2 : Iota), % 6.69/6.92 Or (Eq (rhasLeader (skS.0 1 a) (skS.0 5 a a_1)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 3 a_2)) True)) % 6.69/6.92 Clause #143 (by forward demodulation #[62, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.92 (Or (Eq False True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.69/6.92 Clause #144 (by clausification #[143]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.69/6.92 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.69/6.92 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.69/6.92 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.69/6.92 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.69/6.92 Clause #146 (by clausification #[142]): ∀ (a a_1 a_2 : Iota), % 6.77/6.95 Or (Eq (rhasLeader (skS.0 1 a) (skS.0 5 a a_1)) True) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Or (Eq True False) (Eq True False))) % 6.77/6.95 Clause #148 (by clausification #[146]): ∀ (a a_1 a_2 : Iota), % 6.77/6.95 Or (Eq (rhasLeader (skS.0 1 a) (skS.0 5 a a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq True False)) % 6.77/6.95 Clause #149 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), Or (Eq (rhasLeader (skS.0 1 a) (skS.0 5 a a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.77/6.95 Clause #150 (by superposition #[149, 18]): ∀ (a a_1 a_2 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True)) % 6.77/6.95 Clause #152 (by clausification #[150]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) % 6.77/6.95 Clause #157 (by forward demodulation #[77, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.77/6.95 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.77/6.95 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.77/6.95 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.77/6.95 (Or (Eq False True) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.77/6.95 Clause #158 (by clausification #[157]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.77/6.95 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.77/6.95 (Or (Eq (xsd_string (skS.0 3 a_1)) False) % 6.77/6.95 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.77/6.95 Clause #159 (by superposition #[158, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.95 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.77/6.95 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.95 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq False True)))) % 6.77/6.95 Clause #173 (by clausification #[159]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.95 Or (Eq (xsd_string (skS.0 3 a)) False) % 6.77/6.95 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False))) % 6.77/6.95 Clause #175 (by superposition #[173, 7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.95 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.77/6.95 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) % 6.77/6.95 (Or (Eq False True) (Eq (xsd_integer (skS.0 3 a_2)) True)))) % 6.77/6.95 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.95 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) % 6.77/6.95 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq (xsd_integer (skS.0 3 a_2)) True))) % 6.77/6.95 Clause #177 (by eliminate duplicate literals #[176]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.95 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False)) % 6.77/6.95 Clause #178 (by superposition #[177, 135]): ∀ (a a_1 a_2 a_3 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.95 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) False) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_3)) True) (Eq False True))) % 6.77/6.95 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 a_3 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.95 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) False) (Eq (xsd_integer (skS.0 3 a_3)) True)) % 6.77/6.95 Clause #180 (by superposition #[179, 152]): ∀ (a a_1 a_2 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq (xsd_integer (skS.0 3 a_2)) True) (Eq False True))) % 6.77/6.95 Clause #181 (by clausification #[180]): ∀ (a a_1 a_2 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.95 (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) True)) % 6.77/6.95 Clause #183 (by equality factoring #[181]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Ne True True) (Eq (xsd_integer (skS.0 3 a_1)) True)) % 6.77/6.95 Clause #192 (by clausification #[183]): ∀ (a a_1 : Iota), % 6.77/6.95 Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Or (Eq True False) (Eq True False))) % 6.77/6.97 Clause #194 (by clausification #[192]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq (xsd_integer (skS.0 3 a_1)) True) (Eq True False)) % 6.77/6.97 Clause #195 (by clausification #[194]): ∀ (a a_1 : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq (xsd_integer (skS.0 3 a_1)) True) % 6.77/6.97 Clause #197 (by equality factoring #[195]): ∀ (a : Iota), Or (Ne True True) (Eq (xsd_integer (skS.0 3 a)) True) % 6.77/6.97 Clause #198 (by clausification #[197]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Or (Eq True False) (Eq True False)) % 6.77/6.97 Clause #200 (by clausification #[198]): ∀ (a : Iota), Or (Eq (xsd_integer (skS.0 3 a)) True) (Eq True False) % 6.77/6.97 Clause #201 (by clausification #[200]): ∀ (a : Iota), Eq (xsd_integer (skS.0 3 a)) True % 6.77/6.97 Clause #202 (by backward demodulation #[201, 83]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.77/6.97 (Or (Eq True False) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.77/6.97 Clause #203 (by backward demodulation #[201, 127]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.77/6.97 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.77/6.97 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.77/6.97 (Or (Eq True False) (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True)))) % 6.77/6.97 Clause #204 (by backward demodulation #[201, 144]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.77/6.97 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.77/6.97 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.77/6.97 (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.77/6.97 Clause #205 (by clausification #[202]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.77/6.97 Clause #208 (by superposition #[205, 18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.77/6.97 (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True))) % 6.77/6.97 Clause #210 (by clausification #[208]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.77/6.97 Clause #212 (by superposition #[210, 17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True) (Eq True False))) % 6.77/6.97 Clause #214 (by clausification #[212]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) (Eq (rhasLeader (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True)) % 6.77/6.97 Clause #216 (by superposition #[214, 17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq True False))) % 6.77/6.97 Clause #219 (by clausification #[216]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.77/6.97 Clause #220 (by superposition #[219, 8]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True) % 6.77/6.97 (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_4)) False))) % 6.77/6.97 Clause #226 (by clausification #[220]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.77/6.97 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True) (Eq (xsd_integer (skS.0 3 a_4)) False)) % 6.77/6.97 Clause #227 (by superposition #[226, 201]): ∀ (a a_1 a_2 a_3 : Iota), % 6.77/6.97 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.77/6.97 (Or (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True) (Eq False True)) % 6.83/7.00 Clause #228 (by clausification #[227]): ∀ (a a_1 a_2 a_3 : Iota), % 6.83/7.00 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) (Eq (rhasLeader (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True) % 6.83/7.00 Clause #230 (by superposition #[228, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 6.83/7.00 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) % 6.83/7.00 (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True)) % 6.83/7.00 Clause #231 (by clausification #[230]): ∀ (a a_1 a_2 a_3 : Iota), % 6.83/7.00 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) (Eq (rhasHead (skS.0 1 a_2) (skS.0 5 a_2 a_3)) True) % 6.83/7.00 Clause #232 (by superposition #[231, 18]): ∀ (a a_1 a_2 a_3 : Iota), % 6.83/7.00 Or (Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True) % 6.83/7.00 (Or (Eq True False) (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True)) % 6.83/7.00 Clause #235 (by clausification #[232]): ∀ (a a_1 a_2 a_3 : Iota), % 6.83/7.00 Or (Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True) (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) % 6.83/7.00 Clause #252 (by clausification #[204]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.00 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.00 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_2) (skS.0 4 a_2 a_3)) True) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))) % 6.83/7.00 Clause #253 (by superposition #[252, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq False True))) % 6.83/7.00 Clause #254 (by clausification #[253]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False)) % 6.83/7.00 Clause #256 (by superposition #[254, 235]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.83/7.00 (Or (Eq False True) (Eq (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True))) % 6.83/7.00 Clause #257 (by clausification #[256]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq (rhasHead (skS.0 0 a_3) (skS.0 4 a_3 a_4)) True)) % 6.83/7.00 Clause #260 (by equality factoring #[257]): ∀ (a a_1 a_2 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Ne True True) (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True)) % 6.83/7.00 Clause #262 (by clausification #[260]): ∀ (a a_1 a_2 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.00 (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Or (Eq True False) (Eq True False))) % 6.83/7.00 Clause #264 (by clausification #[262]): ∀ (a a_1 a_2 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq True False)) % 6.83/7.00 Clause #265 (by clausification #[264]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (rhasHead (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.83/7.00 Clause #267 (by superposition #[265, 17]): ∀ (a a_1 a_2 : Iota), % 6.83/7.00 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) (Eq True False)) % 6.83/7.00 Clause #268 (by clausification #[267]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) True) % 6.83/7.00 Clause #269 (by superposition #[268, 8]): ∀ (a a_1 a_2 : Iota), % 6.83/7.00 Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_2)) False)) % 6.83/7.00 Clause #271 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) False) % 6.83/7.00 Clause #272 (by superposition #[271, 201]): ∀ (a a_1 : Iota), Or (Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True) (Eq False True) % 6.83/7.00 Clause #273 (by clausification #[272]): ∀ (a a_1 : Iota), Eq (rhasLeader (skS.0 0 a) (skS.0 4 a a_1)) True % 6.83/7.00 Clause #282 (by clausification #[203]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.00 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.00 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.00 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.83/7.00 (Eq (rhasLeader (skS.0 1 a_4) (skS.0 5 a_4 a_5)) True))) % 6.83/7.02 Clause #283 (by superposition #[282, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True) (Eq False True))) % 6.83/7.02 Clause #284 (by clausification #[283]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) (Eq (rhasLeader (skS.0 1 a_3) (skS.0 5 a_3 a_4)) True)) % 6.83/7.02 Clause #285 (by superposition #[284, 273]): ∀ (a a_1 a_2 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (rhasLeader (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) (Eq False True)) % 6.83/7.02 Clause #286 (by clausification #[285]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (rhasLeader (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) % 6.83/7.02 Clause #288 (by superposition #[286, 18]): ∀ (a a_1 a_2 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True)) % 6.83/7.02 Clause #290 (by clausification #[288]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) True) % 6.83/7.02 Clause #291 (by superposition #[290, 8]): ∀ (a a_1 a_2 : Iota), % 6.83/7.02 Or (Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True) (Or (Eq True False) (Eq (xsd_integer (skS.0 3 a_2)) False)) % 6.83/7.02 Clause #293 (by clausification #[291]): ∀ (a a_1 a_2 : Iota), Or (Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True) (Eq (xsd_integer (skS.0 3 a_2)) False) % 6.83/7.02 Clause #294 (by superposition #[293, 201]): ∀ (a a_1 : Iota), Or (Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True) (Eq False True) % 6.83/7.02 Clause #295 (by clausification #[294]): ∀ (a a_1 : Iota), Eq (rhasHead (skS.0 1 a) (skS.0 5 a a_1)) True % 6.83/7.02 Clause #306 (by forward demodulation #[125, 14]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.02 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.02 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.83/7.02 (Or (Eq False True) % 6.83/7.02 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))))) % 6.83/7.02 Clause #307 (by clausification #[306]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.02 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.02 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.83/7.02 (Or (Eq (xsd_integer (skS.0 3 a_1)) False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.83/7.02 Clause #308 (by forward demodulation #[307, 201]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.02 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.02 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.83/7.02 (Or (Eq True False) (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False)))) % 6.83/7.02 Clause #309 (by clausification #[308]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 6.83/7.02 Or (Eq (cowlThing (skS.0 2 a)) False) % 6.83/7.02 (Or (Eq (xsd_string (skS.0 3 a_1)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_2) (skS.0 4 a_2 a_3)) False) % 6.83/7.02 (Eq (rhasHead (skS.0 1 a_4) (skS.0 5 a_4 a_5)) False))) % 6.83/7.02 Clause #310 (by superposition #[309, 13]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) % 6.83/7.02 (Or (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False) (Eq False True))) % 6.83/7.02 Clause #311 (by clausification #[310]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) % 6.83/7.02 (Or (Eq (rhasLeader (skS.0 0 a_1) (skS.0 4 a_1 a_2)) False) (Eq (rhasHead (skS.0 1 a_3) (skS.0 5 a_3 a_4)) False)) % 6.83/7.02 Clause #312 (by superposition #[311, 273]): ∀ (a a_1 a_2 : Iota), % 6.83/7.02 Or (Eq (xsd_string (skS.0 3 a)) True) (Or (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) False) (Eq False True)) % 6.83/7.02 Clause #313 (by clausification #[312]): ∀ (a a_1 a_2 : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq (rhasHead (skS.0 1 a_1) (skS.0 5 a_1 a_2)) False) % 6.83/7.02 Clause #314 (by superposition #[313, 295]): ∀ (a : Iota), Or (Eq (xsd_string (skS.0 3 a)) True) (Eq False True) % 6.83/7.02 Clause #315 (by clausification #[314]): ∀ (a : Iota), Eq (xsd_string (skS.0 3 a)) True % 6.83/7.03 Clause #316 (by superposition #[315, 8]): ∀ (a : Iota), Or (Eq True False) (Eq (xsd_integer (skS.0 3 a)) False) % 6.83/7.03 Clause #317 (by clausification #[316]): ∀ (a : Iota), Eq (xsd_integer (skS.0 3 a)) False % 6.83/7.03 Clause #318 (by superposition #[317, 201]): Eq False True % 6.83/7.03 Clause #319 (by clausification #[318]): False % 6.83/7.03 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------