%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT009+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:14 AM UTC 2026 % Result : Theorem 14.55s 14.86s % Output : Proof 15.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT009+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.05 % Command : duper %s % 0.11/0.36 % Computer : n014.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Mon Sep 7 11:46:26 UTC 2026 % 0.11/0.37 % CPUTime : % 14.55/14.86 SZS status Theorem for theBenchmark.p % 14.55/14.86 SZS output start Proof for theBenchmark.p % 14.55/14.86 Clause #0 (by assumption #[]): Eq (∀ (X T : Iota), organization X T → Exists fun I => inertia X I T) True % 14.55/14.86 Clause #1 (by assumption #[]): Eq % 14.55/14.86 (∀ (X Y T1 T2 Rp1 Rp2 I1 I2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 14.55/14.86 (reorganization_free Y T2 T2)) % 14.55/14.86 (reproducibility X Rp1 T1)) % 14.55/14.86 (reproducibility Y Rp2 T2)) % 14.55/14.86 (inertia X I1 T1)) % 14.55/14.86 (inertia Y I2 T2) → % 14.55/14.86 Iff (greater Rp2 Rp1) (greater I2 I1)) % 14.55/14.86 True % 14.55/14.86 Clause #2 (by assumption #[]): Eq % 14.55/14.86 (∀ (X Y C S1 S2 I1 I2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (And (organization X T1) (organization Y T2)) (class X C T1)) (class Y C T2)) % 14.55/14.86 (size X S1 T1)) % 14.55/14.86 (size Y S2 T2)) % 14.55/14.86 (inertia X I1 T1)) % 14.55/14.86 (inertia Y I2 T2)) % 14.55/14.86 (greater S2 S1) → % 14.55/14.86 greater I2 I1) % 14.55/14.86 True % 14.55/14.86 Clause #3 (by assumption #[]): Eq % 14.55/14.86 (Not % 14.55/14.86 (∀ (X Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 14.55/14.86 (reorganization_free Y T2 T2)) % 14.55/14.86 (class X C T1)) % 14.55/14.86 (class Y C T2)) % 14.55/14.86 (reproducibility X Rp1 T1)) % 14.55/14.86 (reproducibility Y Rp2 T2)) % 14.55/14.86 (size X S1 T1)) % 14.55/14.86 (size Y S2 T2)) % 14.55/14.86 (greater S2 S1) → % 14.55/14.86 greater Rp2 Rp1)) % 14.55/14.86 True % 14.55/14.86 Clause #4 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (T : Iota), organization a T → Exists fun I => inertia a I T) True % 14.55/14.86 Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), Eq (organization a a_1 → Exists fun I => inertia a I a_1) True % 14.55/14.86 Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), Or (Eq (organization a a_1) False) (Eq (Exists fun I => inertia a I a_1) True) % 14.55/14.86 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a a_1) False) (Eq (inertia a (skS.0 0 a a_1 a_2) a_1) True) % 14.55/14.86 Clause #8 (by clausification #[2]): ∀ (a : Iota), % 14.55/14.86 Eq % 14.55/14.86 (∀ (Y C S1 S2 I1 I2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (And (organization a T1) (organization Y T2)) (class a C T1)) (class Y C T2)) % 14.55/14.86 (size a S1 T1)) % 14.55/14.86 (size Y S2 T2)) % 14.55/14.86 (inertia a I1 T1)) % 14.55/14.86 (inertia Y I2 T2)) % 14.55/14.86 (greater S2 S1) → % 14.55/14.86 greater I2 I1) % 14.55/14.86 True % 14.55/14.86 Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota), % 14.55/14.86 Eq % 14.55/14.86 (∀ (C S1 S2 I1 I2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a C T1)) (class a_1 C T2)) % 14.55/14.86 (size a S1 T1)) % 14.55/14.86 (size a_1 S2 T2)) % 14.55/14.86 (inertia a I1 T1)) % 14.55/14.86 (inertia a_1 I2 T2)) % 14.55/14.86 (greater S2 S1) → % 14.55/14.86 greater I2 I1) % 14.55/14.86 True % 14.55/14.86 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), % 14.55/14.86 Eq % 14.55/14.86 (∀ (S1 S2 I1 I2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2)) % 14.55/14.86 (size a S1 T1)) % 14.55/14.86 (size a_1 S2 T2)) % 14.55/14.86 (inertia a I1 T1)) % 14.55/14.86 (inertia a_1 I2 T2)) % 14.55/14.86 (greater S2 S1) → % 14.55/14.86 greater I2 I1) % 14.55/14.86 True % 14.55/14.86 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 a_3 : Iota), % 14.55/14.86 Eq % 14.55/14.86 (∀ (S2 I1 I2 T1 T2 : Iota), % 14.55/14.86 And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And % 14.55/14.86 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2)) % 14.55/14.86 (size a a_3 T1)) % 14.55/14.86 (size a_1 S2 T2)) % 14.55/14.86 (inertia a I1 T1)) % 14.55/14.86 (inertia a_1 I2 T2)) % 14.55/14.86 (greater S2 a_3) → % 14.65/14.90 greater I2 I1) % 14.65/14.90 True % 14.65/14.90 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.65/14.90 Eq % 14.65/14.90 (∀ (I1 I2 T1 T2 : Iota), % 14.65/14.90 And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2)) % 14.65/14.90 (size a a_3 T1)) % 14.65/14.90 (size a_1 a_4 T2)) % 14.65/14.90 (inertia a I1 T1)) % 14.65/14.90 (inertia a_1 I2 T2)) % 14.65/14.90 (greater a_4 a_3) → % 14.65/14.90 greater I2 I1) % 14.65/14.90 True % 14.65/14.90 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.65/14.90 Eq % 14.65/14.90 (∀ (I2 T1 T2 : Iota), % 14.65/14.90 And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2)) % 14.65/14.90 (size a a_3 T1)) % 14.65/14.90 (size a_1 a_4 T2)) % 14.65/14.90 (inertia a a_5 T1)) % 14.65/14.90 (inertia a_1 I2 T2)) % 14.65/14.90 (greater a_4 a_3) → % 14.65/14.90 greater I2 a_5) % 14.65/14.90 True % 14.65/14.90 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.65/14.90 Eq % 14.65/14.90 (∀ (T1 T2 : Iota), % 14.65/14.90 And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2)) % 14.65/14.90 (size a a_3 T1)) % 14.65/14.90 (size a_1 a_4 T2)) % 14.65/14.90 (inertia a a_5 T1)) % 14.65/14.90 (inertia a_1 a_6 T2)) % 14.65/14.90 (greater a_4 a_3) → % 14.65/14.90 greater a_6 a_5) % 14.65/14.90 True % 14.65/14.90 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.65/14.90 Eq % 14.65/14.90 (∀ (T2 : Iota), % 14.65/14.90 And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a a_1) (organization a_2 T2)) (class a a_3 a_1)) (class a_2 a_3 T2)) % 14.65/14.90 (size a a_4 a_1)) % 14.65/14.90 (size a_2 a_5 T2)) % 14.65/14.90 (inertia a a_6 a_1)) % 14.65/14.90 (inertia a_2 a_7 T2)) % 14.65/14.90 (greater a_5 a_4) → % 14.65/14.90 greater a_7 a_6) % 14.65/14.90 True % 14.65/14.90 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.90 Eq % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a a_1) (organization a_2 a_3)) (class a a_4 a_1)) (class a_2 a_4 a_3)) % 14.65/14.90 (size a a_5 a_1)) % 14.65/14.90 (size a_2 a_6 a_3)) % 14.65/14.90 (inertia a a_7 a_1)) % 14.65/14.90 (inertia a_2 a_8 a_3)) % 14.65/14.90 (greater a_6 a_5) → % 14.65/14.90 greater a_8 a_7) % 14.65/14.90 True % 14.65/14.90 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.90 Or % 14.65/14.90 (Eq % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (And (organization a a_1) (organization a_2 a_3)) (class a a_4 a_1)) (class a_2 a_4 a_3)) % 14.65/14.90 (size a a_5 a_1)) % 14.65/14.90 (size a_2 a_6 a_3)) % 14.65/14.90 (inertia a a_7 a_1)) % 14.65/14.90 (inertia a_2 a_8 a_3)) % 14.65/14.90 (greater a_6 a_5)) % 14.65/14.90 False) % 14.65/14.90 (Eq (greater a_8 a_7) True) % 14.65/14.90 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.90 Or (Eq (greater a a_1) True) % 14.65/14.90 (Or % 14.65/14.90 (Eq % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (organization a_2 a_3) (organization a_4 a_5)) (class a_2 a_6 a_3)) (class a_4 a_6 a_5)) % 14.65/14.90 (size a_2 a_7 a_3)) % 14.65/14.90 (size a_4 a_8 a_5)) % 14.65/14.90 (inertia a_2 a_1 a_3)) % 14.65/14.90 (inertia a_4 a a_5)) % 14.65/14.90 False) % 14.65/14.90 (Eq (greater a_8 a_7) False)) % 14.65/14.90 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.90 Or (Eq (greater a a_1) True) % 14.65/14.90 (Or (Eq (greater a_2 a_3) False) % 14.65/14.90 (Or % 14.65/14.90 (Eq % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And % 14.65/14.90 (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (class a_4 a_8 a_5)) (class a_6 a_8 a_7)) % 14.65/14.90 (size a_4 a_3 a_5)) % 14.65/14.90 (size a_6 a_2 a_7)) % 14.65/14.90 (inertia a_4 a_1 a_5)) % 14.65/14.90 False) % 14.65/14.90 (Eq (inertia a_6 a a_7) False))) % 14.65/14.90 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.90 Or (Eq (greater a a_1) True) % 14.65/14.90 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or % 14.65/14.95 (Eq % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5)) % 14.65/14.95 (size a_6 a_3 a_7)) % 14.65/14.95 (size a_4 a_2 a_5)) % 14.65/14.95 False) % 14.65/14.95 (Eq (inertia a_6 a_1 a_7) False)))) % 14.65/14.95 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.95 Or (Eq (greater a a_1) True) % 14.65/14.95 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or (Eq (inertia a_6 a_1 a_7) False) % 14.65/14.95 (Or % 14.65/14.95 (Eq % 14.65/14.95 (And % 14.65/14.95 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5)) % 14.65/14.95 (size a_6 a_3 a_7)) % 14.65/14.95 False) % 14.65/14.95 (Eq (size a_4 a_2 a_5) False))))) % 14.65/14.95 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.95 Or (Eq (greater a a_1) True) % 14.65/14.95 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or (Eq (inertia a_6 a_1 a_7) False) % 14.65/14.95 (Or (Eq (size a_4 a_2 a_5) False) % 14.65/14.95 (Or % 14.65/14.95 (Eq % 14.65/14.95 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5)) % 14.65/14.95 False) % 14.65/14.95 (Eq (size a_6 a_3 a_7) False)))))) % 14.65/14.95 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.95 Or (Eq (greater a a_1) True) % 14.65/14.95 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or (Eq (inertia a_6 a_1 a_7) False) % 14.65/14.95 (Or (Eq (size a_4 a_2 a_5) False) % 14.65/14.95 (Or (Eq (size a_6 a_3 a_7) False) % 14.65/14.95 (Or (Eq (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) False) % 14.65/14.95 (Eq (class a_4 a_8 a_5) False))))))) % 14.65/14.95 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.95 Or (Eq (greater a a_1) True) % 14.65/14.95 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or (Eq (inertia a_6 a_1 a_7) False) % 14.65/14.95 (Or (Eq (size a_4 a_2 a_5) False) % 14.65/14.95 (Or (Eq (size a_6 a_3 a_7) False) % 14.65/14.95 (Or (Eq (class a_4 a_8 a_5) False) % 14.65/14.95 (Or (Eq (And (organization a_6 a_7) (organization a_4 a_5)) False) (Eq (class a_6 a_8 a_7) False)))))))) % 14.65/14.95 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.65/14.95 Or (Eq (greater a a_1) True) % 14.65/14.95 (Or (Eq (greater a_2 a_3) False) % 14.65/14.95 (Or (Eq (inertia a_4 a a_5) False) % 14.65/14.95 (Or (Eq (inertia a_6 a_1 a_7) False) % 14.65/14.95 (Or (Eq (size a_4 a_2 a_5) False) % 14.65/14.95 (Or (Eq (size a_6 a_3 a_7) False) % 14.65/14.95 (Or (Eq (class a_4 a_8 a_5) False) % 14.65/14.95 (Or (Eq (class a_6 a_8 a_7) False) % 14.65/14.95 (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False))))))))) % 14.65/14.95 Clause #26 (by clausification #[3]): Eq % 14.65/14.95 (∀ (X Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.95 And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 14.65/14.95 (reorganization_free Y T2 T2)) % 14.65/14.95 (class X C T1)) % 14.65/14.95 (class Y C T2)) % 14.65/14.95 (reproducibility X Rp1 T1)) % 14.65/14.95 (reproducibility Y Rp2 T2)) % 14.65/14.95 (size X S1 T1)) % 14.65/14.95 (size Y S2 T2)) % 14.65/14.95 (greater S2 S1) → % 14.65/14.95 greater Rp2 Rp1) % 14.65/14.95 False % 14.65/14.95 Clause #27 (by clausification #[26]): ∀ (a : Iota), % 14.65/14.95 Eq % 14.65/14.95 (Not % 14.65/14.95 (∀ (Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.95 And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And % 14.65/14.95 (And (And (organization (skS.0 1 a) T1) (organization Y T2)) % 14.65/14.95 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/14.95 (reorganization_free Y T2 T2)) % 14.65/14.95 (class (skS.0 1 a) C T1)) % 14.65/14.99 (class Y C T2)) % 14.65/14.99 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/14.99 (reproducibility Y Rp2 T2)) % 14.65/14.99 (size (skS.0 1 a) S1 T1)) % 14.65/14.99 (size Y S2 T2)) % 14.65/14.99 (greater S2 S1) → % 14.65/14.99 greater Rp2 Rp1)) % 14.65/14.99 True % 14.65/14.99 Clause #28 (by clausification #[27]): ∀ (a : Iota), % 14.65/14.99 Eq % 14.65/14.99 (∀ (Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.99 And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And (And (organization (skS.0 1 a) T1) (organization Y T2)) % 14.65/14.99 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/14.99 (reorganization_free Y T2 T2)) % 14.65/14.99 (class (skS.0 1 a) C T1)) % 14.65/14.99 (class Y C T2)) % 14.65/14.99 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/14.99 (reproducibility Y Rp2 T2)) % 14.65/14.99 (size (skS.0 1 a) S1 T1)) % 14.65/14.99 (size Y S2 T2)) % 14.65/14.99 (greater S2 S1) → % 14.65/14.99 greater Rp2 Rp1) % 14.65/14.99 False % 14.65/14.99 Clause #29 (by clausification #[28]): ∀ (a a_1 : Iota), % 14.65/14.99 Eq % 14.65/14.99 (Not % 14.65/14.99 (∀ (C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.99 And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/14.99 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/14.99 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/14.99 (class (skS.0 1 a) C T1)) % 14.65/14.99 (class (skS.0 2 a a_1) C T2)) % 14.65/14.99 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/14.99 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/14.99 (size (skS.0 1 a) S1 T1)) % 14.65/14.99 (size (skS.0 2 a a_1) S2 T2)) % 14.65/14.99 (greater S2 S1) → % 14.65/14.99 greater Rp2 Rp1)) % 14.65/14.99 True % 14.65/14.99 Clause #30 (by clausification #[29]): ∀ (a a_1 : Iota), % 14.65/14.99 Eq % 14.65/14.99 (∀ (C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.99 And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/14.99 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/14.99 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/14.99 (class (skS.0 1 a) C T1)) % 14.65/14.99 (class (skS.0 2 a a_1) C T2)) % 14.65/14.99 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/14.99 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/14.99 (size (skS.0 1 a) S1 T1)) % 14.65/14.99 (size (skS.0 2 a a_1) S2 T2)) % 14.65/14.99 (greater S2 S1) → % 14.65/14.99 greater Rp2 Rp1) % 14.65/14.99 False % 14.65/14.99 Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 : Iota), % 14.65/14.99 Eq % 14.65/14.99 (Not % 14.65/14.99 (∀ (Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.99 And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/14.99 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/14.99 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/14.99 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/14.99 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.65/14.99 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/14.99 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/14.99 (size (skS.0 1 a) S1 T1)) % 14.65/14.99 (size (skS.0 2 a a_1) S2 T2)) % 14.65/14.99 (greater S2 S1) → % 14.65/14.99 greater Rp2 Rp1)) % 14.65/14.99 True % 14.65/14.99 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 : Iota), % 14.65/14.99 Eq % 14.65/14.99 (∀ (Rp1 Rp2 S1 S2 T1 T2 : Iota), % 14.65/14.99 And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And % 14.65/14.99 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/15.04 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/15.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/15.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/15.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.65/15.04 (reproducibility (skS.0 1 a) Rp1 T1)) % 14.65/15.04 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/15.04 (size (skS.0 1 a) S1 T1)) % 14.65/15.04 (size (skS.0 2 a a_1) S2 T2)) % 14.65/15.04 (greater S2 S1) → % 14.65/15.04 greater Rp2 Rp1) % 14.65/15.04 False % 14.65/15.04 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 : Iota), % 14.65/15.04 Eq % 14.65/15.04 (Not % 14.65/15.04 (∀ (Rp2 S1 S2 T1 T2 : Iota), % 14.65/15.04 And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/15.04 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/15.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/15.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/15.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.65/15.04 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.65/15.04 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/15.04 (size (skS.0 1 a) S1 T1)) % 14.65/15.04 (size (skS.0 2 a a_1) S2 T2)) % 14.65/15.04 (greater S2 S1) → % 14.65/15.04 greater Rp2 (skS.0 4 a a_1 a_2 a_3))) % 14.65/15.04 True % 14.65/15.04 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 a_3 : Iota), % 14.65/15.04 Eq % 14.65/15.04 (∀ (Rp2 S1 S2 T1 T2 : Iota), % 14.65/15.04 And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/15.04 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/15.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/15.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/15.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.65/15.04 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.65/15.04 (reproducibility (skS.0 2 a a_1) Rp2 T2)) % 14.65/15.04 (size (skS.0 1 a) S1 T1)) % 14.65/15.04 (size (skS.0 2 a a_1) S2 T2)) % 14.65/15.04 (greater S2 S1) → % 14.65/15.04 greater Rp2 (skS.0 4 a a_1 a_2 a_3)) % 14.65/15.04 False % 14.65/15.04 Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.65/15.04 Eq % 14.65/15.04 (Not % 14.65/15.04 (∀ (S1 S2 T1 T2 : Iota), % 14.65/15.04 And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/15.04 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/15.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/15.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/15.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.65/15.04 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.65/15.04 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.65/15.04 (size (skS.0 1 a) S1 T1)) % 14.65/15.04 (size (skS.0 2 a a_1) S2 T2)) % 14.65/15.04 (greater S2 S1) → % 14.65/15.04 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))) % 14.65/15.04 True % 14.65/15.04 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.65/15.04 Eq % 14.65/15.04 (∀ (S1 S2 T1 T2 : Iota), % 14.65/15.04 And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And % 14.65/15.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.65/15.04 (reorganization_free (skS.0 1 a) T1 T1)) % 14.65/15.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.65/15.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.65/15.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.09 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.79/15.09 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.09 (size (skS.0 1 a) S1 T1)) % 14.79/15.09 (size (skS.0 2 a a_1) S2 T2)) % 14.79/15.09 (greater S2 S1) → % 14.79/15.09 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 14.79/15.09 False % 14.79/15.09 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.79/15.09 Eq % 14.79/15.09 (Not % 14.79/15.09 (∀ (S2 T1 T2 : Iota), % 14.79/15.09 And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.79/15.09 (reorganization_free (skS.0 1 a) T1 T1)) % 14.79/15.09 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.79/15.09 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.79/15.09 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.09 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.79/15.09 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.09 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 14.79/15.09 (size (skS.0 2 a a_1) S2 T2)) % 14.79/15.09 (greater S2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.79/15.09 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))) % 14.79/15.09 True % 14.79/15.09 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.79/15.09 Eq % 14.79/15.09 (∀ (S2 T1 T2 : Iota), % 14.79/15.09 And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.79/15.09 (reorganization_free (skS.0 1 a) T1 T1)) % 14.79/15.09 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.79/15.09 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.79/15.09 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.09 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.79/15.09 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.09 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 14.79/15.09 (size (skS.0 2 a a_1) S2 T2)) % 14.79/15.09 (greater S2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.79/15.09 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 14.79/15.09 False % 14.79/15.09 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.79/15.09 Eq % 14.79/15.09 (Not % 14.79/15.09 (∀ (T1 T2 : Iota), % 14.79/15.09 And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.79/15.09 (reorganization_free (skS.0 1 a) T1 T1)) % 14.79/15.09 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.79/15.09 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.79/15.09 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.09 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.79/15.09 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.09 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 14.79/15.09 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 14.79/15.09 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.79/15.09 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))) % 14.79/15.09 True % 14.79/15.09 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.79/15.09 Eq % 14.79/15.09 (∀ (T1 T2 : Iota), % 14.79/15.09 And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And % 14.79/15.09 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 14.79/15.09 (reorganization_free (skS.0 1 a) T1 T1)) % 14.79/15.14 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.79/15.14 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 14.79/15.14 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.14 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 14.79/15.14 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.14 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 14.79/15.14 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 14.79/15.14 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.79/15.14 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 14.79/15.14 False % 14.79/15.14 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.79/15.14 Eq % 14.79/15.14 (Not % 14.79/15.14 (∀ (T2 : Iota), % 14.79/15.14 And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And % 14.79/15.14 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.79/15.14 (organization (skS.0 2 a a_1) T2)) % 14.79/15.14 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.79/15.14 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.79/15.14 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.79/15.14 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.79/15.14 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.79/15.14 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.79/15.14 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.79/15.14 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.79/15.14 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 14.79/15.14 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.89/15.14 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))) % 14.89/15.14 True % 14.89/15.14 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.89/15.14 Eq % 14.89/15.14 (∀ (T2 : Iota), % 14.89/15.14 And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.89/15.14 (organization (skS.0 2 a a_1) T2)) % 14.89/15.14 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.89/15.14 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.14 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 14.89/15.14 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.14 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 14.89/15.14 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.14 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 14.89/15.14 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.14 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 14.89/15.14 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.89/15.14 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 14.89/15.14 False % 14.89/15.14 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.89/15.14 Eq % 14.89/15.14 (Not % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And % 14.89/15.14 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.89/15.14 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.14 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.89/15.18 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 14.89/15.18 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 14.89/15.18 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.89/15.18 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))) % 14.89/15.18 True % 14.89/15.18 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.89/15.18 Eq % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.89/15.18 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.89/15.18 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 14.89/15.18 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) → % 14.89/15.18 greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 14.89/15.18 False % 14.89/15.18 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.89/15.18 Eq % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And % 14.89/15.18 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.89/15.18 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.89/15.18 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 14.89/15.18 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.89/15.18 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.89/15.18 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5))) % 14.95/15.23 True % 14.95/15.23 Clause #46 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) False % 14.95/15.23 Clause #47 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.95/15.23 Eq (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) True % 14.95/15.23 Clause #48 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 14.95/15.23 Eq % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 14.95/15.23 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 14.95/15.23 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.95/15.23 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 14.95/15.23 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.95/15.23 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.95/15.23 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 14.95/15.23 (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 14.95/15.23 True % 14.95/15.23 Clause #49 (by superposition #[47, 25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 14.95/15.23 Or (Eq (greater a a_1) True) % 14.95/15.23 (Or (Eq True False) % 14.95/15.23 (Or (Eq (inertia a_2 a a_3) False) % 14.95/15.23 (Or (Eq (inertia a_4 a_1 a_5) False) % 14.95/15.23 (Or (Eq (size a_2 (skS.0 7 a_6 a_7 a_8 a_9 a_10 a_11 a_12) a_3) False) % 14.95/15.23 (Or (Eq (size a_4 (skS.0 6 a_6 a_7 a_8 a_9 a_10 a_11) a_5) False) % 14.95/15.23 (Or (Eq (class a_2 a_13 a_3) False) % 14.95/15.23 (Or (Eq (class a_4 a_13 a_5) False) % 14.95/15.23 (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False))))))))) % 14.95/15.23 Clause #50 (by clausification #[1]): ∀ (a : Iota), % 14.95/15.23 Eq % 14.95/15.23 (∀ (Y T1 T2 Rp1 Rp2 I1 I2 : Iota), % 14.95/15.23 And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And (And (And (organization a T1) (organization Y T2)) (reorganization_free a T1 T1)) % 14.95/15.23 (reorganization_free Y T2 T2)) % 14.95/15.23 (reproducibility a Rp1 T1)) % 14.95/15.23 (reproducibility Y Rp2 T2)) % 14.95/15.23 (inertia a I1 T1)) % 14.95/15.23 (inertia Y I2 T2) → % 14.95/15.23 Iff (greater Rp2 Rp1) (greater I2 I1)) % 14.95/15.23 True % 14.95/15.23 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 14.95/15.23 Eq % 14.95/15.23 (∀ (T1 T2 Rp1 Rp2 I1 I2 : Iota), % 14.95/15.23 And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 14.95/15.23 (reorganization_free a_1 T2 T2)) % 14.95/15.23 (reproducibility a Rp1 T1)) % 14.95/15.23 (reproducibility a_1 Rp2 T2)) % 14.95/15.23 (inertia a I1 T1)) % 14.95/15.23 (inertia a_1 I2 T2) → % 14.95/15.23 Iff (greater Rp2 Rp1) (greater I2 I1)) % 14.95/15.23 True % 14.95/15.23 Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 : Iota), % 14.95/15.23 Eq % 14.95/15.23 (∀ (T2 Rp1 Rp2 I1 I2 : Iota), % 14.95/15.23 And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And % 14.95/15.23 (And (And (And (organization a a_1) (organization a_2 T2)) (reorganization_free a a_1 a_1)) % 14.95/15.23 (reorganization_free a_2 T2 T2)) % 14.95/15.23 (reproducibility a Rp1 a_1)) % 14.95/15.23 (reproducibility a_2 Rp2 T2)) % 14.95/15.23 (inertia a I1 a_1)) % 14.95/15.23 (inertia a_2 I2 T2) → % 14.95/15.23 Iff (greater Rp2 Rp1) (greater I2 I1)) % 14.95/15.23 True % 14.95/15.23 Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 : Iota), % 14.95/15.27 Eq % 14.95/15.27 (∀ (Rp1 Rp2 I1 I2 : Iota), % 14.95/15.27 And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a Rp1 a_1)) % 14.95/15.27 (reproducibility a_2 Rp2 a_3)) % 14.95/15.27 (inertia a I1 a_1)) % 14.95/15.27 (inertia a_2 I2 a_3) → % 14.95/15.27 Iff (greater Rp2 Rp1) (greater I2 I1)) % 14.95/15.27 True % 14.95/15.27 Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 14.95/15.27 Eq % 14.95/15.27 (∀ (Rp2 I1 I2 : Iota), % 14.95/15.27 And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 Rp2 a_3)) % 14.95/15.27 (inertia a I1 a_1)) % 14.95/15.27 (inertia a_2 I2 a_3) → % 14.95/15.27 Iff (greater Rp2 a_4) (greater I2 I1)) % 14.95/15.27 True % 14.95/15.27 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 14.95/15.27 Eq % 14.95/15.27 (∀ (I1 I2 : Iota), % 14.95/15.27 And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 a_5 a_3)) % 14.95/15.27 (inertia a I1 a_1)) % 14.95/15.27 (inertia a_2 I2 a_3) → % 14.95/15.27 Iff (greater a_5 a_4) (greater I2 I1)) % 14.95/15.27 True % 14.95/15.27 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 14.95/15.27 Eq % 14.95/15.27 (∀ (I2 : Iota), % 14.95/15.27 And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 a_5 a_3)) % 14.95/15.27 (inertia a a_6 a_1)) % 14.95/15.27 (inertia a_2 I2 a_3) → % 14.95/15.27 Iff (greater a_5 a_4) (greater I2 a_6)) % 14.95/15.27 True % 14.95/15.27 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.95/15.27 Eq % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 a_5 a_3)) % 14.95/15.27 (inertia a a_6 a_1)) % 14.95/15.27 (inertia a_2 a_7 a_3) → % 14.95/15.27 Iff (greater a_5 a_4) (greater a_7 a_6)) % 14.95/15.27 True % 14.95/15.27 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.95/15.27 Or % 14.95/15.27 (Eq % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 a_5 a_3)) % 14.95/15.27 (inertia a a_6 a_1)) % 14.95/15.27 (inertia a_2 a_7 a_3)) % 14.95/15.27 False) % 14.95/15.27 (Eq (Iff (greater a_5 a_4) (greater a_7 a_6)) True) % 14.95/15.27 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.95/15.27 Or (Eq (Iff (greater a a_1) (greater a_2 a_3)) True) % 14.95/15.27 (Or % 14.95/15.27 (Eq % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (reorganization_free a_4 a_5 a_5)) % 14.95/15.27 (reorganization_free a_6 a_7 a_7)) % 14.95/15.27 (reproducibility a_4 a_1 a_5)) % 14.95/15.27 (reproducibility a_6 a a_7)) % 14.95/15.27 (inertia a_4 a_3 a_5)) % 14.95/15.27 False) % 14.95/15.27 (Eq (inertia a_6 a_2 a_7) False)) % 14.95/15.27 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 14.95/15.27 Or % 14.95/15.27 (Eq % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And % 14.95/15.27 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 14.95/15.27 (reorganization_free a_2 a_3 a_3)) % 14.95/15.27 (reproducibility a a_4 a_1)) % 14.95/15.27 (reproducibility a_2 a_5 a_3)) % 14.95/15.27 (inertia a a_6 a_1)) % 15.05/15.32 False) % 15.05/15.32 (Or (Eq (inertia a_2 a_7 a_3) False) (Or (Eq (greater a_5 a_4) True) (Eq (greater a_7 a_6) False))) % 15.05/15.32 Clause #62 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or % 15.05/15.32 (Eq % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And (And (And (organization a_6 a_7) (organization a a_2)) (reorganization_free a_6 a_7 a_7)) % 15.05/15.32 (reorganization_free a a_2 a_2)) % 15.05/15.32 (reproducibility a_6 a_4 a_7)) % 15.05/15.32 (reproducibility a a_3 a_2)) % 15.05/15.32 False) % 15.05/15.32 (Eq (inertia a_6 a_5 a_7) False)))) % 15.05/15.32 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or (Eq (inertia a_6 a_5 a_7) False) % 15.05/15.32 (Or % 15.05/15.32 (Eq % 15.05/15.32 (And % 15.05/15.32 (And (And (And (organization a_6 a_7) (organization a a_2)) (reorganization_free a_6 a_7 a_7)) % 15.05/15.32 (reorganization_free a a_2 a_2)) % 15.05/15.32 (reproducibility a_6 a_4 a_7)) % 15.05/15.32 False) % 15.05/15.32 (Eq (reproducibility a a_3 a_2) False))))) % 15.05/15.32 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or (Eq (inertia a_6 a_5 a_7) False) % 15.05/15.32 (Or (Eq (reproducibility a a_3 a_2) False) % 15.05/15.32 (Or % 15.05/15.32 (Eq % 15.05/15.32 (And (And (And (organization a_6 a_7) (organization a a_2)) (reorganization_free a_6 a_7 a_7)) % 15.05/15.32 (reorganization_free a a_2 a_2)) % 15.05/15.32 False) % 15.05/15.32 (Eq (reproducibility a_6 a_4 a_7) False)))))) % 15.05/15.32 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or (Eq (inertia a_6 a_5 a_7) False) % 15.05/15.32 (Or (Eq (reproducibility a a_3 a_2) False) % 15.05/15.32 (Or (Eq (reproducibility a_6 a_4 a_7) False) % 15.05/15.32 (Or (Eq (And (And (organization a_6 a_7) (organization a a_2)) (reorganization_free a_6 a_7 a_7)) False) % 15.05/15.32 (Eq (reorganization_free a a_2 a_2) False))))))) % 15.05/15.32 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or (Eq (inertia a_6 a_5 a_7) False) % 15.05/15.32 (Or (Eq (reproducibility a a_3 a_2) False) % 15.05/15.32 (Or (Eq (reproducibility a_6 a_4 a_7) False) % 15.05/15.32 (Or (Eq (reorganization_free a a_2 a_2) False) % 15.05/15.32 (Or (Eq (And (organization a_6 a_7) (organization a a_2)) False) % 15.05/15.32 (Eq (reorganization_free a_6 a_7 a_7) False)))))))) % 15.05/15.32 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.32 Or (Eq (inertia a a_1 a_2) False) % 15.05/15.32 (Or (Eq (greater a_3 a_4) True) % 15.05/15.32 (Or (Eq (greater a_1 a_5) False) % 15.05/15.32 (Or (Eq (inertia a_6 a_5 a_7) False) % 15.05/15.32 (Or (Eq (reproducibility a a_3 a_2) False) % 15.05/15.32 (Or (Eq (reproducibility a_6 a_4 a_7) False) % 15.05/15.32 (Or (Eq (reorganization_free a a_2 a_2) False) % 15.05/15.32 (Or (Eq (reorganization_free a_6 a_7 a_7) False) % 15.05/15.32 (Or (Eq (organization a_6 a_7) False) (Eq (organization a a_2) False))))))))) % 15.05/15.32 Clause #68 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.32 Eq (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True % 15.05/15.32 Clause #69 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.32 Eq % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And % 15.05/15.32 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.05/15.32 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.32 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.05/15.38 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.05/15.38 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 True % 15.05/15.38 Clause #76 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 15.05/15.38 Or (Eq (greater a a_1) True) % 15.05/15.38 (Or (Eq (inertia a_2 a a_3) False) % 15.05/15.38 (Or (Eq (inertia a_4 a_1 a_5) False) % 15.05/15.38 (Or (Eq (size a_2 (skS.0 7 a_6 a_7 a_8 a_9 a_10 a_11 a_12) a_3) False) % 15.05/15.38 (Or (Eq (size a_4 (skS.0 6 a_6 a_7 a_8 a_9 a_10 a_11) a_5) False) % 15.05/15.38 (Or (Eq (class a_2 a_13 a_3) False) % 15.05/15.38 (Or (Eq (class a_4 a_13 a_5) False) % 15.05/15.38 (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False)))))))) % 15.05/15.38 Clause #77 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.38 Eq (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 15.05/15.38 Clause #78 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.38 Eq % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.05/15.38 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.05/15.38 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.05/15.38 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 True % 15.05/15.38 Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.38 Eq (reproducibility (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True % 15.05/15.38 Clause #80 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.38 Eq % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.05/15.38 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.05/15.38 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.05/15.38 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.05/15.38 (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.05/15.38 True % 15.05/15.38 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.05/15.38 Eq (reproducibility (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 15.05/15.38 Clause #82 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.05/15.38 Eq % 15.05/15.38 (And % 15.05/15.38 (And % 15.05/15.38 (And % 15.15/15.43 (And % 15.15/15.43 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.15/15.43 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.15/15.43 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 True % 15.15/15.43 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True % 15.15/15.43 Clause #84 (by clausification #[82]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq % 15.15/15.43 (And % 15.15/15.43 (And % 15.15/15.43 (And % 15.15/15.43 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.15/15.43 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.15/15.43 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 True % 15.15/15.43 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.15/15.43 Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 15.15/15.43 Clause #86 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq % 15.15/15.43 (And % 15.15/15.43 (And % 15.15/15.43 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 15.15/15.43 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.15/15.43 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 True % 15.15/15.43 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq % 15.15/15.43 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.15/15.43 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.15/15.43 True % 15.15/15.43 Clause #88 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq % 15.15/15.43 (And % 15.15/15.43 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 15.15/15.43 True % 15.15/15.43 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.15/15.43 Eq (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 True % 15.15/15.43 Clause #90 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq % 15.15/15.43 (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.43 (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))) % 15.15/15.43 True % 15.15/15.43 Clause #91 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True % 15.15/15.43 Clause #92 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 15.15/15.43 Clause #93 (by superposition #[91, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 15.15/15.43 Or (Eq True False) % 15.15/15.43 (Eq % 15.15/15.43 (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.15/15.43 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.15/15.43 True) % 15.15/15.43 Clause #94 (by superposition #[92, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.43 Or (Eq True False) % 15.15/15.43 (Eq % 15.15/15.48 (inertia (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8) % 15.15/15.48 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.48 True) % 15.15/15.48 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 15.15/15.48 Eq % 15.15/15.48 (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.15/15.48 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.15/15.48 True % 15.15/15.48 Clause #96 (by superposition #[95, 67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : Iota), % 15.15/15.48 Or (Eq True False) % 15.15/15.48 (Or (Eq (greater a a_1) True) % 15.15/15.48 (Or (Eq (greater (skS.0 0 (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.15/15.48 (Or (Eq (inertia a_13 a_12 a_14) False) % 15.15/15.48 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.15/15.48 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 15.15/15.48 (Or % 15.15/15.48 (Eq % 15.15/15.48 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.15/15.48 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.15/15.48 False) % 15.15/15.48 (Or (Eq (reorganization_free a_13 a_14 a_14) False) % 15.15/15.48 (Or (Eq (organization a_13 a_14) False) % 15.15/15.48 (Eq (organization (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False))))))))) % 15.15/15.48 Clause #98 (by superposition #[95, 76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota), % 15.15/15.48 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True) % 15.15/15.48 (Or (Eq True False) % 15.15/15.48 (Or (Eq (inertia a_11 a_10 a_12) False) % 15.15/15.48 (Or % 15.15/15.48 (Eq % 15.15/15.48 (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19) % 15.15/15.48 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.15/15.48 False) % 15.15/15.48 (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False) % 15.15/15.48 (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.15/15.48 (Or (Eq (class a_11 a_20 a_12) False) % 15.15/15.48 (Or (Eq (organization a_11 a_12) False) % 15.15/15.48 (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)))))))) % 15.15/15.48 Clause #99 (by clausification #[94]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 15.15/15.48 Eq % 15.15/15.48 (inertia (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8) % 15.15/15.48 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.15/15.48 True % 15.15/15.48 Clause #118 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : Iota), % 15.15/15.48 Or (Eq (greater a a_1) True) % 15.15/15.48 (Or (Eq (greater (skS.0 0 (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.15/15.48 (Or (Eq (inertia a_13 a_12 a_14) False) % 15.15/15.48 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.15/15.48 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 15.15/15.48 (Or % 15.15/15.48 (Eq % 15.15/15.48 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.15/15.48 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.15/15.48 False) % 15.15/15.48 (Or (Eq (reorganization_free a_13 a_14 a_14) False) % 15.15/15.48 (Or (Eq (organization a_13 a_14) False) % 15.15/15.48 (Eq (organization (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False)))))))) % 15.15/15.48 Clause #119 (by forward demodulation #[118, 91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : Iota), % 15.15/15.48 Or (Eq (greater a a_1) True) % 15.15/15.48 (Or (Eq (greater (skS.0 0 (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.15/15.48 (Or (Eq (inertia a_13 a_12 a_14) False) % 15.15/15.48 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.15/15.48 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 15.15/15.48 (Or % 15.15/15.48 (Eq % 15.15/15.48 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.25/15.54 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.25/15.54 False) % 15.25/15.54 (Or (Eq (reorganization_free a_13 a_14 a_14) False) % 15.25/15.54 (Or (Eq (organization a_13 a_14) False) (Eq True False)))))))) % 15.25/15.54 Clause #120 (by clausification #[119]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 : Iota), % 15.25/15.54 Or (Eq (greater a a_1) True) % 15.25/15.54 (Or (Eq (greater (skS.0 0 (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.25/15.54 (Or (Eq (inertia a_13 a_12 a_14) False) % 15.25/15.54 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.25/15.54 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.25/15.54 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.25/15.54 False) % 15.25/15.54 (Or (Eq (reorganization_free a_13 a_14 a_14) False) (Eq (organization a_13 a_14) False))))))) % 15.25/15.54 Clause #128 (by clausification #[98]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota), % 15.25/15.54 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True) % 15.25/15.54 (Or (Eq (inertia a_11 a_10 a_12) False) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19) % 15.25/15.54 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.25/15.54 False) % 15.25/15.54 (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False) % 15.25/15.54 (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.25/15.54 (Or (Eq (class a_11 a_20 a_12) False) % 15.25/15.54 (Or (Eq (organization a_11 a_12) False) % 15.25/15.54 (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False))))))) % 15.25/15.54 Clause #129 (by forward demodulation #[128, 91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota), % 15.25/15.54 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True) % 15.25/15.54 (Or (Eq (inertia a_11 a_10 a_12) False) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19) % 15.25/15.54 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.25/15.54 False) % 15.25/15.54 (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False) % 15.25/15.54 (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.25/15.54 (Or (Eq (class a_11 a_20 a_12) False) (Or (Eq (organization a_11 a_12) False) (Eq True False))))))) % 15.25/15.54 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota), % 15.25/15.54 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True) % 15.25/15.54 (Or (Eq (inertia a_11 a_10 a_12) False) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19) % 15.25/15.54 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.25/15.54 False) % 15.25/15.54 (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False) % 15.25/15.54 (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.25/15.54 (Or (Eq (class a_11 a_20 a_12) False) (Eq (organization a_11 a_12) False)))))) % 15.25/15.54 Clause #132 (by superposition #[130, 99]): ∀ % 15.25/15.54 (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 : % 15.25/15.54 Iota), % 15.25/15.54 Or % 15.25/15.54 (Eq % 15.25/15.54 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.25/15.54 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.25/15.54 True) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.25/15.54 False) % 15.25/15.54 (Or % 15.25/15.54 (Eq % 15.25/15.54 (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24) % 15.25/15.54 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) % 15.35/15.60 False) % 15.35/15.60 (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.60 (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.60 (Or (Eq (organization (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.60 (Eq False True)))))) % 15.35/15.60 Clause #136 (by clausification #[132]): ∀ % 15.35/15.60 (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 : % 15.35/15.60 Iota), % 15.35/15.60 Or % 15.35/15.60 (Eq % 15.35/15.60 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.60 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.35/15.60 True) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.35/15.60 False) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24) % 15.35/15.60 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) % 15.35/15.60 False) % 15.35/15.60 (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.60 (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.60 (Eq (organization (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False))))) % 15.35/15.60 Clause #137 (by forward demodulation #[136, 92]): ∀ % 15.35/15.60 (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 : % 15.35/15.60 Iota), % 15.35/15.60 Or % 15.35/15.60 (Eq % 15.35/15.60 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.60 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.35/15.60 True) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.35/15.60 False) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24) % 15.35/15.60 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) % 15.35/15.60 False) % 15.35/15.60 (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.60 (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.60 (Eq True False))))) % 15.35/15.60 Clause #138 (by clausification #[137]): ∀ % 15.35/15.60 (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 : % 15.35/15.60 Iota), % 15.35/15.60 Or % 15.35/15.60 (Eq % 15.35/15.60 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.60 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.35/15.60 True) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.35/15.60 False) % 15.35/15.60 (Or % 15.35/15.60 (Eq % 15.35/15.60 (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24) % 15.35/15.60 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) % 15.35/15.60 False) % 15.35/15.60 (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.60 (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)))) % 15.35/15.60 Clause #139 (by superposition #[138, 68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 : Iota), % 15.35/15.60 Or % 15.35/15.60 (Eq % 15.35/15.60 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.60 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.35/15.60 True) % 15.35/15.60 (Or % 15.35/15.60 (Eq (size (skS.0 1 a_10) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.60 (Or (Eq (class (skS.0 2 a a_1) a_19 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.60 (Or (Eq (class (skS.0 1 a_10) a_19 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) (Eq False True)))) % 15.35/15.60 Clause #143 (by clausification #[139]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 : Iota), % 15.35/15.60 Or % 15.35/15.60 (Eq % 15.35/15.60 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)) % 15.35/15.66 True) % 15.35/15.66 (Or % 15.35/15.66 (Eq (size (skS.0 1 a_10) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) % 15.35/15.66 (Or (Eq (class (skS.0 2 a a_1) a_19 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.66 (Eq (class (skS.0 1 a_10) a_19 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False))) % 15.35/15.66 Clause #144 (by superposition #[143, 77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 15.35/15.66 Or % 15.35/15.66 (Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True) % 15.35/15.66 (Or (Eq (class (skS.0 2 a a_1) a_13 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.66 (Or (Eq (class (skS.0 1 a) a_13 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False) (Eq False True))) % 15.35/15.66 Clause #145 (by clausification #[144]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota), % 15.35/15.66 Or % 15.35/15.66 (Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True) % 15.35/15.66 (Or (Eq (class (skS.0 2 a a_1) a_13 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False) % 15.35/15.66 (Eq (class (skS.0 1 a) a_13 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False)) % 15.35/15.66 Clause #146 (by superposition #[145, 83]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.35/15.66 Or % 15.35/15.66 (Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True) % 15.35/15.66 (Or (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False) (Eq False True)) % 15.35/15.66 Clause #147 (by clausification #[146]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.35/15.66 Or % 15.35/15.66 (Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True) % 15.35/15.66 (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False) % 15.35/15.66 Clause #148 (by forward demodulation #[147, 85]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.35/15.66 Or % 15.35/15.66 (Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True) % 15.35/15.66 (Eq True False) % 15.35/15.66 Clause #149 (by clausification #[148]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.35/15.66 Eq % 15.35/15.66 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) % 15.35/15.66 (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12)) % 15.35/15.66 True % 15.35/15.66 Clause #150 (by superposition #[149, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 : Iota), % 15.35/15.66 Or (Eq (greater a a_1) True) % 15.35/15.66 (Or (Eq True False) % 15.35/15.66 (Or (Eq (inertia a_2 (skS.0 0 (skS.0 1 a_3) (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.35/15.66 (Or (Eq (reproducibility (skS.0 2 a_3 a_4) a (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15)) False) % 15.35/15.66 (Or (Eq (reproducibility a_2 a_1 a_12) False) % 15.35/15.66 (Or % 15.35/15.66 (Eq % 15.35/15.66 (reorganization_free (skS.0 2 a_3 a_4) (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15) % 15.35/15.66 (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15)) % 15.35/15.66 False) % 15.35/15.66 (Or (Eq (reorganization_free a_2 a_12 a_12) False) (Eq (organization a_2 a_12) False))))))) % 15.35/15.66 Clause #157 (by clausification #[150]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 : Iota), % 15.35/15.66 Or (Eq (greater a a_1) True) % 15.35/15.66 (Or (Eq (inertia a_2 (skS.0 0 (skS.0 1 a_3) (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 15.35/15.66 (Or (Eq (reproducibility (skS.0 2 a_3 a_4) a (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15)) False) % 15.35/15.66 (Or (Eq (reproducibility a_2 a_1 a_12) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a_3 a_4) (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15) % 15.45/15.71 (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_13 a_14 a_15)) % 15.45/15.71 False) % 15.45/15.71 (Or (Eq (reorganization_free a_2 a_12 a_12) False) (Eq (organization a_2 a_12) False)))))) % 15.45/15.71 Clause #158 (by superposition #[157, 99]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.45/15.71 Or (Eq (greater a a_1) True) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.45/15.71 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.45/15.71 False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12) % 15.45/15.71 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) % 15.45/15.71 False) % 15.45/15.71 (Or (Eq (organization (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False) (Eq False True)))))) % 15.45/15.71 Clause #162 (by clausification #[158]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.45/15.71 Or (Eq (greater a a_1) True) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.45/15.71 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.45/15.71 False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12) % 15.45/15.71 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) % 15.45/15.71 False) % 15.45/15.71 (Eq (organization (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False))))) % 15.45/15.71 Clause #163 (by forward demodulation #[162, 92]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.45/15.71 Or (Eq (greater a a_1) True) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.45/15.71 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.45/15.71 False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12) % 15.45/15.71 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) % 15.45/15.71 False) % 15.45/15.71 (Eq True False))))) % 15.45/15.71 Clause #164 (by clausification #[163]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota), % 15.45/15.71 Or (Eq (greater a a_1) True) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 15.45/15.71 (skS.0 9 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 15.45/15.71 False) % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 1 a_2) (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12) % 15.45/15.71 (skS.0 8 a_2 a_3 a_4 a_5 a_6 a_7 a_11 a_12)) % 15.45/15.71 False)))) % 15.45/15.71 Clause #165 (by superposition #[164, 79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 15.45/15.71 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True) % 15.45/15.71 (Or (Eq (reproducibility (skS.0 1 a) a_5 (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8)) False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.71 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_6 a_9 a_10 a_11) % 15.45/15.71 (skS.0 9 a a_1 a_2 a_3 a_4 a_6 a_9 a_10 a_11)) % 15.45/15.71 False) % 15.45/15.71 (Or % 15.45/15.71 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8)) % 15.45/15.75 False) % 15.45/15.75 (Eq False True)))) % 15.45/15.75 Clause #166 (by clausification #[165]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 15.45/15.75 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True) % 15.45/15.75 (Or (Eq (reproducibility (skS.0 1 a) a_5 (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8)) False) % 15.45/15.75 (Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_6 a_9 a_10 a_11) % 15.45/15.75 (skS.0 9 a a_1 a_2 a_3 a_4 a_6 a_9 a_10 a_11)) % 15.45/15.75 False) % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_6 a_7 a_8)) % 15.45/15.75 False))) % 15.45/15.75 Clause #167 (by superposition #[166, 81]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 15.45/15.75 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) True) % 15.45/15.75 (Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.45/15.75 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.45/15.75 False) % 15.45/15.75 (Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)) % 15.45/15.75 False) % 15.45/15.75 (Eq False True))) % 15.45/15.75 Clause #168 (by clausification #[167]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 15.45/15.75 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) True) % 15.45/15.75 (Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.45/15.75 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.45/15.75 False) % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)) % 15.45/15.75 False)) % 15.45/15.75 Clause #169 (by forward demodulation #[168, 46]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 15.45/15.75 Or (Eq False True) % 15.45/15.75 (Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.45/15.75 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.45/15.75 False) % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)) % 15.45/15.75 False)) % 15.45/15.75 Clause #170 (by clausification #[169]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 15.45/15.75 Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) % 15.45/15.75 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) % 15.45/15.75 False) % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10) % 15.45/15.75 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)) % 15.45/15.75 False) % 15.45/15.75 Clause #171 (by superposition #[170, 87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.45/15.75 Or % 15.45/15.75 (Eq % 15.45/15.75 (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.45/15.75 False) % 15.45/15.75 (Eq False True) % 15.45/15.75 Clause #172 (by clausification #[171]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 15.45/15.75 Eq (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) % 15.45/15.75 False % 15.45/15.75 Clause #173 (by superposition #[172, 89]): Eq False True % 15.45/15.75 Clause #174 (by clausification #[173]): False % 15.45/15.75 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------