%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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 7.65s 7.94s % Output : Proof 8.25s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : MGT010+1 : TPTP v9.3.0. Released v2.0.0. % 0.00/0.04 % Command : duper %s % 0.09/0.35 % Computer : n026.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 11:50:42 UTC 2026 % 0.09/0.36 % CPUTime : % 7.65/7.94 SZS status Theorem for theBenchmark.p % 7.65/7.94 SZS output start Proof for theBenchmark.p % 7.65/7.94 Clause #0 (by assumption #[]): Eq (∀ (X T : Iota), organization X T → Exists fun Rp => reproducibility X Rp T) True % 7.65/7.94 Clause #1 (by assumption #[]): Eq % 7.65/7.94 (∀ (X Y T1 T2 R1 R2 A1 A2 Rp1 Rp2 : Iota), % 7.65/7.94 And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And (And (And (And (organization X T1) (organization Y T2)) (reliability X R1 T1)) (reliability Y R2 T2)) % 7.65/7.94 (accountability X A1 T1)) % 7.65/7.94 (accountability Y A2 T2)) % 7.65/7.94 (reproducibility X Rp1 T1)) % 7.65/7.94 (reproducibility Y Rp2 T2) → % 7.65/7.94 Iff (greater Rp2 Rp1) (And (greater R2 R1) (greater A2 A1))) % 7.65/7.94 True % 7.65/7.94 Clause #2 (by assumption #[]): Eq % 7.65/7.94 (∀ (X Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 7.65/7.94 And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 7.65/7.94 (reorganization_free Y T2 T2)) % 7.65/7.94 (class X C T1)) % 7.65/7.94 (class Y C T2)) % 7.65/7.94 (reproducibility X Rp1 T1)) % 7.65/7.94 (reproducibility Y Rp2 T2)) % 7.65/7.94 (size X S1 T1)) % 7.65/7.94 (size Y S2 T2)) % 7.65/7.94 (greater S2 S1) → % 7.65/7.94 greater Rp2 Rp1) % 7.65/7.94 True % 7.65/7.94 Clause #3 (by assumption #[]): Eq % 7.65/7.94 (Not % 7.65/7.94 (∀ (X Y C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/7.94 And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 7.65/7.94 (reorganization_free Y T2 T2)) % 7.65/7.94 (class X C T1)) % 7.65/7.94 (class Y C T2)) % 7.65/7.94 (reliability X R1 T1)) % 7.65/7.94 (reliability Y R2 T2)) % 7.65/7.94 (accountability X A1 T1)) % 7.65/7.94 (accountability Y A2 T2)) % 7.65/7.94 (size X S1 T1)) % 7.65/7.94 (size Y S2 T2)) % 7.65/7.94 (greater S2 S1) → % 7.65/7.94 And (greater R2 R1) (greater A2 A1))) % 7.65/7.94 True % 7.65/7.94 Clause #4 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (T : Iota), organization a T → Exists fun Rp => reproducibility a Rp T) True % 7.65/7.94 Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), Eq (organization a a_1 → Exists fun Rp => reproducibility a Rp a_1) True % 7.65/7.94 Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), Or (Eq (organization a a_1) False) (Eq (Exists fun Rp => reproducibility a Rp a_1) True) % 7.65/7.94 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a a_1) False) (Eq (reproducibility a (skS.0 0 a a_1 a_2) a_1) True) % 7.65/7.94 Clause #8 (by clausification #[2]): ∀ (a : Iota), % 7.65/7.94 Eq % 7.65/7.94 (∀ (Y C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 7.65/7.94 And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And (And (And (organization a T1) (organization Y T2)) (reorganization_free a T1 T1)) % 7.65/7.94 (reorganization_free Y T2 T2)) % 7.65/7.94 (class a C T1)) % 7.65/7.94 (class Y C T2)) % 7.65/7.94 (reproducibility a Rp1 T1)) % 7.65/7.94 (reproducibility Y Rp2 T2)) % 7.65/7.94 (size a S1 T1)) % 7.65/7.94 (size Y S2 T2)) % 7.65/7.94 (greater S2 S1) → % 7.65/7.94 greater Rp2 Rp1) % 7.65/7.94 True % 7.65/7.94 Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota), % 7.65/7.94 Eq % 7.65/7.94 (∀ (C Rp1 Rp2 S1 S2 T1 T2 : Iota), % 7.65/7.94 And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And % 7.65/7.94 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.94 (reorganization_free a_1 T2 T2)) % 7.65/7.94 (class a C T1)) % 7.65/7.94 (class a_1 C T2)) % 7.65/7.94 (reproducibility a Rp1 T1)) % 7.65/7.94 (reproducibility a_1 Rp2 T2)) % 7.65/7.94 (size a S1 T1)) % 7.65/7.94 (size a_1 S2 T2)) % 7.65/7.94 (greater S2 S1) → % 7.65/7.94 greater Rp2 Rp1) % 7.65/7.94 True % 7.65/7.94 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (Rp1 Rp2 S1 S2 T1 T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.95 (reorganization_free a_1 T2 T2)) % 7.65/7.95 (class a a_2 T1)) % 7.65/7.95 (class a_1 a_2 T2)) % 7.65/7.95 (reproducibility a Rp1 T1)) % 7.65/7.95 (reproducibility a_1 Rp2 T2)) % 7.65/7.95 (size a S1 T1)) % 7.65/7.95 (size a_1 S2 T2)) % 7.65/7.95 (greater S2 S1) → % 7.65/7.95 greater Rp2 Rp1) % 7.65/7.95 True % 7.65/7.95 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (Rp2 S1 S2 T1 T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.95 (reorganization_free a_1 T2 T2)) % 7.65/7.95 (class a a_2 T1)) % 7.65/7.95 (class a_1 a_2 T2)) % 7.65/7.95 (reproducibility a a_3 T1)) % 7.65/7.95 (reproducibility a_1 Rp2 T2)) % 7.65/7.95 (size a S1 T1)) % 7.65/7.95 (size a_1 S2 T2)) % 7.65/7.95 (greater S2 S1) → % 7.65/7.95 greater Rp2 a_3) % 7.65/7.95 True % 7.65/7.95 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (S1 S2 T1 T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.95 (reorganization_free a_1 T2 T2)) % 7.65/7.95 (class a a_2 T1)) % 7.65/7.95 (class a_1 a_2 T2)) % 7.65/7.95 (reproducibility a a_3 T1)) % 7.65/7.95 (reproducibility a_1 a_4 T2)) % 7.65/7.95 (size a S1 T1)) % 7.65/7.95 (size a_1 S2 T2)) % 7.65/7.95 (greater S2 S1) → % 7.65/7.95 greater a_4 a_3) % 7.65/7.95 True % 7.65/7.95 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (S2 T1 T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.95 (reorganization_free a_1 T2 T2)) % 7.65/7.95 (class a a_2 T1)) % 7.65/7.95 (class a_1 a_2 T2)) % 7.65/7.95 (reproducibility a a_3 T1)) % 7.65/7.95 (reproducibility a_1 a_4 T2)) % 7.65/7.95 (size a a_5 T1)) % 7.65/7.95 (size a_1 S2 T2)) % 7.65/7.95 (greater S2 a_5) → % 7.65/7.95 greater a_4 a_3) % 7.65/7.95 True % 7.65/7.95 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (T1 T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1)) % 7.65/7.95 (reorganization_free a_1 T2 T2)) % 7.65/7.95 (class a a_2 T1)) % 7.65/7.95 (class a_1 a_2 T2)) % 7.65/7.95 (reproducibility a a_3 T1)) % 7.65/7.95 (reproducibility a_1 a_4 T2)) % 7.65/7.95 (size a a_5 T1)) % 7.65/7.95 (size a_1 a_6 T2)) % 7.65/7.95 (greater a_6 a_5) → % 7.65/7.95 greater a_4 a_3) % 7.65/7.95 True % 7.65/7.95 Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 7.65/7.95 Eq % 7.65/7.95 (∀ (T2 : Iota), % 7.65/7.95 And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And % 7.65/7.95 (And (And (And (organization a a_1) (organization a_2 T2)) (reorganization_free a a_1 a_1)) % 7.65/7.95 (reorganization_free a_2 T2 T2)) % 7.65/7.95 (class a a_3 a_1)) % 7.65/7.95 (class a_2 a_3 T2)) % 7.65/7.95 (reproducibility a a_4 a_1)) % 7.65/7.95 (reproducibility a_2 a_5 T2)) % 7.65/7.95 (size a a_6 a_1)) % 7.65/7.95 (size a_2 a_7 T2)) % 7.65/7.97 (greater a_7 a_6) → % 7.65/7.97 greater a_5 a_4) % 7.65/7.97 True % 7.65/7.97 Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 7.65/7.97 (reorganization_free a_2 a_3 a_3)) % 7.65/7.97 (class a a_4 a_1)) % 7.65/7.97 (class a_2 a_4 a_3)) % 7.65/7.97 (reproducibility a a_5 a_1)) % 7.65/7.97 (reproducibility a_2 a_6 a_3)) % 7.65/7.97 (size a a_7 a_1)) % 7.65/7.97 (size a_2 a_8 a_3)) % 7.65/7.97 (greater a_8 a_7) → % 7.65/7.97 greater a_6 a_5) % 7.65/7.97 True % 7.65/7.97 Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Or % 7.65/7.97 (Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1)) % 7.65/7.97 (reorganization_free a_2 a_3 a_3)) % 7.65/7.97 (class a a_4 a_1)) % 7.65/7.97 (class a_2 a_4 a_3)) % 7.65/7.97 (reproducibility a a_5 a_1)) % 7.65/7.97 (reproducibility a_2 a_6 a_3)) % 7.65/7.97 (size a a_7 a_1)) % 7.65/7.97 (size a_2 a_8 a_3)) % 7.65/7.97 (greater a_8 a_7)) % 7.65/7.97 False) % 7.65/7.97 (Eq (greater a_6 a_5) True) % 7.65/7.97 Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Or (Eq (greater a a_1) True) % 7.65/7.97 (Or % 7.65/7.97 (Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a_2 a_3) (organization a_4 a_5)) (reorganization_free a_2 a_3 a_3)) % 7.65/7.97 (reorganization_free a_4 a_5 a_5)) % 7.65/7.97 (class a_2 a_6 a_3)) % 7.65/7.97 (class a_4 a_6 a_5)) % 7.65/7.97 (reproducibility a_2 a_1 a_3)) % 7.65/7.97 (reproducibility a_4 a a_5)) % 7.65/7.97 (size a_2 a_7 a_3)) % 7.65/7.97 (size a_4 a_8 a_5)) % 7.65/7.97 False) % 7.65/7.97 (Eq (greater a_8 a_7) False)) % 7.65/7.97 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Or (Eq (greater a a_1) True) % 7.65/7.97 (Or (Eq (greater a_2 a_3) False) % 7.65/7.97 (Or % 7.65/7.97 (Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (reorganization_free a_4 a_5 a_5)) % 7.65/7.97 (reorganization_free a_6 a_7 a_7)) % 7.65/7.97 (class a_4 a_8 a_5)) % 7.65/7.97 (class a_6 a_8 a_7)) % 7.65/7.97 (reproducibility a_4 a_1 a_5)) % 7.65/7.97 (reproducibility a_6 a a_7)) % 7.65/7.97 (size a_4 a_3 a_5)) % 7.65/7.97 False) % 7.65/7.97 (Eq (size a_6 a_2 a_7) False))) % 7.65/7.97 Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Or (Eq (greater a a_1) True) % 7.65/7.97 (Or (Eq (greater a_2 a_3) False) % 7.65/7.97 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.97 (Or % 7.65/7.97 (Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.97 (reorganization_free a_4 a_5 a_5)) % 7.65/7.97 (class a_6 a_8 a_7)) % 7.65/7.97 (class a_4 a_8 a_5)) % 7.65/7.97 (reproducibility a_6 a_1 a_7)) % 7.65/7.97 (reproducibility a_4 a a_5)) % 7.65/7.97 False) % 7.65/7.97 (Eq (size a_6 a_3 a_7) False)))) % 7.65/7.97 Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.97 Or (Eq (greater a a_1) True) % 7.65/7.97 (Or (Eq (greater a_2 a_3) False) % 7.65/7.97 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.97 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.97 (Or % 7.65/7.97 (Eq % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And % 7.65/7.97 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.97 (reorganization_free a_4 a_5 a_5)) % 7.65/7.97 (class a_6 a_8 a_7)) % 7.65/7.99 (class a_4 a_8 a_5)) % 7.65/7.99 (reproducibility a_6 a_1 a_7)) % 7.65/7.99 False) % 7.65/7.99 (Eq (reproducibility a_4 a a_5) False))))) % 7.65/7.99 Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or % 7.65/7.99 (Eq % 7.65/7.99 (And % 7.65/7.99 (And % 7.65/7.99 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.99 (reorganization_free a_4 a_5 a_5)) % 7.65/7.99 (class a_6 a_8 a_7)) % 7.65/7.99 (class a_4 a_8 a_5)) % 7.65/7.99 False) % 7.65/7.99 (Eq (reproducibility a_6 a_1 a_7) False)))))) % 7.65/7.99 Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or (Eq (reproducibility a_6 a_1 a_7) False) % 7.65/7.99 (Or % 7.65/7.99 (Eq % 7.65/7.99 (And % 7.65/7.99 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.99 (reorganization_free a_4 a_5 a_5)) % 7.65/7.99 (class a_6 a_8 a_7)) % 7.65/7.99 False) % 7.65/7.99 (Eq (class a_4 a_8 a_5) False))))))) % 7.65/7.99 Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or (Eq (reproducibility a_6 a_1 a_7) False) % 7.65/7.99 (Or (Eq (class a_4 a_8 a_5) False) % 7.65/7.99 (Or % 7.65/7.99 (Eq % 7.65/7.99 (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.99 (reorganization_free a_4 a_5 a_5)) % 7.65/7.99 False) % 7.65/7.99 (Eq (class a_6 a_8 a_7) False)))))))) % 7.65/7.99 Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or (Eq (reproducibility a_6 a_1 a_7) False) % 7.65/7.99 (Or (Eq (class a_4 a_8 a_5) False) % 7.65/7.99 (Or (Eq (class a_6 a_8 a_7) False) % 7.65/7.99 (Or % 7.65/7.99 (Eq (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) % 7.65/7.99 False) % 7.65/7.99 (Eq (reorganization_free a_4 a_5 a_5) False))))))))) % 7.65/7.99 Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or (Eq (reproducibility a_6 a_1 a_7) False) % 7.65/7.99 (Or (Eq (class a_4 a_8 a_5) False) % 7.65/7.99 (Or (Eq (class a_6 a_8 a_7) False) % 7.65/7.99 (Or (Eq (reorganization_free a_4 a_5 a_5) False) % 7.65/7.99 (Or (Eq (And (organization a_6 a_7) (organization a_4 a_5)) False) % 7.65/7.99 (Eq (reorganization_free a_6 a_7 a_7) False)))))))))) % 7.65/7.99 Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.65/7.99 Or (Eq (greater a a_1) True) % 7.65/7.99 (Or (Eq (greater a_2 a_3) False) % 7.65/7.99 (Or (Eq (size a_4 a_2 a_5) False) % 7.65/7.99 (Or (Eq (size a_6 a_3 a_7) False) % 7.65/7.99 (Or (Eq (reproducibility a_4 a a_5) False) % 7.65/7.99 (Or (Eq (reproducibility a_6 a_1 a_7) False) % 7.65/7.99 (Or (Eq (class a_4 a_8 a_5) False) % 7.65/7.99 (Or (Eq (class a_6 a_8 a_7) False) % 7.65/7.99 (Or (Eq (reorganization_free a_4 a_5 a_5) False) % 7.65/8.00 (Or (Eq (reorganization_free a_6 a_7 a_7) False) % 7.65/8.00 (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False))))))))))) % 7.65/8.00 Clause #28 (by clausification #[3]): Eq % 7.65/8.00 (∀ (X Y C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.00 And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1)) % 7.65/8.00 (reorganization_free Y T2 T2)) % 7.65/8.00 (class X C T1)) % 7.65/8.00 (class Y C T2)) % 7.65/8.00 (reliability X R1 T1)) % 7.65/8.00 (reliability Y R2 T2)) % 7.65/8.00 (accountability X A1 T1)) % 7.65/8.00 (accountability Y A2 T2)) % 7.65/8.00 (size X S1 T1)) % 7.65/8.00 (size Y S2 T2)) % 7.65/8.00 (greater S2 S1) → % 7.65/8.00 And (greater R2 R1) (greater A2 A1)) % 7.65/8.00 False % 7.65/8.00 Clause #29 (by clausification #[28]): ∀ (a : Iota), % 7.65/8.00 Eq % 7.65/8.00 (Not % 7.65/8.00 (∀ (Y C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.00 And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And (And (organization (skS.0 1 a) T1) (organization Y T2)) % 7.65/8.00 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.00 (reorganization_free Y T2 T2)) % 7.65/8.00 (class (skS.0 1 a) C T1)) % 7.65/8.00 (class Y C T2)) % 7.65/8.00 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.00 (reliability Y R2 T2)) % 7.65/8.00 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.00 (accountability Y A2 T2)) % 7.65/8.00 (size (skS.0 1 a) S1 T1)) % 7.65/8.00 (size Y S2 T2)) % 7.65/8.00 (greater S2 S1) → % 7.65/8.00 And (greater R2 R1) (greater A2 A1))) % 7.65/8.00 True % 7.65/8.00 Clause #30 (by clausification #[29]): ∀ (a : Iota), % 7.65/8.00 Eq % 7.65/8.00 (∀ (Y C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.00 And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And (And (organization (skS.0 1 a) T1) (organization Y T2)) % 7.65/8.00 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.00 (reorganization_free Y T2 T2)) % 7.65/8.00 (class (skS.0 1 a) C T1)) % 7.65/8.00 (class Y C T2)) % 7.65/8.00 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.00 (reliability Y R2 T2)) % 7.65/8.00 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.00 (accountability Y A2 T2)) % 7.65/8.00 (size (skS.0 1 a) S1 T1)) % 7.65/8.00 (size Y S2 T2)) % 7.65/8.00 (greater S2 S1) → % 7.65/8.00 And (greater R2 R1) (greater A2 A1)) % 7.65/8.00 False % 7.65/8.00 Clause #31 (by clausification #[30]): ∀ (a a_1 : Iota), % 7.65/8.00 Eq % 7.65/8.00 (Not % 7.65/8.00 (∀ (C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.00 And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And % 7.65/8.00 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.65/8.00 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.00 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.65/8.00 (class (skS.0 1 a) C T1)) % 7.65/8.00 (class (skS.0 2 a a_1) C T2)) % 7.65/8.00 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.00 (reliability (skS.0 2 a a_1) R2 T2)) % 7.65/8.00 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.00 (accountability (skS.0 2 a a_1) A2 T2)) % 7.65/8.00 (size (skS.0 1 a) S1 T1)) % 7.65/8.00 (size (skS.0 2 a a_1) S2 T2)) % 7.65/8.00 (greater S2 S1) → % 7.65/8.02 And (greater R2 R1) (greater A2 A1))) % 7.65/8.02 True % 7.65/8.02 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), % 7.65/8.02 Eq % 7.65/8.02 (∀ (C R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.02 And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.65/8.02 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.02 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.65/8.02 (class (skS.0 1 a) C T1)) % 7.65/8.02 (class (skS.0 2 a a_1) C T2)) % 7.65/8.02 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.02 (reliability (skS.0 2 a a_1) R2 T2)) % 7.65/8.02 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.02 (accountability (skS.0 2 a a_1) A2 T2)) % 7.65/8.02 (size (skS.0 1 a) S1 T1)) % 7.65/8.02 (size (skS.0 2 a a_1) S2 T2)) % 7.65/8.02 (greater S2 S1) → % 7.65/8.02 And (greater R2 R1) (greater A2 A1)) % 7.65/8.02 False % 7.65/8.02 Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 : Iota), % 7.65/8.02 Eq % 7.65/8.02 (Not % 7.65/8.02 (∀ (R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.02 And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.65/8.02 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.02 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.65/8.02 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.65/8.02 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.65/8.02 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.02 (reliability (skS.0 2 a a_1) R2 T2)) % 7.65/8.02 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.02 (accountability (skS.0 2 a a_1) A2 T2)) % 7.65/8.02 (size (skS.0 1 a) S1 T1)) % 7.65/8.02 (size (skS.0 2 a a_1) S2 T2)) % 7.65/8.02 (greater S2 S1) → % 7.65/8.02 And (greater R2 R1) (greater A2 A1))) % 7.65/8.02 True % 7.65/8.02 Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 : Iota), % 7.65/8.02 Eq % 7.65/8.02 (∀ (R1 R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.02 And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.65/8.02 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.02 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.65/8.02 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.65/8.02 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.65/8.02 (reliability (skS.0 1 a) R1 T1)) % 7.65/8.02 (reliability (skS.0 2 a a_1) R2 T2)) % 7.65/8.02 (accountability (skS.0 1 a) A1 T1)) % 7.65/8.02 (accountability (skS.0 2 a a_1) A2 T2)) % 7.65/8.02 (size (skS.0 1 a) S1 T1)) % 7.65/8.02 (size (skS.0 2 a a_1) S2 T2)) % 7.65/8.02 (greater S2 S1) → % 7.65/8.02 And (greater R2 R1) (greater A2 A1)) % 7.65/8.02 False % 7.65/8.02 Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 a_3 : Iota), % 7.65/8.02 Eq % 7.65/8.02 (Not % 7.65/8.02 (∀ (R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.65/8.02 And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And % 7.65/8.02 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.65/8.02 (reorganization_free (skS.0 1 a) T1 T1)) % 7.65/8.02 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.65/8.02 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.65/8.02 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.04 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.04 (reliability (skS.0 2 a a_1) R2 T2)) % 7.78/8.04 (accountability (skS.0 1 a) A1 T1)) % 7.78/8.04 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.04 (size (skS.0 1 a) S1 T1)) % 7.78/8.04 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.04 (greater S2 S1) → % 7.78/8.04 And (greater R2 (skS.0 4 a a_1 a_2 a_3)) (greater A2 A1))) % 7.78/8.04 True % 7.78/8.04 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 : Iota), % 7.78/8.04 Eq % 7.78/8.04 (∀ (R2 A1 A2 S1 S2 T1 T2 : Iota), % 7.78/8.04 And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.04 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.04 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.04 (reliability (skS.0 2 a a_1) R2 T2)) % 7.78/8.04 (accountability (skS.0 1 a) A1 T1)) % 7.78/8.04 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.04 (size (skS.0 1 a) S1 T1)) % 7.78/8.04 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.04 (greater S2 S1) → % 7.78/8.04 And (greater R2 (skS.0 4 a a_1 a_2 a_3)) (greater A2 A1)) % 7.78/8.04 False % 7.78/8.04 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/8.04 Eq % 7.78/8.04 (Not % 7.78/8.04 (∀ (A1 A2 S1 S2 T1 T2 : Iota), % 7.78/8.04 And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.04 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.04 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.04 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.04 (accountability (skS.0 1 a) A1 T1)) % 7.78/8.04 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.04 (size (skS.0 1 a) S1 T1)) % 7.78/8.04 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.04 (greater S2 S1) → % 7.78/8.04 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) (greater A2 A1))) % 7.78/8.04 True % 7.78/8.04 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.78/8.04 Eq % 7.78/8.04 (∀ (A1 A2 S1 S2 T1 T2 : Iota), % 7.78/8.04 And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And % 7.78/8.04 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.04 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.04 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.04 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.04 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.04 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.04 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.04 (accountability (skS.0 1 a) A1 T1)) % 7.78/8.04 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.04 (size (skS.0 1 a) S1 T1)) % 7.78/8.04 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.04 (greater S2 S1) → % 7.78/8.04 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) (greater A2 A1)) % 7.78/8.06 False % 7.78/8.06 Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.78/8.06 Eq % 7.78/8.06 (Not % 7.78/8.06 (∀ (A2 S1 S2 T1 T2 : Iota), % 7.78/8.06 And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.06 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.06 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.06 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.06 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.06 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.06 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.06 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.06 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.06 (size (skS.0 1 a) S1 T1)) % 7.78/8.06 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.06 (greater S2 S1) → % 7.78/8.06 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.06 (greater A2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5)))) % 7.78/8.06 True % 7.78/8.06 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.78/8.06 Eq % 7.78/8.06 (∀ (A2 S1 S2 T1 T2 : Iota), % 7.78/8.06 And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.06 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.06 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.06 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.06 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.06 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.06 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.06 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.06 (accountability (skS.0 2 a a_1) A2 T2)) % 7.78/8.06 (size (skS.0 1 a) S1 T1)) % 7.78/8.06 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.06 (greater S2 S1) → % 7.78/8.06 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) (greater A2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5))) % 7.78/8.06 False % 7.78/8.06 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.78/8.06 Eq % 7.78/8.06 (Not % 7.78/8.06 (∀ (S1 S2 T1 T2 : Iota), % 7.78/8.06 And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And % 7.78/8.06 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.06 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.06 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.06 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.06 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.06 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.06 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.06 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.06 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.06 (size (skS.0 1 a) S1 T1)) % 7.78/8.06 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.06 (greater S2 S1) → % 7.78/8.06 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.06 (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)))) % 7.78/8.06 True % 7.78/8.06 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.78/8.06 Eq % 7.78/8.06 (∀ (S1 S2 T1 T2 : Iota), % 7.78/8.07 And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.07 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.07 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.07 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.07 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.07 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.07 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.07 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.07 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.07 (size (skS.0 1 a) S1 T1)) % 7.78/8.07 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.07 (greater S2 S1) → % 7.78/8.07 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.07 (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))) % 7.78/8.07 False % 7.78/8.07 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 7.78/8.07 Eq % 7.78/8.07 (Not % 7.78/8.07 (∀ (S2 T1 T2 : Iota), % 7.78/8.07 And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.07 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.07 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.07 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.07 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.07 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.07 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.07 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.07 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.07 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) T1)) % 7.78/8.07 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.07 (greater S2 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.07 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.07 (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)))) % 7.78/8.07 True % 7.78/8.07 Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 7.78/8.07 Eq % 7.78/8.07 (∀ (S2 T1 T2 : Iota), % 7.78/8.07 And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And % 7.78/8.07 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.07 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.07 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.07 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.07 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.07 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.07 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.07 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.07 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.07 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) T1)) % 7.78/8.07 (size (skS.0 2 a a_1) S2 T2)) % 7.78/8.07 (greater S2 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.07 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.07 (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))) % 7.78/8.10 False % 7.78/8.10 Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.78/8.10 Eq % 7.78/8.10 (Not % 7.78/8.10 (∀ (T1 T2 : Iota), % 7.78/8.10 And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.10 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.10 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.10 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.10 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.10 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.10 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.10 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.10 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.10 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) T1)) % 7.78/8.10 (size (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) T2)) % 7.78/8.10 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.10 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.10 (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)))) % 7.78/8.10 True % 7.78/8.10 Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.78/8.10 Eq % 7.78/8.10 (∀ (T1 T2 : Iota), % 7.78/8.10 And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2)) % 7.78/8.10 (reorganization_free (skS.0 1 a) T1 T1)) % 7.78/8.10 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.10 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1)) % 7.78/8.10 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.10 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1)) % 7.78/8.10 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.10 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1)) % 7.78/8.10 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.10 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) T1)) % 7.78/8.10 (size (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) T2)) % 7.78/8.10 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.10 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.10 (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))) % 7.78/8.10 False % 7.78/8.10 Clause #47 (by clausification #[46]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.78/8.10 Eq % 7.78/8.10 (Not % 7.78/8.10 (∀ (T2 : Iota), % 7.78/8.10 And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And % 7.78/8.10 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.78/8.10 (organization (skS.0 2 a a_1) T2)) % 7.78/8.10 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.78/8.10 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.10 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.10 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.10 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.12 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.12 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.12 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (size (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) T2)) % 7.78/8.12 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.12 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.12 (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)))) % 7.78/8.12 True % 7.78/8.12 Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.78/8.12 Eq % 7.78/8.12 (∀ (T2 : Iota), % 7.78/8.12 And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.78/8.12 (organization (skS.0 2 a a_1) T2)) % 7.78/8.12 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (reorganization_free (skS.0 2 a a_1) T2 T2)) % 7.78/8.12 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2)) % 7.78/8.12 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2)) % 7.78/8.12 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2)) % 7.78/8.12 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (size (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) T2)) % 7.78/8.12 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.78/8.12 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.78/8.12 (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))) % 7.78/8.12 False % 7.78/8.12 Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.78/8.12 Eq % 7.78/8.12 (Not % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And % 7.78/8.12 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.78/8.12 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.78/8.12 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.78/8.12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.78/8.12 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.78/8.12 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.78/8.12 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) % 7.88/8.14 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.88/8.14 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) % 7.88/8.14 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (size (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) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.88/8.14 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.88/8.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)))) % 7.88/8.14 True % 7.88/8.14 Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.88/8.14 Eq % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.88/8.14 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.88/8.14 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.88/8.14 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.14 (size (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) % 7.88/8.14 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.14 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) → % 7.88/8.14 And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.88/8.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))) % 7.88/8.14 False % 7.88/8.14 Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.88/8.14 Eq % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And % 7.88/8.14 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.88/8.14 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.88/8.15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.88/8.15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (size (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) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))) % 7.88/8.15 True % 7.88/8.15 Clause #52 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.88/8.15 Eq % 7.88/8.15 (And (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) % 7.88/8.15 (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))) % 7.88/8.15 False % 7.88/8.15 Clause #53 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.88/8.15 Eq (greater (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True % 7.88/8.15 Clause #54 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.88/8.15 Eq % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And % 7.88/8.15 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.88/8.15 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.88/8.15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) % 7.88/8.15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.88/8.15 (size (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) % 7.88/8.15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.88/8.15 True % 7.88/8.15 Clause #55 (by superposition #[53, 27]): ∀ (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), % 7.88/8.15 Or (Eq (greater a a_1) True) % 7.88/8.15 (Or (Eq True False) % 7.88/8.17 (Or (Eq (size a_2 (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) a_12) False) % 7.88/8.17 (Or (Eq (size a_13 (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_14) False) % 7.88/8.17 (Or (Eq (reproducibility a_2 a a_12) False) % 7.88/8.17 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 7.88/8.17 (Or (Eq (class a_2 a_15 a_12) False) % 7.88/8.17 (Or (Eq (class a_13 a_15 a_14) False) % 7.88/8.17 (Or (Eq (reorganization_free a_2 a_12 a_12) False) % 7.88/8.17 (Or (Eq (reorganization_free a_13 a_14 a_14) False) % 7.88/8.17 (Or (Eq (organization a_13 a_14) False) (Eq (organization a_2 a_12) False))))))))))) % 7.88/8.17 Clause #56 (by clausification #[1]): ∀ (a : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (Y T1 T2 R1 R2 A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (And (organization a T1) (organization Y T2)) (reliability a R1 T1)) (reliability Y R2 T2)) % 7.88/8.17 (accountability a A1 T1)) % 7.88/8.17 (accountability Y A2 T2)) % 7.88/8.17 (reproducibility a Rp1 T1)) % 7.88/8.17 (reproducibility Y Rp2 T2) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater R2 R1) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #57 (by clausification #[56]): ∀ (a a_1 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (T1 T2 R1 R2 A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (organization a T1) (organization a_1 T2)) (reliability a R1 T1)) % 7.88/8.17 (reliability a_1 R2 T2)) % 7.88/8.17 (accountability a A1 T1)) % 7.88/8.17 (accountability a_1 A2 T2)) % 7.88/8.17 (reproducibility a Rp1 T1)) % 7.88/8.17 (reproducibility a_1 Rp2 T2) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater R2 R1) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (T2 R1 R2 A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (organization a a_1) (organization a_2 T2)) (reliability a R1 a_1)) % 7.88/8.17 (reliability a_2 R2 T2)) % 7.88/8.17 (accountability a A1 a_1)) % 7.88/8.17 (accountability a_2 A2 T2)) % 7.88/8.17 (reproducibility a Rp1 a_1)) % 7.88/8.17 (reproducibility a_2 Rp2 T2) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater R2 R1) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (R1 R2 A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a R1 a_1)) % 7.88/8.17 (reliability a_2 R2 a_3)) % 7.88/8.17 (accountability a A1 a_1)) % 7.88/8.17 (accountability a_2 A2 a_3)) % 7.88/8.17 (reproducibility a Rp1 a_1)) % 7.88/8.17 (reproducibility a_2 Rp2 a_3) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater R2 R1) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (R2 A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.17 (reliability a_2 R2 a_3)) % 7.88/8.17 (accountability a A1 a_1)) % 7.88/8.17 (accountability a_2 A2 a_3)) % 7.88/8.17 (reproducibility a Rp1 a_1)) % 7.88/8.17 (reproducibility a_2 Rp2 a_3) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater R2 a_4) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (A1 A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And % 7.88/8.17 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.17 (reliability a_2 a_5 a_3)) % 7.88/8.17 (accountability a A1 a_1)) % 7.88/8.17 (accountability a_2 A2 a_3)) % 7.88/8.17 (reproducibility a Rp1 a_1)) % 7.88/8.17 (reproducibility a_2 Rp2 a_3) → % 7.88/8.17 Iff (greater Rp2 Rp1) (And (greater a_5 a_4) (greater A2 A1))) % 7.88/8.17 True % 7.88/8.17 Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.88/8.17 Eq % 7.88/8.17 (∀ (A2 Rp1 Rp2 : Iota), % 7.88/8.17 And % 7.88/8.17 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 A2 a_3)) % 7.88/8.19 (reproducibility a Rp1 a_1)) % 7.88/8.19 (reproducibility a_2 Rp2 a_3) → % 7.88/8.19 Iff (greater Rp2 Rp1) (And (greater a_5 a_4) (greater A2 a_6))) % 7.88/8.19 True % 7.88/8.19 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 7.88/8.19 Eq % 7.88/8.19 (∀ (Rp1 Rp2 : Iota), % 7.88/8.19 And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 a_7 a_3)) % 7.88/8.19 (reproducibility a Rp1 a_1)) % 7.88/8.19 (reproducibility a_2 Rp2 a_3) → % 7.88/8.19 Iff (greater Rp2 Rp1) (And (greater a_5 a_4) (greater a_7 a_6))) % 7.88/8.19 True % 7.88/8.19 Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 7.88/8.19 Eq % 7.88/8.19 (∀ (Rp2 : Iota), % 7.88/8.19 And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 a_7 a_3)) % 7.88/8.19 (reproducibility a a_8 a_1)) % 7.88/8.19 (reproducibility a_2 Rp2 a_3) → % 7.88/8.19 Iff (greater Rp2 a_8) (And (greater a_5 a_4) (greater a_7 a_6))) % 7.88/8.19 True % 7.88/8.19 Clause #65 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.88/8.19 Eq % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 a_7 a_3)) % 7.88/8.19 (reproducibility a a_8 a_1)) % 7.88/8.19 (reproducibility a_2 a_9 a_3) → % 7.88/8.19 Iff (greater a_9 a_8) (And (greater a_5 a_4) (greater a_7 a_6))) % 7.88/8.19 True % 7.88/8.19 Clause #66 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.88/8.19 Or % 7.88/8.19 (Eq % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 a_7 a_3)) % 7.88/8.19 (reproducibility a a_8 a_1)) % 7.88/8.19 (reproducibility a_2 a_9 a_3)) % 7.88/8.19 False) % 7.88/8.19 (Eq (Iff (greater a_9 a_8) (And (greater a_5 a_4) (greater a_7 a_6))) True) % 7.88/8.19 Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.88/8.19 Or (Eq (Iff (greater a a_1) (And (greater a_2 a_3) (greater a_4 a_5))) True) % 7.88/8.19 (Or % 7.88/8.19 (Eq % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a_6 a_7) (organization a_8 a_9)) (reliability a_6 a_3 a_7)) % 7.88/8.19 (reliability a_8 a_2 a_9)) % 7.88/8.19 (accountability a_6 a_5 a_7)) % 7.88/8.19 (accountability a_8 a_4 a_9)) % 7.88/8.19 (reproducibility a_6 a_1 a_7)) % 7.88/8.19 False) % 7.88/8.19 (Eq (reproducibility a_8 a a_9) False)) % 7.88/8.19 Clause #69 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.88/8.19 Or % 7.88/8.19 (Eq % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1)) % 7.88/8.19 (reliability a_2 a_5 a_3)) % 7.88/8.19 (accountability a a_6 a_1)) % 7.88/8.19 (accountability a_2 a_7 a_3)) % 7.88/8.19 (reproducibility a a_8 a_1)) % 7.88/8.19 False) % 7.88/8.19 (Or (Eq (reproducibility a_2 a_9 a_3) False) % 7.88/8.19 (Or (Eq (greater a_9 a_8) False) (Eq (And (greater a_5 a_4) (greater a_7 a_6)) True))) % 7.88/8.19 Clause #77 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.88/8.19 Or (Eq (reproducibility a a_1 a_2) False) % 7.88/8.19 (Or (Eq (greater a_1 a_3) False) % 7.88/8.19 (Or (Eq (And (greater a_4 a_5) (greater a_6 a_7)) True) % 7.88/8.19 (Or % 7.88/8.19 (Eq % 7.88/8.19 (And % 7.88/8.19 (And % 7.88/8.19 (And (And (And (organization a_8 a_9) (organization a a_2)) (reliability a_8 a_5 a_9)) % 7.95/8.20 (reliability a a_4 a_2)) % 7.95/8.20 (accountability a_8 a_7 a_9)) % 7.95/8.20 (accountability a a_6 a_2)) % 7.95/8.20 False) % 7.95/8.20 (Eq (reproducibility a_8 a_3 a_9) False)))) % 7.95/8.20 Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or % 7.95/8.20 (Eq % 7.95/8.20 (And % 7.95/8.20 (And % 7.95/8.20 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_6 a_5)) % 7.95/8.20 (reliability a a_7 a_2)) % 7.95/8.20 (accountability a_4 a_8 a_5)) % 7.95/8.20 (accountability a a_9 a_2)) % 7.95/8.20 False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) (Eq (greater a_9 a_8) True)))) % 7.95/8.20 Clause #79 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or % 7.95/8.20 (Eq % 7.95/8.20 (And % 7.95/8.20 (And % 7.95/8.20 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_6 a_5)) % 7.95/8.20 (reliability a a_7 a_2)) % 7.95/8.20 (accountability a_4 a_8 a_5)) % 7.95/8.20 (accountability a a_9 a_2)) % 7.95/8.20 False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) (Eq (greater a_7 a_6) True)))) % 7.95/8.20 Clause #80 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.20 (Or (Eq (greater a_6 a_7) True) % 7.95/8.20 (Or % 7.95/8.20 (Eq % 7.95/8.20 (And % 7.95/8.20 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_8 a_5)) % 7.95/8.20 (reliability a a_9 a_2)) % 7.95/8.20 (accountability a_4 a_7 a_5)) % 7.95/8.20 False) % 7.95/8.20 (Eq (accountability a a_6 a_2) False))))) % 7.95/8.20 Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.20 (Or (Eq (greater a_6 a_7) True) % 7.95/8.20 (Or (Eq (accountability a a_6 a_2) False) % 7.95/8.20 (Or % 7.95/8.20 (Eq % 7.95/8.20 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_8 a_5)) % 7.95/8.20 (reliability a a_9 a_2)) % 7.95/8.20 False) % 7.95/8.20 (Eq (accountability a_4 a_7 a_5) False)))))) % 7.95/8.20 Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.20 (Or (Eq (greater a_6 a_7) True) % 7.95/8.20 (Or (Eq (accountability a a_6 a_2) False) % 7.95/8.20 (Or (Eq (accountability a_4 a_7 a_5) False) % 7.95/8.20 (Or (Eq (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_8 a_5)) False) % 7.95/8.20 (Eq (reliability a a_9 a_2) False))))))) % 7.95/8.20 Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.20 (Or (Eq (greater a_6 a_7) True) % 7.95/8.20 (Or (Eq (accountability a a_6 a_2) False) % 7.95/8.20 (Or (Eq (accountability a_4 a_7 a_5) False) % 7.95/8.20 (Or (Eq (reliability a a_8 a_2) False) % 7.95/8.20 (Or (Eq (And (organization a_4 a_5) (organization a a_2)) False) % 7.95/8.20 (Eq (reliability a_4 a_9 a_5) False)))))))) % 7.95/8.20 Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.20 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.20 (Or (Eq (greater a_1 a_3) False) % 7.95/8.20 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.20 (Or (Eq (greater a_6 a_7) True) % 7.95/8.20 (Or (Eq (accountability a a_6 a_2) False) % 7.95/8.20 (Or (Eq (accountability a_4 a_7 a_5) False) % 7.95/8.20 (Or (Eq (reliability a a_8 a_2) False) % 7.95/8.20 (Or (Eq (reliability a_4 a_9 a_5) False) % 7.95/8.22 (Or (Eq (organization a_4 a_5) False) (Eq (organization a a_2) False))))))))) % 7.95/8.22 Clause #85 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 7.95/8.22 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)) False) % 7.95/8.22 (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)) False) % 7.95/8.22 Clause #86 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.22 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.22 (Or (Eq (greater a_1 a_3) False) % 7.95/8.22 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.22 (Or (Eq (greater a_6 a_7) True) % 7.95/8.22 (Or % 7.95/8.22 (Eq % 7.95/8.22 (And % 7.95/8.22 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_7 a_5)) % 7.95/8.22 (reliability a a_6 a_2)) % 7.95/8.22 (accountability a_4 a_8 a_5)) % 7.95/8.22 False) % 7.95/8.22 (Eq (accountability a a_9 a_2) False))))) % 7.95/8.22 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.22 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.22 (Or (Eq (greater a_1 a_3) False) % 7.95/8.22 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.22 (Or (Eq (greater a_6 a_7) True) % 7.95/8.22 (Or (Eq (accountability a a_8 a_2) False) % 7.95/8.22 (Or % 7.95/8.22 (Eq % 7.95/8.22 (And (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_7 a_5)) % 7.95/8.22 (reliability a a_6 a_2)) % 7.95/8.22 False) % 7.95/8.22 (Eq (accountability a_4 a_9 a_5) False)))))) % 7.95/8.22 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.22 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.22 (Or (Eq (greater a_1 a_3) False) % 7.95/8.22 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.22 (Or (Eq (greater a_6 a_7) True) % 7.95/8.22 (Or (Eq (accountability a a_8 a_2) False) % 7.95/8.22 (Or (Eq (accountability a_4 a_9 a_5) False) % 7.95/8.22 (Or (Eq (And (And (organization a_4 a_5) (organization a a_2)) (reliability a_4 a_7 a_5)) False) % 7.95/8.22 (Eq (reliability a a_6 a_2) False))))))) % 7.95/8.22 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.22 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.22 (Or (Eq (greater a_1 a_3) False) % 7.95/8.22 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.22 (Or (Eq (greater a_6 a_7) True) % 7.95/8.22 (Or (Eq (accountability a a_8 a_2) False) % 7.95/8.22 (Or (Eq (accountability a_4 a_9 a_5) False) % 7.95/8.22 (Or (Eq (reliability a a_6 a_2) False) % 7.95/8.22 (Or (Eq (And (organization a_4 a_5) (organization a a_2)) False) % 7.95/8.22 (Eq (reliability a_4 a_7 a_5) False)))))))) % 7.95/8.22 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.22 Or (Eq (reproducibility a a_1 a_2) False) % 7.95/8.22 (Or (Eq (greater a_1 a_3) False) % 7.95/8.22 (Or (Eq (reproducibility a_4 a_3 a_5) False) % 7.95/8.22 (Or (Eq (greater a_6 a_7) True) % 7.95/8.22 (Or (Eq (accountability a a_8 a_2) False) % 7.95/8.22 (Or (Eq (accountability a_4 a_9 a_5) False) % 7.95/8.22 (Or (Eq (reliability a a_6 a_2) False) % 7.95/8.23 (Or (Eq (reliability a_4 a_7 a_5) False) % 7.95/8.23 (Or (Eq (organization a_4 a_5) False) (Eq (organization a a_2) False))))))))) % 7.95/8.23 Clause #91 (by clausification #[55]): ∀ (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), % 7.95/8.23 Or (Eq (greater a a_1) True) % 7.95/8.23 (Or (Eq (size a_2 (skS.0 9 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11) a_12) False) % 7.95/8.23 (Or (Eq (size a_13 (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_14) False) % 7.95/8.23 (Or (Eq (reproducibility a_2 a a_12) False) % 7.95/8.23 (Or (Eq (reproducibility a_13 a_1 a_14) False) % 7.95/8.23 (Or (Eq (class a_2 a_15 a_12) False) % 7.95/8.23 (Or (Eq (class a_13 a_15 a_14) False) % 7.95/8.23 (Or (Eq (reorganization_free a_2 a_12 a_12) False) % 7.95/8.23 (Or (Eq (reorganization_free a_13 a_14 a_14) False) % 7.95/8.23 (Or (Eq (organization a_13 a_14) False) (Eq (organization a_2 a_12) False)))))))))) % 7.95/8.23 Clause #92 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.23 Eq % 7.95/8.25 (size (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) % 7.95/8.25 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 7.95/8.25 True % 7.95/8.25 Clause #93 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.25 Eq % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And % 7.95/8.25 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.95/8.25 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.25 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.95/8.25 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.25 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.95/8.25 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.25 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.25 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.25 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.25 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.95/8.25 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.25 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.25 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.95/8.25 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.25 (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.25 True % 7.95/8.25 Clause #94 (by superposition #[92, 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 : Iota), % 7.95/8.25 Or (Eq (greater a a_1) True) % 7.95/8.25 (Or (Eq True False) % 7.95/8.25 (Or (Eq (size a_2 (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) False) % 7.95/8.25 (Or (Eq (reproducibility (skS.0 2 a_3 a_4) a (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) False) % 7.95/8.25 (Or (Eq (reproducibility a_2 a_1 a_11) False) % 7.95/8.25 (Or (Eq (class (skS.0 2 a_3 a_4) a_15 (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) False) % 7.95/8.25 (Or (Eq (class a_2 a_15 a_11) False) % 7.95/8.25 (Or % 7.95/8.25 (Eq % 7.95/8.25 (reorganization_free (skS.0 2 a_3 a_4) (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14) % 7.95/8.25 (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) % 7.95/8.25 False) % 7.95/8.25 (Or (Eq (reorganization_free a_2 a_11 a_11) False) % 7.95/8.25 (Or (Eq (organization a_2 a_11) False) % 7.95/8.25 (Eq (organization (skS.0 2 a_3 a_4) (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) % 7.95/8.25 False)))))))))) % 7.95/8.25 Clause #95 (by clausification #[94]): ∀ (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), % 7.95/8.25 Or (Eq (greater a a_1) True) % 7.95/8.25 (Or (Eq (size a_2 (skS.0 8 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) False) % 7.95/8.25 (Or (Eq (reproducibility (skS.0 2 a_3 a_4) a (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) False) % 7.95/8.25 (Or (Eq (reproducibility a_2 a_1 a_11) False) % 7.95/8.25 (Or (Eq (class (skS.0 2 a_3 a_4) a_15 (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) False) % 7.95/8.25 (Or (Eq (class a_2 a_15 a_11) False) % 7.95/8.25 (Or % 7.95/8.25 (Eq % 7.95/8.25 (reorganization_free (skS.0 2 a_3 a_4) (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14) % 7.95/8.25 (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) % 7.95/8.25 False) % 7.95/8.25 (Or (Eq (reorganization_free a_2 a_11 a_11) False) % 7.95/8.25 (Or (Eq (organization a_2 a_11) False) % 7.95/8.25 (Eq (organization (skS.0 2 a_3 a_4) (skS.0 11 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_12 a_13 a_14)) % 7.95/8.25 False))))))))) % 7.95/8.27 Clause #96 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.27 Eq (size (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True % 7.95/8.27 Clause #97 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.27 Eq % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.95/8.27 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.95/8.27 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.27 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.95/8.27 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.27 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.27 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) % 7.95/8.27 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.27 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.95/8.27 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 True % 7.95/8.27 Clause #98 (by superposition #[96, 95]): ∀ (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), % 7.95/8.27 Or (Eq (greater a a_1) True) % 7.95/8.27 (Or (Eq True False) % 7.95/8.27 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 7.95/8.27 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.27 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 7.95/8.27 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.27 (Or % 7.95/8.27 (Eq % 7.95/8.27 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 7.95/8.27 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 7.95/8.27 False) % 7.95/8.27 (Or % 7.95/8.27 (Eq % 7.95/8.27 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 7.95/8.27 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 7.95/8.27 False) % 7.95/8.27 (Or (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.27 (Eq (organization (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 7.95/8.27 False))))))))) % 7.95/8.27 Clause #99 (by clausification #[97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.27 Eq % 7.95/8.27 (accountability (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) % 7.95/8.27 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 7.95/8.27 True % 7.95/8.27 Clause #100 (by clausification #[97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.27 Eq % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And % 7.95/8.27 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.95/8.27 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.27 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.95/8.27 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.27 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.95/8.27 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 True % 7.95/8.29 Clause #101 (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 : Iota), % 7.95/8.29 Or (Eq (greater a a_1) True) % 7.95/8.29 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 7.95/8.29 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.29 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 7.95/8.29 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.29 (Or % 7.95/8.29 (Eq % 7.95/8.29 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 7.95/8.29 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 7.95/8.29 False) % 7.95/8.29 (Or % 7.95/8.29 (Eq % 7.95/8.29 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 7.95/8.29 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 7.95/8.29 False) % 7.95/8.29 (Or (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 7.95/8.29 (Eq (organization (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 7.95/8.29 False)))))))) % 7.95/8.29 Clause #102 (by clausification #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 7.95/8.29 Eq (accountability (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True % 7.95/8.29 Clause #103 (by clausification #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.29 Eq % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.95/8.29 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.95/8.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 7.95/8.29 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 7.95/8.29 (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 True % 7.95/8.29 Clause #104 (by clausification #[103]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.29 Eq (reliability (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 7.95/8.29 True % 7.95/8.29 Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 7.95/8.29 Eq % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And % 7.95/8.29 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 7.95/8.29 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 7.95/8.29 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 7.95/8.29 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.31 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 True % 8.05/8.31 Clause #106 (by clausification #[105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 8.05/8.31 Eq (reliability (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True % 8.05/8.31 Clause #107 (by clausification #[105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.31 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 8.05/8.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.31 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 True % 8.05/8.31 Clause #108 (by clausification #[107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) True % 8.05/8.31 Clause #109 (by clausification #[107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.31 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 8.05/8.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.31 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 True % 8.05/8.31 Clause #110 (by clausification #[109]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 8.05/8.31 Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True % 8.05/8.31 Clause #111 (by clausification #[109]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq % 8.05/8.31 (And % 8.05/8.31 (And % 8.05/8.31 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.31 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 8.05/8.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.31 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 True % 8.05/8.31 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq % 8.05/8.31 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.31 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.31 True % 8.05/8.31 Clause #113 (by clausification #[111]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.31 Eq % 8.05/8.31 (And % 8.05/8.31 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.31 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.31 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 8.05/8.31 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9))) % 8.05/8.31 True % 8.05/8.31 Clause #114 (by clausification #[113]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 8.05/8.33 Eq % 8.05/8.33 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) % 8.05/8.33 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.33 True % 8.05/8.33 Clause #115 (by clausification #[113]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.33 Eq % 8.05/8.33 (And (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.33 (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10))) % 8.05/8.33 True % 8.05/8.33 Clause #116 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.33 Eq (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) True % 8.05/8.33 Clause #117 (by clausification #[115]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 8.05/8.33 Eq (organization (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) True % 8.05/8.33 Clause #119 (by backward demodulation #[116, 101]): ∀ (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), % 8.05/8.33 Or (Eq (greater a a_1) True) % 8.05/8.33 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.33 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.33 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.33 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.33 (Or % 8.05/8.33 (Eq % 8.05/8.33 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 8.05/8.33 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 8.05/8.33 False) % 8.05/8.33 (Or % 8.05/8.33 (Eq % 8.05/8.33 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 8.05/8.33 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 8.05/8.33 False) % 8.05/8.33 (Or (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.33 (Eq True False)))))))) % 8.05/8.33 Clause #120 (by superposition #[116, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 8.05/8.33 Or (Eq True False) % 8.05/8.33 (Eq % 8.05/8.33 (reproducibility (skS.0 2 a a_1) % 8.05/8.33 (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.05/8.33 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.33 True) % 8.05/8.33 Clause #121 (by superposition #[117, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.33 Or (Eq True False) % 8.05/8.33 (Eq % 8.05/8.33 (reproducibility (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_10) % 8.05/8.33 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.33 True) % 8.05/8.33 Clause #122 (by clausification #[121]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.05/8.33 Eq % 8.05/8.33 (reproducibility (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9) a_10) % 8.05/8.33 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9)) % 8.05/8.33 True % 8.05/8.33 Clause #128 (by clausification #[120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 8.05/8.33 Eq % 8.05/8.33 (reproducibility (skS.0 2 a a_1) % 8.05/8.33 (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.05/8.33 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.33 True % 8.05/8.33 Clause #130 (by superposition #[128, 84]): ∀ (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 : Iota), % 8.05/8.33 Or (Eq True False) % 8.05/8.33 (Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.05/8.33 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.05/8.33 (Or (Eq (greater a_15 a_16) True) % 8.05/8.33 (Or (Eq (accountability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.33 (Or (Eq (accountability a_13 a_16 a_14) False) % 8.05/8.33 (Or (Eq (reliability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.33 (Or (Eq (reliability a_13 a_18 a_14) False) % 8.05/8.36 (Or (Eq (organization a_13 a_14) False) % 8.05/8.36 (Eq (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.36 False))))))))) % 8.05/8.36 Clause #131 (by superposition #[128, 90]): ∀ (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 : Iota), % 8.05/8.36 Or (Eq True False) % 8.05/8.36 (Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.05/8.36 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.05/8.36 (Or (Eq (greater a_15 a_16) True) % 8.05/8.36 (Or (Eq (accountability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (accountability a_13 a_18 a_14) False) % 8.05/8.36 (Or (Eq (reliability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (reliability a_13 a_16 a_14) False) % 8.05/8.36 (Or (Eq (organization a_13 a_14) False) % 8.05/8.36 (Eq (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.36 False))))))))) % 8.05/8.36 Clause #143 (by clausification #[131]): ∀ (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 : Iota), % 8.05/8.36 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.05/8.36 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.05/8.36 (Or (Eq (greater a_15 a_16) True) % 8.05/8.36 (Or (Eq (accountability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (accountability a_13 a_18 a_14) False) % 8.05/8.36 (Or (Eq (reliability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (reliability a_13 a_16 a_14) False) % 8.05/8.36 (Or (Eq (organization a_13 a_14) False) % 8.05/8.36 (Eq (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False)))))))) % 8.05/8.36 Clause #144 (by forward demodulation #[143, 116]): ∀ (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 : Iota), % 8.05/8.36 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.05/8.36 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.05/8.36 (Or (Eq (greater a_15 a_16) True) % 8.05/8.36 (Or (Eq (accountability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (accountability a_13 a_18 a_14) False) % 8.05/8.36 (Or (Eq (reliability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (reliability a_13 a_16 a_14) False) (Or (Eq (organization a_13 a_14) False) (Eq True False)))))))) % 8.05/8.36 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 a_14 a_15 a_16 a_17 a_18 : Iota), % 8.05/8.36 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.05/8.36 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.05/8.36 (Or (Eq (greater a_15 a_16) True) % 8.05/8.36 (Or (Eq (accountability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (accountability a_13 a_18 a_14) False) % 8.05/8.36 (Or (Eq (reliability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.36 (Or (Eq (reliability a_13 a_16 a_14) False) (Eq (organization a_13 a_14) False))))))) % 8.05/8.36 Clause #146 (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 a_15 : Iota), % 8.05/8.36 Or (Eq (greater a a_1) True) % 8.05/8.36 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.36 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.36 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.36 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 8.05/8.38 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 8.05/8.38 False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 8.05/8.38 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 8.05/8.38 False) % 8.05/8.38 (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False))))))) % 8.05/8.38 Clause #147 (by forward demodulation #[146, 117]): ∀ (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), % 8.05/8.38 Or (Eq (greater a a_1) True) % 8.05/8.38 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.38 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.38 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.38 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 8.05/8.38 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 8.05/8.38 False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 8.05/8.38 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 8.05/8.38 False) % 8.05/8.38 (Eq True False))))))) % 8.05/8.38 Clause #148 (by clausification #[147]): ∀ (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), % 8.05/8.38 Or (Eq (greater a a_1) True) % 8.05/8.38 (Or (Eq (reproducibility (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.38 (Or (Eq (reproducibility (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.38 (Or (Eq (class (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.05/8.38 (Or (Eq (class (skS.0 1 a_2) a_15 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 2 a_2 a_3) (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12) % 8.05/8.38 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) % 8.05/8.38 False) % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14) % 8.05/8.38 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) % 8.05/8.38 False)))))) % 8.05/8.38 Clause #149 (by superposition #[148, 128]): ∀ (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), % 8.05/8.38 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) True) % 8.05/8.38 (Or (Eq (reproducibility (skS.0 1 a) a_12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) False) % 8.05/8.38 (Or (Eq (class (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.05/8.38 (Or (Eq (class (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.05/8.38 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.05/8.38 False) % 8.05/8.38 (Or % 8.05/8.38 (Eq % 8.05/8.38 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14) % 8.05/8.38 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) % 8.05/8.38 False) % 8.05/8.38 (Eq False True)))))) % 8.05/8.38 Clause #150 (by clausification #[130]): ∀ (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 : Iota), % 8.05/8.38 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.15/8.40 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.15/8.40 (Or (Eq (greater a_15 a_16) True) % 8.15/8.40 (Or (Eq (accountability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (accountability a_13 a_16 a_14) False) % 8.15/8.40 (Or (Eq (reliability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (reliability a_13 a_18 a_14) False) % 8.15/8.40 (Or (Eq (organization a_13 a_14) False) % 8.15/8.40 (Eq (organization (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False)))))))) % 8.15/8.40 Clause #151 (by forward demodulation #[150, 116]): ∀ (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 : Iota), % 8.15/8.40 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.15/8.40 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.15/8.40 (Or (Eq (greater a_15 a_16) True) % 8.15/8.40 (Or (Eq (accountability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (accountability a_13 a_16 a_14) False) % 8.15/8.40 (Or (Eq (reliability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (reliability a_13 a_18 a_14) False) (Or (Eq (organization a_13 a_14) False) (Eq True False)))))))) % 8.15/8.40 Clause #152 (by clausification #[151]): ∀ (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 : Iota), % 8.15/8.40 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) False) % 8.15/8.40 (Or (Eq (reproducibility a_13 a_12 a_14) False) % 8.15/8.40 (Or (Eq (greater a_15 a_16) True) % 8.15/8.40 (Or (Eq (accountability (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (accountability a_13 a_16 a_14) False) % 8.15/8.40 (Or (Eq (reliability (skS.0 2 a a_1) a_17 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (reliability a_13 a_18 a_14) False) (Eq (organization a_13 a_14) False))))))) % 8.15/8.40 Clause #176 (by clausification #[149]): ∀ (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), % 8.15/8.40 Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 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) True) % 8.15/8.40 (Or (Eq (reproducibility (skS.0 1 a) a_12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) False) % 8.15/8.40 (Or (Eq (class (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (class (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) False) % 8.15/8.40 (Or % 8.15/8.40 (Eq % 8.15/8.40 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.40 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.40 False) % 8.15/8.40 (Eq % 8.15/8.40 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14) % 8.15/8.40 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_13 a_14)) % 8.15/8.40 False))))) % 8.15/8.40 Clause #177 (by superposition #[176, 122]): ∀ (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), % 8.15/8.40 Or % 8.15/8.40 (Eq % 8.15/8.40 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.40 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.40 True) % 8.15/8.40 (Or (Eq (class (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.40 (Or (Eq (class (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) False) % 8.15/8.40 (Or % 8.15/8.40 (Eq % 8.15/8.40 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.40 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.40 False) % 8.15/8.40 (Or % 8.15/8.40 (Eq % 8.15/8.40 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.40 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.40 False) % 8.15/8.40 (Eq False True))))) % 8.15/8.42 Clause #178 (by clausification #[177]): ∀ (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), % 8.15/8.42 Or % 8.15/8.42 (Eq % 8.15/8.42 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.42 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.42 True) % 8.15/8.42 (Or (Eq (class (skS.0 2 a a_1) a_15 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) False) % 8.15/8.42 (Or (Eq (class (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) False) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.42 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.42 False) % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.42 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.42 False)))) % 8.15/8.42 Clause #179 (by superposition #[178, 108]): ∀ (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), % 8.15/8.42 Or % 8.15/8.42 (Eq % 8.15/8.42 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.42 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.42 True) % 8.15/8.42 (Or (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) False) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.42 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.42 False) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.42 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.42 False) % 8.15/8.42 (Eq False True)))) % 8.15/8.42 Clause #184 (by clausification #[179]): ∀ (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), % 8.15/8.42 Or % 8.15/8.42 (Eq % 8.15/8.42 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.42 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.42 True) % 8.15/8.42 (Or (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) False) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.42 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.42 False) % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.42 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.42 False))) % 8.15/8.42 Clause #185 (by forward demodulation #[184, 110]): ∀ (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), % 8.15/8.42 Or % 8.15/8.42 (Eq % 8.15/8.42 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.42 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.42 True) % 8.15/8.42 (Or (Eq True False) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.42 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.42 False) % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.42 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.42 False))) % 8.15/8.42 Clause #186 (by clausification #[185]): ∀ (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), % 8.15/8.42 Or % 8.15/8.42 (Eq % 8.15/8.42 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.42 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.42 True) % 8.15/8.42 (Or % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) % 8.15/8.42 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10)) % 8.15/8.42 False) % 8.15/8.42 (Eq % 8.15/8.42 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.42 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.45 False)) % 8.15/8.45 Clause #187 (by superposition #[186, 112]): ∀ (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), % 8.15/8.45 Or % 8.15/8.45 (Eq % 8.15/8.45 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.45 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.45 True) % 8.15/8.45 (Or % 8.15/8.45 (Eq % 8.15/8.45 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.45 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.45 False) % 8.15/8.45 (Eq False True)) % 8.15/8.45 Clause #188 (by clausification #[187]): ∀ (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), % 8.15/8.45 Or % 8.15/8.45 (Eq % 8.15/8.45 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.45 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.45 True) % 8.15/8.45 (Eq % 8.15/8.45 (reorganization_free (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) % 8.15/8.45 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13)) % 8.15/8.45 False) % 8.15/8.45 Clause #189 (by superposition #[188, 114]): ∀ (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), % 8.15/8.45 Or % 8.15/8.45 (Eq % 8.15/8.45 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.45 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.45 True) % 8.15/8.45 (Eq False True) % 8.15/8.45 Clause #190 (by clausification #[189]): ∀ (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), % 8.15/8.45 Eq % 8.15/8.45 (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) % 8.15/8.45 (skS.0 0 (skS.0 1 a) (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_12 a_13) a_14)) % 8.15/8.45 True % 8.15/8.45 Clause #191 (by superposition #[190, 145]): ∀ (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), % 8.15/8.45 Or (Eq True False) % 8.15/8.45 (Or % 8.15/8.45 (Eq (reproducibility a (skS.0 0 (skS.0 1 a_1) (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) % 8.15/8.45 False) % 8.15/8.45 (Or (Eq (greater a_13 a_14) True) % 8.15/8.45 (Or (Eq (accountability (skS.0 2 a_1 a_2) a_15 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_16 a_17 a_18)) False) % 8.15/8.45 (Or (Eq (accountability a a_19 a_12) False) % 8.15/8.45 (Or % 8.15/8.45 (Eq (reliability (skS.0 2 a_1 a_2) a_13 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_16 a_17 a_18)) False) % 8.15/8.45 (Or (Eq (reliability a a_14 a_12) False) (Eq (organization a a_12) False))))))) % 8.15/8.45 Clause #192 (by superposition #[190, 152]): ∀ (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), % 8.15/8.45 Or (Eq True False) % 8.15/8.45 (Or % 8.15/8.45 (Eq (reproducibility a (skS.0 0 (skS.0 1 a_1) (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) % 8.15/8.45 False) % 8.15/8.45 (Or (Eq (greater a_13 a_14) True) % 8.15/8.45 (Or (Eq (accountability (skS.0 2 a_1 a_2) a_13 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_15 a_16 a_17)) False) % 8.15/8.45 (Or (Eq (accountability a a_14 a_12) False) % 8.15/8.45 (Or % 8.15/8.45 (Eq (reliability (skS.0 2 a_1 a_2) a_18 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_15 a_16 a_17)) False) % 8.15/8.45 (Or (Eq (reliability a a_19 a_12) False) (Eq (organization a a_12) False))))))) % 8.15/8.45 Clause #202 (by clausification #[192]): ∀ (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), % 8.15/8.45 Or % 8.15/8.45 (Eq (reproducibility a (skS.0 0 (skS.0 1 a_1) (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 8.15/8.45 (Or (Eq (greater a_13 a_14) True) % 8.15/8.45 (Or (Eq (accountability (skS.0 2 a_1 a_2) a_13 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_15 a_16 a_17)) False) % 8.15/8.45 (Or (Eq (accountability a a_14 a_12) False) % 8.15/8.45 (Or (Eq (reliability (skS.0 2 a_1 a_2) a_18 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_15 a_16 a_17)) False) % 8.15/8.45 (Or (Eq (reliability a a_19 a_12) False) (Eq (organization a a_12) False)))))) % 8.15/8.45 Clause #203 (by superposition #[202, 122]): ∀ (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 : Iota), % 8.15/8.45 Or (Eq (greater a a_1) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (accountability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 1 a_2) a_16 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Or (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Eq False True)))))) % 8.15/8.47 Clause #205 (by clausification #[191]): ∀ (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), % 8.15/8.47 Or % 8.15/8.47 (Eq (reproducibility a (skS.0 0 (skS.0 1 a_1) (skS.0 10 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10) a_11) a_12) False) % 8.15/8.47 (Or (Eq (greater a_13 a_14) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_1 a_2) a_15 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_16 a_17 a_18)) False) % 8.15/8.47 (Or (Eq (accountability a a_19 a_12) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_1 a_2) a_13 (skS.0 11 a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_16 a_17 a_18)) False) % 8.15/8.47 (Or (Eq (reliability a a_14 a_12) False) (Eq (organization a a_12) False)))))) % 8.15/8.47 Clause #206 (by superposition #[205, 122]): ∀ (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 : Iota), % 8.15/8.47 Or (Eq (greater a a_1) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_2 a_3) a_4 (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.47 (Or (Eq (accountability (skS.0 1 a_2) a_14 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.47 (Or (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.47 (Eq False True)))))) % 8.15/8.47 Clause #207 (by clausification #[203]): ∀ (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 : Iota), % 8.15/8.47 Or (Eq (greater a a_1) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (accountability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 1 a_2) a_16 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False))))) % 8.15/8.47 Clause #208 (by forward demodulation #[207, 117]): ∀ (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 : Iota), % 8.15/8.47 Or (Eq (greater a a_1) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (accountability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 1 a_2) a_16 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Eq True False))))) % 8.15/8.47 Clause #209 (by clausification #[208]): ∀ (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 : Iota), % 8.15/8.47 Or (Eq (greater a a_1) True) % 8.15/8.47 (Or (Eq (accountability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Or (Eq (accountability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.15/8.47 (Or (Eq (reliability (skS.0 2 a_2 a_3) a_15 (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.15/8.47 (Eq (reliability (skS.0 1 a_2) a_16 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False)))) % 8.15/8.47 Clause #210 (by superposition #[209, 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 a_13 a_14 a_15 : Iota), % 8.15/8.49 Or (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) True) % 8.15/8.49 (Or (Eq (accountability (skS.0 1 a) a_7 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a a_1) a_11 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_12 a_13 a_14)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False) % 8.15/8.49 (Eq False True)))) % 8.15/8.49 Clause #211 (by clausification #[210]): ∀ (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), % 8.15/8.49 Or (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) a_7) True) % 8.15/8.49 (Or (Eq (accountability (skS.0 1 a) a_7 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a a_1) a_11 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_12 a_13 a_14)) False) % 8.15/8.49 (Eq (reliability (skS.0 1 a) a_15 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False))) % 8.15/8.49 Clause #212 (by superposition #[211, 102]): ∀ (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), % 8.15/8.49 Or (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) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a a_1) a_7 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10 a_11)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 1 a) a_12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_13 a_14)) False) (Eq False True))) % 8.15/8.49 Clause #213 (by clausification #[212]): ∀ (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), % 8.15/8.49 Or (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) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a a_1) a_7 (skS.0 11 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10 a_11)) False) % 8.15/8.49 (Eq (reliability (skS.0 1 a) a_12 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_13 a_14)) False)) % 8.15/8.49 Clause #214 (by superposition #[213, 104]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.15/8.49 Or (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) % 8.15/8.49 (Or (Eq (reliability (skS.0 1 a) a_7 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False) (Eq False True)) % 8.15/8.49 Clause #215 (by clausification #[214]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.15/8.49 Or (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) % 8.15/8.49 (Eq (reliability (skS.0 1 a) a_7 (skS.0 10 a a_1 a_2 a_3 a_4 a_5 a_6 a_8 a_9 a_10)) False) % 8.15/8.49 Clause #216 (by superposition #[215, 106]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.15/8.49 Or (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) (Eq False True) % 8.15/8.49 Clause #218 (by clausification #[216]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.15/8.49 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 % 8.15/8.49 Clause #228 (by clausification #[206]): ∀ (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 : Iota), % 8.15/8.49 Or (Eq (greater a a_1) True) % 8.15/8.49 (Or (Eq (accountability (skS.0 2 a_2 a_3) a_4 (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.49 (Or (Eq (accountability (skS.0 1 a_2) a_14 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.49 (Eq (organization (skS.0 1 a_2) (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False))))) % 8.15/8.49 Clause #229 (by forward demodulation #[228, 117]): ∀ (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 : Iota), % 8.15/8.49 Or (Eq (greater a a_1) True) % 8.15/8.49 (Or (Eq (accountability (skS.0 2 a_2 a_3) a_4 (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.49 (Or (Eq (accountability (skS.0 1 a_2) a_14 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.15/8.49 (Or (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.25/8.52 (Eq True False))))) % 8.25/8.52 Clause #230 (by clausification #[229]): ∀ (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 : Iota), % 8.25/8.52 Or (Eq (greater a a_1) True) % 8.25/8.52 (Or (Eq (accountability (skS.0 2 a_2 a_3) a_4 (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.25/8.52 (Or (Eq (accountability (skS.0 1 a_2) a_14 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False) % 8.25/8.52 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13)) False) % 8.25/8.52 (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_5 a_6 a_7 a_8 a_9 a_10 a_15 a_16)) False)))) % 8.25/8.52 Clause #231 (by superposition #[230, 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 a_13 a_14 a_15 : Iota), % 8.25/8.52 Or (Eq (greater a a_1) True) % 8.25/8.52 (Or (Eq (accountability (skS.0 1 a_2) a_3 (skS.0 10 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.25/8.52 (Or (Eq (reliability (skS.0 2 a_2 a_4) a (skS.0 11 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_13 a_14 a_15)) False) % 8.25/8.52 (Or (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.25/8.52 (Eq False True)))) % 8.25/8.52 Clause #232 (by clausification #[231]): ∀ (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), % 8.25/8.52 Or (Eq (greater a a_1) True) % 8.25/8.52 (Or (Eq (accountability (skS.0 1 a_2) a_3 (skS.0 10 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.25/8.52 (Or (Eq (reliability (skS.0 2 a_2 a_4) a (skS.0 11 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_13 a_14 a_15)) False) % 8.25/8.52 (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False))) % 8.25/8.52 Clause #233 (by superposition #[232, 102]): ∀ (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), % 8.25/8.52 Or (Eq (greater a a_1) True) % 8.25/8.52 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.25/8.52 (Or (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False) % 8.25/8.52 (Eq False True))) % 8.25/8.52 Clause #234 (by clausification #[233]): ∀ (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), % 8.25/8.52 Or (Eq (greater a a_1) True) % 8.25/8.52 (Or (Eq (reliability (skS.0 2 a_2 a_3) a (skS.0 11 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12)) False) % 8.25/8.52 (Eq (reliability (skS.0 1 a_2) a_1 (skS.0 10 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_13 a_14)) False)) % 8.25/8.52 Clause #235 (by superposition #[234, 104]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.25/8.52 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True) % 8.25/8.52 (Or (Eq (reliability (skS.0 1 a) a_5 (skS.0 10 a a_1 a_2 a_3 a_4 a_6 a_7 a_8 a_9 a_10)) False) (Eq False True)) % 8.25/8.52 Clause #237 (by clausification #[235]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 8.25/8.52 Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True) % 8.25/8.52 (Eq (reliability (skS.0 1 a) a_5 (skS.0 10 a a_1 a_2 a_3 a_4 a_6 a_7 a_8 a_9 a_10)) False) % 8.25/8.52 Clause #238 (by superposition #[237, 106]): ∀ (a a_1 a_2 a_3 a_4 : Iota), 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) (Eq False True) % 8.25/8.52 Clause #239 (by clausification #[238]): ∀ (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)) True % 8.25/8.52 Clause #240 (by backward demodulation #[239, 85]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.25/8.52 Or (Eq True False) (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)) False) % 8.25/8.52 Clause #249 (by clausification #[240]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 8.25/8.52 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)) False % 8.25/8.52 Clause #250 (by superposition #[249, 218]): Eq False True % 8.25/8.52 Clause #251 (by clausification #[250]): False % 8.25/8.52 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------