Duper---1.0.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Duper---1.0
% Problem  : MGT004+1 : TPTP v9.3.0. Released v2.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : duper %s

% Computer : n031.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:13 AM UTC 2026

% Result   : Theorem 22.25s 22.55s
% Output   : Proof 22.65s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem    : MGT004+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.04  % Command    : duper %s
% 0.09/0.37  % Computer : n031.cluster.edu
% 0.09/0.37  % Model    : x86_64 x86_64
% 0.09/0.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37  % Memory   : 8046.5625MB
% 0.09/0.37  % OS       : Linux 6.8.0-71-generic
% 0.09/0.37  % CPULimit   : 300
% 0.09/0.37  % WCLimit    : 300
% 0.09/0.37  % DateTime   : Mon Sep  7 11:38:41 UTC 2026
% 0.09/0.37  % CPUTime    : 
% 22.25/22.55  SZS status Theorem for theBenchmark.p
% 22.25/22.55  SZS output start Proof for theBenchmark.p
% 22.25/22.55  Clause #0 (by assumption #[]): Eq (∀ (X T : Iota), organization X T → Exists fun R => reliability X R T) True
% 22.25/22.55  Clause #1 (by assumption #[]): Eq (∀ (X T : Iota), organization X T → Exists fun A => accountability X A T) True
% 22.25/22.55  Clause #2 (by assumption #[]): Eq
% 22.25/22.55    (∀ (X Y R1 R2 A1 A2 P1 P2 T1 T2 : Iota),
% 22.25/22.55      And
% 22.25/22.55          (And
% 22.25/22.55            (And
% 22.25/22.55              (And
% 22.25/22.55                (And
% 22.25/22.55                  (And
% 22.25/22.55                    (And (And (And (organization X T1) (organization Y T2)) (reliability X R1 T1)) (reliability Y R2 T2))
% 22.25/22.55                    (accountability X A1 T1))
% 22.25/22.55                  (accountability Y A2 T2))
% 22.25/22.55                (survival_chance X P1 T1))
% 22.25/22.55              (survival_chance Y P2 T2))
% 22.25/22.55            (greater R2 R1))
% 22.25/22.55          (greater A2 A1) →
% 22.25/22.55        greater P2 P1)
% 22.25/22.55    True
% 22.25/22.55  Clause #3 (by assumption #[]): Eq
% 22.25/22.55    (∀ (X R1 R2 A1 A2 T1 T2 Ta Tb : Iota),
% 22.25/22.55      And
% 22.25/22.55          (And
% 22.25/22.55            (And
% 22.25/22.55              (And
% 22.25/22.55                (And
% 22.25/22.55                  (And
% 22.25/22.55                    (And (And (And (organization X T1) (organization X T2)) (reorganization X Ta Tb))
% 22.25/22.55                      (reliability X R1 T1))
% 22.25/22.55                    (reliability X R2 T2))
% 22.25/22.55                  (accountability X A1 T1))
% 22.25/22.55                (accountability X A2 T2))
% 22.25/22.55              (Not (greater Ta T1)))
% 22.25/22.55            (greater T2 T1))
% 22.25/22.55          (Not (greater T2 Tb)) →
% 22.25/22.55        And (greater R1 R2) (greater A1 A2))
% 22.25/22.55    True
% 22.25/22.55  Clause #4 (by assumption #[]): Eq
% 22.25/22.55    (Not
% 22.25/22.55      (∀ (X P1 P2 T1 T2 Ta Tb : Iota),
% 22.25/22.55        And
% 22.25/22.55            (And
% 22.25/22.55              (And
% 22.25/22.55                (And
% 22.25/22.55                  (And (And (And (organization X T1) (organization X T2)) (reorganization X Ta Tb))
% 22.25/22.55                    (survival_chance X P1 T1))
% 22.25/22.55                  (survival_chance X P2 T2))
% 22.25/22.55                (Not (greater Ta T1)))
% 22.25/22.55              (greater T2 T1))
% 22.25/22.55            (Not (greater T2 Tb)) →
% 22.25/22.55          greater P1 P2))
% 22.25/22.55    True
% 22.25/22.55  Clause #5 (by clausification #[1]): ∀ (a : Iota), Eq (∀ (T : Iota), organization a T → Exists fun A => accountability a A T) True
% 22.25/22.55  Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), Eq (organization a a_1 → Exists fun A => accountability a A a_1) True
% 22.25/22.55  Clause #7 (by clausification #[6]): ∀ (a a_1 : Iota), Or (Eq (organization a a_1) False) (Eq (Exists fun A => accountability a A a_1) True)
% 22.25/22.55  Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a a_1) False) (Eq (accountability a (skS.0 0 a a_1 a_2) a_1) True)
% 22.25/22.55  Clause #9 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (T : Iota), organization a T → Exists fun R => reliability a R T) True
% 22.25/22.55  Clause #10 (by clausification #[9]): ∀ (a a_1 : Iota), Eq (organization a a_1 → Exists fun R => reliability a R a_1) True
% 22.25/22.55  Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Or (Eq (organization a a_1) False) (Eq (Exists fun R => reliability a R a_1) True)
% 22.25/22.55  Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a a_1) False) (Eq (reliability a (skS.0 1 a a_1 a_2) a_1) True)
% 22.25/22.55  Clause #13 (by clausification #[4]): Eq
% 22.25/22.55    (∀ (X P1 P2 T1 T2 Ta Tb : Iota),
% 22.25/22.55      And
% 22.25/22.55          (And
% 22.25/22.55            (And
% 22.25/22.55              (And
% 22.25/22.55                (And (And (And (organization X T1) (organization X T2)) (reorganization X Ta Tb))
% 22.25/22.55                  (survival_chance X P1 T1))
% 22.25/22.55                (survival_chance X P2 T2))
% 22.25/22.55              (Not (greater Ta T1)))
% 22.25/22.55            (greater T2 T1))
% 22.25/22.55          (Not (greater T2 Tb)) →
% 22.25/22.55        greater P1 P2)
% 22.25/22.55    False
% 22.25/22.55  Clause #14 (by clausification #[13]): ∀ (a : Iota),
% 22.25/22.55    Eq
% 22.25/22.55      (Not
% 22.25/22.55        (∀ (P1 P2 T1 T2 Ta Tb : Iota),
% 22.25/22.55          And
% 22.25/22.55              (And
% 22.25/22.55                (And
% 22.25/22.55                  (And
% 22.25/22.55                    (And
% 22.25/22.55                      (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.55                        (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.55                      (survival_chance (skS.0 2 a) P1 T1))
% 22.25/22.55                    (survival_chance (skS.0 2 a) P2 T2))
% 22.25/22.55                  (Not (greater Ta T1)))
% 22.25/22.55                (greater T2 T1))
% 22.25/22.55              (Not (greater T2 Tb)) →
% 22.25/22.55            greater P1 P2))
% 22.25/22.55      True
% 22.25/22.55  Clause #15 (by clausification #[14]): ∀ (a : Iota),
% 22.25/22.55    Eq
% 22.25/22.55      (∀ (P1 P2 T1 T2 Ta Tb : Iota),
% 22.25/22.57        And
% 22.25/22.57            (And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.57                      (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                    (survival_chance (skS.0 2 a) P1 T1))
% 22.25/22.57                  (survival_chance (skS.0 2 a) P2 T2))
% 22.25/22.57                (Not (greater Ta T1)))
% 22.25/22.57              (greater T2 T1))
% 22.25/22.57            (Not (greater T2 Tb)) →
% 22.25/22.57          greater P1 P2)
% 22.25/22.57      False
% 22.25/22.57  Clause #16 (by clausification #[15]): ∀ (a a_1 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (Not
% 22.25/22.57        (∀ (P2 T1 T2 Ta Tb : Iota),
% 22.25/22.57          And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And
% 22.25/22.57                      (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.57                        (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                      (survival_chance (skS.0 2 a) (skS.0 3 a a_1) T1))
% 22.25/22.57                    (survival_chance (skS.0 2 a) P2 T2))
% 22.25/22.57                  (Not (greater Ta T1)))
% 22.25/22.57                (greater T2 T1))
% 22.25/22.57              (Not (greater T2 Tb)) →
% 22.25/22.57            greater (skS.0 3 a a_1) P2))
% 22.25/22.57      True
% 22.25/22.57  Clause #17 (by clausification #[16]): ∀ (a a_1 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (∀ (P2 T1 T2 Ta Tb : Iota),
% 22.25/22.57        And
% 22.25/22.57            (And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.57                      (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) T1))
% 22.25/22.57                  (survival_chance (skS.0 2 a) P2 T2))
% 22.25/22.57                (Not (greater Ta T1)))
% 22.25/22.57              (greater T2 T1))
% 22.25/22.57            (Not (greater T2 Tb)) →
% 22.25/22.57          greater (skS.0 3 a a_1) P2)
% 22.25/22.57      False
% 22.25/22.57  Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (Not
% 22.25/22.57        (∀ (T1 T2 Ta Tb : Iota),
% 22.25/22.57          And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And
% 22.25/22.57                      (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.57                        (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                      (survival_chance (skS.0 2 a) (skS.0 3 a a_1) T1))
% 22.25/22.57                    (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) T2))
% 22.25/22.57                  (Not (greater Ta T1)))
% 22.25/22.57                (greater T2 T1))
% 22.25/22.57              (Not (greater T2 Tb)) →
% 22.25/22.57            greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))
% 22.25/22.57      True
% 22.25/22.57  Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (∀ (T1 T2 Ta Tb : Iota),
% 22.25/22.57        And
% 22.25/22.57            (And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And (And (organization (skS.0 2 a) T1) (organization (skS.0 2 a) T2))
% 22.25/22.57                      (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) T1))
% 22.25/22.57                  (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) T2))
% 22.25/22.57                (Not (greater Ta T1)))
% 22.25/22.57              (greater T2 T1))
% 22.25/22.57            (Not (greater T2 Tb)) →
% 22.25/22.57          greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))
% 22.25/22.57      False
% 22.25/22.57  Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (Not
% 22.25/22.57        (∀ (T2 Ta Tb : Iota),
% 22.25/22.57          And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And
% 22.25/22.57                      (And (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) (organization (skS.0 2 a) T2))
% 22.25/22.57                        (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.57                      (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.57                    (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) T2))
% 22.25/22.57                  (Not (greater Ta (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.57                (greater T2 (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.57              (Not (greater T2 Tb)) →
% 22.25/22.57            greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))
% 22.25/22.57      True
% 22.25/22.57  Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 : Iota),
% 22.25/22.57    Eq
% 22.25/22.57      (∀ (T2 Ta Tb : Iota),
% 22.25/22.57        And
% 22.25/22.57            (And
% 22.25/22.57              (And
% 22.25/22.57                (And
% 22.25/22.57                  (And
% 22.25/22.57                    (And (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) (organization (skS.0 2 a) T2))
% 22.25/22.57                      (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.59                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59                  (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) T2))
% 22.25/22.59                (Not (greater Ta (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.59              (greater T2 (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59            (Not (greater T2 Tb)) →
% 22.25/22.59          greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))
% 22.25/22.59      False
% 22.25/22.59  Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.25/22.59    Eq
% 22.25/22.59      (Not
% 22.25/22.59        (∀ (Ta Tb : Iota),
% 22.25/22.59          And
% 22.25/22.59              (And
% 22.25/22.59                (And
% 22.25/22.59                  (And
% 22.25/22.59                    (And
% 22.25/22.59                      (And
% 22.25/22.59                        (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.25/22.59                          (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                        (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.59                      (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59                    (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                  (Not (greater Ta (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.59                (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59              (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) Tb)) →
% 22.25/22.59            greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))
% 22.25/22.59      True
% 22.25/22.59  Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.25/22.59    Eq
% 22.25/22.59      (∀ (Ta Tb : Iota),
% 22.25/22.59        And
% 22.25/22.59            (And
% 22.25/22.59              (And
% 22.25/22.59                (And
% 22.25/22.59                  (And
% 22.25/22.59                    (And
% 22.25/22.59                      (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.25/22.59                        (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                      (reorganization (skS.0 2 a) Ta Tb))
% 22.25/22.59                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59                  (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                (Not (greater Ta (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.59              (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59            (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) Tb)) →
% 22.25/22.59          greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))
% 22.25/22.59      False
% 22.25/22.59  Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.25/22.59    Eq
% 22.25/22.59      (Not
% 22.25/22.59        (∀ (Tb : Iota),
% 22.25/22.59          And
% 22.25/22.59              (And
% 22.25/22.59                (And
% 22.25/22.59                  (And
% 22.25/22.59                    (And
% 22.25/22.59                      (And
% 22.25/22.59                        (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.25/22.59                          (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                        (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) Tb))
% 22.25/22.59                      (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59                    (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                  (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.59                (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59              (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) Tb)) →
% 22.25/22.59            greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))
% 22.25/22.59      True
% 22.25/22.59  Clause #25 (by clausification #[24]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.25/22.59    Eq
% 22.25/22.59      (∀ (Tb : Iota),
% 22.25/22.59        And
% 22.25/22.59            (And
% 22.25/22.59              (And
% 22.25/22.59                (And
% 22.25/22.59                  (And
% 22.25/22.59                    (And
% 22.25/22.59                      (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.25/22.59                        (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                      (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) Tb))
% 22.25/22.59                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59                  (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.25/22.59                (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.25/22.59              (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.25/22.59            (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) Tb)) →
% 22.25/22.59          greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))
% 22.25/22.59      False
% 22.25/22.59  Clause #26 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.25/22.59    Eq
% 22.25/22.59      (Not
% 22.35/22.60        (And
% 22.35/22.60            (And
% 22.35/22.60              (And
% 22.35/22.60                (And
% 22.35/22.60                  (And
% 22.35/22.60                    (And
% 22.35/22.60                      (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.35/22.60                        (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60                      (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.35/22.60                    (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60                  (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60                (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.35/22.60              (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60            (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6))) →
% 22.35/22.60          greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)))
% 22.35/22.60      True
% 22.35/22.60  Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.60    Eq
% 22.35/22.60      (And
% 22.35/22.60          (And
% 22.35/22.60            (And
% 22.35/22.60              (And
% 22.35/22.60                (And
% 22.35/22.60                  (And
% 22.35/22.60                    (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.35/22.60                      (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60                    (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.35/22.60                  (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60                (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60              (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.35/22.60            (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60          (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6))) →
% 22.35/22.60        greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2))
% 22.35/22.60      False
% 22.35/22.60  Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.60    Eq
% 22.35/22.60      (And
% 22.35/22.60        (And
% 22.35/22.60          (And
% 22.35/22.60            (And
% 22.35/22.60              (And
% 22.35/22.60                (And
% 22.35/22.60                  (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.35/22.60                    (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60                  (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.35/22.60                (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60              (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60            (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.35/22.60          (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60        (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6))))
% 22.35/22.60      True
% 22.35/22.60  Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 : Iota), Eq (greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) False
% 22.35/22.60  Clause #30 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.60    Eq (Not (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6))) True
% 22.35/22.60  Clause #31 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.60    Eq
% 22.35/22.60      (And
% 22.35/22.60        (And
% 22.35/22.60          (And
% 22.35/22.60            (And
% 22.35/22.60              (And
% 22.35/22.60                (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.35/22.60                  (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60                (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.35/22.60              (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60            (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.35/22.60          (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.35/22.60        (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)))
% 22.35/22.60      True
% 22.35/22.60  Clause #32 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), Eq (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) False
% 22.35/22.60  Clause #33 (by clausification #[2]): ∀ (a : Iota),
% 22.35/22.60    Eq
% 22.35/22.60      (∀ (Y R1 R2 A1 A2 P1 P2 T1 T2 : Iota),
% 22.35/22.60        And
% 22.35/22.60            (And
% 22.35/22.60              (And
% 22.35/22.60                (And
% 22.35/22.60                  (And
% 22.35/22.60                    (And
% 22.35/22.60                      (And (And (And (organization a T1) (organization Y T2)) (reliability a R1 T1))
% 22.35/22.62                        (reliability Y R2 T2))
% 22.35/22.62                      (accountability a A1 T1))
% 22.35/22.62                    (accountability Y A2 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance Y P2 T2))
% 22.35/22.62              (greater R2 R1))
% 22.35/22.62            (greater A2 A1) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #34 (by clausification #[33]): ∀ (a a_1 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (R1 R2 A1 A2 P1 P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a R1 T1))
% 22.35/22.62                        (reliability a_1 R2 T2))
% 22.35/22.62                      (accountability a A1 T1))
% 22.35/22.62                    (accountability a_1 A2 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater R2 R1))
% 22.35/22.62            (greater A2 A1) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (R2 A1 A2 P1 P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.62                        (reliability a_1 R2 T2))
% 22.35/22.62                      (accountability a A1 T1))
% 22.35/22.62                    (accountability a_1 A2 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater R2 a_2))
% 22.35/22.62            (greater A2 A1) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (A1 A2 P1 P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.62                        (reliability a_1 a_3 T2))
% 22.35/22.62                      (accountability a A1 T1))
% 22.35/22.62                    (accountability a_1 A2 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater a_3 a_2))
% 22.35/22.62            (greater A2 A1) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (A2 P1 P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.62                        (reliability a_1 a_3 T2))
% 22.35/22.62                      (accountability a a_4 T1))
% 22.35/22.62                    (accountability a_1 A2 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater a_3 a_2))
% 22.35/22.62            (greater A2 a_4) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (P1 P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.62                        (reliability a_1 a_3 T2))
% 22.35/22.62                      (accountability a a_4 T1))
% 22.35/22.62                    (accountability a_1 a_5 T2))
% 22.35/22.62                  (survival_chance a P1 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater a_3 a_2))
% 22.35/22.62            (greater a_5 a_4) →
% 22.35/22.62          greater P2 P1)
% 22.35/22.62      True
% 22.35/22.62  Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.62    Eq
% 22.35/22.62      (∀ (P2 T1 T2 : Iota),
% 22.35/22.62        And
% 22.35/22.62            (And
% 22.35/22.62              (And
% 22.35/22.62                (And
% 22.35/22.62                  (And
% 22.35/22.62                    (And
% 22.35/22.62                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.62                        (reliability a_1 a_3 T2))
% 22.35/22.62                      (accountability a a_4 T1))
% 22.35/22.62                    (accountability a_1 a_5 T2))
% 22.35/22.62                  (survival_chance a a_6 T1))
% 22.35/22.62                (survival_chance a_1 P2 T2))
% 22.35/22.62              (greater a_3 a_2))
% 22.35/22.63            (greater a_5 a_4) →
% 22.35/22.63          greater P2 a_6)
% 22.35/22.63      True
% 22.35/22.63  Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.35/22.63    Eq
% 22.35/22.63      (∀ (T1 T2 : Iota),
% 22.35/22.63        And
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And
% 22.35/22.63                      (And (And (And (organization a T1) (organization a_1 T2)) (reliability a a_2 T1))
% 22.35/22.63                        (reliability a_1 a_3 T2))
% 22.35/22.63                      (accountability a a_4 T1))
% 22.35/22.63                    (accountability a_1 a_5 T2))
% 22.35/22.63                  (survival_chance a a_6 T1))
% 22.35/22.63                (survival_chance a_1 a_7 T2))
% 22.35/22.63              (greater a_3 a_2))
% 22.35/22.63            (greater a_5 a_4) →
% 22.35/22.63          greater a_7 a_6)
% 22.35/22.63      True
% 22.35/22.63  Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.63    Eq
% 22.35/22.63      (∀ (T2 : Iota),
% 22.35/22.63        And
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And
% 22.35/22.63                      (And (And (And (organization a a_1) (organization a_2 T2)) (reliability a a_3 a_1))
% 22.35/22.63                        (reliability a_2 a_4 T2))
% 22.35/22.63                      (accountability a a_5 a_1))
% 22.35/22.63                    (accountability a_2 a_6 T2))
% 22.35/22.63                  (survival_chance a a_7 a_1))
% 22.35/22.63                (survival_chance a_2 a_8 T2))
% 22.35/22.63              (greater a_4 a_3))
% 22.35/22.63            (greater a_6 a_5) →
% 22.35/22.63          greater a_8 a_7)
% 22.35/22.63      True
% 22.35/22.63  Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.63    Eq
% 22.35/22.63      (And
% 22.35/22.63          (And
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1))
% 22.35/22.63                      (reliability a_2 a_5 a_3))
% 22.35/22.63                    (accountability a a_6 a_1))
% 22.35/22.63                  (accountability a_2 a_7 a_3))
% 22.35/22.63                (survival_chance a a_8 a_1))
% 22.35/22.63              (survival_chance a_2 a_9 a_3))
% 22.35/22.63            (greater a_5 a_4))
% 22.35/22.63          (greater a_7 a_6) →
% 22.35/22.63        greater a_9 a_8)
% 22.35/22.63      True
% 22.35/22.63  Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.63    Or
% 22.35/22.63      (Eq
% 22.35/22.63        (And
% 22.35/22.63          (And
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reliability a a_4 a_1))
% 22.35/22.63                      (reliability a_2 a_5 a_3))
% 22.35/22.63                    (accountability a a_6 a_1))
% 22.35/22.63                  (accountability a_2 a_7 a_3))
% 22.35/22.63                (survival_chance a a_8 a_1))
% 22.35/22.63              (survival_chance a_2 a_9 a_3))
% 22.35/22.63            (greater a_5 a_4))
% 22.35/22.63          (greater a_7 a_6))
% 22.35/22.63        False)
% 22.35/22.63      (Eq (greater a_9 a_8) True)
% 22.35/22.63  Clause #44 (by clausification #[43]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.63    Or (Eq (greater a a_1) True)
% 22.35/22.63      (Or
% 22.35/22.63        (Eq
% 22.35/22.63          (And
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And (And (And (organization a_2 a_3) (organization a_4 a_5)) (reliability a_2 a_6 a_3))
% 22.35/22.63                      (reliability a_4 a_7 a_5))
% 22.35/22.63                    (accountability a_2 a_8 a_3))
% 22.35/22.63                  (accountability a_4 a_9 a_5))
% 22.35/22.63                (survival_chance a_2 a_1 a_3))
% 22.35/22.63              (survival_chance a_4 a a_5))
% 22.35/22.63            (greater a_7 a_6))
% 22.35/22.63          False)
% 22.35/22.63        (Eq (greater a_9 a_8) False))
% 22.35/22.63  Clause #45 (by clausification #[44]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.63    Or (Eq (greater a a_1) True)
% 22.35/22.63      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.63        (Or
% 22.35/22.63          (Eq
% 22.35/22.63            (And
% 22.35/22.63              (And
% 22.35/22.63                (And
% 22.35/22.63                  (And
% 22.35/22.63                    (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (reliability a_4 a_8 a_5))
% 22.35/22.63                      (reliability a_6 a_9 a_7))
% 22.35/22.63                    (accountability a_4 a_3 a_5))
% 22.35/22.63                  (accountability a_6 a_2 a_7))
% 22.35/22.63                (survival_chance a_4 a_1 a_5))
% 22.35/22.63              (survival_chance a_6 a a_7))
% 22.35/22.63            False)
% 22.35/22.63          (Eq (greater a_9 a_8) False)))
% 22.35/22.63  Clause #46 (by clausification #[45]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.63    Or (Eq (greater a a_1) True)
% 22.35/22.63      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.63        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or
% 22.35/22.65            (Eq
% 22.35/22.65              (And
% 22.35/22.65                (And
% 22.35/22.65                  (And
% 22.35/22.65                    (And (And (And (organization a_6 a_7) (organization a_8 a_9)) (reliability a_6 a_5 a_7))
% 22.35/22.65                      (reliability a_8 a_4 a_9))
% 22.35/22.65                    (accountability a_6 a_3 a_7))
% 22.35/22.65                  (accountability a_8 a_2 a_9))
% 22.35/22.65                (survival_chance a_6 a_1 a_7))
% 22.35/22.65              False)
% 22.35/22.65            (Eq (survival_chance a_8 a a_9) False))))
% 22.35/22.65  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),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or
% 22.35/22.65              (Eq
% 22.35/22.65                (And
% 22.35/22.65                  (And
% 22.35/22.65                    (And (And (And (organization a_8 a_9) (organization a_6 a_7)) (reliability a_8 a_5 a_9))
% 22.35/22.65                      (reliability a_6 a_4 a_7))
% 22.35/22.65                    (accountability a_8 a_3 a_9))
% 22.35/22.65                  (accountability a_6 a_2 a_7))
% 22.35/22.65                False)
% 22.35/22.65              (Eq (survival_chance a_8 a_1 a_9) False)))))
% 22.35/22.65  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),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or (Eq (survival_chance a_8 a_1 a_9) False)
% 22.35/22.65              (Or
% 22.35/22.65                (Eq
% 22.35/22.65                  (And
% 22.35/22.65                    (And (And (And (organization a_8 a_9) (organization a_6 a_7)) (reliability a_8 a_5 a_9))
% 22.35/22.65                      (reliability a_6 a_4 a_7))
% 22.35/22.65                    (accountability a_8 a_3 a_9))
% 22.35/22.65                  False)
% 22.35/22.65                (Eq (accountability a_6 a_2 a_7) False))))))
% 22.35/22.65  Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or (Eq (survival_chance a_8 a_1 a_9) False)
% 22.35/22.65              (Or (Eq (accountability a_6 a_2 a_7) False)
% 22.35/22.65                (Or
% 22.35/22.65                  (Eq
% 22.35/22.65                    (And (And (And (organization a_8 a_9) (organization a_6 a_7)) (reliability a_8 a_5 a_9))
% 22.35/22.65                      (reliability a_6 a_4 a_7))
% 22.35/22.65                    False)
% 22.35/22.65                  (Eq (accountability a_8 a_3 a_9) False)))))))
% 22.35/22.65  Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or (Eq (survival_chance a_8 a_1 a_9) False)
% 22.35/22.65              (Or (Eq (accountability a_6 a_2 a_7) False)
% 22.35/22.65                (Or (Eq (accountability a_8 a_3 a_9) False)
% 22.35/22.65                  (Or (Eq (And (And (organization a_8 a_9) (organization a_6 a_7)) (reliability a_8 a_5 a_9)) False)
% 22.35/22.65                    (Eq (reliability a_6 a_4 a_7) False))))))))
% 22.35/22.65  Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or (Eq (survival_chance a_8 a_1 a_9) False)
% 22.35/22.65              (Or (Eq (accountability a_6 a_2 a_7) False)
% 22.35/22.65                (Or (Eq (accountability a_8 a_3 a_9) False)
% 22.35/22.65                  (Or (Eq (reliability a_6 a_4 a_7) False)
% 22.35/22.65                    (Or (Eq (And (organization a_8 a_9) (organization a_6 a_7)) False)
% 22.35/22.65                      (Eq (reliability a_8 a_5 a_9) False)))))))))
% 22.35/22.65  Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.35/22.65    Or (Eq (greater a a_1) True)
% 22.35/22.65      (Or (Eq (greater a_2 a_3) False)
% 22.35/22.65        (Or (Eq (greater a_4 a_5) False)
% 22.35/22.65          (Or (Eq (survival_chance a_6 a a_7) False)
% 22.35/22.65            (Or (Eq (survival_chance a_8 a_1 a_9) False)
% 22.35/22.65              (Or (Eq (accountability a_6 a_2 a_7) False)
% 22.35/22.65                (Or (Eq (accountability a_8 a_3 a_9) False)
% 22.35/22.65                  (Or (Eq (reliability a_6 a_4 a_7) False)
% 22.35/22.65                    (Or (Eq (reliability a_8 a_5 a_9) False)
% 22.35/22.67                      (Or (Eq (organization a_8 a_9) False) (Eq (organization a_6 a_7) False))))))))))
% 22.35/22.67  Clause #53 (by clausification #[3]): ∀ (a : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (R1 R2 A1 A2 T1 T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a T1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a R1 T1))
% 22.35/22.67                      (reliability a R2 T2))
% 22.35/22.67                    (accountability a A1 T1))
% 22.35/22.67                  (accountability a A2 T2))
% 22.35/22.67                (Not (greater Ta T1)))
% 22.35/22.67              (greater T2 T1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater R1 R2) (greater A1 A2))
% 22.35/22.67      True
% 22.35/22.67  Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (R2 A1 A2 T1 T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a T1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a a_1 T1))
% 22.35/22.67                      (reliability a R2 T2))
% 22.35/22.67                    (accountability a A1 T1))
% 22.35/22.67                  (accountability a A2 T2))
% 22.35/22.67                (Not (greater Ta T1)))
% 22.35/22.67              (greater T2 T1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater a_1 R2) (greater A1 A2))
% 22.35/22.67      True
% 22.35/22.67  Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (A1 A2 T1 T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a T1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a a_1 T1))
% 22.35/22.67                      (reliability a a_2 T2))
% 22.35/22.67                    (accountability a A1 T1))
% 22.35/22.67                  (accountability a A2 T2))
% 22.35/22.67                (Not (greater Ta T1)))
% 22.35/22.67              (greater T2 T1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater a_1 a_2) (greater A1 A2))
% 22.35/22.67      True
% 22.35/22.67  Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (A2 T1 T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a T1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a a_1 T1))
% 22.35/22.67                      (reliability a a_2 T2))
% 22.35/22.67                    (accountability a a_3 T1))
% 22.35/22.67                  (accountability a A2 T2))
% 22.35/22.67                (Not (greater Ta T1)))
% 22.35/22.67              (greater T2 T1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater a_1 a_2) (greater a_3 A2))
% 22.35/22.67      True
% 22.35/22.67  Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (T1 T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a T1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a a_1 T1))
% 22.35/22.67                      (reliability a a_2 T2))
% 22.35/22.67                    (accountability a a_3 T1))
% 22.35/22.67                  (accountability a a_4 T2))
% 22.35/22.67                (Not (greater Ta T1)))
% 22.35/22.67              (greater T2 T1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater a_1 a_2) (greater a_3 a_4))
% 22.35/22.67      True
% 22.35/22.67  Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.35/22.67    Eq
% 22.35/22.67      (∀ (T2 Ta Tb : Iota),
% 22.35/22.67        And
% 22.35/22.67            (And
% 22.35/22.67              (And
% 22.35/22.67                (And
% 22.35/22.67                  (And
% 22.35/22.67                    (And
% 22.35/22.67                      (And (And (And (organization a a_1) (organization a T2)) (reorganization a Ta Tb))
% 22.35/22.67                        (reliability a a_2 a_1))
% 22.35/22.67                      (reliability a a_3 T2))
% 22.35/22.67                    (accountability a a_4 a_1))
% 22.35/22.67                  (accountability a a_5 T2))
% 22.35/22.67                (Not (greater Ta a_1)))
% 22.35/22.67              (greater T2 a_1))
% 22.35/22.67            (Not (greater T2 Tb)) →
% 22.35/22.67          And (greater a_2 a_3) (greater a_4 a_5))
% 22.35/22.67      True
% 22.35/22.67  Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.35/22.67    Eq
% 22.35/22.68      (∀ (Ta Tb : Iota),
% 22.35/22.68        And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And
% 22.35/22.68                    (And
% 22.35/22.68                      (And (And (And (organization a a_1) (organization a a_2)) (reorganization a Ta Tb))
% 22.35/22.68                        (reliability a a_3 a_1))
% 22.35/22.68                      (reliability a a_4 a_2))
% 22.35/22.68                    (accountability a a_5 a_1))
% 22.35/22.68                  (accountability a a_6 a_2))
% 22.35/22.68                (Not (greater Ta a_1)))
% 22.35/22.68              (greater a_2 a_1))
% 22.35/22.68            (Not (greater a_2 Tb)) →
% 22.35/22.68          And (greater a_3 a_4) (greater a_5 a_6))
% 22.35/22.68      True
% 22.35/22.68  Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.35/22.68    Eq
% 22.35/22.68      (∀ (Tb : Iota),
% 22.35/22.68        And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And
% 22.35/22.68                    (And
% 22.35/22.68                      (And (And (And (organization a a_1) (organization a a_2)) (reorganization a a_3 Tb))
% 22.35/22.68                        (reliability a a_4 a_1))
% 22.35/22.68                      (reliability a a_5 a_2))
% 22.35/22.68                    (accountability a a_6 a_1))
% 22.35/22.68                  (accountability a a_7 a_2))
% 22.35/22.68                (Not (greater a_3 a_1)))
% 22.35/22.68              (greater a_2 a_1))
% 22.35/22.68            (Not (greater a_2 Tb)) →
% 22.35/22.68          And (greater a_4 a_5) (greater a_6 a_7))
% 22.35/22.68      True
% 22.35/22.68  Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.68    Eq
% 22.35/22.68      (And
% 22.35/22.68          (And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And
% 22.35/22.68                    (And (And (And (organization a a_1) (organization a a_2)) (reorganization a a_3 a_4))
% 22.35/22.68                      (reliability a a_5 a_1))
% 22.35/22.68                    (reliability a a_6 a_2))
% 22.35/22.68                  (accountability a a_7 a_1))
% 22.35/22.68                (accountability a a_8 a_2))
% 22.35/22.68              (Not (greater a_3 a_1)))
% 22.35/22.68            (greater a_2 a_1))
% 22.35/22.68          (Not (greater a_2 a_4)) →
% 22.35/22.68        And (greater a_5 a_6) (greater a_7 a_8))
% 22.35/22.68      True
% 22.35/22.68  Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.68    Or
% 22.35/22.68      (Eq
% 22.35/22.68        (And
% 22.35/22.68          (And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And
% 22.35/22.68                    (And (And (And (organization a a_1) (organization a a_2)) (reorganization a a_3 a_4))
% 22.35/22.68                      (reliability a a_5 a_1))
% 22.35/22.68                    (reliability a a_6 a_2))
% 22.35/22.68                  (accountability a a_7 a_1))
% 22.35/22.68                (accountability a a_8 a_2))
% 22.35/22.68              (Not (greater a_3 a_1)))
% 22.35/22.68            (greater a_2 a_1))
% 22.35/22.68          (Not (greater a_2 a_4)))
% 22.35/22.68        False)
% 22.35/22.68      (Eq (And (greater a_5 a_6) (greater a_7 a_8)) True)
% 22.35/22.68  Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.68    Or (Eq (And (greater a a_1) (greater a_2 a_3)) True)
% 22.35/22.68      (Or
% 22.35/22.68        (Eq
% 22.35/22.68          (And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And
% 22.35/22.68                    (And (And (And (organization a_4 a_5) (organization a_4 a_6)) (reorganization a_4 a_7 a_8))
% 22.35/22.68                      (reliability a_4 a a_5))
% 22.35/22.68                    (reliability a_4 a_1 a_6))
% 22.35/22.68                  (accountability a_4 a_2 a_5))
% 22.35/22.68                (accountability a_4 a_3 a_6))
% 22.35/22.68              (Not (greater a_7 a_5)))
% 22.35/22.68            (greater a_6 a_5))
% 22.35/22.68          False)
% 22.35/22.68        (Eq (Not (greater a_6 a_8)) False))
% 22.35/22.68  Clause #64 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.68    Or
% 22.35/22.68      (Eq
% 22.35/22.68        (And
% 22.35/22.68          (And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And (And (And (organization a a_1) (organization a a_2)) (reorganization a a_3 a_4))
% 22.35/22.68                    (reliability a a_5 a_1))
% 22.35/22.68                  (reliability a a_6 a_2))
% 22.35/22.68                (accountability a a_7 a_1))
% 22.35/22.68              (accountability a a_8 a_2))
% 22.35/22.68            (Not (greater a_3 a_1)))
% 22.35/22.68          (greater a_2 a_1))
% 22.35/22.68        False)
% 22.35/22.68      (Or (Eq (Not (greater a_2 a_4)) False) (Eq (greater a_7 a_8) True))
% 22.35/22.68  Clause #65 (by clausification #[63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.35/22.68    Or
% 22.35/22.68      (Eq
% 22.35/22.68        (And
% 22.35/22.68          (And
% 22.35/22.68            (And
% 22.35/22.68              (And
% 22.35/22.68                (And
% 22.35/22.68                  (And (And (And (organization a a_1) (organization a a_2)) (reorganization a a_3 a_4))
% 22.35/22.68                    (reliability a a_5 a_1))
% 22.35/22.68                  (reliability a a_6 a_2))
% 22.45/22.70                (accountability a a_7 a_1))
% 22.45/22.70              (accountability a a_8 a_2))
% 22.45/22.70            (Not (greater a_3 a_1)))
% 22.45/22.70          (greater a_2 a_1))
% 22.45/22.70        False)
% 22.45/22.70      (Or (Eq (Not (greater a_2 a_4)) False) (Eq (greater a_5 a_6) True))
% 22.45/22.70  Clause #66 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (Not (greater a a_1)) False)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) True)
% 22.45/22.70        (Or
% 22.45/22.70          (Eq
% 22.45/22.70            (And
% 22.45/22.70              (And
% 22.45/22.70                (And
% 22.45/22.70                  (And
% 22.45/22.70                    (And (And (And (organization a_4 a_5) (organization a_4 a)) (reorganization a_4 a_6 a_1))
% 22.45/22.70                      (reliability a_4 a_7 a_5))
% 22.45/22.70                    (reliability a_4 a_8 a))
% 22.45/22.70                  (accountability a_4 a_2 a_5))
% 22.45/22.70                (accountability a_4 a_3 a))
% 22.45/22.70              (Not (greater a_6 a_5)))
% 22.45/22.70            False)
% 22.45/22.70          (Eq (greater a a_5) False)))
% 22.45/22.70  Clause #67 (by clausification #[66]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or
% 22.45/22.70        (Eq
% 22.45/22.70          (And
% 22.45/22.70            (And
% 22.45/22.70              (And
% 22.45/22.70                (And
% 22.45/22.70                  (And (And (And (organization a_2 a_3) (organization a_2 a_4)) (reorganization a_2 a_5 a_6))
% 22.45/22.70                    (reliability a_2 a_7 a_3))
% 22.45/22.70                  (reliability a_2 a_8 a_4))
% 22.45/22.70                (accountability a_2 a a_3))
% 22.45/22.70              (accountability a_2 a_1 a_4))
% 22.45/22.70            (Not (greater a_5 a_3)))
% 22.45/22.70          False)
% 22.45/22.70        (Or (Eq (greater a_4 a_3) False) (Eq (greater a_4 a_6) True)))
% 22.45/22.70  Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.70        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.70          (Or
% 22.45/22.70            (Eq
% 22.45/22.70              (And
% 22.45/22.70                (And
% 22.45/22.70                  (And
% 22.45/22.70                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.70                      (reliability a_5 a_7 a_3))
% 22.45/22.70                    (reliability a_5 a_8 a_2))
% 22.45/22.70                  (accountability a_5 a a_3))
% 22.45/22.70                (accountability a_5 a_1 a_2))
% 22.45/22.70              False)
% 22.45/22.70            (Eq (Not (greater a_6 a_3)) False))))
% 22.45/22.70  Clause #69 (by clausification #[68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.70        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.70          (Or (Eq (Not (greater a_5 a_3)) False)
% 22.45/22.70            (Or
% 22.45/22.70              (Eq
% 22.45/22.70                (And
% 22.45/22.70                  (And
% 22.45/22.70                    (And (And (And (organization a_6 a_3) (organization a_6 a_2)) (reorganization a_6 a_5 a_4))
% 22.45/22.70                      (reliability a_6 a_7 a_3))
% 22.45/22.70                    (reliability a_6 a_8 a_2))
% 22.45/22.70                  (accountability a_6 a a_3))
% 22.45/22.70                False)
% 22.45/22.70              (Eq (accountability a_6 a_1 a_2) False)))))
% 22.45/22.70  Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.70        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.70          (Or
% 22.45/22.70            (Eq
% 22.45/22.70              (And
% 22.45/22.70                (And
% 22.45/22.70                  (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.70                    (reliability a_5 a_7 a_3))
% 22.45/22.70                  (reliability a_5 a_8 a_2))
% 22.45/22.70                (accountability a_5 a a_3))
% 22.45/22.70              False)
% 22.45/22.70            (Or (Eq (accountability a_5 a_1 a_2) False) (Eq (greater a_6 a_3) True)))))
% 22.45/22.70  Clause #71 (by clausification #[70]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.70        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.70          (Or (Eq (accountability a_5 a_1 a_2) False)
% 22.45/22.70            (Or (Eq (greater a_6 a_3) True)
% 22.45/22.70              (Or
% 22.45/22.70                (Eq
% 22.45/22.70                  (And
% 22.45/22.70                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.70                      (reliability a_5 a_7 a_3))
% 22.45/22.70                    (reliability a_5 a_8 a_2))
% 22.45/22.70                  False)
% 22.45/22.70                (Eq (accountability a_5 a a_3) False))))))
% 22.45/22.70  Clause #72 (by clausification #[71]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.70    Or (Eq (greater a a_1) True)
% 22.45/22.70      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.72        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.72          (Or (Eq (accountability a_5 a_1 a_2) False)
% 22.45/22.72            (Or (Eq (greater a_6 a_3) True)
% 22.45/22.72              (Or (Eq (accountability a_5 a a_3) False)
% 22.45/22.72                (Or
% 22.45/22.72                  (Eq
% 22.45/22.72                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.72                      (reliability a_5 a_7 a_3))
% 22.45/22.72                    False)
% 22.45/22.72                  (Eq (reliability a_5 a_8 a_2) False)))))))
% 22.45/22.72  Clause #73 (by clausification #[72]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (greater a a_1) True)
% 22.45/22.72      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.72        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.72          (Or (Eq (accountability a_5 a_1 a_2) False)
% 22.45/22.72            (Or (Eq (greater a_6 a_3) True)
% 22.45/22.72              (Or (Eq (accountability a_5 a a_3) False)
% 22.45/22.72                (Or (Eq (reliability a_5 a_7 a_2) False)
% 22.45/22.72                  (Or (Eq (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4)) False)
% 22.45/22.72                    (Eq (reliability a_5 a_8 a_3) False))))))))
% 22.45/22.72  Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (greater a a_1) True)
% 22.45/22.72      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.72        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.72          (Or (Eq (accountability a_5 a_1 a_2) False)
% 22.45/22.72            (Or (Eq (greater a_6 a_3) True)
% 22.45/22.72              (Or (Eq (accountability a_5 a a_3) False)
% 22.45/22.72                (Or (Eq (reliability a_5 a_7 a_2) False)
% 22.45/22.72                  (Or (Eq (reliability a_5 a_8 a_3) False)
% 22.45/22.72                    (Or (Eq (And (organization a_5 a_3) (organization a_5 a_2)) False)
% 22.45/22.72                      (Eq (reorganization a_5 a_6 a_4) False)))))))))
% 22.45/22.72  Clause #75 (by clausification #[74]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (greater a a_1) True)
% 22.45/22.72      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.72        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.72          (Or (Eq (accountability a_5 a_1 a_2) False)
% 22.45/22.72            (Or (Eq (greater a_6 a_3) True)
% 22.45/22.72              (Or (Eq (accountability a_5 a a_3) False)
% 22.45/22.72                (Or (Eq (reliability a_5 a_7 a_2) False)
% 22.45/22.72                  (Or (Eq (reliability a_5 a_8 a_3) False)
% 22.45/22.72                    (Or (Eq (reorganization a_5 a_6 a_4) False)
% 22.45/22.72                      (Or (Eq (organization a_5 a_3) False) (Eq (organization a_5 a_2) False))))))))))
% 22.45/22.72  Clause #76 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (Not (greater a a_1)) False)
% 22.45/22.72      (Or (Eq (greater a_2 a_3) True)
% 22.45/22.72        (Or
% 22.45/22.72          (Eq
% 22.45/22.72            (And
% 22.45/22.72              (And
% 22.45/22.72                (And
% 22.45/22.72                  (And
% 22.45/22.72                    (And (And (And (organization a_4 a_5) (organization a_4 a)) (reorganization a_4 a_6 a_1))
% 22.45/22.72                      (reliability a_4 a_2 a_5))
% 22.45/22.72                    (reliability a_4 a_3 a))
% 22.45/22.72                  (accountability a_4 a_7 a_5))
% 22.45/22.72                (accountability a_4 a_8 a))
% 22.45/22.72              (Not (greater a_6 a_5)))
% 22.45/22.72            False)
% 22.45/22.72          (Eq (greater a a_5) False)))
% 22.45/22.72  Clause #77 (by clausification #[76]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (greater a a_1) True)
% 22.45/22.72      (Or
% 22.45/22.72        (Eq
% 22.45/22.72          (And
% 22.45/22.72            (And
% 22.45/22.72              (And
% 22.45/22.72                (And
% 22.45/22.72                  (And (And (And (organization a_2 a_3) (organization a_2 a_4)) (reorganization a_2 a_5 a_6))
% 22.45/22.72                    (reliability a_2 a a_3))
% 22.45/22.72                  (reliability a_2 a_1 a_4))
% 22.45/22.72                (accountability a_2 a_7 a_3))
% 22.45/22.72              (accountability a_2 a_8 a_4))
% 22.45/22.72            (Not (greater a_5 a_3)))
% 22.45/22.72          False)
% 22.45/22.72        (Or (Eq (greater a_4 a_3) False) (Eq (greater a_4 a_6) True)))
% 22.45/22.72  Clause #78 (by clausification #[77]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.72    Or (Eq (greater a a_1) True)
% 22.45/22.72      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.72        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.72          (Or
% 22.45/22.72            (Eq
% 22.45/22.72              (And
% 22.45/22.72                (And
% 22.45/22.72                  (And
% 22.45/22.72                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.72                      (reliability a_5 a a_3))
% 22.45/22.72                    (reliability a_5 a_1 a_2))
% 22.45/22.72                  (accountability a_5 a_7 a_3))
% 22.45/22.72                (accountability a_5 a_8 a_2))
% 22.45/22.72              False)
% 22.45/22.72            (Eq (Not (greater a_6 a_3)) False))))
% 22.45/22.73  Clause #79 (by clausification #[78]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (Not (greater a_5 a_3)) False)
% 22.45/22.73            (Or
% 22.45/22.73              (Eq
% 22.45/22.73                (And
% 22.45/22.73                  (And
% 22.45/22.73                    (And (And (And (organization a_6 a_3) (organization a_6 a_2)) (reorganization a_6 a_5 a_4))
% 22.45/22.73                      (reliability a_6 a a_3))
% 22.45/22.73                    (reliability a_6 a_1 a_2))
% 22.45/22.73                  (accountability a_6 a_7 a_3))
% 22.45/22.73                False)
% 22.45/22.73              (Eq (accountability a_6 a_8 a_2) False)))))
% 22.45/22.73  Clause #80 (by clausification #[79]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or
% 22.45/22.73            (Eq
% 22.45/22.73              (And
% 22.45/22.73                (And
% 22.45/22.73                  (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_6 a_4))
% 22.45/22.73                    (reliability a_5 a a_3))
% 22.45/22.73                  (reliability a_5 a_1 a_2))
% 22.45/22.73                (accountability a_5 a_7 a_3))
% 22.45/22.73              False)
% 22.45/22.73            (Or (Eq (accountability a_5 a_8 a_2) False) (Eq (greater a_6 a_3) True)))))
% 22.45/22.73  Clause #81 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (accountability a_5 a_6 a_2) False)
% 22.45/22.73            (Or (Eq (greater a_7 a_3) True)
% 22.45/22.73              (Or
% 22.45/22.73                (Eq
% 22.45/22.73                  (And
% 22.45/22.73                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_7 a_4))
% 22.45/22.73                      (reliability a_5 a a_3))
% 22.45/22.73                    (reliability a_5 a_1 a_2))
% 22.45/22.73                  False)
% 22.45/22.73                (Eq (accountability a_5 a_8 a_3) False))))))
% 22.45/22.73  Clause #82 (by clausification #[81]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (accountability a_5 a_6 a_2) False)
% 22.45/22.73            (Or (Eq (greater a_7 a_3) True)
% 22.45/22.73              (Or (Eq (accountability a_5 a_8 a_3) False)
% 22.45/22.73                (Or
% 22.45/22.73                  (Eq
% 22.45/22.73                    (And (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_7 a_4))
% 22.45/22.73                      (reliability a_5 a a_3))
% 22.45/22.73                    False)
% 22.45/22.73                  (Eq (reliability a_5 a_1 a_2) False)))))))
% 22.45/22.73  Clause #83 (by clausification #[82]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (accountability a_5 a_6 a_2) False)
% 22.45/22.73            (Or (Eq (greater a_7 a_3) True)
% 22.45/22.73              (Or (Eq (accountability a_5 a_8 a_3) False)
% 22.45/22.73                (Or (Eq (reliability a_5 a_1 a_2) False)
% 22.45/22.73                  (Or (Eq (And (And (organization a_5 a_3) (organization a_5 a_2)) (reorganization a_5 a_7 a_4)) False)
% 22.45/22.73                    (Eq (reliability a_5 a a_3) False))))))))
% 22.45/22.73  Clause #84 (by clausification #[83]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (accountability a_5 a_6 a_2) False)
% 22.45/22.73            (Or (Eq (greater a_7 a_3) True)
% 22.45/22.73              (Or (Eq (accountability a_5 a_8 a_3) False)
% 22.45/22.73                (Or (Eq (reliability a_5 a_1 a_2) False)
% 22.45/22.73                  (Or (Eq (reliability a_5 a a_3) False)
% 22.45/22.73                    (Or (Eq (And (organization a_5 a_3) (organization a_5 a_2)) False)
% 22.45/22.73                      (Eq (reorganization a_5 a_7 a_4) False)))))))))
% 22.45/22.73  Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.45/22.73    Or (Eq (greater a a_1) True)
% 22.45/22.73      (Or (Eq (greater a_2 a_3) False)
% 22.45/22.73        (Or (Eq (greater a_2 a_4) True)
% 22.45/22.73          (Or (Eq (accountability a_5 a_6 a_2) False)
% 22.45/22.73            (Or (Eq (greater a_7 a_3) True)
% 22.45/22.73              (Or (Eq (accountability a_5 a_8 a_3) False)
% 22.45/22.73                (Or (Eq (reliability a_5 a_1 a_2) False)
% 22.45/22.73                  (Or (Eq (reliability a_5 a a_3) False)
% 22.45/22.76                    (Or (Eq (reorganization a_5 a_7 a_4) False)
% 22.45/22.76                      (Or (Eq (organization a_5 a_3) False) (Eq (organization a_5 a_2) False))))))))))
% 22.45/22.76  Clause #86 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (greater (skS.0 6 a a_1 a_2 a_3 a_4) (skS.0 5 a a_1 a_2 a_3)) True
% 22.45/22.76  Clause #87 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.45/22.76    Eq
% 22.45/22.76      (And
% 22.45/22.76        (And
% 22.45/22.76          (And
% 22.45/22.76            (And
% 22.45/22.76              (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.45/22.76                (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.76              (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.45/22.76            (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.45/22.76          (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.76        (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))))
% 22.45/22.76      True
% 22.45/22.76  Clause #89 (by superposition #[86, 75]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.45/22.76    Or (Eq (greater a a_1) True)
% 22.45/22.76      (Or (Eq True False)
% 22.45/22.76        (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.45/22.76          (Or (Eq (accountability a_8 a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76            (Or (Eq (greater a_9 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.45/22.76              (Or (Eq (accountability a_8 a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                (Or (Eq (reliability a_8 a_10 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76                  (Or (Eq (reliability a_8 a_11 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                    (Or (Eq (reorganization a_8 a_9 a_7) False)
% 22.45/22.76                      (Or (Eq (organization a_8 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                        (Eq (organization a_8 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False))))))))))
% 22.45/22.76  Clause #90 (by superposition #[86, 85]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.45/22.76    Or (Eq (greater a a_1) True)
% 22.45/22.76      (Or (Eq True False)
% 22.45/22.76        (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.45/22.76          (Or (Eq (accountability a_8 a_9 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76            (Or (Eq (greater a_10 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.45/22.76              (Or (Eq (accountability a_8 a_11 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                (Or (Eq (reliability a_8 a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76                  (Or (Eq (reliability a_8 a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                    (Or (Eq (reorganization a_8 a_10 a_7) False)
% 22.45/22.76                      (Or (Eq (organization a_8 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                        (Eq (organization a_8 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False))))))))))
% 22.45/22.76  Clause #94 (by clausification #[90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.45/22.76    Or (Eq (greater a a_1) True)
% 22.45/22.76      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.45/22.76        (Or (Eq (accountability a_8 a_9 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76          (Or (Eq (greater a_10 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.45/22.76            (Or (Eq (accountability a_8 a_11 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76              (Or (Eq (reliability a_8 a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.76                (Or (Eq (reliability a_8 a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                  (Or (Eq (reorganization a_8 a_10 a_7) False)
% 22.45/22.76                    (Or (Eq (organization a_8 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.76                      (Eq (organization a_8 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)))))))))
% 22.45/22.76  Clause #95 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (Not (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3))) True
% 22.45/22.76  Clause #96 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.45/22.76    Eq
% 22.45/22.76      (And
% 22.45/22.76        (And
% 22.45/22.76          (And
% 22.45/22.76            (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3))
% 22.45/22.76              (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.76            (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.45/22.76          (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.45/22.76        (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.78      True
% 22.45/22.78  Clause #97 (by clausification #[95]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), Eq (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 5 a a_1 a_2 a_3)) False
% 22.45/22.78  Clause #98 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.45/22.78    Or (Eq (greater a a_1) True)
% 22.45/22.78      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.45/22.78        (Or (Eq (accountability a_8 a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.78          (Or (Eq (greater a_9 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.45/22.78            (Or (Eq (accountability a_8 a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.78              (Or (Eq (reliability a_8 a_10 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.45/22.78                (Or (Eq (reliability a_8 a_11 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.78                  (Or (Eq (reorganization a_8 a_9 a_7) False)
% 22.45/22.78                    (Or (Eq (organization a_8 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.45/22.78                      (Eq (organization a_8 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)))))))))
% 22.45/22.78  Clause #99 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (survival_chance (skS.0 2 a) (skS.0 4 a a_1 a_2) (skS.0 6 a a_1 a_2 a_3 a_4)) True
% 22.45/22.78  Clause #100 (by clausification #[96]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.45/22.78    Eq
% 22.45/22.78      (And
% 22.45/22.78        (And
% 22.45/22.78          (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.78          (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.45/22.78        (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)))
% 22.45/22.78      True
% 22.45/22.78  Clause #102 (by clausification #[100]): ∀ (a a_1 a_2 a_3 : Iota), Eq (survival_chance (skS.0 2 a) (skS.0 3 a a_1) (skS.0 5 a a_1 a_2 a_3)) True
% 22.45/22.78  Clause #103 (by clausification #[100]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.45/22.78    Eq
% 22.45/22.78      (And (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.78        (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)))
% 22.45/22.78      True
% 22.45/22.78  Clause #105 (by clausification #[103]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.45/22.78    Eq (reorganization (skS.0 2 a) (skS.0 7 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6)) True
% 22.45/22.78  Clause #106 (by clausification #[103]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.45/22.78    Eq (And (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)))
% 22.45/22.78      True
% 22.45/22.78  Clause #107 (by clausification #[106]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (organization (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4)) True
% 22.45/22.78  Clause #108 (by clausification #[106]): ∀ (a a_1 a_2 a_3 : Iota), Eq (organization (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3)) True
% 22.45/22.78  Clause #109 (by superposition #[107, 8]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.45/22.78    Or (Eq True False)
% 22.45/22.78      (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_4))
% 22.45/22.78        True)
% 22.45/22.78  Clause #110 (by superposition #[107, 12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.45/22.78    Or (Eq True False)
% 22.45/22.78      (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_4))
% 22.45/22.78        True)
% 22.45/22.78  Clause #116 (by superposition #[108, 8]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.45/22.78    Or (Eq True False)
% 22.45/22.78      (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 5 a a_1 a_2 a_3)) True)
% 22.45/22.78  Clause #117 (by superposition #[108, 12]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.45/22.78    Or (Eq True False)
% 22.45/22.78      (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 5 a a_1 a_2 a_3)) True)
% 22.45/22.78  Clause #118 (by clausification #[117]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.45/22.78    Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 5 a a_1 a_2 a_3)) True
% 22.45/22.78  Clause #119 (by clausification #[116]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 22.45/22.78    Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 5 a a_1 a_2 a_3)) True
% 22.45/22.78  Clause #120 (by clausification #[110]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.45/22.78    Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_4)) True
% 22.55/22.80  Clause #121 (by clausification #[109]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 22.55/22.80    Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_4)) True
% 22.55/22.80  Clause #122 (by superposition #[121, 94]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.80    Or (Eq (greater a a_1) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.80        (Or (Eq True False)
% 22.55/22.80          (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.80            (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80              (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.80                (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                  (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False)
% 22.55/22.80                    (Or (Eq (organization (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                      (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)))))))))
% 22.55/22.80  Clause #123 (by superposition #[121, 98]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.80    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.80        (Or (Eq True False)
% 22.55/22.80          (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.80            (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.80              (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.80                  (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False)
% 22.55/22.80                    (Or (Eq (organization (skS.0 2 a_1) (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.80                      (Eq (organization (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)))))))))
% 22.55/22.80  Clause #129 (by clausification #[122]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.80    Or (Eq (greater a a_1) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.80        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.80          (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80            (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.80              (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False)
% 22.55/22.80                  (Or (Eq (organization (skS.0 2 a_2) (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                    (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False))))))))
% 22.55/22.80  Clause #130 (by forward demodulation #[129, 108]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.80    Or (Eq (greater a a_1) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.80        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.80          (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80            (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.80              (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False)
% 22.55/22.80                  (Or (Eq True False) (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False))))))))
% 22.55/22.80  Clause #131 (by clausification #[130]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.80    Or (Eq (greater a a_1) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.80        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.80          (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80            (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.80              (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.80                (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False)
% 22.55/22.80                  (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)))))))
% 22.55/22.80  Clause #132 (by forward demodulation #[131, 107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.80    Or (Eq (greater a a_1) True)
% 22.55/22.80      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.83          (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83            (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.83              (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83                (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False) (Eq True False)))))))
% 22.55/22.83  Clause #133 (by clausification #[132]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.83    Or (Eq (greater a a_1) True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.83          (Or (Eq (accountability (skS.0 2 a_2) a_9 (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83            (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.83              (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83                (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False))))))
% 22.55/22.83  Clause #134 (by superposition #[133, 119]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or (Eq (greater a a_1) True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.83          (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.83            (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83              (Or (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False) (Eq False True))))))
% 22.55/22.83  Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or (Eq (greater a a_1) True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a_2 a_3 a_4 a_5 a_6) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_2 a_3 a_4 a_5)) True)
% 22.55/22.83          (Or (Eq (reliability (skS.0 2 a_2) a_1 (skS.0 6 a_2 a_3 a_4 a_5 a_6)) False)
% 22.55/22.83            (Or (Eq (reliability (skS.0 2 a_2) a (skS.0 5 a_2 a_3 a_4 a_5)) False)
% 22.55/22.83              (Eq (reorganization (skS.0 2 a_2) a_8 a_7) False)))))
% 22.55/22.83  Clause #136 (by superposition #[135, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or (Eq (greater a (skS.0 1 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.83          (Or (Eq (reliability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.83            (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False) (Eq False True)))))
% 22.55/22.83  Clause #137 (by clausification #[136]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or (Eq (greater a (skS.0 1 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.83          (Or (Eq (reliability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.83            (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False))))
% 22.55/22.83  Clause #138 (by superposition #[137, 118]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or
% 22.55/22.83      (Eq
% 22.55/22.83        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.83        True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.83          (Or (Eq (reorganization (skS.0 2 a) a_8 a_7) False) (Eq False True))))
% 22.55/22.83  Clause #139 (by clausification #[138]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.83    Or
% 22.55/22.83      (Eq
% 22.55/22.83        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.83        True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.83        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True) (Eq (reorganization (skS.0 2 a) a_8 a_7) False)))
% 22.55/22.83  Clause #140 (by superposition #[139, 105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 22.55/22.83    Or
% 22.55/22.83      (Eq
% 22.55/22.83        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.83        True)
% 22.55/22.83      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) (skS.0 8 a a_7 a_8 a_9 a_10 a_11 a_12)) True)
% 22.55/22.83        (Or (Eq (greater (skS.0 7 a a_7 a_8 a_9 a_10 a_11) (skS.0 5 a a_1 a_2 a_3)) True) (Eq False True)))
% 22.55/22.85  Clause #141 (by clausification #[140]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 22.55/22.85    Or
% 22.55/22.85      (Eq
% 22.55/22.85        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.85        True)
% 22.55/22.85      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) (skS.0 8 a a_7 a_8 a_9 a_10 a_11 a_12)) True)
% 22.55/22.85        (Eq (greater (skS.0 7 a a_7 a_8 a_9 a_10 a_11) (skS.0 5 a a_1 a_2 a_3)) True))
% 22.55/22.85  Clause #146 (by superposition #[141, 32]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.55/22.85    Or
% 22.55/22.85      (Eq
% 22.55/22.85        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.85        True)
% 22.55/22.85      (Or (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_5 a_7) (skS.0 5 a a_1 a_2 a_3)) True) (Eq True False))
% 22.55/22.85  Clause #154 (by clausification #[146]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.55/22.85    Or
% 22.55/22.85      (Eq
% 22.55/22.85        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.85        True)
% 22.55/22.85      (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_5 a_7) (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.85  Clause #159 (by superposition #[154, 97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.55/22.85    Or
% 22.55/22.85      (Eq
% 22.55/22.85        (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.85        True)
% 22.55/22.85      (Eq True False)
% 22.55/22.85  Clause #164 (by clausification #[159]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.55/22.85    Eq (greater (skS.0 1 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.85      True
% 22.55/22.85  Clause #188 (by clausification #[123]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.85    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.85      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.85        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.85          (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85            (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.85              (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85                (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False)
% 22.55/22.85                  (Or (Eq (organization (skS.0 2 a_1) (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85                    (Eq (organization (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False))))))))
% 22.55/22.85  Clause #189 (by forward demodulation #[188, 108]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.85    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.85      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.85        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.85          (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85            (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.85              (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85                (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False)
% 22.55/22.85                  (Or (Eq True False) (Eq (organization (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False))))))))
% 22.55/22.85  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 : Iota),
% 22.55/22.85    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.85      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.85        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.85          (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85            (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.85              (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.85                (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False)
% 22.55/22.85                  (Eq (organization (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)))))))
% 22.55/22.85  Clause #191 (by forward demodulation #[190, 107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.85    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.85      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.88          (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.88            (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.88              (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.88                (Or (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False) (Eq True False)))))))
% 22.55/22.88  Clause #192 (by clausification #[191]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.88    Or (Eq (greater a (skS.0 0 (skS.0 2 a_1) (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_6)) True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a_1 a_2 a_3 a_4 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a_1 a_2 a_3 a_4)) True)
% 22.55/22.88          (Or (Eq (accountability (skS.0 2 a_1) a (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.88            (Or (Eq (reliability (skS.0 2 a_1) a_9 (skS.0 6 a_1 a_2 a_3 a_4 a_5)) False)
% 22.55/22.88              (Or (Eq (reliability (skS.0 2 a_1) a_10 (skS.0 5 a_1 a_2 a_3 a_4)) False)
% 22.55/22.88                (Eq (reorganization (skS.0 2 a_1) a_8 a_7) False))))))
% 22.55/22.88  Clause #193 (by superposition #[192, 119]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.88          (Or (Eq (reliability (skS.0 2 a) a_9 (skS.0 6 a a_1 a_2 a_3 a_5)) False)
% 22.55/22.88            (Or (Eq (reliability (skS.0 2 a) a_10 (skS.0 5 a a_1 a_2 a_3)) False)
% 22.55/22.88              (Or (Eq (reorganization (skS.0 2 a) a_8 a_7) False) (Eq False True))))))
% 22.55/22.88  Clause #194 (by clausification #[193]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.88          (Or (Eq (reliability (skS.0 2 a) a_9 (skS.0 6 a a_1 a_2 a_3 a_5)) False)
% 22.55/22.88            (Or (Eq (reliability (skS.0 2 a) a_10 (skS.0 5 a a_1 a_2 a_3)) False)
% 22.55/22.88              (Eq (reorganization (skS.0 2 a) a_8 a_7) False)))))
% 22.55/22.88  Clause #195 (by superposition #[194, 120]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.88          (Or (Eq (reliability (skS.0 2 a) a_9 (skS.0 5 a a_1 a_2 a_3)) False)
% 22.55/22.88            (Or (Eq (reorganization (skS.0 2 a) a_8 a_7) False) (Eq False True)))))
% 22.55/22.88  Clause #196 (by clausification #[195]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.88          (Or (Eq (reliability (skS.0 2 a) a_9 (skS.0 5 a a_1 a_2 a_3)) False)
% 22.55/22.88            (Eq (reorganization (skS.0 2 a) a_8 a_7) False))))
% 22.55/22.88  Clause #197 (by superposition #[196, 118]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True)
% 22.55/22.88          (Or (Eq (reorganization (skS.0 2 a) a_8 a_7) False) (Eq False True))))
% 22.55/22.88  Clause #198 (by clausification #[197]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 22.55/22.88    Or
% 22.55/22.88      (Eq
% 22.55/22.88        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.55/22.88        True)
% 22.55/22.88      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) a_7) True)
% 22.55/22.88        (Or (Eq (greater a_8 (skS.0 5 a a_1 a_2 a_3)) True) (Eq (reorganization (skS.0 2 a) a_8 a_7) False)))
% 22.65/22.90  Clause #199 (by superposition #[198, 105]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 22.65/22.90    Or
% 22.65/22.90      (Eq
% 22.65/22.90        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90        True)
% 22.65/22.90      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) (skS.0 8 a a_7 a_8 a_9 a_10 a_11 a_12)) True)
% 22.65/22.90        (Or (Eq (greater (skS.0 7 a a_7 a_8 a_9 a_10 a_11) (skS.0 5 a a_1 a_2 a_3)) True) (Eq False True)))
% 22.65/22.90  Clause #200 (by clausification #[199]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 22.65/22.90    Or
% 22.65/22.90      (Eq
% 22.65/22.90        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90        True)
% 22.65/22.90      (Or (Eq (greater (skS.0 6 a a_1 a_2 a_3 a_5) (skS.0 8 a a_7 a_8 a_9 a_10 a_11 a_12)) True)
% 22.65/22.90        (Eq (greater (skS.0 7 a a_7 a_8 a_9 a_10 a_11) (skS.0 5 a a_1 a_2 a_3)) True))
% 22.65/22.90  Clause #206 (by superposition #[200, 32]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.65/22.90    Or
% 22.65/22.90      (Eq
% 22.65/22.90        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90        True)
% 22.65/22.90      (Or (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_5 a_7) (skS.0 5 a a_1 a_2 a_3)) True) (Eq True False))
% 22.65/22.90  Clause #212 (by clausification #[206]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 22.65/22.90    Or
% 22.65/22.90      (Eq
% 22.65/22.90        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90        True)
% 22.65/22.90      (Eq (greater (skS.0 7 a a_1 a_2 a_3 a_5 a_7) (skS.0 5 a a_1 a_2 a_3)) True)
% 22.65/22.90  Clause #218 (by superposition #[212, 97]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.90    Or
% 22.65/22.90      (Eq
% 22.65/22.90        (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90        True)
% 22.65/22.90      (Eq True False)
% 22.65/22.90  Clause #227 (by clausification #[218]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.90    Eq (greater (skS.0 0 (skS.0 2 a) (skS.0 5 a a_1 a_2 a_3) a_4) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_5) a_6))
% 22.65/22.90      True
% 22.65/22.90  Clause #228 (by superposition #[227, 52]): ∀ (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),
% 22.65/22.90    Or (Eq (greater a a_1) True)
% 22.65/22.90      (Or (Eq True False)
% 22.65/22.90        (Or (Eq (greater a_2 a_3) False)
% 22.65/22.90          (Or (Eq (survival_chance a_4 a a_5) False)
% 22.65/22.90            (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 22.65/22.90              (Or (Eq (accountability a_4 (skS.0 0 (skS.0 2 a_8) (skS.0 5 a_8 a_9 a_10 a_11) a_12) a_5) False)
% 22.65/22.90                (Or (Eq (accountability a_6 (skS.0 0 (skS.0 2 a_8) (skS.0 6 a_8 a_9 a_10 a_11 a_13) a_14) a_7) False)
% 22.65/22.90                  (Or (Eq (reliability a_4 a_2 a_5) False)
% 22.65/22.90                    (Or (Eq (reliability a_6 a_3 a_7) False)
% 22.65/22.90                      (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False))))))))))
% 22.65/22.90  Clause #233 (by clausification #[228]): ∀ (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),
% 22.65/22.90    Or (Eq (greater a a_1) True)
% 22.65/22.90      (Or (Eq (greater a_2 a_3) False)
% 22.65/22.90        (Or (Eq (survival_chance a_4 a a_5) False)
% 22.65/22.90          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 22.65/22.90            (Or (Eq (accountability a_4 (skS.0 0 (skS.0 2 a_8) (skS.0 5 a_8 a_9 a_10 a_11) a_12) a_5) False)
% 22.65/22.90              (Or (Eq (accountability a_6 (skS.0 0 (skS.0 2 a_8) (skS.0 6 a_8 a_9 a_10 a_11 a_13) a_14) a_7) False)
% 22.65/22.90                (Or (Eq (reliability a_4 a_2 a_5) False)
% 22.65/22.90                  (Or (Eq (reliability a_6 a_3 a_7) False)
% 22.65/22.90                    (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False)))))))))
% 22.65/22.90  Clause #235 (by superposition #[233, 164]): ∀ (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),
% 22.65/22.90    Or (Eq (greater a a_1) True)
% 22.65/22.90      (Or (Eq (survival_chance a_2 a a_3) False)
% 22.65/22.90        (Or (Eq (survival_chance a_4 a_1 a_5) False)
% 22.65/22.90          (Or (Eq (accountability a_2 (skS.0 0 (skS.0 2 a_6) (skS.0 5 a_6 a_7 a_8 a_9) a_10) a_3) False)
% 22.65/22.90            (Or (Eq (accountability a_4 (skS.0 0 (skS.0 2 a_6) (skS.0 6 a_6 a_7 a_8 a_9 a_11) a_12) a_5) False)
% 22.65/22.90              (Or (Eq (reliability a_2 (skS.0 1 (skS.0 2 a_13) (skS.0 5 a_13 a_14 a_15 a_16) a_17) a_3) False)
% 22.65/22.90                (Or (Eq (reliability a_4 (skS.0 1 (skS.0 2 a_13) (skS.0 6 a_13 a_14 a_15 a_16 a_18) a_19) a_5) False)
% 22.65/22.93                  (Or (Eq (organization a_4 a_5) False) (Or (Eq (organization a_2 a_3) False) (Eq False True)))))))))
% 22.65/22.93  Clause #248 (by clausification #[235]): ∀ (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),
% 22.65/22.93    Or (Eq (greater a a_1) True)
% 22.65/22.93      (Or (Eq (survival_chance a_2 a a_3) False)
% 22.65/22.93        (Or (Eq (survival_chance a_4 a_1 a_5) False)
% 22.65/22.93          (Or (Eq (accountability a_2 (skS.0 0 (skS.0 2 a_6) (skS.0 5 a_6 a_7 a_8 a_9) a_10) a_3) False)
% 22.65/22.93            (Or (Eq (accountability a_4 (skS.0 0 (skS.0 2 a_6) (skS.0 6 a_6 a_7 a_8 a_9 a_11) a_12) a_5) False)
% 22.65/22.93              (Or (Eq (reliability a_2 (skS.0 1 (skS.0 2 a_13) (skS.0 5 a_13 a_14 a_15 a_16) a_17) a_3) False)
% 22.65/22.93                (Or (Eq (reliability a_4 (skS.0 1 (skS.0 2 a_13) (skS.0 6 a_13 a_14 a_15 a_16 a_18) a_19) a_5) False)
% 22.65/22.93                  (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False))))))))
% 22.65/22.93  Clause #250 (by superposition #[248, 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 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 22.65/22.93    Or (Eq (greater (skS.0 3 a a_1) a_2) True)
% 22.65/22.93      (Or (Eq (survival_chance a_3 a_2 a_4) False)
% 22.65/22.93        (Or
% 22.65/22.93          (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93            False)
% 22.65/22.93          (Or (Eq (accountability a_3 (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13) a_4) False)
% 22.65/22.93            (Or
% 22.65/22.93              (Eq
% 22.65/22.93                (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_14) (skS.0 5 a_14 a_15 a_16 a_17) a_18)
% 22.65/22.93                  (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93                False)
% 22.65/22.93              (Or (Eq (reliability a_3 (skS.0 1 (skS.0 2 a_14) (skS.0 6 a_14 a_15 a_16 a_17 a_19) a_20) a_4) False)
% 22.65/22.93                (Or (Eq (organization a_3 a_4) False)
% 22.65/22.93                  (Or (Eq (organization (skS.0 2 a) (skS.0 5 a a_1 a_10 a_11)) False) (Eq False True))))))))
% 22.65/22.93  Clause #338 (by clausification #[250]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 22.65/22.93    Or (Eq (greater (skS.0 3 a a_1) a_2) True)
% 22.65/22.93      (Or (Eq (survival_chance a_3 a_2 a_4) False)
% 22.65/22.93        (Or
% 22.65/22.93          (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93            False)
% 22.65/22.93          (Or (Eq (accountability a_3 (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13) a_4) False)
% 22.65/22.93            (Or
% 22.65/22.93              (Eq
% 22.65/22.93                (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_14) (skS.0 5 a_14 a_15 a_16 a_17) a_18)
% 22.65/22.93                  (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93                False)
% 22.65/22.93              (Or (Eq (reliability a_3 (skS.0 1 (skS.0 2 a_14) (skS.0 6 a_14 a_15 a_16 a_17 a_19) a_20) a_4) False)
% 22.65/22.93                (Or (Eq (organization a_3 a_4) False)
% 22.65/22.93                  (Eq (organization (skS.0 2 a) (skS.0 5 a a_1 a_10 a_11)) False)))))))
% 22.65/22.93  Clause #339 (by forward demodulation #[338, 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 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 22.65/22.93    Or (Eq (greater (skS.0 3 a a_1) a_2) True)
% 22.65/22.93      (Or (Eq (survival_chance a_3 a_2 a_4) False)
% 22.65/22.93        (Or
% 22.65/22.93          (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93            False)
% 22.65/22.93          (Or (Eq (accountability a_3 (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13) a_4) False)
% 22.65/22.93            (Or
% 22.65/22.93              (Eq
% 22.65/22.93                (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_14) (skS.0 5 a_14 a_15 a_16 a_17) a_18)
% 22.65/22.93                  (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.93                False)
% 22.65/22.93              (Or (Eq (reliability a_3 (skS.0 1 (skS.0 2 a_14) (skS.0 6 a_14 a_15 a_16 a_17 a_19) a_20) a_4) False)
% 22.65/22.93                (Or (Eq (organization a_3 a_4) False) (Eq True False)))))))
% 22.65/22.93  Clause #340 (by clausification #[339]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 22.65/22.93    Or (Eq (greater (skS.0 3 a a_1) a_2) True)
% 22.65/22.93      (Or (Eq (survival_chance a_3 a_2 a_4) False)
% 22.65/22.93        (Or
% 22.65/22.93          (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95            False)
% 22.65/22.95          (Or (Eq (accountability a_3 (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13) a_4) False)
% 22.65/22.95            (Or
% 22.65/22.95              (Eq
% 22.65/22.95                (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_14) (skS.0 5 a_14 a_15 a_16 a_17) a_18)
% 22.65/22.95                  (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95                False)
% 22.65/22.95              (Or (Eq (reliability a_3 (skS.0 1 (skS.0 2 a_14) (skS.0 6 a_14 a_15 a_16 a_17 a_19) a_20) a_4) False)
% 22.65/22.95                (Eq (organization a_3 a_4) False))))))
% 22.65/22.95  Clause #341 (by superposition #[340, 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 a_16 a_17 a_18 a_19 a_20 a_21 a_22 : Iota),
% 22.65/22.95    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.95      (Or
% 22.65/22.95        (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95          False)
% 22.65/22.95        (Or
% 22.65/22.95          (Eq
% 22.65/22.95            (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13)
% 22.65/22.95              (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95            False)
% 22.65/22.95          (Or
% 22.65/22.95            (Eq
% 22.65/22.95              (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_16) (skS.0 5 a_16 a_17 a_18 a_19) a_20)
% 22.65/22.95                (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95              False)
% 22.65/22.95            (Or
% 22.65/22.95              (Eq
% 22.65/22.95                (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_16) (skS.0 6 a_16 a_17 a_18 a_19 a_21) a_22)
% 22.65/22.95                  (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95                False)
% 22.65/22.95              (Or (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_14 a_15)) False) (Eq False True))))))
% 22.65/22.95  Clause #495 (by clausification #[341]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 : Iota),
% 22.65/22.95    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.95      (Or
% 22.65/22.95        (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95          False)
% 22.65/22.95        (Or
% 22.65/22.95          (Eq
% 22.65/22.95            (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13)
% 22.65/22.95              (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95            False)
% 22.65/22.95          (Or
% 22.65/22.95            (Eq
% 22.65/22.95              (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_16) (skS.0 5 a_16 a_17 a_18 a_19) a_20)
% 22.65/22.95                (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95              False)
% 22.65/22.95            (Or
% 22.65/22.95              (Eq
% 22.65/22.95                (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_16) (skS.0 6 a_16 a_17 a_18 a_19 a_21) a_22)
% 22.65/22.95                  (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95                False)
% 22.65/22.95              (Eq (organization (skS.0 2 a_2) (skS.0 6 a_2 a_3 a_4 a_14 a_15)) False)))))
% 22.65/22.95  Clause #496 (by forward demodulation #[495, 107]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 : Iota),
% 22.65/22.95    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.95      (Or
% 22.65/22.95        (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95          False)
% 22.65/22.95        (Or
% 22.65/22.95          (Eq
% 22.65/22.95            (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13)
% 22.65/22.95              (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95            False)
% 22.65/22.95          (Or
% 22.65/22.95            (Eq
% 22.65/22.95              (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_16) (skS.0 5 a_16 a_17 a_18 a_19) a_20)
% 22.65/22.95                (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95              False)
% 22.65/22.95            (Or
% 22.65/22.95              (Eq
% 22.65/22.95                (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_16) (skS.0 6 a_16 a_17 a_18 a_19 a_21) a_22)
% 22.65/22.95                  (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.95                False)
% 22.65/22.95              (Eq True False)))))
% 22.65/22.95  Clause #497 (by clausification #[496]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 : Iota),
% 22.65/22.95    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.95      (Or
% 22.65/22.95        (Eq (accountability (skS.0 2 a) (skS.0 0 (skS.0 2 a_5) (skS.0 5 a_5 a_6 a_7 a_8) a_9) (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.95          False)
% 22.65/22.95        (Or
% 22.65/22.95          (Eq
% 22.65/22.95            (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a_5) (skS.0 6 a_5 a_6 a_7 a_8 a_12) a_13)
% 22.65/22.97              (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.97            False)
% 22.65/22.97          (Or
% 22.65/22.97            (Eq
% 22.65/22.97              (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_16) (skS.0 5 a_16 a_17 a_18 a_19) a_20)
% 22.65/22.97                (skS.0 5 a a_1 a_10 a_11))
% 22.65/22.97              False)
% 22.65/22.97            (Eq
% 22.65/22.97              (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_16) (skS.0 6 a_16 a_17 a_18 a_19 a_21) a_22)
% 22.65/22.97                (skS.0 6 a_2 a_3 a_4 a_14 a_15))
% 22.65/22.97              False))))
% 22.65/22.97  Clause #498 (by superposition #[497, 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 a_16 a_17 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.97      (Or
% 22.65/22.97        (Eq
% 22.65/22.97          (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_5 a_6 a_7) a_8)
% 22.65/22.97            (skS.0 6 a_2 a_3 a_4 a_9 a_10))
% 22.65/22.97          False)
% 22.65/22.97        (Or
% 22.65/22.97          (Eq
% 22.65/22.97            (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_11) (skS.0 5 a_11 a_12 a_13 a_14) a_15) (skS.0 5 a a_1 a_5 a_6))
% 22.65/22.97            False)
% 22.65/22.97          (Or
% 22.65/22.97            (Eq
% 22.65/22.97              (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_11) (skS.0 6 a_11 a_12 a_13 a_14 a_16) a_17)
% 22.65/22.97                (skS.0 6 a_2 a_3 a_4 a_9 a_10))
% 22.65/22.97              False)
% 22.65/22.97            (Eq False True))))
% 22.65/22.97  Clause #499 (by clausification #[498]): ∀ (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 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a_2 a_3 a_4)) True)
% 22.65/22.97      (Or
% 22.65/22.97        (Eq
% 22.65/22.97          (accountability (skS.0 2 a_2) (skS.0 0 (skS.0 2 a) (skS.0 6 a a_1 a_5 a_6 a_7) a_8)
% 22.65/22.97            (skS.0 6 a_2 a_3 a_4 a_9 a_10))
% 22.65/22.97          False)
% 22.65/22.97        (Or
% 22.65/22.97          (Eq
% 22.65/22.97            (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_11) (skS.0 5 a_11 a_12 a_13 a_14) a_15) (skS.0 5 a a_1 a_5 a_6))
% 22.65/22.97            False)
% 22.65/22.97          (Eq
% 22.65/22.97            (reliability (skS.0 2 a_2) (skS.0 1 (skS.0 2 a_11) (skS.0 6 a_11 a_12 a_13 a_14 a_16) a_17)
% 22.65/22.97              (skS.0 6 a_2 a_3 a_4 a_9 a_10))
% 22.65/22.97            False)))
% 22.65/22.97  Clause #500 (by superposition #[499, 121]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True)
% 22.65/22.97      (Or
% 22.65/22.97        (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_3) (skS.0 5 a_3 a_4 a_5 a_6) a_7) (skS.0 5 a a_1 a_2 a_8)) False)
% 22.65/22.97        (Or
% 22.65/22.97          (Eq
% 22.65/22.97            (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_3) (skS.0 6 a_3 a_4 a_5 a_6 a_9) a_10)
% 22.65/22.97              (skS.0 6 a a_1 a_2 a_8 a_11))
% 22.65/22.97            False)
% 22.65/22.97          (Eq False True)))
% 22.65/22.97  Clause #501 (by clausification #[500]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True)
% 22.65/22.97      (Or
% 22.65/22.97        (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_3) (skS.0 5 a_3 a_4 a_5 a_6) a_7) (skS.0 5 a a_1 a_2 a_8)) False)
% 22.65/22.97        (Eq
% 22.65/22.97          (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a_3) (skS.0 6 a_3 a_4 a_5 a_6 a_9) a_10)
% 22.65/22.97            (skS.0 6 a a_1 a_2 a_8 a_11))
% 22.65/22.97          False))
% 22.65/22.97  Clause #502 (by superposition #[501, 118]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True)
% 22.65/22.97      (Or
% 22.65/22.97        (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_6))
% 22.65/22.97          False)
% 22.65/22.97        (Eq False True))
% 22.65/22.97  Clause #503 (by clausification #[502]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.97    Or (Eq (greater (skS.0 3 a a_1) (skS.0 4 a a_1 a_2)) True)
% 22.65/22.97      (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_6))
% 22.65/22.97        False)
% 22.65/22.97  Clause #504 (by forward demodulation #[503, 29]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.97    Or (Eq False True)
% 22.65/22.97      (Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_6))
% 22.65/22.97        False)
% 22.65/22.97  Clause #505 (by clausification #[504]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 22.65/22.97    Eq (reliability (skS.0 2 a) (skS.0 1 (skS.0 2 a) (skS.0 6 a a_1 a_2 a_3 a_4) a_5) (skS.0 6 a a_1 a_2 a_3 a_6)) False
% 22.65/22.97  Clause #506 (by superposition #[505, 120]): Eq False True
% 22.65/22.97  Clause #508 (by clausification #[506]): False
% 22.65/22.97  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------