Duper---1.0.THM-Prf.s

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

% Computer : n015.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 18.26s 18.59s
% Output   : Proof 19.16s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem    : MGT008+1 : TPTP v9.3.0. Released v2.0.0.
% 0.00/0.05  % Command    : duper %s
% 0.11/0.38  % Computer : n015.cluster.edu
% 0.11/0.38  % Model    : x86_64 x86_64
% 0.11/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38  % Memory   : 8046.5625MB
% 0.11/0.38  % OS       : Linux 6.8.0-71-generic
% 0.11/0.39  % CPULimit   : 300
% 0.11/0.39  % WCLimit    : 300
% 0.11/0.39  % DateTime   : Mon Sep  7 11:48:00 UTC 2026
% 0.11/0.39  % CPUTime    : 
% 18.26/18.59  SZS status Theorem for theBenchmark.p
% 18.26/18.59  SZS output start Proof for theBenchmark.p
% 18.26/18.59  Clause #0 (by assumption #[]): Eq (∀ (X T : Iota), organization X T → Exists fun I => inertia X I T) True
% 18.26/18.59  Clause #1 (by assumption #[]): Eq
% 18.26/18.59    (∀ (X Y C S1 S2 I1 I2 T1 T2 : Iota),
% 18.26/18.59      And
% 18.26/18.59          (And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And (And (And (And (organization X T1) (organization Y T2)) (class X C T1)) (class Y C T2))
% 18.26/18.59                  (size X S1 T1))
% 18.26/18.59                (size Y S2 T2))
% 18.26/18.59              (inertia X I1 T1))
% 18.26/18.59            (inertia Y I2 T2))
% 18.26/18.59          (greater S2 S1) →
% 18.26/18.59        greater I2 I1)
% 18.26/18.59    True
% 18.26/18.59  Clause #2 (by assumption #[]): Eq
% 18.26/18.59    (∀ (X Y T1 T2 I1 I2 P1 P2 : Iota),
% 18.26/18.59      And
% 18.26/18.59          (And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And
% 18.26/18.59                  (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1))
% 18.26/18.59                    (reorganization_free Y T2 T2))
% 18.26/18.59                  (inertia X I1 T1))
% 18.26/18.59                (inertia Y I2 T2))
% 18.26/18.59              (survival_chance X P1 T1))
% 18.26/18.59            (survival_chance Y P2 T2))
% 18.26/18.59          (greater I2 I1) →
% 18.26/18.59        greater P2 P1)
% 18.26/18.59    True
% 18.26/18.59  Clause #3 (by assumption #[]): Eq
% 18.26/18.59    (Not
% 18.26/18.59      (∀ (X Y C P1 P2 S1 S2 T1 T2 : Iota),
% 18.26/18.59        And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And
% 18.26/18.59                  (And
% 18.26/18.59                    (And
% 18.26/18.59                      (And
% 18.26/18.59                        (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1))
% 18.26/18.59                          (reorganization_free Y T2 T2))
% 18.26/18.59                        (class X C T1))
% 18.26/18.59                      (class Y C T2))
% 18.26/18.59                    (survival_chance X P1 T1))
% 18.26/18.59                  (survival_chance Y P2 T2))
% 18.26/18.59                (size X S1 T1))
% 18.26/18.59              (size Y S2 T2))
% 18.26/18.59            (greater S2 S1) →
% 18.26/18.59          greater P2 P1))
% 18.26/18.59    True
% 18.26/18.59  Clause #4 (by clausification #[0]): ∀ (a : Iota), Eq (∀ (T : Iota), organization a T → Exists fun I => inertia a I T) True
% 18.26/18.59  Clause #5 (by clausification #[4]): ∀ (a a_1 : Iota), Eq (organization a a_1 → Exists fun I => inertia a I a_1) True
% 18.26/18.59  Clause #6 (by clausification #[5]): ∀ (a a_1 : Iota), Or (Eq (organization a a_1) False) (Eq (Exists fun I => inertia a I a_1) True)
% 18.26/18.59  Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 : Iota), Or (Eq (organization a a_1) False) (Eq (inertia a (skS.0 0 a a_1 a_2) a_1) True)
% 18.26/18.59  Clause #8 (by clausification #[2]): ∀ (a : Iota),
% 18.26/18.59    Eq
% 18.26/18.59      (∀ (Y T1 T2 I1 I2 P1 P2 : Iota),
% 18.26/18.59        And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And
% 18.26/18.59                  (And
% 18.26/18.59                    (And (And (And (organization a T1) (organization Y T2)) (reorganization_free a T1 T1))
% 18.26/18.59                      (reorganization_free Y T2 T2))
% 18.26/18.59                    (inertia a I1 T1))
% 18.26/18.59                  (inertia Y I2 T2))
% 18.26/18.59                (survival_chance a P1 T1))
% 18.26/18.59              (survival_chance Y P2 T2))
% 18.26/18.59            (greater I2 I1) →
% 18.26/18.59          greater P2 P1)
% 18.26/18.59      True
% 18.26/18.59  Clause #9 (by clausification #[8]): ∀ (a a_1 : Iota),
% 18.26/18.59    Eq
% 18.26/18.59      (∀ (T1 T2 I1 I2 P1 P2 : Iota),
% 18.26/18.59        And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And
% 18.26/18.59                  (And
% 18.26/18.59                    (And (And (And (organization a T1) (organization a_1 T2)) (reorganization_free a T1 T1))
% 18.26/18.59                      (reorganization_free a_1 T2 T2))
% 18.26/18.59                    (inertia a I1 T1))
% 18.26/18.59                  (inertia a_1 I2 T2))
% 18.26/18.59                (survival_chance a P1 T1))
% 18.26/18.59              (survival_chance a_1 P2 T2))
% 18.26/18.59            (greater I2 I1) →
% 18.26/18.59          greater P2 P1)
% 18.26/18.59      True
% 18.26/18.59  Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 : Iota),
% 18.26/18.59    Eq
% 18.26/18.59      (∀ (T2 I1 I2 P1 P2 : Iota),
% 18.26/18.59        And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.26/18.59                (And
% 18.26/18.59                  (And
% 18.26/18.59                    (And (And (And (organization a a_1) (organization a_2 T2)) (reorganization_free a a_1 a_1))
% 18.26/18.59                      (reorganization_free a_2 T2 T2))
% 18.26/18.59                    (inertia a I1 a_1))
% 18.26/18.59                  (inertia a_2 I2 T2))
% 18.26/18.59                (survival_chance a P1 a_1))
% 18.26/18.59              (survival_chance a_2 P2 T2))
% 18.26/18.59            (greater I2 I1) →
% 18.26/18.59          greater P2 P1)
% 18.26/18.59      True
% 18.26/18.59  Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 a_3 : Iota),
% 18.26/18.59    Eq
% 18.26/18.59      (∀ (I1 I2 P1 P2 : Iota),
% 18.26/18.59        And
% 18.26/18.59            (And
% 18.26/18.59              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And
% 18.36/18.62                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                      (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                    (inertia a I1 a_1))
% 18.36/18.62                  (inertia a_2 I2 a_3))
% 18.36/18.62                (survival_chance a P1 a_1))
% 18.36/18.62              (survival_chance a_2 P2 a_3))
% 18.36/18.62            (greater I2 I1) →
% 18.36/18.62          greater P2 P1)
% 18.36/18.62      True
% 18.36/18.62  Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 18.36/18.62    Eq
% 18.36/18.62      (∀ (I2 P1 P2 : Iota),
% 18.36/18.62        And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And
% 18.36/18.62                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                      (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                    (inertia a a_4 a_1))
% 18.36/18.62                  (inertia a_2 I2 a_3))
% 18.36/18.62                (survival_chance a P1 a_1))
% 18.36/18.62              (survival_chance a_2 P2 a_3))
% 18.36/18.62            (greater I2 a_4) →
% 18.36/18.62          greater P2 P1)
% 18.36/18.62      True
% 18.36/18.62  Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 18.36/18.62    Eq
% 18.36/18.62      (∀ (P1 P2 : Iota),
% 18.36/18.62        And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And
% 18.36/18.62                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                      (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                    (inertia a a_4 a_1))
% 18.36/18.62                  (inertia a_2 a_5 a_3))
% 18.36/18.62                (survival_chance a P1 a_1))
% 18.36/18.62              (survival_chance a_2 P2 a_3))
% 18.36/18.62            (greater a_5 a_4) →
% 18.36/18.62          greater P2 P1)
% 18.36/18.62      True
% 18.36/18.62  Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 18.36/18.62    Eq
% 18.36/18.62      (∀ (P2 : Iota),
% 18.36/18.62        And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And
% 18.36/18.62                    (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                      (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                    (inertia a a_4 a_1))
% 18.36/18.62                  (inertia a_2 a_5 a_3))
% 18.36/18.62                (survival_chance a a_6 a_1))
% 18.36/18.62              (survival_chance a_2 P2 a_3))
% 18.36/18.62            (greater a_5 a_4) →
% 18.36/18.62          greater P2 a_6)
% 18.36/18.62      True
% 18.36/18.62  Clause #15 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.62    Eq
% 18.36/18.62      (And
% 18.36/18.62          (And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                    (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                  (inertia a a_4 a_1))
% 18.36/18.62                (inertia a_2 a_5 a_3))
% 18.36/18.62              (survival_chance a a_6 a_1))
% 18.36/18.62            (survival_chance a_2 a_7 a_3))
% 18.36/18.62          (greater a_5 a_4) →
% 18.36/18.62        greater a_7 a_6)
% 18.36/18.62      True
% 18.36/18.62  Clause #16 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.62    Or
% 18.36/18.62      (Eq
% 18.36/18.62        (And
% 18.36/18.62          (And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And (And (And (organization a a_1) (organization a_2 a_3)) (reorganization_free a a_1 a_1))
% 18.36/18.62                    (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                  (inertia a a_4 a_1))
% 18.36/18.62                (inertia a_2 a_5 a_3))
% 18.36/18.62              (survival_chance a a_6 a_1))
% 18.36/18.62            (survival_chance a_2 a_7 a_3))
% 18.36/18.62          (greater a_5 a_4))
% 18.36/18.62        False)
% 18.36/18.62      (Eq (greater a_7 a_6) True)
% 18.36/18.62  Clause #17 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.62    Or (Eq (greater a a_1) True)
% 18.36/18.62      (Or
% 18.36/18.62        (Eq
% 18.36/18.62          (And
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And (And (And (organization a_2 a_3) (organization a_4 a_5)) (reorganization_free a_2 a_3 a_3))
% 18.36/18.62                    (reorganization_free a_4 a_5 a_5))
% 18.36/18.62                  (inertia a_2 a_6 a_3))
% 18.36/18.62                (inertia a_4 a_7 a_5))
% 18.36/18.62              (survival_chance a_2 a_1 a_3))
% 18.36/18.62            (survival_chance a_4 a a_5))
% 18.36/18.62          False)
% 18.36/18.62        (Eq (greater a_7 a_6) False))
% 18.36/18.62  Clause #18 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.62    Or (Eq (greater a a_1) True)
% 18.36/18.62      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.62        (Or
% 18.36/18.62          (Eq
% 18.36/18.62            (And
% 18.36/18.62              (And
% 18.36/18.62                (And
% 18.36/18.62                  (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (reorganization_free a_4 a_5 a_5))
% 18.36/18.66                    (reorganization_free a_6 a_7 a_7))
% 18.36/18.66                  (inertia a_4 a_3 a_5))
% 18.36/18.66                (inertia a_6 a_2 a_7))
% 18.36/18.66              (survival_chance a_4 a_1 a_5))
% 18.36/18.66            False)
% 18.36/18.66          (Eq (survival_chance a_6 a a_7) False)))
% 18.36/18.66  Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or
% 18.36/18.66            (Eq
% 18.36/18.66              (And
% 18.36/18.66                (And
% 18.36/18.66                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7))
% 18.36/18.66                    (reorganization_free a_4 a_5 a_5))
% 18.36/18.66                  (inertia a_6 a_3 a_7))
% 18.36/18.66                (inertia a_4 a_2 a_5))
% 18.36/18.66              False)
% 18.36/18.66            (Eq (survival_chance a_6 a_1 a_7) False))))
% 18.36/18.66  Clause #20 (by clausification #[19]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 18.36/18.66            (Or
% 18.36/18.66              (Eq
% 18.36/18.66                (And
% 18.36/18.66                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7))
% 18.36/18.66                    (reorganization_free a_4 a_5 a_5))
% 18.36/18.66                  (inertia a_6 a_3 a_7))
% 18.36/18.66                False)
% 18.36/18.66              (Eq (inertia a_4 a_2 a_5) False)))))
% 18.36/18.66  Clause #21 (by clausification #[20]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 18.36/18.66            (Or (Eq (inertia a_4 a_2 a_5) False)
% 18.36/18.66              (Or
% 18.36/18.66                (Eq
% 18.36/18.66                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7))
% 18.36/18.66                    (reorganization_free a_4 a_5 a_5))
% 18.36/18.66                  False)
% 18.36/18.66                (Eq (inertia a_6 a_3 a_7) False))))))
% 18.36/18.66  Clause #22 (by clausification #[21]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 18.36/18.66            (Or (Eq (inertia a_4 a_2 a_5) False)
% 18.36/18.66              (Or (Eq (inertia a_6 a_3 a_7) False)
% 18.36/18.66                (Or (Eq (And (And (organization a_6 a_7) (organization a_4 a_5)) (reorganization_free a_6 a_7 a_7)) False)
% 18.36/18.66                  (Eq (reorganization_free a_4 a_5 a_5) False)))))))
% 18.36/18.66  Clause #23 (by clausification #[22]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 18.36/18.66            (Or (Eq (inertia a_4 a_2 a_5) False)
% 18.36/18.66              (Or (Eq (inertia a_6 a_3 a_7) False)
% 18.36/18.66                (Or (Eq (reorganization_free a_4 a_5 a_5) False)
% 18.36/18.66                  (Or (Eq (And (organization a_6 a_7) (organization a_4 a_5)) False)
% 18.36/18.66                    (Eq (reorganization_free a_6 a_7 a_7) False))))))))
% 18.36/18.66  Clause #24 (by clausification #[23]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.36/18.66    Or (Eq (greater a a_1) True)
% 18.36/18.66      (Or (Eq (greater a_2 a_3) False)
% 18.36/18.66        (Or (Eq (survival_chance a_4 a a_5) False)
% 18.36/18.66          (Or (Eq (survival_chance a_6 a_1 a_7) False)
% 18.36/18.66            (Or (Eq (inertia a_4 a_2 a_5) False)
% 18.36/18.66              (Or (Eq (inertia a_6 a_3 a_7) False)
% 18.36/18.66                (Or (Eq (reorganization_free a_4 a_5 a_5) False)
% 18.36/18.66                  (Or (Eq (reorganization_free a_6 a_7 a_7) False)
% 18.36/18.66                    (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False)))))))))
% 18.36/18.66  Clause #25 (by clausification #[1]): ∀ (a : Iota),
% 18.36/18.66    Eq
% 18.36/18.66      (∀ (Y C S1 S2 I1 I2 T1 T2 : Iota),
% 18.36/18.66        And
% 18.36/18.66            (And
% 18.36/18.66              (And
% 18.36/18.66                (And
% 18.36/18.66                  (And (And (And (And (organization a T1) (organization Y T2)) (class a C T1)) (class Y C T2))
% 18.36/18.66                    (size a S1 T1))
% 18.36/18.66                  (size Y S2 T2))
% 18.36/18.66                (inertia a I1 T1))
% 18.36/18.66              (inertia Y I2 T2))
% 18.46/18.71            (greater S2 S1) →
% 18.46/18.71          greater I2 I1)
% 18.46/18.71      True
% 18.46/18.71  Clause #26 (by clausification #[25]): ∀ (a a_1 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (C S1 S2 I1 I2 T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a C T1)) (class a_1 C T2))
% 18.46/18.71                    (size a S1 T1))
% 18.46/18.71                  (size a_1 S2 T2))
% 18.46/18.71                (inertia a I1 T1))
% 18.46/18.71              (inertia a_1 I2 T2))
% 18.46/18.71            (greater S2 S1) →
% 18.46/18.71          greater I2 I1)
% 18.46/18.71      True
% 18.46/18.71  Clause #27 (by clausification #[26]): ∀ (a a_1 a_2 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (S1 S2 I1 I2 T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2))
% 18.46/18.71                    (size a S1 T1))
% 18.46/18.71                  (size a_1 S2 T2))
% 18.46/18.71                (inertia a I1 T1))
% 18.46/18.71              (inertia a_1 I2 T2))
% 18.46/18.71            (greater S2 S1) →
% 18.46/18.71          greater I2 I1)
% 18.46/18.71      True
% 18.46/18.71  Clause #28 (by clausification #[27]): ∀ (a a_1 a_2 a_3 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (S2 I1 I2 T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2))
% 18.46/18.71                    (size a a_3 T1))
% 18.46/18.71                  (size a_1 S2 T2))
% 18.46/18.71                (inertia a I1 T1))
% 18.46/18.71              (inertia a_1 I2 T2))
% 18.46/18.71            (greater S2 a_3) →
% 18.46/18.71          greater I2 I1)
% 18.46/18.71      True
% 18.46/18.71  Clause #29 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (I1 I2 T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2))
% 18.46/18.71                    (size a a_3 T1))
% 18.46/18.71                  (size a_1 a_4 T2))
% 18.46/18.71                (inertia a I1 T1))
% 18.46/18.71              (inertia a_1 I2 T2))
% 18.46/18.71            (greater a_4 a_3) →
% 18.46/18.71          greater I2 I1)
% 18.46/18.71      True
% 18.46/18.71  Clause #30 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (I2 T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2))
% 18.46/18.71                    (size a a_3 T1))
% 18.46/18.71                  (size a_1 a_4 T2))
% 18.46/18.71                (inertia a a_5 T1))
% 18.46/18.71              (inertia a_1 I2 T2))
% 18.46/18.71            (greater a_4 a_3) →
% 18.46/18.71          greater I2 a_5)
% 18.46/18.71      True
% 18.46/18.71  Clause #31 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (T1 T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a T1) (organization a_1 T2)) (class a a_2 T1)) (class a_1 a_2 T2))
% 18.46/18.71                    (size a a_3 T1))
% 18.46/18.71                  (size a_1 a_4 T2))
% 18.46/18.71                (inertia a a_5 T1))
% 18.46/18.71              (inertia a_1 a_6 T2))
% 18.46/18.71            (greater a_4 a_3) →
% 18.46/18.71          greater a_6 a_5)
% 18.46/18.71      True
% 18.46/18.71  Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (∀ (T2 : Iota),
% 18.46/18.71        And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And
% 18.46/18.71                  (And (And (And (And (organization a a_1) (organization a_2 T2)) (class a a_3 a_1)) (class a_2 a_3 T2))
% 18.46/18.71                    (size a a_4 a_1))
% 18.46/18.71                  (size a_2 a_5 T2))
% 18.46/18.71                (inertia a a_6 a_1))
% 18.46/18.71              (inertia a_2 a_7 T2))
% 18.46/18.71            (greater a_5 a_4) →
% 18.46/18.71          greater a_7 a_6)
% 18.46/18.71      True
% 18.46/18.71  Clause #33 (by clausification #[32]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.71    Eq
% 18.46/18.71      (And
% 18.46/18.71          (And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And (And (And (And (organization a a_1) (organization a_2 a_3)) (class a a_4 a_1)) (class a_2 a_4 a_3))
% 18.46/18.71                  (size a a_5 a_1))
% 18.46/18.71                (size a_2 a_6 a_3))
% 18.46/18.71              (inertia a a_7 a_1))
% 18.46/18.71            (inertia a_2 a_8 a_3))
% 18.46/18.71          (greater a_6 a_5) →
% 18.46/18.71        greater a_8 a_7)
% 18.46/18.71      True
% 18.46/18.71  Clause #34 (by clausification #[33]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.71    Or
% 18.46/18.71      (Eq
% 18.46/18.71        (And
% 18.46/18.71          (And
% 18.46/18.71            (And
% 18.46/18.71              (And
% 18.46/18.71                (And (And (And (And (organization a a_1) (organization a_2 a_3)) (class a a_4 a_1)) (class a_2 a_4 a_3))
% 18.46/18.75                  (size a a_5 a_1))
% 18.46/18.75                (size a_2 a_6 a_3))
% 18.46/18.75              (inertia a a_7 a_1))
% 18.46/18.75            (inertia a_2 a_8 a_3))
% 18.46/18.75          (greater a_6 a_5))
% 18.46/18.75        False)
% 18.46/18.75      (Eq (greater a_8 a_7) True)
% 18.46/18.75  Clause #35 (by clausification #[34]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or
% 18.46/18.75        (Eq
% 18.46/18.75          (And
% 18.46/18.75            (And
% 18.46/18.75              (And
% 18.46/18.75                (And
% 18.46/18.75                  (And (And (And (organization a_2 a_3) (organization a_4 a_5)) (class a_2 a_6 a_3)) (class a_4 a_6 a_5))
% 18.46/18.75                  (size a_2 a_7 a_3))
% 18.46/18.75                (size a_4 a_8 a_5))
% 18.46/18.75              (inertia a_2 a_1 a_3))
% 18.46/18.75            (inertia a_4 a a_5))
% 18.46/18.75          False)
% 18.46/18.75        (Eq (greater a_8 a_7) False))
% 18.46/18.75  Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or
% 18.46/18.75          (Eq
% 18.46/18.75            (And
% 18.46/18.75              (And
% 18.46/18.75                (And
% 18.46/18.75                  (And (And (And (organization a_4 a_5) (organization a_6 a_7)) (class a_4 a_8 a_5)) (class a_6 a_8 a_7))
% 18.46/18.75                  (size a_4 a_3 a_5))
% 18.46/18.75                (size a_6 a_2 a_7))
% 18.46/18.75              (inertia a_4 a_1 a_5))
% 18.46/18.75            False)
% 18.46/18.75          (Eq (inertia a_6 a a_7) False)))
% 18.46/18.75  Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or
% 18.46/18.75            (Eq
% 18.46/18.75              (And
% 18.46/18.75                (And
% 18.46/18.75                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5))
% 18.46/18.75                  (size a_6 a_3 a_7))
% 18.46/18.75                (size a_4 a_2 a_5))
% 18.46/18.75              False)
% 18.46/18.75            (Eq (inertia a_6 a_1 a_7) False))))
% 18.46/18.75  Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or (Eq (inertia a_6 a_1 a_7) False)
% 18.46/18.75            (Or
% 18.46/18.75              (Eq
% 18.46/18.75                (And
% 18.46/18.75                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5))
% 18.46/18.75                  (size a_6 a_3 a_7))
% 18.46/18.75                False)
% 18.46/18.75              (Eq (size a_4 a_2 a_5) False)))))
% 18.46/18.75  Clause #39 (by clausification #[38]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or (Eq (inertia a_6 a_1 a_7) False)
% 18.46/18.75            (Or (Eq (size a_4 a_2 a_5) False)
% 18.46/18.75              (Or
% 18.46/18.75                (Eq
% 18.46/18.75                  (And (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) (class a_4 a_8 a_5))
% 18.46/18.75                  False)
% 18.46/18.75                (Eq (size a_6 a_3 a_7) False))))))
% 18.46/18.75  Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or (Eq (inertia a_6 a_1 a_7) False)
% 18.46/18.75            (Or (Eq (size a_4 a_2 a_5) False)
% 18.46/18.75              (Or (Eq (size a_6 a_3 a_7) False)
% 18.46/18.75                (Or (Eq (And (And (organization a_6 a_7) (organization a_4 a_5)) (class a_6 a_8 a_7)) False)
% 18.46/18.75                  (Eq (class a_4 a_8 a_5) False)))))))
% 18.46/18.75  Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or (Eq (inertia a_6 a_1 a_7) False)
% 18.46/18.75            (Or (Eq (size a_4 a_2 a_5) False)
% 18.46/18.75              (Or (Eq (size a_6 a_3 a_7) False)
% 18.46/18.75                (Or (Eq (class a_4 a_8 a_5) False)
% 18.46/18.75                  (Or (Eq (And (organization a_6 a_7) (organization a_4 a_5)) False) (Eq (class a_6 a_8 a_7) False))))))))
% 18.46/18.75  Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.46/18.75    Or (Eq (greater a a_1) True)
% 18.46/18.75      (Or (Eq (greater a_2 a_3) False)
% 18.46/18.75        (Or (Eq (inertia a_4 a a_5) False)
% 18.46/18.75          (Or (Eq (inertia a_6 a_1 a_7) False)
% 18.46/18.75            (Or (Eq (size a_4 a_2 a_5) False)
% 18.46/18.79              (Or (Eq (size a_6 a_3 a_7) False)
% 18.46/18.79                (Or (Eq (class a_4 a_8 a_5) False)
% 18.46/18.79                  (Or (Eq (class a_6 a_8 a_7) False)
% 18.46/18.79                    (Or (Eq (organization a_6 a_7) False) (Eq (organization a_4 a_5) False)))))))))
% 18.46/18.79  Clause #43 (by clausification #[3]): Eq
% 18.46/18.79    (∀ (X Y C P1 P2 S1 S2 T1 T2 : Iota),
% 18.46/18.79      And
% 18.46/18.79          (And
% 18.46/18.79            (And
% 18.46/18.79              (And
% 18.46/18.79                (And
% 18.46/18.79                  (And
% 18.46/18.79                    (And
% 18.46/18.79                      (And (And (And (organization X T1) (organization Y T2)) (reorganization_free X T1 T1))
% 18.46/18.79                        (reorganization_free Y T2 T2))
% 18.46/18.79                      (class X C T1))
% 18.46/18.79                    (class Y C T2))
% 18.46/18.79                  (survival_chance X P1 T1))
% 18.46/18.79                (survival_chance Y P2 T2))
% 18.46/18.79              (size X S1 T1))
% 18.46/18.79            (size Y S2 T2))
% 18.46/18.79          (greater S2 S1) →
% 18.46/18.79        greater P2 P1)
% 18.46/18.79    False
% 18.46/18.79  Clause #44 (by clausification #[43]): ∀ (a : Iota),
% 18.46/18.79    Eq
% 18.46/18.79      (Not
% 18.46/18.79        (∀ (Y C P1 P2 S1 S2 T1 T2 : Iota),
% 18.46/18.79          And
% 18.46/18.79              (And
% 18.46/18.79                (And
% 18.46/18.79                  (And
% 18.46/18.79                    (And
% 18.46/18.79                      (And
% 18.46/18.79                        (And
% 18.46/18.79                          (And
% 18.46/18.79                            (And (And (organization (skS.0 1 a) T1) (organization Y T2))
% 18.46/18.79                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.46/18.79                            (reorganization_free Y T2 T2))
% 18.46/18.79                          (class (skS.0 1 a) C T1))
% 18.46/18.79                        (class Y C T2))
% 18.46/18.79                      (survival_chance (skS.0 1 a) P1 T1))
% 18.46/18.79                    (survival_chance Y P2 T2))
% 18.46/18.79                  (size (skS.0 1 a) S1 T1))
% 18.46/18.79                (size Y S2 T2))
% 18.46/18.79              (greater S2 S1) →
% 18.46/18.79            greater P2 P1))
% 18.46/18.79      True
% 18.46/18.79  Clause #45 (by clausification #[44]): ∀ (a : Iota),
% 18.46/18.79    Eq
% 18.46/18.79      (∀ (Y C P1 P2 S1 S2 T1 T2 : Iota),
% 18.46/18.79        And
% 18.46/18.79            (And
% 18.46/18.79              (And
% 18.46/18.79                (And
% 18.46/18.79                  (And
% 18.46/18.79                    (And
% 18.46/18.79                      (And
% 18.46/18.79                        (And
% 18.46/18.79                          (And (And (organization (skS.0 1 a) T1) (organization Y T2))
% 18.46/18.79                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.46/18.79                          (reorganization_free Y T2 T2))
% 18.46/18.79                        (class (skS.0 1 a) C T1))
% 18.46/18.79                      (class Y C T2))
% 18.46/18.79                    (survival_chance (skS.0 1 a) P1 T1))
% 18.46/18.79                  (survival_chance Y P2 T2))
% 18.46/18.79                (size (skS.0 1 a) S1 T1))
% 18.46/18.79              (size Y S2 T2))
% 18.46/18.79            (greater S2 S1) →
% 18.46/18.79          greater P2 P1)
% 18.46/18.79      False
% 18.46/18.79  Clause #46 (by clausification #[45]): ∀ (a a_1 : Iota),
% 18.46/18.79    Eq
% 18.46/18.79      (Not
% 18.46/18.79        (∀ (C P1 P2 S1 S2 T1 T2 : Iota),
% 18.46/18.79          And
% 18.46/18.79              (And
% 18.46/18.79                (And
% 18.46/18.79                  (And
% 18.46/18.79                    (And
% 18.46/18.79                      (And
% 18.46/18.79                        (And
% 18.46/18.79                          (And
% 18.46/18.79                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.46/18.79                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.46/18.79                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.46/18.79                          (class (skS.0 1 a) C T1))
% 18.46/18.79                        (class (skS.0 2 a a_1) C T2))
% 18.46/18.79                      (survival_chance (skS.0 1 a) P1 T1))
% 18.46/18.79                    (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.46/18.79                  (size (skS.0 1 a) S1 T1))
% 18.46/18.79                (size (skS.0 2 a a_1) S2 T2))
% 18.46/18.79              (greater S2 S1) →
% 18.46/18.79            greater P2 P1))
% 18.46/18.79      True
% 18.46/18.79  Clause #47 (by clausification #[46]): ∀ (a a_1 : Iota),
% 18.46/18.79    Eq
% 18.46/18.79      (∀ (C P1 P2 S1 S2 T1 T2 : Iota),
% 18.46/18.79        And
% 18.46/18.79            (And
% 18.46/18.79              (And
% 18.46/18.79                (And
% 18.46/18.79                  (And
% 18.46/18.79                    (And
% 18.46/18.79                      (And
% 18.46/18.79                        (And
% 18.46/18.79                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.46/18.79                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.46/18.79                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.46/18.79                        (class (skS.0 1 a) C T1))
% 18.46/18.79                      (class (skS.0 2 a a_1) C T2))
% 18.46/18.79                    (survival_chance (skS.0 1 a) P1 T1))
% 18.46/18.79                  (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.56/18.84                (size (skS.0 1 a) S1 T1))
% 18.56/18.84              (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.84            (greater S2 S1) →
% 18.56/18.84          greater P2 P1)
% 18.56/18.84      False
% 18.56/18.84  Clause #48 (by clausification #[47]): ∀ (a a_1 a_2 : Iota),
% 18.56/18.84    Eq
% 18.56/18.84      (Not
% 18.56/18.84        (∀ (P1 P2 S1 S2 T1 T2 : Iota),
% 18.56/18.84          And
% 18.56/18.84              (And
% 18.56/18.84                (And
% 18.56/18.84                  (And
% 18.56/18.84                    (And
% 18.56/18.84                      (And
% 18.56/18.84                        (And
% 18.56/18.84                          (And
% 18.56/18.84                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.84                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.84                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.84                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.84                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.84                      (survival_chance (skS.0 1 a) P1 T1))
% 18.56/18.84                    (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.56/18.84                  (size (skS.0 1 a) S1 T1))
% 18.56/18.84                (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.84              (greater S2 S1) →
% 18.56/18.84            greater P2 P1))
% 18.56/18.84      True
% 18.56/18.84  Clause #49 (by clausification #[48]): ∀ (a a_1 a_2 : Iota),
% 18.56/18.84    Eq
% 18.56/18.84      (∀ (P1 P2 S1 S2 T1 T2 : Iota),
% 18.56/18.84        And
% 18.56/18.84            (And
% 18.56/18.84              (And
% 18.56/18.84                (And
% 18.56/18.84                  (And
% 18.56/18.84                    (And
% 18.56/18.84                      (And
% 18.56/18.84                        (And
% 18.56/18.84                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.84                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.84                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.84                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.84                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.84                    (survival_chance (skS.0 1 a) P1 T1))
% 18.56/18.84                  (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.56/18.84                (size (skS.0 1 a) S1 T1))
% 18.56/18.84              (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.84            (greater S2 S1) →
% 18.56/18.84          greater P2 P1)
% 18.56/18.84      False
% 18.56/18.84  Clause #50 (by clausification #[49]): ∀ (a a_1 a_2 a_3 : Iota),
% 18.56/18.84    Eq
% 18.56/18.84      (Not
% 18.56/18.84        (∀ (P2 S1 S2 T1 T2 : Iota),
% 18.56/18.84          And
% 18.56/18.84              (And
% 18.56/18.84                (And
% 18.56/18.84                  (And
% 18.56/18.84                    (And
% 18.56/18.84                      (And
% 18.56/18.84                        (And
% 18.56/18.84                          (And
% 18.56/18.84                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.84                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.84                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.84                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.84                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.84                      (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.84                    (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.56/18.84                  (size (skS.0 1 a) S1 T1))
% 18.56/18.84                (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.84              (greater S2 S1) →
% 18.56/18.84            greater P2 (skS.0 4 a a_1 a_2 a_3)))
% 18.56/18.84      True
% 18.56/18.84  Clause #51 (by clausification #[50]): ∀ (a a_1 a_2 a_3 : Iota),
% 18.56/18.84    Eq
% 18.56/18.84      (∀ (P2 S1 S2 T1 T2 : Iota),
% 18.56/18.84        And
% 18.56/18.84            (And
% 18.56/18.84              (And
% 18.56/18.84                (And
% 18.56/18.84                  (And
% 18.56/18.84                    (And
% 18.56/18.84                      (And
% 18.56/18.84                        (And
% 18.56/18.84                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.84                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.84                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.84                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.84                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.84                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.84                  (survival_chance (skS.0 2 a a_1) P2 T2))
% 18.56/18.84                (size (skS.0 1 a) S1 T1))
% 18.56/18.84              (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.84            (greater S2 S1) →
% 18.56/18.84          greater P2 (skS.0 4 a a_1 a_2 a_3))
% 18.56/18.84      False
% 18.56/18.84  Clause #52 (by clausification #[51]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 18.56/18.84    Eq
% 18.56/18.84      (Not
% 18.56/18.84        (∀ (S1 S2 T1 T2 : Iota),
% 18.56/18.84          And
% 18.56/18.84              (And
% 18.56/18.84                (And
% 18.56/18.84                  (And
% 18.56/18.84                    (And
% 18.56/18.88                      (And
% 18.56/18.88                        (And
% 18.56/18.88                          (And
% 18.56/18.88                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.88                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.88                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.88                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.88                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.88                      (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.88                    (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.56/18.88                  (size (skS.0 1 a) S1 T1))
% 18.56/18.88                (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.88              (greater S2 S1) →
% 18.56/18.88            greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)))
% 18.56/18.88      True
% 18.56/18.88  Clause #53 (by clausification #[52]): ∀ (a a_1 a_2 a_3 a_4 : Iota),
% 18.56/18.88    Eq
% 18.56/18.88      (∀ (S1 S2 T1 T2 : Iota),
% 18.56/18.88        And
% 18.56/18.88            (And
% 18.56/18.88              (And
% 18.56/18.88                (And
% 18.56/18.88                  (And
% 18.56/18.88                    (And
% 18.56/18.88                      (And
% 18.56/18.88                        (And
% 18.56/18.88                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.88                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.88                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.88                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.88                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.88                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.88                  (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.56/18.88                (size (skS.0 1 a) S1 T1))
% 18.56/18.88              (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.88            (greater S2 S1) →
% 18.56/18.88          greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))
% 18.56/18.88      False
% 18.56/18.88  Clause #54 (by clausification #[53]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 18.56/18.88    Eq
% 18.56/18.88      (Not
% 18.56/18.88        (∀ (S2 T1 T2 : Iota),
% 18.56/18.88          And
% 18.56/18.88              (And
% 18.56/18.88                (And
% 18.56/18.88                  (And
% 18.56/18.88                    (And
% 18.56/18.88                      (And
% 18.56/18.88                        (And
% 18.56/18.88                          (And
% 18.56/18.88                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.88                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.88                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.88                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.88                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.88                      (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.88                    (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.56/18.88                  (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1))
% 18.56/18.88                (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.88              (greater S2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.56/18.88            greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)))
% 18.56/18.88      True
% 18.56/18.88  Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota),
% 18.56/18.88    Eq
% 18.56/18.88      (∀ (S2 T1 T2 : Iota),
% 18.56/18.88        And
% 18.56/18.88            (And
% 18.56/18.88              (And
% 18.56/18.88                (And
% 18.56/18.88                  (And
% 18.56/18.88                    (And
% 18.56/18.88                      (And
% 18.56/18.88                        (And
% 18.56/18.88                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.56/18.88                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.56/18.88                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.56/18.88                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.56/18.88                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.56/18.88                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.56/18.88                  (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.56/18.88                (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1))
% 18.56/18.88              (size (skS.0 2 a a_1) S2 T2))
% 18.56/18.88            (greater S2 (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.56/18.88          greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))
% 18.56/18.88      False
% 18.56/18.88  Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 18.56/18.88    Eq
% 18.56/18.88      (Not
% 18.56/18.88        (∀ (T1 T2 : Iota),
% 18.56/18.88          And
% 18.56/18.88              (And
% 18.56/18.88                (And
% 18.66/18.92                  (And
% 18.66/18.92                    (And
% 18.66/18.92                      (And
% 18.66/18.92                        (And
% 18.66/18.92                          (And
% 18.66/18.92                            (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.66/18.92                              (reorganization_free (skS.0 1 a) T1 T1))
% 18.66/18.92                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.66/18.92                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.66/18.92                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.66/18.92                      (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.66/18.92                    (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.66/18.92                  (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1))
% 18.66/18.92                (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2))
% 18.66/18.92              (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/18.92            greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)))
% 18.66/18.92      True
% 18.66/18.92  Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 18.66/18.92    Eq
% 18.66/18.92      (∀ (T1 T2 : Iota),
% 18.66/18.92        And
% 18.66/18.92            (And
% 18.66/18.92              (And
% 18.66/18.92                (And
% 18.66/18.92                  (And
% 18.66/18.92                    (And
% 18.66/18.92                      (And
% 18.66/18.92                        (And
% 18.66/18.92                          (And (And (organization (skS.0 1 a) T1) (organization (skS.0 2 a a_1) T2))
% 18.66/18.92                            (reorganization_free (skS.0 1 a) T1 T1))
% 18.66/18.92                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.66/18.92                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) T1))
% 18.66/18.92                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.66/18.92                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) T1))
% 18.66/18.92                  (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.66/18.92                (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) T1))
% 18.66/18.92              (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2))
% 18.66/18.92            (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/18.92          greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))
% 18.66/18.92      False
% 18.66/18.92  Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.66/18.92    Eq
% 18.66/18.92      (Not
% 18.66/18.92        (∀ (T2 : Iota),
% 18.66/18.92          And
% 18.66/18.92              (And
% 18.66/18.92                (And
% 18.66/18.92                  (And
% 18.66/18.92                    (And
% 18.66/18.92                      (And
% 18.66/18.92                        (And
% 18.66/18.92                          (And
% 18.66/18.92                            (And
% 18.66/18.92                              (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/18.92                                (organization (skS.0 2 a a_1) T2))
% 18.66/18.92                              (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/18.92                                (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.92                            (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.66/18.92                          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.92                        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.66/18.92                      (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.92                    (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.66/18.92                  (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.92                (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2))
% 18.66/18.92              (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/18.92            greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)))
% 18.66/18.92      True
% 18.66/18.92  Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.66/18.92    Eq
% 18.66/18.92      (∀ (T2 : Iota),
% 18.66/18.92        And
% 18.66/18.92            (And
% 18.66/18.92              (And
% 18.66/18.92                (And
% 18.66/18.92                  (And
% 18.66/18.92                    (And
% 18.66/18.92                      (And
% 18.66/18.92                        (And
% 18.66/18.92                          (And
% 18.66/18.92                            (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/18.92                              (organization (skS.0 2 a a_1) T2))
% 18.66/18.92                            (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/18.96                              (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                          (reorganization_free (skS.0 2 a a_1) T2 T2))
% 18.66/18.96                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) T2))
% 18.66/18.96                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                  (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) T2))
% 18.66/18.96                (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96              (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) T2))
% 18.66/18.96            (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/18.96          greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))
% 18.66/18.96      False
% 18.66/18.96  Clause #60 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.66/18.96    Eq
% 18.66/18.96      (Not
% 18.66/18.96        (And
% 18.66/18.96            (And
% 18.66/18.96              (And
% 18.66/18.96                (And
% 18.66/18.96                  (And
% 18.66/18.96                    (And
% 18.66/18.96                      (And
% 18.66/18.96                        (And
% 18.66/18.96                          (And
% 18.66/18.96                            (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/18.96                              (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                            (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/18.96                              (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                          (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.66/18.96                            (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                      (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                    (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                  (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4)
% 18.66/18.96                    (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96              (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96            (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/18.96          greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)))
% 18.66/18.96      True
% 18.66/18.96  Clause #61 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.66/18.96    Eq
% 18.66/18.96      (And
% 18.66/18.96          (And
% 18.66/18.96            (And
% 18.66/18.96              (And
% 18.66/18.96                (And
% 18.66/18.96                  (And
% 18.66/18.96                    (And
% 18.66/18.96                      (And
% 18.66/18.96                        (And
% 18.66/18.96                          (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/18.96                            (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                          (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/18.96                            (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                        (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.66/18.96                          (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                      (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                    (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96                  (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96                (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96              (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/18.96            (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/18.96          (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) →
% 18.66/19.01        greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3))
% 18.66/19.01      False
% 18.66/19.01  Clause #62 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.66/19.01    Eq
% 18.66/19.01      (And
% 18.66/19.01        (And
% 18.66/19.01          (And
% 18.66/19.01            (And
% 18.66/19.01              (And
% 18.66/19.01                (And
% 18.66/19.01                  (And
% 18.66/19.01                    (And
% 18.66/19.01                      (And
% 18.66/19.01                        (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/19.01                          (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01                        (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/19.01                          (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01                      (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.66/19.01                        (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01                    (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01                  (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01                (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01              (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01            (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01          (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01        (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)))
% 18.66/19.01      True
% 18.66/19.01  Clause #63 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) False
% 18.66/19.01  Clause #64 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota),
% 18.66/19.01    Eq (greater (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 6 a a_1 a_2 a_3 a_4 a_5)) True
% 18.66/19.01  Clause #65 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.66/19.01    Eq
% 18.66/19.01      (And
% 18.66/19.01        (And
% 18.66/19.01          (And
% 18.66/19.01            (And
% 18.66/19.01              (And
% 18.66/19.01                (And
% 18.66/19.01                  (And
% 18.66/19.01                    (And
% 18.66/19.01                      (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.66/19.01                        (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01                      (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.66/19.01                        (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01                    (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.66/19.01                      (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01                  (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01                (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01              (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01            (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01          (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.66/19.01        (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.66/19.01      True
% 18.66/19.01  Clause #67 (by superposition #[64, 42]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota),
% 18.66/19.01    Or (Eq (greater a a_1) True)
% 18.66/19.01      (Or (Eq True False)
% 18.66/19.01        (Or (Eq (inertia a_2 a a_3) False)
% 18.66/19.01          (Or (Eq (inertia a_4 a_1 a_5) False)
% 18.66/19.01            (Or (Eq (size a_2 (skS.0 7 a_6 a_7 a_8 a_9 a_10 a_11 a_12) a_3) False)
% 18.66/19.01              (Or (Eq (size a_4 (skS.0 6 a_6 a_7 a_8 a_9 a_10 a_11) a_5) False)
% 18.66/19.01                (Or (Eq (class a_2 a_13 a_3) False)
% 18.66/19.01                  (Or (Eq (class a_4 a_13 a_5) False)
% 18.66/19.01                    (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False)))))))))
% 18.66/19.01  Clause #68 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.66/19.01    Eq (size (skS.0 2 a a_1) (skS.0 7 a a_1 a_2 a_3 a_4 a_5 a_6) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True
% 18.79/19.06  Clause #69 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.06    Eq
% 18.79/19.06      (And
% 18.79/19.06        (And
% 18.79/19.06          (And
% 18.79/19.06            (And
% 18.79/19.06              (And
% 18.79/19.06                (And
% 18.79/19.06                  (And
% 18.79/19.06                    (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.06                      (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06                    (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.06                      (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06                  (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.06                    (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06                (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06              (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06            (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06          (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06        (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06      True
% 18.79/19.06  Clause #71 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota),
% 18.79/19.06    Or (Eq (greater a a_1) True)
% 18.79/19.06      (Or (Eq (inertia a_2 a a_3) False)
% 18.79/19.06        (Or (Eq (inertia a_4 a_1 a_5) False)
% 18.79/19.06          (Or (Eq (size a_2 (skS.0 7 a_6 a_7 a_8 a_9 a_10 a_11 a_12) a_3) False)
% 18.79/19.06            (Or (Eq (size a_4 (skS.0 6 a_6 a_7 a_8 a_9 a_10 a_11) a_5) False)
% 18.79/19.06              (Or (Eq (class a_2 a_13 a_3) False)
% 18.79/19.06                (Or (Eq (class a_4 a_13 a_5) False)
% 18.79/19.06                  (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False))))))))
% 18.79/19.06  Clause #72 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.79/19.06    Eq (size (skS.0 1 a) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True
% 18.79/19.06  Clause #73 (by clausification #[69]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.06    Eq
% 18.79/19.06      (And
% 18.79/19.06        (And
% 18.79/19.06          (And
% 18.79/19.06            (And
% 18.79/19.06              (And
% 18.79/19.06                (And
% 18.79/19.06                  (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.06                    (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06                  (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.06                    (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06                (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.06                  (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06              (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06            (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06          (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06        (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06      True
% 18.79/19.06  Clause #74 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.06    Eq (survival_chance (skS.0 2 a a_1) (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True
% 18.79/19.06  Clause #75 (by clausification #[73]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.06    Eq
% 18.79/19.06      (And
% 18.79/19.06        (And
% 18.79/19.06          (And
% 18.79/19.06            (And
% 18.79/19.06              (And
% 18.79/19.06                (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.06                  (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06                (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.06                  (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06              (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.06                (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06            (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.06          (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.06        (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12      True
% 18.79/19.12  Clause #79 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.79/19.12    Eq (survival_chance (skS.0 1 a) (skS.0 4 a a_1 a_2 a_3) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True
% 18.79/19.12  Clause #80 (by clausification #[75]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (And
% 18.79/19.12        (And
% 18.79/19.12          (And
% 18.79/19.12            (And
% 18.79/19.12              (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12                (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12              (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.12                (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12            (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.12              (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12          (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12        (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12      True
% 18.79/19.12  Clause #86 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq (class (skS.0 2 a a_1) (skS.0 3 a a_1 a_2) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True
% 18.79/19.12  Clause #87 (by clausification #[80]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (And
% 18.79/19.12        (And
% 18.79/19.12          (And
% 18.79/19.12            (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12              (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12            (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.12              (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12          (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.12            (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12        (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12      True
% 18.79/19.12  Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.79/19.12    Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True
% 18.79/19.12  Clause #89 (by clausification #[87]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (And
% 18.79/19.12        (And
% 18.79/19.12          (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12            (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12          (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)
% 18.79/19.12            (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12        (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.12          (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12      True
% 18.79/19.12  Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 18.79/19.12        (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.79/19.12      True
% 18.79/19.12  Clause #91 (by clausification #[89]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (And
% 18.79/19.12        (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12          (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12        (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)))
% 18.79/19.12      True
% 18.79/19.12  Clause #92 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 18.79/19.12    Eq (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12      True
% 18.79/19.12  Clause #93 (by clausification #[91]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq
% 18.79/19.12      (And (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.79/19.12        (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)))
% 18.79/19.12      True
% 18.79/19.12  Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.79/19.12    Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) True
% 18.79/19.12  Clause #96 (by clausification #[93]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), Eq (organization (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7)) True
% 18.79/19.12  Clause #99 (by superposition #[95, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 18.89/19.17    Or (Eq True False)
% 18.89/19.17      (Eq
% 18.89/19.17        (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.89/19.17          (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17        True)
% 18.89/19.17  Clause #101 (by superposition #[96, 7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.89/19.17    Or (Eq True False)
% 18.89/19.17      (Eq
% 18.89/19.17        (inertia (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8)
% 18.89/19.17          (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.89/19.17        True)
% 18.89/19.17  Clause #102 (by clausification #[101]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota),
% 18.89/19.17    Eq
% 18.89/19.17      (inertia (skS.0 1 a) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) a_8)
% 18.89/19.17        (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 18.89/19.17      True
% 18.89/19.17  Clause #104 (by clausification #[99]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota),
% 18.89/19.17    Eq
% 18.89/19.17      (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.89/19.17        (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17      True
% 18.89/19.17  Clause #105 (by superposition #[104, 71]): ∀ (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),
% 18.89/19.17    Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True)
% 18.89/19.17      (Or (Eq True False)
% 18.89/19.17        (Or (Eq (inertia a_11 a_10 a_12) False)
% 18.89/19.17          (Or
% 18.89/19.17            (Eq
% 18.89/19.17              (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19)
% 18.89/19.17                (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17              False)
% 18.89/19.17            (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False)
% 18.89/19.17              (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.89/19.17                (Or (Eq (class a_11 a_20 a_12) False)
% 18.89/19.17                  (Or (Eq (organization a_11 a_12) False)
% 18.89/19.17                    (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False))))))))
% 18.89/19.17  Clause #122 (by clausification #[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 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 18.89/19.17    Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True)
% 18.89/19.17      (Or (Eq (inertia a_11 a_10 a_12) False)
% 18.89/19.17        (Or
% 18.89/19.17          (Eq
% 18.89/19.17            (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19)
% 18.89/19.17              (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17            False)
% 18.89/19.17          (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False)
% 18.89/19.17            (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.89/19.17              (Or (Eq (class a_11 a_20 a_12) False)
% 18.89/19.17                (Or (Eq (organization a_11 a_12) False)
% 18.89/19.17                  (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)))))))
% 18.89/19.17  Clause #123 (by forward demodulation #[122, 95]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 : Iota),
% 18.89/19.17    Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True)
% 18.89/19.17      (Or (Eq (inertia a_11 a_10 a_12) False)
% 18.89/19.17        (Or
% 18.89/19.17          (Eq
% 18.89/19.17            (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19)
% 18.89/19.17              (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17            False)
% 18.89/19.17          (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False)
% 18.89/19.17            (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.89/19.17              (Or (Eq (class a_11 a_20 a_12) False) (Or (Eq (organization a_11 a_12) False) (Eq True False)))))))
% 18.89/19.17  Clause #124 (by clausification #[123]): ∀ (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),
% 18.89/19.17    Or (Eq (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9) a_10) True)
% 18.89/19.17      (Or (Eq (inertia a_11 a_10 a_12) False)
% 18.89/19.17        (Or
% 18.89/19.17          (Eq
% 18.89/19.17            (size (skS.0 2 a a_1) (skS.0 7 a_13 a_14 a_15 a_16 a_17 a_18 a_19)
% 18.89/19.17              (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.89/19.17            False)
% 18.89/19.17          (Or (Eq (size a_11 (skS.0 6 a_13 a_14 a_15 a_16 a_17 a_18) a_12) False)
% 18.96/19.23            (Or (Eq (class (skS.0 2 a a_1) a_20 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.96/19.23              (Or (Eq (class a_11 a_20 a_12) False) (Eq (organization a_11 a_12) False))))))
% 18.96/19.23  Clause #125 (by superposition #[124, 102]): ∀
% 18.96/19.23    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 :
% 18.96/19.23      Iota),
% 18.96/19.23    Or
% 18.96/19.23      (Eq
% 18.96/19.23        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.96/19.23          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 18.96/19.23        True)
% 18.96/19.23      (Or
% 18.96/19.23        (Eq
% 18.96/19.23          (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.96/19.23          False)
% 18.96/19.23        (Or
% 18.96/19.23          (Eq
% 18.96/19.23            (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24)
% 18.96/19.23              (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17))
% 18.96/19.23            False)
% 18.96/19.23          (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.96/19.23            (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 18.96/19.23              (Or (Eq (organization (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 18.96/19.23                (Eq False True))))))
% 18.96/19.23  Clause #140 (by clausification #[125]): ∀
% 18.96/19.23    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 :
% 18.96/19.23      Iota),
% 18.96/19.23    Or
% 18.96/19.23      (Eq
% 18.96/19.23        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.96/19.23          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 18.96/19.23        True)
% 18.96/19.23      (Or
% 18.96/19.23        (Eq
% 18.96/19.23          (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.96/19.23          False)
% 18.96/19.23        (Or
% 18.96/19.23          (Eq
% 18.96/19.23            (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24)
% 18.96/19.23              (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17))
% 18.96/19.23            False)
% 18.96/19.23          (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.96/19.23            (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 18.96/19.23              (Eq (organization (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)))))
% 18.96/19.23  Clause #141 (by forward demodulation #[140, 96]): ∀
% 18.96/19.23    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 :
% 18.96/19.23      Iota),
% 18.96/19.23    Or
% 18.96/19.23      (Eq
% 18.96/19.23        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.96/19.23          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 18.96/19.23        True)
% 18.96/19.23      (Or
% 18.96/19.23        (Eq
% 18.96/19.23          (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.96/19.23          False)
% 18.96/19.23        (Or
% 18.96/19.23          (Eq
% 18.96/19.23            (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24)
% 18.96/19.23              (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17))
% 18.96/19.23            False)
% 18.96/19.23          (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.96/19.23            (Or (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 18.96/19.23              (Eq True False)))))
% 18.96/19.23  Clause #142 (by clausification #[141]): ∀
% 18.96/19.23    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 :
% 18.96/19.23      Iota),
% 18.96/19.23    Or
% 18.96/19.23      (Eq
% 18.96/19.23        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 18.96/19.23          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 18.96/19.23        True)
% 18.96/19.23      (Or
% 18.96/19.23        (Eq
% 18.96/19.23          (size (skS.0 2 a a_1) (skS.0 7 a_19 a_20 a_21 a_22 a_23 a_24 a_25) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 18.96/19.23          False)
% 18.96/19.23        (Or
% 18.96/19.23          (Eq
% 18.96/19.23            (size (skS.0 1 a_10) (skS.0 6 a_19 a_20 a_21 a_22 a_23 a_24)
% 18.96/19.23              (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17))
% 18.96/19.23            False)
% 18.96/19.23          (Or (Eq (class (skS.0 2 a a_1) a_26 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 18.96/19.23            (Eq (class (skS.0 1 a_10) a_26 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False))))
% 19.06/19.30  Clause #143 (by superposition #[142, 68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 : Iota),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 19.06/19.30        True)
% 19.06/19.30      (Or
% 19.06/19.30        (Eq (size (skS.0 1 a_10) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 19.06/19.30        (Or (Eq (class (skS.0 2 a a_1) a_19 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 19.06/19.30          (Or (Eq (class (skS.0 1 a_10) a_19 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False) (Eq False True))))
% 19.06/19.30  Clause #144 (by clausification #[143]): ∀ (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),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a_10) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18))
% 19.06/19.30        True)
% 19.06/19.30      (Or
% 19.06/19.30        (Eq (size (skS.0 1 a_10) (skS.0 6 a a_1 a_2 a_3 a_4 a_5) (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)
% 19.06/19.30        (Or (Eq (class (skS.0 2 a a_1) a_19 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 19.06/19.30          (Eq (class (skS.0 1 a_10) a_19 (skS.0 8 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17)) False)))
% 19.06/19.30  Clause #145 (by superposition #[144, 72]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30        True)
% 19.06/19.30      (Or (Eq (class (skS.0 2 a a_1) a_13 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 19.06/19.30        (Or (Eq (class (skS.0 1 a) a_13 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False) (Eq False True)))
% 19.06/19.30  Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 : Iota),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30        True)
% 19.06/19.30      (Or (Eq (class (skS.0 2 a a_1) a_13 (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)) False)
% 19.06/19.30        (Eq (class (skS.0 1 a) a_13 (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False))
% 19.06/19.30  Clause #147 (by superposition #[146, 86]): ∀ (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),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30        True)
% 19.06/19.30      (Or (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False) (Eq False True))
% 19.06/19.30  Clause #151 (by clausification #[147]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30        True)
% 19.06/19.30      (Eq (class (skS.0 1 a) (skS.0 3 a a_1 a_2) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11)) False)
% 19.06/19.30  Clause #152 (by forward demodulation #[151, 88]): ∀ (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),
% 19.06/19.30    Or
% 19.06/19.30      (Eq
% 19.06/19.30        (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30          (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30        True)
% 19.06/19.30      (Eq True False)
% 19.06/19.30  Clause #153 (by clausification #[152]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 : Iota),
% 19.06/19.30    Eq
% 19.06/19.30      (greater (skS.0 0 (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8) a_9)
% 19.06/19.30        (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_10 a_11) a_12))
% 19.06/19.30      True
% 19.06/19.30  Clause #154 (by superposition #[153, 24]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 : Iota),
% 19.06/19.30    Or (Eq (greater a a_1) True)
% 19.06/19.30      (Or (Eq True False)
% 19.06/19.30        (Or (Eq (survival_chance a_2 a a_3) False)
% 19.06/19.30          (Or (Eq (survival_chance a_4 a_1 a_5) False)
% 19.06/19.36            (Or
% 19.06/19.36              (Eq (inertia a_2 (skS.0 0 (skS.0 2 a_6 a_7) (skS.0 9 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14) a_15) a_3)
% 19.06/19.36                False)
% 19.06/19.36              (Or (Eq (inertia a_4 (skS.0 0 (skS.0 1 a_6) (skS.0 8 a_6 a_7 a_8 a_9 a_10 a_11 a_16 a_17) a_18) a_5) False)
% 19.06/19.36                (Or (Eq (reorganization_free a_2 a_3 a_3) False)
% 19.06/19.36                  (Or (Eq (reorganization_free a_4 a_5 a_5) False)
% 19.06/19.36                    (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False)))))))))
% 19.06/19.36  Clause #159 (by clausification #[154]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 : Iota),
% 19.06/19.36    Or (Eq (greater a a_1) True)
% 19.06/19.36      (Or (Eq (survival_chance a_2 a a_3) False)
% 19.06/19.36        (Or (Eq (survival_chance a_4 a_1 a_5) False)
% 19.06/19.36          (Or
% 19.06/19.36            (Eq (inertia a_2 (skS.0 0 (skS.0 2 a_6 a_7) (skS.0 9 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14) a_15) a_3)
% 19.06/19.36              False)
% 19.06/19.36            (Or (Eq (inertia a_4 (skS.0 0 (skS.0 1 a_6) (skS.0 8 a_6 a_7 a_8 a_9 a_10 a_11 a_16 a_17) a_18) a_5) False)
% 19.06/19.36              (Or (Eq (reorganization_free a_2 a_3 a_3) False)
% 19.06/19.36                (Or (Eq (reorganization_free a_4 a_5 a_5) False)
% 19.06/19.36                  (Or (Eq (organization a_4 a_5) False) (Eq (organization a_2 a_3) False))))))))
% 19.06/19.36  Clause #160 (by superposition #[159, 74]): ∀
% 19.06/19.36    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 :
% 19.06/19.36      Iota),
% 19.06/19.36    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True)
% 19.06/19.36      (Or (Eq (survival_chance a_6 a_5 a_7) False)
% 19.06/19.36        (Or
% 19.06/19.36          (Eq
% 19.06/19.36            (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_8 a_9) (skS.0 9 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16) a_17)
% 19.06/19.36              (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.06/19.36            False)
% 19.06/19.36          (Or (Eq (inertia a_6 (skS.0 0 (skS.0 1 a_8) (skS.0 8 a_8 a_9 a_10 a_11 a_12 a_13 a_22 a_23) a_24) a_7) False)
% 19.06/19.36            (Or
% 19.06/19.36              (Eq
% 19.06/19.36                (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)
% 19.06/19.36                  (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.06/19.36                False)
% 19.06/19.36              (Or (Eq (reorganization_free a_6 a_7 a_7) False)
% 19.06/19.36                (Or (Eq (organization a_6 a_7) False)
% 19.06/19.36                  (Or (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)) False)
% 19.06/19.36                    (Eq False True))))))))
% 19.06/19.36  Clause #175 (by clausification #[160]): ∀
% 19.06/19.36    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 :
% 19.06/19.36      Iota),
% 19.06/19.36    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True)
% 19.06/19.36      (Or (Eq (survival_chance a_6 a_5 a_7) False)
% 19.06/19.36        (Or
% 19.06/19.36          (Eq
% 19.06/19.36            (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_8 a_9) (skS.0 9 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16) a_17)
% 19.06/19.36              (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.06/19.36            False)
% 19.06/19.36          (Or (Eq (inertia a_6 (skS.0 0 (skS.0 1 a_8) (skS.0 8 a_8 a_9 a_10 a_11 a_12 a_13 a_22 a_23) a_24) a_7) False)
% 19.06/19.36            (Or
% 19.06/19.36              (Eq
% 19.06/19.36                (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)
% 19.06/19.36                  (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.06/19.36                False)
% 19.06/19.36              (Or (Eq (reorganization_free a_6 a_7 a_7) False)
% 19.06/19.36                (Or (Eq (organization a_6 a_7) False)
% 19.06/19.36                  (Eq (organization (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)) False)))))))
% 19.06/19.36  Clause #176 (by forward demodulation #[175, 95]): ∀
% 19.06/19.36    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 :
% 19.06/19.36      Iota),
% 19.06/19.36    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True)
% 19.06/19.36      (Or (Eq (survival_chance a_6 a_5 a_7) False)
% 19.06/19.36        (Or
% 19.06/19.36          (Eq
% 19.06/19.36            (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_8 a_9) (skS.0 9 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16) a_17)
% 19.06/19.36              (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.06/19.36            False)
% 19.06/19.36          (Or (Eq (inertia a_6 (skS.0 0 (skS.0 1 a_8) (skS.0 8 a_8 a_9 a_10 a_11 a_12 a_13 a_22 a_23) a_24) a_7) False)
% 19.06/19.36            (Or
% 19.16/19.42              (Eq
% 19.16/19.42                (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)
% 19.16/19.42                  (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.16/19.42                False)
% 19.16/19.42              (Or (Eq (reorganization_free a_6 a_7 a_7) False) (Or (Eq (organization a_6 a_7) False) (Eq True False)))))))
% 19.16/19.42  Clause #177 (by clausification #[176]): ∀
% 19.16/19.42    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 :
% 19.16/19.42      Iota),
% 19.16/19.42    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) a_5) True)
% 19.16/19.42      (Or (Eq (survival_chance a_6 a_5 a_7) False)
% 19.16/19.42        (Or
% 19.16/19.42          (Eq
% 19.16/19.42            (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_8 a_9) (skS.0 9 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16) a_17)
% 19.16/19.42              (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.16/19.42            False)
% 19.16/19.42          (Or (Eq (inertia a_6 (skS.0 0 (skS.0 1 a_8) (skS.0 8 a_8 a_9 a_10 a_11 a_12 a_13 a_22 a_23) a_24) a_7) False)
% 19.16/19.42            (Or
% 19.16/19.42              (Eq
% 19.16/19.42                (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21)
% 19.16/19.42                  (skS.0 9 a a_1 a_2 a_3 a_4 a_18 a_19 a_20 a_21))
% 19.16/19.42                False)
% 19.16/19.42              (Or (Eq (reorganization_free a_6 a_7 a_7) False) (Eq (organization a_6 a_7) False))))))
% 19.16/19.42  Clause #179 (by superposition #[177, 79]): ∀
% 19.16/19.42    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 a_27 a_28 a_29 :
% 19.16/19.42      Iota),
% 19.16/19.42    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.42      (Or
% 19.16/19.42        (Eq
% 19.16/19.42          (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_9 a_10) (skS.0 9 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)
% 19.16/19.42            (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.42          False)
% 19.16/19.42        (Or
% 19.16/19.42          (Eq
% 19.16/19.42            (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a_9) (skS.0 8 a_9 a_10 a_11 a_12 a_13 a_14 a_23 a_24) a_25)
% 19.16/19.42              (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.42            False)
% 19.16/19.42          (Or
% 19.16/19.42            (Eq
% 19.16/19.42              (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22)
% 19.16/19.42                (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.42              False)
% 19.16/19.42            (Or
% 19.16/19.42              (Eq
% 19.16/19.42                (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)
% 19.16/19.42                  (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.42                False)
% 19.16/19.42              (Or (Eq (organization (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)) False)
% 19.16/19.42                (Eq False True))))))
% 19.16/19.42  Clause #203 (by clausification #[179]): ∀
% 19.16/19.42    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 a_27 a_28 a_29 :
% 19.16/19.42      Iota),
% 19.16/19.42    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.42      (Or
% 19.16/19.42        (Eq
% 19.16/19.42          (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_9 a_10) (skS.0 9 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)
% 19.16/19.42            (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.42          False)
% 19.16/19.42        (Or
% 19.16/19.42          (Eq
% 19.16/19.42            (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a_9) (skS.0 8 a_9 a_10 a_11 a_12 a_13 a_14 a_23 a_24) a_25)
% 19.16/19.42              (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.42            False)
% 19.16/19.42          (Or
% 19.16/19.42            (Eq
% 19.16/19.42              (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22)
% 19.16/19.42                (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.42              False)
% 19.16/19.42            (Or
% 19.16/19.42              (Eq
% 19.16/19.42                (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)
% 19.16/19.42                  (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.42                False)
% 19.16/19.42              (Eq (organization (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)) False)))))
% 19.16/19.42  Clause #204 (by forward demodulation #[203, 96]): ∀
% 19.16/19.42    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 a_27 a_28 a_29 :
% 19.16/19.42      Iota),
% 19.16/19.42    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.42      (Or
% 19.16/19.42        (Eq
% 19.16/19.42          (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_9 a_10) (skS.0 9 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)
% 19.16/19.47            (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.47          False)
% 19.16/19.47        (Or
% 19.16/19.47          (Eq
% 19.16/19.47            (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a_9) (skS.0 8 a_9 a_10 a_11 a_12 a_13 a_14 a_23 a_24) a_25)
% 19.16/19.47              (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.47            False)
% 19.16/19.47          (Or
% 19.16/19.47            (Eq
% 19.16/19.47              (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22)
% 19.16/19.47                (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.47              False)
% 19.16/19.47            (Or
% 19.16/19.47              (Eq
% 19.16/19.47                (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)
% 19.16/19.47                  (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.47                False)
% 19.16/19.47              (Eq True False)))))
% 19.16/19.47  Clause #205 (by clausification #[204]): ∀
% 19.16/19.47    (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 a_20 a_21 a_22 a_23 a_24 a_25 a_26 a_27 a_28 a_29 :
% 19.16/19.47      Iota),
% 19.16/19.47    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.47      (Or
% 19.16/19.47        (Eq
% 19.16/19.47          (inertia (skS.0 2 a a_1) (skS.0 0 (skS.0 2 a_9 a_10) (skS.0 9 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17) a_18)
% 19.16/19.47            (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.47          False)
% 19.16/19.47        (Or
% 19.16/19.47          (Eq
% 19.16/19.47            (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a_9) (skS.0 8 a_9 a_10 a_11 a_12 a_13 a_14 a_23 a_24) a_25)
% 19.16/19.47              (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.47            False)
% 19.16/19.47          (Or
% 19.16/19.47            (Eq
% 19.16/19.47              (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22)
% 19.16/19.47                (skS.0 9 a a_1 a_2 a_3 a_4 a_19 a_20 a_21 a_22))
% 19.16/19.47              False)
% 19.16/19.47            (Eq
% 19.16/19.47              (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29)
% 19.16/19.47                (skS.0 8 a_5 a_6 a_7 a_8 a_26 a_27 a_28 a_29))
% 19.16/19.47              False))))
% 19.16/19.47  Clause #206 (by superposition #[205, 104]): ∀ (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),
% 19.16/19.47    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.47      (Or
% 19.16/19.47        (Eq
% 19.16/19.47          (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_9 a_10 a_11) a_12)
% 19.16/19.47            (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16))
% 19.16/19.47          False)
% 19.16/19.47        (Or
% 19.16/19.47          (Eq
% 19.16/19.47            (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_9 a_17 a_18 a_19)
% 19.16/19.47              (skS.0 9 a a_1 a_2 a_3 a_4 a_9 a_17 a_18 a_19))
% 19.16/19.47            False)
% 19.16/19.47          (Or
% 19.16/19.47            (Eq
% 19.16/19.47              (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16)
% 19.16/19.47                (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16))
% 19.16/19.47              False)
% 19.16/19.47            (Eq False True))))
% 19.16/19.47  Clause #207 (by clausification #[206]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 a_12 a_13 a_14 a_15 a_16 a_17 a_18 a_19 : Iota),
% 19.16/19.47    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a_5 a_6 a_7 a_8)) True)
% 19.16/19.47      (Or
% 19.16/19.47        (Eq
% 19.16/19.47          (inertia (skS.0 1 a_5) (skS.0 0 (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_9 a_10 a_11) a_12)
% 19.16/19.47            (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16))
% 19.16/19.47          False)
% 19.16/19.47        (Or
% 19.16/19.47          (Eq
% 19.16/19.47            (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_9 a_17 a_18 a_19)
% 19.16/19.47              (skS.0 9 a a_1 a_2 a_3 a_4 a_9 a_17 a_18 a_19))
% 19.16/19.47            False)
% 19.16/19.47          (Eq
% 19.16/19.47            (reorganization_free (skS.0 1 a_5) (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16)
% 19.16/19.47              (skS.0 8 a_5 a_6 a_7 a_8 a_13 a_14 a_15 a_16))
% 19.16/19.47            False)))
% 19.16/19.47  Clause #208 (by superposition #[207, 102]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 19.16/19.47    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) True)
% 19.16/19.47      (Or
% 19.16/19.47        (Eq
% 19.16/19.47          (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 19.16/19.47            (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 19.16/19.47          False)
% 19.16/19.47        (Or
% 19.16/19.47          (Eq
% 19.16/19.47            (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)
% 19.16/19.47              (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10))
% 19.16/19.47            False)
% 19.16/19.47          (Eq False True)))
% 19.16/19.47  Clause #212 (by clausification #[208]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 19.16/19.49    Or (Eq (greater (skS.0 5 a a_1 a_2 a_3 a_4) (skS.0 4 a a_1 a_2 a_3)) True)
% 19.16/19.49      (Or
% 19.16/19.49        (Eq
% 19.16/19.49          (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 19.16/19.49            (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 19.16/19.49          False)
% 19.16/19.49        (Eq
% 19.16/19.49          (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)
% 19.16/19.49            (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10))
% 19.16/19.49          False))
% 19.16/19.49  Clause #213 (by forward demodulation #[212, 63]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 19.16/19.49    Or (Eq False True)
% 19.16/19.49      (Or
% 19.16/19.49        (Eq
% 19.16/19.49          (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 19.16/19.49            (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 19.16/19.49          False)
% 19.16/19.49        (Eq
% 19.16/19.49          (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)
% 19.16/19.49            (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10))
% 19.16/19.49          False))
% 19.16/19.49  Clause #214 (by clausification #[213]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota),
% 19.16/19.49    Or
% 19.16/19.49      (Eq
% 19.16/19.49        (reorganization_free (skS.0 2 a a_1) (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8)
% 19.16/19.49          (skS.0 9 a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8))
% 19.16/19.49        False)
% 19.16/19.49      (Eq
% 19.16/19.49        (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10)
% 19.16/19.49          (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_9 a_10))
% 19.16/19.49        False)
% 19.16/19.49  Clause #215 (by superposition #[214, 90]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 19.16/19.49    Or
% 19.16/19.49      (Eq
% 19.16/19.49        (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 19.16/19.49        False)
% 19.16/19.49      (Eq False True)
% 19.16/19.49  Clause #216 (by clausification #[215]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota),
% 19.16/19.49    Eq (reorganization_free (skS.0 1 a) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7) (skS.0 8 a a_1 a_2 a_3 a_4 a_5 a_6 a_7))
% 19.16/19.49      False
% 19.16/19.49  Clause #217 (by superposition #[216, 92]): Eq False True
% 19.16/19.49  Clause #218 (by clausification #[217]): False
% 19.16/19.49  SZS output end Proof for theBenchmark.p
%------------------------------------------------------------------------------