%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEV006^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:02:44 PM UTC 2025 % Result : Theorem 7.37s 7.53s % Output : Proof 7.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEV006^5 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 01:11:38 EDT 2025 % 0.13/0.34 % CPUTime : % 7.37/7.53 SZS status Theorem for theBenchmark.p % 7.37/7.53 SZS output start Proof for theBenchmark.p % 7.37/7.53 Clause #0 (by assumption #[]): Eq % 7.37/7.53 (Not % 7.37/7.53 (∀ (JOIN MEET : a → a → a), % 7.37/7.53 And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And (And (∀ (Xx : a), Eq (JOIN Xx Xx) Xx) (∀ (Xx : a), Eq (MEET Xx Xx) Xx)) % 7.37/7.53 (∀ (Xx Xy Xz : a), Eq (JOIN (JOIN Xx Xy) Xz) (JOIN Xx (JOIN Xy Xz)))) % 7.37/7.53 (∀ (Xx Xy Xz : a), Eq (MEET (MEET Xx Xy) Xz) (MEET Xx (MEET Xy Xz)))) % 7.37/7.53 (∀ (Xx Xy : a), Eq (JOIN Xx Xy) (JOIN Xy Xx))) % 7.37/7.53 (∀ (Xx Xy : a), Eq (MEET Xx Xy) (MEET Xy Xx))) % 7.37/7.53 (∀ (Xx Xy : a), Eq (JOIN (MEET Xx Xy) Xy) Xy)) % 7.37/7.53 (∀ (Xx Xy : a), Eq (MEET (JOIN Xx Xy) Xy) Xy)) % 7.37/7.53 (Exists fun Xx => % 7.37/7.53 Exists fun Xy => % 7.37/7.53 Exists fun Xa => % 7.37/7.53 Exists fun Xb => % 7.37/7.53 Exists fun Xc => % 7.37/7.53 And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.37/7.53 (Ne Xb Xx)) % 7.37/7.53 (Ne Xb Xy)) % 7.37/7.53 (Ne Xc Xx)) % 7.37/7.53 (Ne Xc Xy)) % 7.37/7.53 (Ne Xx Xy))) % 7.37/7.53 (Not (∀ (Xx Xy Xz : a), Eq (JOIN Xx (MEET Xy (JOIN Xx Xz))) (MEET (JOIN Xx Xy) (JOIN Xx Xz)))) → % 7.37/7.53 Exists fun Xx => % 7.37/7.53 Exists fun Xy => % 7.37/7.53 Exists fun Xa => % 7.37/7.53 Exists fun Xb => % 7.37/7.53 Exists fun Xc => % 7.37/7.53 And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And (And (Eq (MEET Xx Xy) Xy) (Eq (JOIN Xx Xy) Xx)) % 7.37/7.53 (Eq (MEET Xx Xa) Xa)) % 7.37/7.53 (Eq (JOIN Xx Xa) Xx)) % 7.37/7.53 (Eq (MEET Xx Xb) Xb)) % 7.37/7.53 (Eq (JOIN Xx Xb) Xx)) % 7.37/7.53 (Eq (MEET Xx Xc) Xc)) % 7.37/7.53 (Eq (JOIN Xx Xc) Xx)) % 7.37/7.53 (Eq (MEET Xa Xb) Xy)) % 7.37/7.53 (Eq (JOIN Xa Xb) Xx)) % 7.37/7.53 (Eq (MEET Xa Xc) Xa)) % 7.37/7.53 (Eq (JOIN Xa Xc) Xc)) % 7.37/7.53 (Eq (MEET Xa Xy) Xy)) % 7.37/7.53 (Eq (JOIN Xa Xy) Xa)) % 7.37/7.53 (Eq (MEET Xb Xc) Xy)) % 7.37/7.53 (Eq (JOIN Xb Xc) Xx)) % 7.37/7.53 (Eq (MEET Xb Xy) Xy)) % 7.37/7.53 (Eq (JOIN Xb Xy) Xb)) % 7.37/7.53 (Eq (MEET Xc Xy) Xy)) % 7.37/7.53 (Eq (JOIN Xc Xy) Xc))) % 7.37/7.53 True % 7.37/7.53 Clause #1 (by clausification #[0]): Eq % 7.37/7.53 (∀ (JOIN MEET : a → a → a), % 7.37/7.53 And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And % 7.37/7.53 (And (And (∀ (Xx : a), Eq (JOIN Xx Xx) Xx) (∀ (Xx : a), Eq (MEET Xx Xx) Xx)) % 7.37/7.53 (∀ (Xx Xy Xz : a), Eq (JOIN (JOIN Xx Xy) Xz) (JOIN Xx (JOIN Xy Xz)))) % 7.37/7.53 (∀ (Xx Xy Xz : a), Eq (MEET (MEET Xx Xy) Xz) (MEET Xx (MEET Xy Xz)))) % 7.37/7.53 (∀ (Xx Xy : a), Eq (JOIN Xx Xy) (JOIN Xy Xx))) % 7.37/7.53 (∀ (Xx Xy : a), Eq (MEET Xx Xy) (MEET Xy Xx))) % 7.37/7.54 (∀ (Xx Xy : a), Eq (JOIN (MEET Xx Xy) Xy) Xy)) % 7.37/7.54 (∀ (Xx Xy : a), Eq (MEET (JOIN Xx Xy) Xy) Xy)) % 7.37/7.54 (Exists fun Xx => % 7.37/7.54 Exists fun Xy => % 7.37/7.54 Exists fun Xa => % 7.37/7.54 Exists fun Xb => % 7.37/7.54 Exists fun Xc => % 7.37/7.54 And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.37/7.54 (Ne Xb Xx)) % 7.37/7.54 (Ne Xb Xy)) % 7.37/7.54 (Ne Xc Xx)) % 7.37/7.54 (Ne Xc Xy)) % 7.37/7.54 (Ne Xx Xy))) % 7.37/7.54 (Not (∀ (Xx Xy Xz : a), Eq (JOIN Xx (MEET Xy (JOIN Xx Xz))) (MEET (JOIN Xx Xy) (JOIN Xx Xz)))) → % 7.37/7.54 Exists fun Xx => % 7.37/7.54 Exists fun Xy => % 7.37/7.54 Exists fun Xa => % 7.37/7.54 Exists fun Xb => % 7.37/7.54 Exists fun Xc => % 7.37/7.54 And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And (And (Eq (MEET Xx Xy) Xy) (Eq (JOIN Xx Xy) Xx)) % 7.37/7.54 (Eq (MEET Xx Xa) Xa)) % 7.37/7.54 (Eq (JOIN Xx Xa) Xx)) % 7.37/7.54 (Eq (MEET Xx Xb) Xb)) % 7.37/7.54 (Eq (JOIN Xx Xb) Xx)) % 7.37/7.54 (Eq (MEET Xx Xc) Xc)) % 7.37/7.54 (Eq (JOIN Xx Xc) Xx)) % 7.37/7.54 (Eq (MEET Xa Xb) Xy)) % 7.37/7.54 (Eq (JOIN Xa Xb) Xx)) % 7.37/7.54 (Eq (MEET Xa Xc) Xa)) % 7.37/7.54 (Eq (JOIN Xa Xc) Xc)) % 7.37/7.54 (Eq (MEET Xa Xy) Xy)) % 7.37/7.54 (Eq (JOIN Xa Xy) Xa)) % 7.37/7.54 (Eq (MEET Xb Xc) Xy)) % 7.37/7.54 (Eq (JOIN Xb Xc) Xx)) % 7.37/7.54 (Eq (MEET Xb Xy) Xy)) % 7.37/7.54 (Eq (JOIN Xb Xy) Xb)) % 7.37/7.54 (Eq (MEET Xc Xy) Xy)) % 7.37/7.54 (Eq (JOIN Xc Xy) Xc)) % 7.37/7.54 False % 7.37/7.54 Clause #2 (by clausification #[1]): ∀ (a_1 : a → a → a), % 7.37/7.54 Eq % 7.37/7.54 (Not % 7.37/7.54 (∀ (MEET : a → a → a), % 7.37/7.54 And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (MEET Xx Xx) Xx)) % 7.37/7.54 (∀ (Xx Xy Xz : a), % 7.37/7.54 Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.37/7.54 (∀ (Xx Xy Xz : a), Eq (MEET (MEET Xx Xy) Xz) (MEET Xx (MEET Xy Xz)))) % 7.37/7.54 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.37/7.54 (∀ (Xx Xy : a), Eq (MEET Xx Xy) (MEET Xy Xx))) % 7.37/7.54 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (MEET Xx Xy) Xy) Xy)) % 7.37/7.54 (∀ (Xx Xy : a), Eq (MEET (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.37/7.54 (Exists fun Xx => % 7.37/7.54 Exists fun Xy => % 7.37/7.54 Exists fun Xa => % 7.37/7.54 Exists fun Xb => % 7.37/7.54 Exists fun Xc => % 7.37/7.54 And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And % 7.37/7.54 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.37/7.54 (Ne Xb Xx)) % 7.37/7.56 (Ne Xb Xy)) % 7.37/7.56 (Ne Xc Xx)) % 7.37/7.56 (Ne Xc Xy)) % 7.37/7.56 (Ne Xx Xy))) % 7.37/7.56 (Not % 7.37/7.56 (∀ (Xx Xy Xz : a), % 7.37/7.56 Eq (skS.0 0 a_1 Xx (MEET Xy (skS.0 0 a_1 Xx Xz))) (MEET (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xx Xz)))) → % 7.37/7.56 Exists fun Xx => % 7.37/7.56 Exists fun Xy => % 7.37/7.56 Exists fun Xa => % 7.37/7.56 Exists fun Xb => % 7.37/7.56 Exists fun Xc => % 7.37/7.56 And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And (And (Eq (MEET Xx Xy) Xy) (Eq (skS.0 0 a_1 Xx Xy) Xx)) % 7.37/7.56 (Eq (MEET Xx Xa) Xa)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xx Xa) Xx)) % 7.37/7.56 (Eq (MEET Xx Xb) Xb)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xx Xb) Xx)) % 7.37/7.56 (Eq (MEET Xx Xc) Xc)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xx Xc) Xx)) % 7.37/7.56 (Eq (MEET Xa Xb) Xy)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xa Xb) Xx)) % 7.37/7.56 (Eq (MEET Xa Xc) Xa)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.37/7.56 (Eq (MEET Xa Xy) Xy)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.37/7.56 (Eq (MEET Xb Xc) Xy)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xb Xc) Xx)) % 7.37/7.56 (Eq (MEET Xb Xy) Xy)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.37/7.56 (Eq (MEET Xc Xy) Xy)) % 7.37/7.56 (Eq (skS.0 0 a_1 Xc Xy) Xc))) % 7.37/7.56 True % 7.37/7.56 Clause #3 (by clausification #[2]): ∀ (a_1 : a → a → a), % 7.37/7.56 Eq % 7.37/7.56 (∀ (MEET : a → a → a), % 7.37/7.56 And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (MEET Xx Xx) Xx)) % 7.37/7.56 (∀ (Xx Xy Xz : a), % 7.37/7.56 Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.37/7.56 (∀ (Xx Xy Xz : a), Eq (MEET (MEET Xx Xy) Xz) (MEET Xx (MEET Xy Xz)))) % 7.37/7.56 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.37/7.56 (∀ (Xx Xy : a), Eq (MEET Xx Xy) (MEET Xy Xx))) % 7.37/7.56 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (MEET Xx Xy) Xy) Xy)) % 7.37/7.56 (∀ (Xx Xy : a), Eq (MEET (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.37/7.56 (Exists fun Xx => % 7.37/7.56 Exists fun Xy => % 7.37/7.56 Exists fun Xa => % 7.37/7.56 Exists fun Xb => % 7.37/7.56 Exists fun Xc => % 7.37/7.56 And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And % 7.37/7.56 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.37/7.56 (Ne Xb Xx)) % 7.37/7.56 (Ne Xb Xy)) % 7.37/7.56 (Ne Xc Xx)) % 7.37/7.56 (Ne Xc Xy)) % 7.37/7.56 (Ne Xx Xy))) % 7.37/7.56 (Not % 7.37/7.56 (∀ (Xx Xy Xz : a), % 7.37/7.56 Eq (skS.0 0 a_1 Xx (MEET Xy (skS.0 0 a_1 Xx Xz))) (MEET (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xx Xz)))) → % 7.37/7.57 Exists fun Xx => % 7.37/7.57 Exists fun Xy => % 7.37/7.57 Exists fun Xa => % 7.37/7.57 Exists fun Xb => % 7.37/7.57 Exists fun Xc => % 7.37/7.57 And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And (And (Eq (MEET Xx Xy) Xy) (Eq (skS.0 0 a_1 Xx Xy) Xx)) % 7.37/7.57 (Eq (MEET Xx Xa) Xa)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xx Xa) Xx)) % 7.37/7.57 (Eq (MEET Xx Xb) Xb)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xx Xb) Xx)) % 7.37/7.57 (Eq (MEET Xx Xc) Xc)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xx Xc) Xx)) % 7.37/7.57 (Eq (MEET Xa Xb) Xy)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xa Xb) Xx)) % 7.37/7.57 (Eq (MEET Xa Xc) Xa)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.37/7.57 (Eq (MEET Xa Xy) Xy)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.37/7.57 (Eq (MEET Xb Xc) Xy)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xb Xc) Xx)) % 7.37/7.57 (Eq (MEET Xb Xy) Xy)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.37/7.57 (Eq (MEET Xc Xy) Xy)) % 7.37/7.57 (Eq (skS.0 0 a_1 Xc Xy) Xc)) % 7.37/7.57 False % 7.37/7.57 Clause #4 (by clausification #[3]): ∀ (a_1 a_2 : a → a → a), % 7.37/7.57 Eq % 7.37/7.57 (Not % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.37/7.57 (∀ (Xx Xy Xz : a), % 7.37/7.57 Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.37/7.57 (∀ (Xx Xy Xz : a), % 7.37/7.57 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.37/7.57 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.37/7.57 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.37/7.57 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.37/7.57 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.37/7.57 (Exists fun Xx => % 7.37/7.57 Exists fun Xy => % 7.37/7.57 Exists fun Xa => % 7.37/7.57 Exists fun Xb => % 7.37/7.57 Exists fun Xc => % 7.37/7.57 And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And % 7.37/7.57 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.37/7.57 (Ne Xb Xx)) % 7.37/7.57 (Ne Xb Xy)) % 7.37/7.57 (Ne Xc Xx)) % 7.37/7.57 (Ne Xc Xy)) % 7.37/7.57 (Ne Xx Xy))) % 7.37/7.57 (Not % 7.37/7.57 (∀ (Xx Xy Xz : a), % 7.37/7.57 Eq (skS.0 0 a_1 Xx (skS.0 1 a_1 a_2 Xy (skS.0 0 a_1 Xx Xz))) % 7.37/7.57 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xx Xz)))) → % 7.37/7.57 Exists fun Xx => % 7.37/7.57 Exists fun Xy => % 7.37/7.57 Exists fun Xa => % 7.37/7.57 Exists fun Xb => % 7.37/7.57 Exists fun Xc => % 7.37/7.57 And % 7.37/7.57 (And % 7.37/7.57 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And (Eq (skS.0 1 a_1 a_2 Xx Xy) Xy) (Eq (skS.0 0 a_1 Xx Xy) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xx Xa) Xa)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xx Xa) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xx Xb) Xb)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xx Xb) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xx Xc) Xc)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xx Xc) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xa Xb) Xy)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xa Xb) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xa Xc) Xa)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xa Xy) Xy)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xb Xc) Xy)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xb Xc) Xx)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xb Xy) Xy)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.43/7.59 (Eq (skS.0 1 a_1 a_2 Xc Xy) Xy)) % 7.43/7.59 (Eq (skS.0 0 a_1 Xc Xy) Xc))) % 7.43/7.59 True % 7.43/7.59 Clause #5 (by clausification #[4]): ∀ (a_1 a_2 : a → a → a), % 7.43/7.59 Eq % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.43/7.59 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.43/7.59 (∀ (Xx Xy Xz : a), % 7.43/7.59 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.43/7.59 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.43/7.59 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.43/7.59 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.43/7.59 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.43/7.59 (Exists fun Xx => % 7.43/7.59 Exists fun Xy => % 7.43/7.59 Exists fun Xa => % 7.43/7.59 Exists fun Xb => % 7.43/7.59 Exists fun Xc => % 7.43/7.59 And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.43/7.59 (Ne Xb Xx)) % 7.43/7.59 (Ne Xb Xy)) % 7.43/7.59 (Ne Xc Xx)) % 7.43/7.59 (Ne Xc Xy)) % 7.43/7.59 (Ne Xx Xy))) % 7.43/7.59 (Not % 7.43/7.59 (∀ (Xx Xy Xz : a), % 7.43/7.59 Eq (skS.0 0 a_1 Xx (skS.0 1 a_1 a_2 Xy (skS.0 0 a_1 Xx Xz))) % 7.43/7.59 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xx Xz)))) → % 7.43/7.59 Exists fun Xx => % 7.43/7.59 Exists fun Xy => % 7.43/7.59 Exists fun Xa => % 7.43/7.59 Exists fun Xb => % 7.43/7.59 Exists fun Xc => % 7.43/7.59 And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.59 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And (And (Eq (skS.0 1 a_1 a_2 Xx Xy) Xy) (Eq (skS.0 0 a_1 Xx Xy) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xx Xa) Xa)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xx Xa) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xx Xb) Xb)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xx Xb) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xx Xc) Xc)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xx Xc) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xa Xb) Xy)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xa Xb) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xa Xc) Xa)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xa Xy) Xy)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xb Xc) Xy)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xb Xc) Xx)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xb Xy) Xy)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.43/7.60 (Eq (skS.0 1 a_1 a_2 Xc Xy) Xy)) % 7.43/7.60 (Eq (skS.0 0 a_1 Xc Xy) Xc)) % 7.43/7.60 False % 7.43/7.60 Clause #6 (by clausification #[5]): ∀ (a_1 a_2 : a → a → a), % 7.43/7.60 Eq % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.43/7.60 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.43/7.60 (∀ (Xx Xy Xz : a), % 7.43/7.60 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.43/7.60 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.43/7.60 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.43/7.60 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.43/7.60 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.43/7.60 (Exists fun Xx => % 7.43/7.60 Exists fun Xy => % 7.43/7.60 Exists fun Xa => % 7.43/7.60 Exists fun Xb => % 7.43/7.60 Exists fun Xc => % 7.43/7.60 And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) % 7.43/7.60 (Ne Xb Xx)) % 7.43/7.60 (Ne Xb Xy)) % 7.43/7.60 (Ne Xc Xx)) % 7.43/7.60 (Ne Xc Xy)) % 7.43/7.60 (Ne Xx Xy))) % 7.43/7.60 (Not % 7.43/7.60 (∀ (Xx Xy Xz : a), % 7.43/7.60 Eq (skS.0 0 a_1 Xx (skS.0 1 a_1 a_2 Xy (skS.0 0 a_1 Xx Xz))) % 7.43/7.60 (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xx Xz))))) % 7.43/7.60 True % 7.43/7.60 Clause #7 (by clausification #[5]): ∀ (a_1 a_2 : a → a → a), % 7.43/7.60 Eq % 7.43/7.60 (Exists fun Xx => % 7.43/7.60 Exists fun Xy => % 7.43/7.60 Exists fun Xa => % 7.43/7.60 Exists fun Xb => % 7.43/7.60 Exists fun Xc => % 7.43/7.60 And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.60 (And % 7.43/7.62 (And (And (Eq (skS.0 1 a_1 a_2 Xx Xy) Xy) (Eq (skS.0 0 a_1 Xx Xy) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xx Xa) Xa)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xx Xa) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xx Xb) Xb)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xx Xb) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xx Xc) Xc)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xx Xc) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xa Xb) Xy)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xa Xb) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xa Xc) Xa)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xa Xy) Xy)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xb Xc) Xy)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xb Xc) Xx)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xb Xy) Xy)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.43/7.62 (Eq (skS.0 1 a_1 a_2 Xc Xy) Xy)) % 7.43/7.62 (Eq (skS.0 0 a_1 Xc Xy) Xc)) % 7.43/7.62 False % 7.43/7.62 Clause #9 (by clausification #[6]): ∀ (a_1 a_2 : a → a → a), % 7.43/7.62 Eq % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.43/7.62 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.43/7.62 (∀ (Xx Xy Xz : a), % 7.43/7.62 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.43/7.62 (Exists fun Xx => % 7.43/7.62 Exists fun Xy => % 7.43/7.62 Exists fun Xa => % 7.43/7.62 Exists fun Xb => % 7.43/7.62 Exists fun Xc => % 7.43/7.62 And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And (And (And (And (And (Ne Xa Xb) (Ne Xa Xc)) (Ne Xa Xx)) (Ne Xa Xy)) (Ne Xb Xc)) (Ne Xb Xx)) % 7.43/7.62 (Ne Xb Xy)) % 7.43/7.62 (Ne Xc Xx)) % 7.43/7.62 (Ne Xc Xy)) % 7.43/7.62 (Ne Xx Xy))) % 7.43/7.62 True % 7.43/7.62 Clause #19 (by clausification #[9]): ∀ (a_1 a_2 : a → a → a), % 7.43/7.62 Eq % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.43/7.62 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.43/7.62 (∀ (Xx Xy Xz : a), % 7.43/7.62 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.43/7.62 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy)) % 7.43/7.62 True % 7.43/7.62 Clause #37 (by clausification #[7]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), % 7.43/7.62 Eq % 7.43/7.62 (Exists fun Xy => % 7.43/7.62 Exists fun Xa => % 7.43/7.62 Exists fun Xb => % 7.43/7.62 Exists fun Xc => % 7.43/7.62 And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.62 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And (And (Eq (skS.0 1 a_1 a_2 a_3 Xy) Xy) (Eq (skS.0 0 a_1 a_3 Xy) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xa) Xa)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xa) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xb) Xb)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xb) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xc) Xc)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xc) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa Xb) Xy)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa Xb) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa Xc) Xa)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa Xy) Xy)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa Xy) Xa)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xb Xc) Xy)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xb Xc) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xb Xy) Xy)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xb Xy) Xb)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xc Xy) Xy)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xc Xy) Xc)) % 7.43/7.63 False % 7.43/7.63 Clause #38 (by clausification #[37]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), % 7.43/7.63 Eq % 7.43/7.63 (Exists fun Xa => % 7.43/7.63 Exists fun Xb => % 7.43/7.63 Exists fun Xc => % 7.43/7.63 And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xa) Xa)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xa) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xb) Xb)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xb) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 Xc) Xc)) % 7.43/7.63 (Eq (skS.0 0 a_1 a_3 Xc) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa Xb) a_4)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa Xb) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa Xc) Xa)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa Xc) Xc)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xa a_4) a_4)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xa a_4) Xa)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xb Xc) a_4)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xb Xc) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xb a_4) a_4)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xb a_4) Xb)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 Xc a_4) a_4)) % 7.43/7.63 (Eq (skS.0 0 a_1 Xc a_4) Xc)) % 7.43/7.63 False % 7.43/7.63 Clause #39 (by clausification #[38]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 : a), % 7.43/7.63 Eq % 7.43/7.63 (Exists fun Xb => % 7.43/7.63 Exists fun Xc => % 7.43/7.63 And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And % 7.43/7.63 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.43/7.63 (Eq (skS.0 1 a_1 a_2 a_3 a_5) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_5) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 Xb) Xb)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 Xb) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 Xc) Xc)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 Xc) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 Xb) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 Xb) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 Xc) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 Xc) Xc)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 Xb Xc) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 Xb Xc) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 Xb a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 Xb a_4) Xb)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 Xc a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 Xc a_4) Xc)) % 7.43/7.65 False % 7.43/7.65 Clause #40 (by clausification #[39]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 a_6 : a), % 7.43/7.65 Eq % 7.43/7.65 (Exists fun Xc => % 7.43/7.65 And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 a_5) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_5) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 a_6) a_6)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_6) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 Xc) Xc)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 Xc) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_6) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 a_6) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 Xc) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 Xc) Xc)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_6 Xc) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_6 Xc) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_6 a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 Xc a_4) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 Xc a_4) Xc)) % 7.43/7.65 False % 7.43/7.65 Clause #41 (by clausification #[40]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 a_6 a_7 : a), % 7.43/7.65 Eq % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And % 7.43/7.65 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 a_5) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_5) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 a_6) a_6)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_6) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_3 a_7) a_7)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_3 a_7) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_6) a_4)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 a_6) a_3)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_7) a_5)) % 7.43/7.65 (Eq (skS.0 0 a_1 a_5 a_7) a_7)) % 7.43/7.65 (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_6 a_7) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_7) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_6 a_4) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_7 a_4) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_7 a_4) a_7)) % 7.49/7.67 False % 7.49/7.67 Clause #42 (by clausification #[41]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 a_6 a_7 : a), % 7.49/7.67 Or % 7.49/7.67 (Eq % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_3 a_5) a_5)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_3 a_5) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_3 a_6) a_6)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_3 a_6) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_3 a_7) a_7)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_3 a_7) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_5 a_6) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_6) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_5 a_7) a_5)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_7) a_7)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_6 a_7) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_7) a_3)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_6 a_4) a_4)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_2 a_7 a_4) a_4)) % 7.49/7.67 False) % 7.49/7.67 (Eq (Eq (skS.0 0 a_1 a_7 a_4) a_7) False) % 7.49/7.67 Clause #43 (by clausification #[42]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.49/7.67 Or (Eq (Eq (skS.0 0 a_1 a_2 a_3) a_2) False) % 7.49/7.67 (Or % 7.49/7.67 (Eq % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And (And (Eq (skS.0 1 a_1 a_4 a_5 a_3) a_3) (Eq (skS.0 0 a_1 a_5 a_3) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_5 a_6) a_6)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_6) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_5 a_7) a_7)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_7) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_2)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_5 a_2) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_3)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_7) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_6)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_2) a_2)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_3)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_7 a_2) a_5)) % 7.49/7.67 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.49/7.67 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.49/7.67 False) % 7.49/7.67 (Eq (Eq (skS.0 1 a_1 a_4 a_2 a_3) a_3) False)) % 7.49/7.67 Clause #44 (by clausification #[43]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 a_6 a_7 : a), % 7.49/7.67 Or % 7.49/7.67 (Eq % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.49/7.67 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And (And (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) (Eq (skS.0 0 a_1 a_3 a_4) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_3 a_5) a_5)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_3 a_5) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_3 a_6) a_6)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_3 a_6) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_3 a_7) a_7)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_3 a_7) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_6) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_6) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_7) a_5)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_7) a_7)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_6 a_7) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_7) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_6 a_4) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.52/7.68 False) % 7.52/7.68 (Or (Eq (Eq (skS.0 1 a_1 a_2 a_7 a_4) a_4) False) (Ne (skS.0 0 a_1 a_7 a_4) a_7)) % 7.52/7.68 Clause #45 (by clausification #[44]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 a_5 a_6 a_7 : a), % 7.52/7.68 Or (Eq (Eq (skS.0 1 a_1 a_2 a_3 a_4) a_4) False) % 7.52/7.68 (Or (Ne (skS.0 0 a_1 a_3 a_4) a_3) % 7.52/7.68 (Or % 7.52/7.68 (Eq % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And (And (Eq (skS.0 1 a_1 a_2 a_5 a_4) a_4) (Eq (skS.0 0 a_1 a_5 a_4) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_6) a_6)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_6) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_7) a_7)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_7) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_5 a_3) a_3)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_3) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_6 a_7) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_7) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_6 a_3) a_6)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_3) a_3)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_6 a_4) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_7 a_3) a_4)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_7 a_3) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_2 a_7 a_4) a_4)) % 7.52/7.68 False) % 7.52/7.68 (Eq (Eq (skS.0 0 a_1 a_7 a_4) a_7) False))) % 7.52/7.68 Clause #46 (by clausification #[45]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.52/7.68 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.68 (Or % 7.52/7.68 (Eq % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And % 7.52/7.68 (And (And (Eq (skS.0 1 a_1 a_4 a_5 a_3) a_3) (Eq (skS.0 0 a_1 a_5 a_3) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_4 a_5 a_6) a_6)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_6) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_4 a_5 a_7) a_7)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_7) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_2)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_5 a_2) a_5)) % 7.52/7.68 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_3)) % 7.52/7.68 (Eq (skS.0 0 a_1 a_6 a_7) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_6)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_2) a_2)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_7 a_2) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.52/7.70 False) % 7.52/7.70 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_3) a_7) False) (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3))) % 7.52/7.70 Clause #47 (by clausification #[46]): ∀ (a_1 : a → a → a) (a_2 a_3 a_4 : a) (a_5 : a → a → a) (a_6 a_7 : a), % 7.52/7.70 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.70 (Or (Eq (Eq (skS.0 0 a_1 a_4 a_3) a_4) False) % 7.52/7.70 (Or (Ne (skS.0 1 a_1 a_5 a_2 a_3) a_3) % 7.52/7.70 (Or % 7.52/7.70 (Eq % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And (And (Eq (skS.0 1 a_1 a_5 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_6 a_7) a_7)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_6 a_4) a_4)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_4) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_6 a_2) a_2)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_7 a_4) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_7 a_4) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_7 a_2) a_7)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_7 a_3) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_5 a_4 a_2) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_4 a_2) a_6)) % 7.52/7.70 False) % 7.52/7.70 (Eq (Eq (skS.0 1 a_1 a_5 a_4 a_3) a_3) False)))) % 7.52/7.70 Clause #48 (by clausification #[47]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.52/7.70 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.70 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.52/7.70 (Or % 7.52/7.70 (Eq % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And % 7.52/7.70 (And (And (Eq (skS.0 1 a_1 a_4 a_5 a_3) a_3) (Eq (skS.0 0 a_1 a_5 a_3) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_5 a_6) a_6)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_5 a_6) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_5 a_7) a_7)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_5 a_7) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_2)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_5 a_2) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_7) a_5)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_6)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_2) a_2)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.70 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_3)) % 7.52/7.70 (Eq (skS.0 0 a_1 a_7 a_2) a_5)) % 7.52/7.70 False) % 7.52/7.70 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3) False) (Ne (skS.0 0 a_1 a_7 a_3) a_7)))) % 7.52/7.70 Clause #49 (by clausification #[48]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.52/7.70 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.70 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.52/7.70 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_5 a_3) a_3) False) % 7.52/7.70 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.52/7.70 (Or % 7.52/7.72 (Eq % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_3)) % 7.52/7.72 False) % 7.52/7.72 (Eq (Eq (skS.0 0 a_1 a_5 a_2) a_6) False))))) % 7.52/7.72 Clause #50 (by clausification #[49]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.52/7.72 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.72 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.52/7.72 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.52/7.72 (Or % 7.52/7.72 (Eq % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_3)) % 7.52/7.72 False) % 7.52/7.72 (Or (Eq (Eq (skS.0 0 a_1 a_5 a_2) a_6) False) (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3))))) % 7.52/7.72 Clause #51 (by clausification #[50]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.52/7.72 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.52/7.72 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.52/7.72 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.52/7.72 (Or (Eq (Eq (skS.0 0 a_1 a_5 a_2) a_6) False) % 7.52/7.72 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.52/7.72 (Or % 7.52/7.72 (Eq % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And % 7.52/7.72 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.52/7.72 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.52/7.72 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.56/7.74 False) % 7.56/7.74 (Eq (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_3) False)))))) % 7.56/7.74 Clause #52 (by clausification #[51]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.56/7.74 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.56/7.74 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.56/7.74 (Or % 7.56/7.74 (Eq % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_3) a_7)) % 7.56/7.74 False) % 7.56/7.74 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_3) False) (Ne (skS.0 0 a_1 a_5 a_2) a_6)))))) % 7.56/7.74 Clause #53 (by clausification #[52]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.56/7.74 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.56/7.74 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.56/7.74 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_5 a_2) a_3) False) % 7.56/7.74 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.56/7.74 (Or % 7.56/7.74 (Eq % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And % 7.56/7.74 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.56/7.74 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.56/7.74 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.56/7.74 False) % 7.56/7.74 (Eq (Eq (skS.0 0 a_1 a_7 a_3) a_7) False))))))) % 7.56/7.74 Clause #54 (by clausification #[53]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.56/7.74 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.56/7.74 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.56/7.74 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.75 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.75 (Or % 7.59/7.75 (Eq % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3)) % 7.59/7.75 False) % 7.59/7.75 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_3) a_7) False) (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3))))))) % 7.59/7.75 Clause #55 (by clausification #[54]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.75 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.75 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.75 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.75 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_3) a_7) False) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.75 (Or % 7.59/7.75 (Eq % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.59/7.75 False) % 7.59/7.75 (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3) False)))))))) % 7.59/7.75 Clause #56 (by clausification #[55]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.75 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.75 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.75 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.75 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.75 (Or % 7.59/7.75 (Eq % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And % 7.59/7.75 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.75 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.75 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_7 a_2) a_2)) % 7.59/7.78 False) % 7.59/7.78 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3) False) (Ne (skS.0 0 a_1 a_7 a_3) a_7)))))))) % 7.59/7.78 Clause #57 (by clausification #[56]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.78 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.78 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_3) a_3) False) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.78 (Or % 7.59/7.78 (Eq % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.59/7.78 False) % 7.59/7.78 (Eq (Eq (skS.0 0 a_1 a_7 a_2) a_2) False))))))))) % 7.59/7.78 Clause #58 (by clausification #[57]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.78 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.78 (Or % 7.59/7.78 (Eq % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And % 7.59/7.78 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.78 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.78 (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7)) % 7.59/7.78 False) % 7.59/7.78 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_2) a_2) False) (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3))))))))) % 7.59/7.78 Clause #59 (by clausification #[58]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.78 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.78 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.78 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.78 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_2) a_2) False) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.79 (Or % 7.59/7.79 (Eq % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.79 False) % 7.59/7.79 (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7) False)))))))))) % 7.59/7.79 Clause #60 (by clausification #[59]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.79 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.79 (Or % 7.59/7.79 (Eq % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_7 a_5) a_6)) % 7.59/7.79 False) % 7.59/7.79 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7) False) (Ne (skS.0 0 a_1 a_7 a_2) a_2)))))))))) % 7.59/7.79 Clause #61 (by clausification #[60]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.79 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.79 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.79 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_2) a_7) False) % 7.59/7.79 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.59/7.79 (Or % 7.59/7.79 (Eq % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And % 7.59/7.79 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.79 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.79 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.81 False) % 7.59/7.81 (Eq (Eq (skS.0 0 a_1 a_7 a_5) a_6) False))))))))))) % 7.59/7.81 Clause #62 (by clausification #[61]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.81 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.59/7.81 (Or % 7.59/7.81 (Eq % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3)) % 7.59/7.81 False) % 7.59/7.81 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_5) a_6) False) (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7))))))))))) % 7.59/7.81 Clause #63 (by clausification #[62]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.81 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.59/7.81 (Or (Eq (Eq (skS.0 0 a_1 a_7 a_5) a_6) False) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.59/7.81 (Or % 7.59/7.81 (Eq % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.59/7.81 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.59/7.81 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.59/7.81 False) % 7.59/7.81 (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3) False)))))))))))) % 7.59/7.81 Clause #64 (by clausification #[63]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.59/7.81 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.59/7.81 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.59/7.81 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.59/7.81 (Or % 7.59/7.81 (Eq % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And % 7.59/7.81 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_2) a_6)) % 7.67/7.83 False) % 7.67/7.83 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3) False) (Ne (skS.0 0 a_1 a_7 a_5) a_6)))))))))))) % 7.67/7.83 Clause #65 (by clausification #[64]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.83 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.83 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_7 a_5) a_3) False) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.83 (Or % 7.67/7.83 (Eq % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.67/7.83 False) % 7.67/7.83 (Eq (Eq (skS.0 0 a_1 a_6 a_2) a_6) False))))))))))))) % 7.67/7.83 Clause #66 (by clausification #[65]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.83 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.83 (Or % 7.67/7.83 (Eq % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And % 7.67/7.83 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.83 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.67/7.83 (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2)) % 7.67/7.83 False) % 7.67/7.83 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_2) a_6) False) (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3))))))))))))) % 7.67/7.83 Clause #67 (by clausification #[66]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.83 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.83 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.83 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.85 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_2) a_6) False) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.85 (Or % 7.67/7.85 (Eq % 7.67/7.85 (And % 7.67/7.85 (And % 7.67/7.85 (And % 7.67/7.85 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.85 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.85 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.67/7.85 False) % 7.67/7.85 (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2) False)))))))))))))) % 7.67/7.85 Clause #68 (by clausification #[67]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.85 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.85 (Or % 7.67/7.85 (Eq % 7.67/7.85 (And % 7.67/7.85 (And % 7.67/7.85 (And % 7.67/7.85 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.85 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.85 (Eq (skS.0 0 a_1 a_6 a_5) a_6)) % 7.67/7.85 False) % 7.67/7.85 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2) False) % 7.67/7.85 (Ne (skS.0 0 a_1 a_6 a_2) a_6)))))))))))))) % 7.67/7.85 Clause #69 (by clausification #[68]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.85 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.85 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.85 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_2) a_2) False) % 7.67/7.85 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.67/7.85 (Or % 7.67/7.85 (Eq % 7.67/7.85 (And % 7.67/7.85 (And % 7.67/7.85 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.85 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.85 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.85 False) % 7.67/7.85 (Eq (Eq (skS.0 0 a_1 a_6 a_5) a_6) False))))))))))))))) % 7.67/7.85 Clause #70 (by clausification #[69]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.85 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.67/7.86 (Or % 7.67/7.86 (Eq % 7.67/7.86 (And % 7.67/7.86 (And % 7.67/7.86 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.86 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.86 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.86 (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5)) % 7.67/7.86 False) % 7.67/7.86 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_5) a_6) False) % 7.67/7.86 (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2))))))))))))))) % 7.67/7.86 Clause #71 (by clausification #[70]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.86 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.67/7.86 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_5) a_6) False) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.67/7.86 (Or % 7.67/7.86 (Eq % 7.67/7.86 (And % 7.67/7.86 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.86 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.86 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.86 False) % 7.67/7.86 (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5) False)))))))))))))))) % 7.67/7.86 Clause #72 (by clausification #[71]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.67/7.86 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.67/7.86 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.67/7.86 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.67/7.86 (Or % 7.67/7.86 (Eq % 7.67/7.86 (And % 7.67/7.86 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.67/7.86 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.67/7.86 (Eq (skS.0 0 a_1 a_6 a_7) a_6)) % 7.67/7.86 False) % 7.67/7.86 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5) False) % 7.67/7.86 (Ne (skS.0 0 a_1 a_6 a_5) a_6)))))))))))))))) % 7.71/7.89 Clause #73 (by clausification #[72]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.89 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.89 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_5) a_5) False) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.89 (Or % 7.71/7.89 (Eq % 7.71/7.89 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.71/7.89 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.71/7.89 False) % 7.71/7.89 (Eq (Eq (skS.0 0 a_1 a_6 a_7) a_6) False))))))))))))))))) % 7.71/7.89 Clause #74 (by clausification #[73]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.89 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.89 (Or % 7.71/7.89 (Eq % 7.71/7.89 (And (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) % 7.71/7.89 (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7)) % 7.71/7.89 False) % 7.71/7.89 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_7) a_6) False) % 7.71/7.89 (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5))))))))))))))))) % 7.71/7.89 Clause #75 (by clausification #[74]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.89 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.89 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.89 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_7) a_6) False) % 7.71/7.89 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.89 (Or % 7.71/7.89 (Eq (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) False) % 7.71/7.89 (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7) False)))))))))))))))))) % 7.71/7.91 Clause #76 (by clausification #[75]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.91 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.91 (Or (Eq (And (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) (Eq (skS.0 0 a_1 a_6 a_3) a_6)) False) % 7.71/7.91 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7) False) % 7.71/7.91 (Ne (skS.0 0 a_1 a_6 a_7) a_6)))))))))))))))))) % 7.71/7.91 Clause #77 (by clausification #[76]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.91 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.91 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_7) a_7) False) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_7) a_6) % 7.71/7.91 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) False) % 7.71/7.91 (Eq (Eq (skS.0 0 a_1 a_6 a_3) a_6) False))))))))))))))))))) % 7.71/7.91 Clause #78 (by clausification #[77]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.91 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.91 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.91 (Or (Ne (skS.0 0 a_1 a_6 a_7) a_6) % 7.71/7.91 (Or (Eq (Eq (skS.0 1 a_1 a_4 a_6 a_3) a_3) False) % 7.71/7.91 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_3) a_6) False) % 7.71/7.91 (Ne (skS.0 1 a_1 a_4 a_6 a_7) a_7))))))))))))))))))) % 7.71/7.91 Clause #79 (by clausification #[78]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.93 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_7) a_6) % 7.71/7.93 (Or (Eq (Eq (skS.0 0 a_1 a_6 a_3) a_6) False) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_7) a_7) % 7.71/7.93 (Ne (skS.0 1 a_1 a_4 a_6 a_3) a_3))))))))))))))))))) % 7.71/7.93 Clause #80 (by clausification #[79]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 a_7 : a), % 7.71/7.93 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_3) a_7) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_2) a_7) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_7 a_5) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_7 a_5) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_5) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_5) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_7) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_7) a_7) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_3) a_3) % 7.71/7.93 (Ne (skS.0 0 a_1 a_6 a_3) a_6))))))))))))))))))) % 7.71/7.93 Clause #81 (by destructive equality resolution #[80]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a) (a_5 a_6 : a), % 7.71/7.93 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_5 a_3) a_5) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_5 a_2) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_3) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_3) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_2) a_6) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 a_6 a_5) (skS.0 0 a_1 a_5 a_2)) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 a_6 a_5) a_3) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_5 a_2) a_2) (skS.0 0 a_1 a_5 a_2)) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_5 a_2) a_2) a_2) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_5 a_2) a_5) (skS.0 0 a_1 a_5 a_2)) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_5 a_2) a_5) a_5) % 7.71/7.93 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_5 a_2) a_6) (skS.0 0 a_1 a_5 a_2)) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_5 a_2) a_6) a_6) % 7.71/7.93 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_5 a_2) a_3) a_3) % 7.71/7.93 (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_5 a_2) a_3) % 7.71/7.93 (skS.0 0 a_1 a_5 a_2))))))))))))))))))) % 7.71/7.93 Clause #82 (by destructive equality resolution #[81]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 a_5 : a), % 7.78/7.95 Or (Ne (skS.0 0 a_1 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) a_2) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) a_4) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) a_5) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_2) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_2) a_5) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 a_4) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_4) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_2) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_2) a_2) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_4) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_4) a_4) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_5) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_5) a_5) % 7.78/7.95 (Or % 7.78/7.95 (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (skS.0 0 a_1 a_4 a_2)))))))))))))))))) % 7.78/7.95 Clause #98 (by clausification #[19]): ∀ (a_1 a_2 : a → a → a), Eq (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 Xx Xy) Xy) Xy) True % 7.78/7.95 Clause #99 (by clausification #[19]): ∀ (a_1 a_2 : a → a → a), % 7.78/7.95 Eq % 7.78/7.95 (And % 7.78/7.95 (And % 7.78/7.95 (And % 7.78/7.95 (And % 7.78/7.95 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.78/7.95 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.78/7.95 (∀ (Xx Xy Xz : a), % 7.78/7.95 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.78/7.95 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.78/7.95 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.78/7.95 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy)) % 7.78/7.95 True % 7.78/7.95 Clause #100 (by clausification #[98]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), Eq (∀ (Xy : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 Xy) Xy) Xy) True % 7.78/7.95 Clause #101 (by clausification #[100]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 a_4) a_4) a_4) True % 7.78/7.95 Clause #102 (by clausification #[101]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 a_4) a_4) a_4 % 7.78/7.95 Clause #104 (by backward contextual literal cutting #[102, 82]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 a_5 : a), % 7.78/7.95 Or (Ne (skS.0 0 a_1 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) a_2) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) a_4) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) a_5) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_2) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_2) a_5) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 a_5 a_4) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_4) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_2) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_4) (skS.0 0 a_1 a_4 a_2)) % 7.78/7.95 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_4) a_4) % 7.78/7.95 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_5) (skS.0 0 a_1 a_4 a_2)) % 7.80/7.98 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_5) a_5) % 7.80/7.98 (Or % 7.80/7.98 (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (skS.0 0 a_1 a_4 a_2))))))))))))))))) % 7.80/7.98 Clause #106 (by clausification #[99]): ∀ (a_1 a_2 : a → a → a), Eq (∀ (Xx Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 Xx Xy) Xy) Xy) True % 7.80/7.98 Clause #107 (by clausification #[99]): ∀ (a_1 a_2 : a → a → a), % 7.80/7.98 Eq % 7.80/7.98 (And % 7.80/7.98 (And % 7.80/7.98 (And % 7.80/7.98 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.80/7.98 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.80/7.98 (∀ (Xx Xy Xz : a), % 7.80/7.98 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.80/7.98 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.80/7.98 (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx))) % 7.80/7.98 True % 7.80/7.98 Clause #108 (by clausification #[106]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), Eq (∀ (Xy : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 a_3 Xy) Xy) Xy) True % 7.80/7.98 Clause #109 (by clausification #[108]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 a_3 a_4) a_4) a_4) True % 7.80/7.98 Clause #110 (by clausification #[109]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 a_3 a_4) a_4) a_4 % 7.80/7.98 Clause #111 (by superposition #[110, 102]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), Eq (skS.0 1 a_1 a_2 a_3 a_3) a_3 % 7.80/7.98 Clause #112 (by superposition #[110, 102]): ∀ (a_1 : a → a → a) (a_2 : a), Eq (skS.0 0 a_1 a_2 a_2) a_2 % 7.80/7.98 Clause #113 (by clausification #[107]): ∀ (a_1 a_2 : a → a → a), Eq (∀ (Xx Xy : a), Eq (skS.0 1 a_1 a_2 Xx Xy) (skS.0 1 a_1 a_2 Xy Xx)) True % 7.80/7.98 Clause #114 (by clausification #[107]): ∀ (a_1 a_2 : a → a → a), % 7.80/7.98 Eq % 7.80/7.98 (And % 7.80/7.98 (And % 7.80/7.98 (And (And (∀ (Xx : a), Eq (skS.0 0 a_1 Xx Xx) Xx) (∀ (Xx : a), Eq (skS.0 1 a_1 a_2 Xx Xx) Xx)) % 7.80/7.98 (∀ (Xx Xy Xz : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 Xx Xy) Xz) (skS.0 0 a_1 Xx (skS.0 0 a_1 Xy Xz)))) % 7.80/7.98 (∀ (Xx Xy Xz : a), % 7.80/7.98 Eq (skS.0 1 a_1 a_2 (skS.0 1 a_1 a_2 Xx Xy) Xz) (skS.0 1 a_1 a_2 Xx (skS.0 1 a_1 a_2 Xy Xz)))) % 7.80/7.98 (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx))) % 7.80/7.98 True % 7.80/7.98 Clause #115 (by clausification #[113]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), Eq (∀ (Xy : a), Eq (skS.0 1 a_1 a_2 a_3 Xy) (skS.0 1 a_1 a_2 Xy a_3)) True % 7.80/7.98 Clause #116 (by clausification #[115]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (Eq (skS.0 1 a_1 a_2 a_3 a_4) (skS.0 1 a_1 a_2 a_4 a_3)) True % 7.80/7.98 Clause #117 (by clausification #[116]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 1 a_1 a_2 a_3 a_4) (skS.0 1 a_1 a_2 a_4 a_3) % 7.80/7.98 Clause #118 (by superposition #[117, 102]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 1 a_1 a_2 a_3 (skS.0 0 a_1 a_4 a_3)) a_3 % 7.80/7.98 Clause #119 (by superposition #[117, 110]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 0 a_1 (skS.0 1 a_1 a_2 a_3 a_4) a_3) a_3 % 7.80/7.98 Clause #120 (by forward demodulation #[104, 117]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 a_5 : a), % 7.80/7.98 Or (Ne (skS.0 0 a_1 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) a_2) % 7.80/7.98 (Or (Ne (skS.0 1 a_1 a_3 a_2 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (Or (Ne (skS.0 0 a_1 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) a_4) % 7.80/7.98 (Or (Ne (skS.0 1 a_1 a_3 a_4 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (Or (Ne (skS.0 0 a_1 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) a_5) % 7.80/7.98 (Or (Ne (skS.0 1 a_1 a_3 a_5 (skS.0 1 a_1 a_3 a_4 a_2)) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.98 (Or (Ne (skS.0 0 a_1 a_5 a_2) a_2) % 7.80/7.98 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_2) a_5) % 7.80/7.98 (Or (Ne (skS.0 0 a_1 a_5 a_4) (skS.0 0 a_1 a_4 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_5 a_4) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_2) (skS.0 0 a_1 a_4 a_2)) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_4) (skS.0 0 a_1 a_4 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 (skS.0 0 a_1 a_4 a_2)) a_4) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) a_5) (skS.0 0 a_1 a_4 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) a_5) a_5) % 7.80/7.99 (Or % 7.80/7.99 (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.99 (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.99 (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_4 a_2) (skS.0 1 a_1 a_3 a_4 a_2)) % 7.80/7.99 (skS.0 0 a_1 a_4 a_2))))))))))))))))) % 7.80/7.99 Clause #122 (by superposition #[120, 111]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 : a), % 7.80/7.99 Or (Ne (skS.0 0 a_1 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) a_4) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 a_2) a_4) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_2) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_2) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_2 (skS.0 0 a_1 a_2 a_2)) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_4) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_2 a_2) a_4) a_4) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_2 a_2) a_2) a_2) % 7.80/7.99 (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_2) (skS.0 0 a_1 a_2 a_2))))))))))))))))) % 7.80/7.99 Clause #128 (by clausification #[114]): ∀ (a_1 : a → a → a), Eq (∀ (Xx Xy : a), Eq (skS.0 0 a_1 Xx Xy) (skS.0 0 a_1 Xy Xx)) True % 7.80/7.99 Clause #130 (by clausification #[128]): ∀ (a_1 : a → a → a) (a_2 : a), Eq (∀ (Xy : a), Eq (skS.0 0 a_1 a_2 Xy) (skS.0 0 a_1 Xy a_2)) True % 7.80/7.99 Clause #131 (by clausification #[130]): ∀ (a_1 : a → a → a) (a_2 a_3 : a), Eq (Eq (skS.0 0 a_1 a_2 a_3) (skS.0 0 a_1 a_3 a_2)) True % 7.80/7.99 Clause #132 (by clausification #[131]): ∀ (a_1 : a → a → a) (a_2 a_3 : a), Eq (skS.0 0 a_1 a_2 a_3) (skS.0 0 a_1 a_3 a_2) % 7.80/7.99 Clause #134 (by superposition #[132, 119]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 : a), Eq (skS.0 0 a_1 a_2 (skS.0 1 a_1 a_3 a_2 a_4)) a_2 % 7.80/7.99 Clause #135 (by superposition #[132, 102]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), Eq (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 a_4) a_3) a_3 % 7.80/7.99 Clause #146 (by superposition #[134, 135]): ∀ (a_1 : a → a → a) (a_2 a_3 : a), Eq (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_3) a_2) (skS.0 0 a_1 a_2 a_3) % 7.80/7.99 Clause #191 (by eliminate duplicate literals #[122]): ∀ (a_1 : a → a → a) (a_2 : a) (a_3 : a → a → a) (a_4 : a), % 7.80/7.99 Or (Ne (skS.0 0 a_1 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_2 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) a_4) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) a_2) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_4 a_2) a_4) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 a_4 a_2) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_2) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 a_2 (skS.0 0 a_1 a_2 a_2)) a_2) % 7.80/7.99 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_2 a_2) a_4) (skS.0 0 a_1 a_2 a_2)) % 7.80/7.99 (Or (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_2 a_2) a_4) a_4) % 7.80/7.99 (Ne (skS.0 1 a_1 a_3 (skS.0 0 a_1 a_2 a_2) a_2) a_2))))))))))) % 7.80/8.02 Clause #192 (by forward demodulation #[191, 112]): ∀ (a_1 : a) (a_2 a_3 : a → a → a) (a_4 : a), % 7.80/8.02 Or (Ne a_1 a_1) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_3 a_1 a_1) a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_4 a_1) a_4) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_3 a_4 a_1) a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_4 a_1) a_1) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_3 a_4 a_1) a_4) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_4 a_1) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 (skS.0 0 a_2 a_1 a_1) a_1) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_3 a_1 (skS.0 0 a_2 a_1 a_1)) a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 (skS.0 0 a_2 a_1 a_1) a_4) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_3 (skS.0 0 a_2 a_1 a_1) a_4) a_4) % 7.80/8.02 (Ne (skS.0 1 a_2 a_3 (skS.0 0 a_2 a_1 a_1) a_1) a_1))))))))))) % 7.80/8.02 Clause #193 (by eliminate resolved literals #[192]): ∀ (a_1 a_2 : a → a → a) (a_3 a_4 : a), % 7.80/8.02 Or (Ne (skS.0 1 a_1 a_2 a_3 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_4 a_3) a_4) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_2 a_4 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_4 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_2 a_4 a_3) a_4) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_4 a_3) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_3) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_2 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_4) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 a_3) a_4) a_4) % 7.80/8.02 (Ne (skS.0 1 a_1 a_2 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))))))) % 7.80/8.02 Clause #194 (by forward demodulation #[193, 111]): ∀ (a_1 : a) (a_2 : a → a → a) (a_3 : a) (a_4 : a → a → a), % 7.80/8.02 Or (Ne a_1 a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_3 a_1) a_3) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_4 a_3 a_1) a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_3 a_1) a_1) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_4 a_3 a_1) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 a_3 a_1) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 (skS.0 0 a_2 a_1 a_1) a_1) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_4 a_1 (skS.0 0 a_2 a_1 a_1)) a_1) % 7.80/8.02 (Or (Ne (skS.0 0 a_2 (skS.0 0 a_2 a_1 a_1) a_3) (skS.0 0 a_2 a_1 a_1)) % 7.80/8.02 (Or (Ne (skS.0 1 a_2 a_4 (skS.0 0 a_2 a_1 a_1) a_3) a_3) % 7.80/8.02 (Ne (skS.0 1 a_2 a_4 (skS.0 0 a_2 a_1 a_1) a_1) a_1)))))))))) % 7.80/8.02 Clause #195 (by eliminate resolved literals #[194]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.80/8.02 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_2 a_3) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_3) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.80/8.02 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3))))))))) % 7.80/8.02 Clause #196 (by forward demodulation #[195, 112]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.80/8.02 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_3) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.80/8.02 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3))))))))) % 7.80/8.02 Clause #197 (by eliminate duplicate literals #[196]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.80/8.02 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.80/8.02 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.80/8.02 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_3) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))))) % 7.86/8.04 Clause #198 (by forward demodulation #[197, 146]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_3 a_3) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))))) % 7.86/8.04 Clause #199 (by eliminate resolved literals #[198]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_3 (skS.0 0 a_1 a_3 a_3)) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3))))))) % 7.86/8.04 Clause #200 (by forward demodulation #[199, 118]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne a_3 a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3))))))) % 7.86/8.04 Clause #201 (by eliminate resolved literals #[200]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 (skS.0 0 a_1 a_3 a_3) a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))) % 7.86/8.04 Clause #202 (by forward demodulation #[201, 112]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_3 a_2) (skS.0 0 a_1 a_3 a_3)) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))) % 7.86/8.04 Clause #203 (by forward demodulation #[202, 112]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_3 a_2) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_2) a_2) % 7.86/8.04 (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))) % 7.86/8.04 Clause #204 (by forward demodulation #[203, 112]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.04 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.04 (Or (Ne (skS.0 0 a_1 a_3 a_2) a_3) % 7.86/8.04 (Or (Ne (skS.0 1 a_1 a_4 a_3 a_2) a_2) (Ne (skS.0 1 a_1 a_4 (skS.0 0 a_1 a_3 a_3) a_3) a_3)))))) % 7.86/8.05 Clause #205 (by forward demodulation #[204, 102]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.05 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.05 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.05 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.05 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) % 7.86/8.05 (Or (Ne (skS.0 0 a_1 a_3 a_2) a_3) (Or (Ne (skS.0 1 a_1 a_4 a_3 a_2) a_2) (Ne a_3 a_3)))))) % 7.86/8.05 Clause #206 (by eliminate resolved literals #[205]): ∀ (a_1 : a → a → a) (a_2 a_3 : a) (a_4 : a → a → a), % 7.86/8.05 Or (Ne (skS.0 0 a_1 a_2 a_3) a_2) % 7.86/8.05 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_3) % 7.86/8.05 (Or (Ne (skS.0 0 a_1 a_2 a_3) a_3) % 7.86/8.05 (Or (Ne (skS.0 1 a_1 a_4 a_2 a_3) a_2) (Or (Ne (skS.0 0 a_1 a_3 a_2) a_3) (Ne (skS.0 1 a_1 a_4 a_3 a_2) a_2))))) % 7.86/8.05 Clause #215 (by superposition #[206, 112]): ∀ (a_1 : a) (a_2 a_3 : a → a → a), % 7.86/8.05 Or (Ne a_1 a_1) % 7.86/8.05 (Or (Ne (skS.0 1 a_2 a_3 a_1 a_1) a_1) % 7.86/8.05 (Or (Ne a_1 a_1) (Or (Ne (skS.0 1 a_2 a_3 a_1 a_1) a_1) (Or (Ne a_1 a_1) (Ne (skS.0 1 a_2 a_3 a_1 a_1) a_1))))) % 7.86/8.05 Clause #279 (by eliminate duplicate literals #[215]): ∀ (a_1 : a) (a_2 a_3 : a → a → a), Or (Ne a_1 a_1) (Ne (skS.0 1 a_2 a_3 a_1 a_1) a_1) % 7.86/8.05 Clause #280 (by eliminate resolved literals #[279]): ∀ (a_1 a_2 : a → a → a) (a_3 : a), Ne (skS.0 1 a_1 a_2 a_3 a_3) a_3 % 7.86/8.05 Clause #281 (by forward demodulation #[280, 111]): ∀ (a_1 : a), Ne a_1 a_1 % 7.86/8.05 Clause #282 (by eliminate resolved literals #[281]): False % 7.86/8.05 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------