%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYN353+1 : TPTP v9.2.0. Released v2.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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:07:28 PM UTC 2025 % Result : Theorem 148.54s 148.77s % Output : Proof 148.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SYN353+1 : TPTP v9.2.0. Released v2.0.0. % 0.08/0.15 % Command : duper %s % 0.16/0.37 % Computer : n009.cluster.edu % 0.16/0.37 % Model : x86_64 x86_64 % 0.16/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.37 % Memory : 8042.1875MB % 0.16/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.37 % CPULimit : 300 % 0.16/0.37 % WCLimit : 300 % 0.16/0.37 % DateTime : Thu Oct 2 15:22:23 EDT 2025 % 0.16/0.37 % CPUTime : % 148.54/148.77 SZS status Theorem for theBenchmark.p % 148.54/148.77 SZS output start Proof for theBenchmark.p % 148.54/148.77 Clause #0 (by assumption #[]): Eq % 148.54/148.77 (Not % 148.54/148.77 (∀ (X : Iota), % 148.54/148.77 Exists fun Y1 => % 148.54/148.77 Exists fun Y2 => % 148.54/148.77 Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f Y1 Y2 Y3 → big_f X X Z → Or (big_f Y2 Y3 Y1) (big_f Y3 Y1 Y2)) → % 148.54/148.77 Iff (big_f Y3 Y1 Y2 → And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y2 Y1 Z) → % 148.54/148.77 Iff (big_f Y2 Y3 Y1 → And (big_f Y1 Y2 Y3) (big_f Y3 Y1 Y2)) (big_f Y1 Z Y2) → % 148.54/148.77 Iff ((big_f Y3 Y1 Y2 → Not (big_f Y2 Y3 Y1)) → big_f Y1 Y2 Y3) (big_f Z Y2 Y1) → % 148.54/148.77 Iff (And (And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y3 Y1 Y2)) (big_f Z Z Z))) % 148.54/148.77 True % 148.54/148.77 Clause #1 (by clausification #[0]): Eq % 148.54/148.77 (∀ (X : Iota), % 148.54/148.77 Exists fun Y1 => % 148.54/148.77 Exists fun Y2 => % 148.54/148.77 Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f Y1 Y2 Y3 → big_f X X Z → Or (big_f Y2 Y3 Y1) (big_f Y3 Y1 Y2)) → % 148.54/148.77 Iff (big_f Y3 Y1 Y2 → And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y2 Y1 Z) → % 148.54/148.77 Iff (big_f Y2 Y3 Y1 → And (big_f Y1 Y2 Y3) (big_f Y3 Y1 Y2)) (big_f Y1 Z Y2) → % 148.54/148.77 Iff ((big_f Y3 Y1 Y2 → Not (big_f Y2 Y3 Y1)) → big_f Y1 Y2 Y3) (big_f Z Y2 Y1) → % 148.54/148.77 Iff (And (And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y3 Y1 Y2)) (big_f Z Z Z)) % 148.54/148.77 False % 148.54/148.77 Clause #2 (by clausification #[1]): ∀ (a : Iota), % 148.54/148.77 Eq % 148.54/148.77 (Not % 148.54/148.77 (Exists fun Y1 => % 148.54/148.77 Exists fun Y2 => % 148.54/148.77 Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f Y1 Y2 Y3 → big_f (skS.0 0 a) (skS.0 0 a) Z → Or (big_f Y2 Y3 Y1) (big_f Y3 Y1 Y2)) → % 148.54/148.77 Iff (big_f Y3 Y1 Y2 → And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y2 Y1 Z) → % 148.54/148.77 Iff (big_f Y2 Y3 Y1 → And (big_f Y1 Y2 Y3) (big_f Y3 Y1 Y2)) (big_f Y1 Z Y2) → % 148.54/148.77 Iff ((big_f Y3 Y1 Y2 → Not (big_f Y2 Y3 Y1)) → big_f Y1 Y2 Y3) (big_f Z Y2 Y1) → % 148.54/148.77 Iff (And (And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y3 Y1 Y2)) (big_f Z Z Z))) % 148.54/148.77 True % 148.54/148.77 Clause #3 (by clausification #[2]): ∀ (a : Iota), % 148.54/148.77 Eq % 148.54/148.77 (Exists fun Y1 => % 148.54/148.77 Exists fun Y2 => % 148.54/148.77 Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f Y1 Y2 Y3 → big_f (skS.0 0 a) (skS.0 0 a) Z → Or (big_f Y2 Y3 Y1) (big_f Y3 Y1 Y2)) → % 148.54/148.77 Iff (big_f Y3 Y1 Y2 → And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y2 Y1 Z) → % 148.54/148.77 Iff (big_f Y2 Y3 Y1 → And (big_f Y1 Y2 Y3) (big_f Y3 Y1 Y2)) (big_f Y1 Z Y2) → % 148.54/148.77 Iff ((big_f Y3 Y1 Y2 → Not (big_f Y2 Y3 Y1)) → big_f Y1 Y2 Y3) (big_f Z Y2 Y1) → % 148.54/148.77 Iff (And (And (big_f Y1 Y2 Y3) (big_f Y2 Y3 Y1)) (big_f Y3 Y1 Y2)) (big_f Z Z Z)) % 148.54/148.77 False % 148.54/148.77 Clause #4 (by clausification #[3]): ∀ (a a_1 : Iota), % 148.54/148.77 Eq % 148.54/148.77 (Exists fun Y2 => % 148.54/148.77 Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f a Y2 Y3 → big_f (skS.0 0 a_1) (skS.0 0 a_1) Z → Or (big_f Y2 Y3 a) (big_f Y3 a Y2)) → % 148.54/148.77 Iff (big_f Y3 a Y2 → And (big_f a Y2 Y3) (big_f Y2 Y3 a)) (big_f Y2 a Z) → % 148.54/148.77 Iff (big_f Y2 Y3 a → And (big_f a Y2 Y3) (big_f Y3 a Y2)) (big_f a Z Y2) → % 148.54/148.77 Iff ((big_f Y3 a Y2 → Not (big_f Y2 Y3 a)) → big_f a Y2 Y3) (big_f Z Y2 a) → % 148.54/148.77 Iff (And (And (big_f a Y2 Y3) (big_f Y2 Y3 a)) (big_f Y3 a Y2)) (big_f Z Z Z)) % 148.54/148.77 False % 148.54/148.77 Clause #5 (by clausification #[4]): ∀ (a a_1 a_2 : Iota), % 148.54/148.77 Eq % 148.54/148.77 (Exists fun Y3 => % 148.54/148.77 ∀ (Z : Iota), % 148.54/148.77 (big_f a a_1 Y3 → big_f (skS.0 0 a_2) (skS.0 0 a_2) Z → Or (big_f a_1 Y3 a) (big_f Y3 a a_1)) → % 148.54/148.77 Iff (big_f Y3 a a_1 → And (big_f a a_1 Y3) (big_f a_1 Y3 a)) (big_f a_1 a Z) → % 148.54/148.77 Iff (big_f a_1 Y3 a → And (big_f a a_1 Y3) (big_f Y3 a a_1)) (big_f a Z a_1) → % 148.54/148.77 Iff ((big_f Y3 a a_1 → Not (big_f a_1 Y3 a)) → big_f a a_1 Y3) (big_f Z a_1 a) → % 148.54/148.77 Iff (And (And (big_f a a_1 Y3) (big_f a_1 Y3 a)) (big_f Y3 a a_1)) (big_f Z Z Z)) % 148.54/148.77 False % 148.54/148.77 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 a_3 : Iota), % 148.54/148.80 Eq % 148.54/148.80 (∀ (Z : Iota), % 148.54/148.80 (big_f a a_1 a_2 → big_f (skS.0 0 a_3) (skS.0 0 a_3) Z → Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) → % 148.54/148.80 Iff (big_f a_2 a a_1 → And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_1 a Z) → % 148.54/148.80 Iff (big_f a_1 a_2 a → And (big_f a a_1 a_2) (big_f a_2 a a_1)) (big_f a Z a_1) → % 148.54/148.80 Iff ((big_f a_2 a a_1 → Not (big_f a_1 a_2 a)) → big_f a a_1 a_2) (big_f Z a_1 a) → % 148.54/148.80 Iff (And (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_2 a a_1)) (big_f Z Z Z)) % 148.54/148.80 False % 148.54/148.80 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq % 148.54/148.80 (Not % 148.54/148.80 ((big_f a a_1 a_2 → % 148.54/148.80 big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4) → Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) → % 148.54/148.80 Iff (big_f a_2 a a_1 → And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_1 a (skS.0 1 a a_1 a_2 a_3 a_4)) → % 148.54/148.80 Iff (big_f a_1 a_2 a → And (big_f a a_1 a_2) (big_f a_2 a a_1)) (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) → % 148.54/148.80 Iff ((big_f a_2 a a_1 → Not (big_f a_1 a_2 a)) → big_f a a_1 a_2) % 148.54/148.80 (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) → % 148.54/148.80 Iff (And (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_2 a a_1)) % 148.54/148.80 (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4)))) % 148.54/148.80 True % 148.54/148.80 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq % 148.54/148.80 ((big_f a a_1 a_2 → % 148.54/148.80 big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4) → Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) → % 148.54/148.80 Iff (big_f a_2 a a_1 → And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_1 a (skS.0 1 a a_1 a_2 a_3 a_4)) → % 148.54/148.80 Iff (big_f a_1 a_2 a → And (big_f a a_1 a_2) (big_f a_2 a a_1)) (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) → % 148.54/148.80 Iff ((big_f a_2 a a_1 → Not (big_f a_1 a_2 a)) → big_f a a_1 a_2) (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) → % 148.54/148.80 Iff (And (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_2 a a_1)) % 148.54/148.80 (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4))) % 148.54/148.80 False % 148.54/148.80 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq % 148.54/148.80 (big_f a a_1 a_2 → % 148.54/148.80 big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4) → Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) % 148.54/148.80 True % 148.54/148.80 Clause #10 (by clausification #[8]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq % 148.54/148.80 (Iff (big_f a a_1 a_2 → And (big_f a_1 a_2 a) (big_f a_2 a a_1)) (big_f a_2 a_1 (skS.0 1 a_1 a_2 a a_3 a_4)) → % 148.54/148.80 Iff (big_f a_2 a a_1 → And (big_f a_1 a_2 a) (big_f a a_1 a_2)) (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) → % 148.54/148.80 Iff ((big_f a a_1 a_2 → Not (big_f a_2 a a_1)) → big_f a_1 a_2 a) (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) → % 148.54/148.80 Iff (And (And (big_f a_1 a_2 a) (big_f a_2 a a_1)) (big_f a a_1 a_2)) % 148.54/148.80 (big_f (skS.0 1 a_1 a_2 a a_3 a_4) (skS.0 1 a_1 a_2 a a_3 a_4) (skS.0 1 a_1 a_2 a a_3 a_4))) % 148.54/148.80 False % 148.54/148.80 Clause #11 (by clausification #[9]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Or (Eq (big_f a a_1 a_2) False) % 148.54/148.80 (Eq (big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4) → Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) True) % 148.54/148.80 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Or (Eq (big_f a a_1 a_2) False) % 148.54/148.80 (Or (Eq (big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4)) False) % 148.54/148.80 (Eq (Or (big_f a_1 a_2 a) (big_f a_2 a a_1)) True)) % 148.54/148.80 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Or (Eq (big_f a a_1 a_2) False) % 148.54/148.80 (Or (Eq (big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a a_1 a_2 a_3 a_4)) False) % 148.54/148.80 (Or (Eq (big_f a_1 a_2 a) True) (Eq (big_f a_2 a a_1) True))) % 148.54/148.80 Clause #14 (by clausification #[10]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq (Iff (big_f a a_1 a_2 → And (big_f a_1 a_2 a) (big_f a_2 a a_1)) (big_f a_2 a_1 (skS.0 1 a_1 a_2 a a_3 a_4))) True % 148.54/148.80 Clause #15 (by clausification #[10]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.54/148.80 Eq % 148.54/148.80 (Iff (big_f a a_1 a_2 → And (big_f a_2 a a_1) (big_f a_1 a_2 a)) (big_f a_2 (skS.0 1 a_2 a a_1 a_3 a_4) a) → % 148.62/148.82 Iff ((big_f a_1 a_2 a → Not (big_f a a_1 a_2)) → big_f a_2 a a_1) (big_f (skS.0 1 a_2 a a_1 a_3 a_4) a a_2) → % 148.62/148.82 Iff (And (And (big_f a_2 a a_1) (big_f a a_1 a_2)) (big_f a_1 a_2 a)) % 148.62/148.82 (big_f (skS.0 1 a_2 a a_1 a_3 a_4) (skS.0 1 a_2 a a_1 a_3 a_4) (skS.0 1 a_2 a a_1 a_3 a_4))) % 148.62/148.82 False % 148.62/148.82 Clause #16 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2 → And (big_f a_1 a_2 a) (big_f a_2 a a_1)) True) % 148.62/148.82 (Eq (big_f a_2 a_1 (skS.0 1 a_1 a_2 a a_3 a_4)) False) % 148.62/148.82 Clause #17 (by clausification #[14]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2 → And (big_f a_1 a_2 a) (big_f a_2 a a_1)) False) % 148.62/148.82 (Eq (big_f a_2 a_1 (skS.0 1 a_1 a_2 a a_3 a_4)) True) % 148.62/148.82 Clause #18 (by clausification #[16]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) False) % 148.62/148.82 (Or (Eq (big_f a_2 a_1 a) False) (Eq (And (big_f a_1 a a_2) (big_f a a_2 a_1)) True)) % 148.62/148.82 Clause #19 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) False) (Or (Eq (big_f a_2 a_1 a) False) (Eq (big_f a a_2 a_1) True)) % 148.62/148.82 Clause #20 (by clausification #[18]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) False) (Or (Eq (big_f a_2 a_1 a) False) (Eq (big_f a_1 a a_2) True)) % 148.62/148.82 Clause #21 (by clausification #[17]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) (Eq (big_f a_2 a_1 a) True) % 148.62/148.82 Clause #25 (by superposition #[21, 13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2) True) % 148.62/148.82 (Or (Eq True False) % 148.62/148.82 (Or (Eq (big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a_2 a_1 (skS.0 1 a_1 a_2 a a_4 a_5) a_3 a_6)) False) % 148.62/148.82 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_4 a_5) a_2) True) % 148.62/148.82 (Eq (big_f (skS.0 1 a_1 a_2 a a_4 a_5) a_2 a_1) True)))) % 148.62/148.82 Clause #27 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Eq (Iff (big_f a a_1 a_2 → And (big_f a_2 a a_1) (big_f a_1 a_2 a)) (big_f a_2 (skS.0 1 a_2 a a_1 a_3 a_4) a)) True % 148.62/148.82 Clause #28 (by clausification #[15]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Eq % 148.62/148.82 (Iff ((big_f a a_1 a_2 → Not (big_f a_2 a a_1)) → big_f a_1 a_2 a) (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) → % 148.62/148.82 Iff (And (And (big_f a_1 a_2 a) (big_f a_2 a a_1)) (big_f a a_1 a_2)) % 148.62/148.82 (big_f (skS.0 1 a_1 a_2 a a_3 a_4) (skS.0 1 a_1 a_2 a a_3 a_4) (skS.0 1 a_1 a_2 a a_3 a_4))) % 148.62/148.82 False % 148.62/148.82 Clause #29 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2 → And (big_f a_2 a a_1) (big_f a_1 a_2 a)) True) % 148.62/148.82 (Eq (big_f a_2 (skS.0 1 a_2 a a_1 a_3 a_4) a) False) % 148.62/148.82 Clause #30 (by clausification #[27]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2 → And (big_f a_2 a a_1) (big_f a_1 a_2 a)) False) % 148.62/148.82 (Eq (big_f a_2 (skS.0 1 a_2 a a_1 a_3 a_4) a) True) % 148.62/148.82 Clause #31 (by clausification #[29]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) False) % 148.62/148.82 (Or (Eq (big_f a_1 a_2 a) False) (Eq (And (big_f a a_1 a_2) (big_f a_2 a a_1)) True)) % 148.62/148.82 Clause #32 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) False) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a_2 a a_1) True)) % 148.62/148.82 Clause #33 (by clausification #[31]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.82 Or (Eq (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) False) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a a_1 a_2) True)) % 148.62/148.82 Clause #37 (by clausification #[30]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (big_f a (skS.0 1 a a_1 a_2 a_3 a_4) a_1) True) (Eq (big_f a_1 a_2 a) True) % 148.62/148.82 Clause #44 (by clausification #[25]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.62/148.82 Or (Eq (big_f a a_1 a_2) True) % 148.62/148.82 (Or (Eq (big_f (skS.0 0 a_3) (skS.0 0 a_3) (skS.0 1 a_2 a_1 (skS.0 1 a_1 a_2 a a_4 a_5) a_3 a_6)) False) % 148.62/148.82 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_4 a_5) a_2) True) (Eq (big_f (skS.0 1 a_1 a_2 a a_4 a_5) a_2 a_1) True))) % 148.62/148.82 Clause #45 (by superposition #[44, 21]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.82 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.82 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.84 (Or (Eq (big_f (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.84 (Or (Eq False True) % 148.62/148.84 (Eq (big_f (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1) (skS.0 0 a_1)) True)))) % 148.62/148.84 Clause #58 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Eq (Iff ((big_f a a_1 a_2 → Not (big_f a_2 a a_1)) → big_f a_1 a_2 a) (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1)) % 148.62/148.84 True % 148.62/148.84 Clause #59 (by clausification #[28]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Eq % 148.62/148.84 (Iff (And (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_2 a a_1)) % 148.62/148.84 (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4))) % 148.62/148.84 False % 148.62/148.84 Clause #60 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq ((big_f a a_1 a_2 → Not (big_f a_2 a a_1)) → big_f a_1 a_2 a) True) % 148.62/148.84 (Eq (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) False) % 148.62/148.84 Clause #61 (by clausification #[58]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq ((big_f a a_1 a_2 → Not (big_f a_2 a a_1)) → big_f a_1 a_2 a) False) % 148.62/148.84 (Eq (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) True) % 148.62/148.84 Clause #62 (by clausification #[60]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) False) % 148.62/148.84 (Or (Eq (big_f a_2 a a_1 → Not (big_f a_1 a_2 a)) False) (Eq (big_f a a_1 a_2) True)) % 148.62/148.84 Clause #63 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) False) (Or (Eq (big_f a a_1 a_2) True) (Eq (big_f a_2 a a_1) True)) % 148.62/148.84 Clause #64 (by clausification #[62]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) False) % 148.62/148.84 (Or (Eq (big_f a a_1 a_2) True) (Eq (Not (big_f a_1 a_2 a)) False)) % 148.62/148.84 Clause #65 (by clausification #[61]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) (Eq (big_f a_2 a a_1 → Not (big_f a_1 a_2 a)) True) % 148.62/148.84 Clause #67 (by clausification #[65]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) % 148.62/148.84 (Or (Eq (big_f a_2 a a_1) False) (Eq (Not (big_f a_1 a_2 a)) True)) % 148.62/148.84 Clause #68 (by clausification #[67]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) (Or (Eq (big_f a_2 a a_1) False) (Eq (big_f a_1 a_2 a) False)) % 148.62/148.84 Clause #75 (by clausification #[64]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) False) (Or (Eq (big_f a a_1 a_2) True) (Eq (big_f a_1 a_2 a) True)) % 148.62/148.84 Clause #112 (by clausification #[59]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (And (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) (big_f a_2 a a_1)) False) % 148.62/148.84 (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4)) False) % 148.62/148.84 Clause #114 (by clausification #[112]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4)) False) % 148.62/148.84 (Or (Eq (And (big_f a a_1 a_2) (big_f a_1 a_2 a)) False) (Eq (big_f a_2 a a_1) False)) % 148.62/148.84 Clause #115 (by clausification #[114]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.62/148.84 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4) (skS.0 1 a a_1 a_2 a_3 a_4)) False) % 148.62/148.84 (Or (Eq (big_f a_2 a a_1) False) (Or (Eq (big_f a a_1 a_2) False) (Eq (big_f a_1 a_2 a) False))) % 148.62/148.84 Clause #152 (by clausification #[45]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.84 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.84 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.84 (Or (Eq (big_f (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.84 (Eq (big_f (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1) (skS.0 0 a_1)) True))) % 148.62/148.84 Clause #153 (by eliminate duplicate literals #[152]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.84 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.84 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.84 (Eq (big_f (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1) (skS.0 0 a_1)) True)) % 148.62/148.87 Clause #158 (by superposition #[153, 63]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq True False) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True) (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True)))) % 148.62/148.87 Clause #225 (by clausification #[158]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True) (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True))) % 148.62/148.87 Clause #226 (by eliminate duplicate literals #[225]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 1 (skS.0 0 a_1) (skS.0 0 a_1) a a_2 a_3) (skS.0 0 a_1)) True) % 148.62/148.87 (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True)) % 148.62/148.87 Clause #228 (by superposition #[226, 33]): ∀ (a a_1 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True) % 148.62/148.87 (Or (Eq True False) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False) (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True)))) % 148.62/148.87 Clause #236 (by clausification #[228]): ∀ (a a_1 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False) (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True))) % 148.62/148.87 Clause #237 (by eliminate duplicate literals #[236]): ∀ (a a_1 : Iota), % 148.62/148.87 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a_1) (skS.0 0 a_1) a) True) (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False)) % 148.62/148.87 Clause #239 (by superposition #[237, 37]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Or (Eq False True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.62/148.87 Clause #433 (by clausification #[239]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)) % 148.62/148.87 Clause #439 (by superposition #[433, 68]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.62/148.87 (Or % 148.62/148.87 (Eq % 148.62/148.87 (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) (skS.0 0 a) % 148.62/148.87 (skS.0 0 a)) % 148.62/148.87 True) % 148.62/148.87 (Or (Eq True False) (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) False)))) % 148.62/148.87 Clause #441 (by superposition #[433, 75]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.62/148.87 (Or (Eq True False) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)))) % 148.62/148.87 Clause #444 (by clausification #[441]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.62/148.87 Clause #445 (by eliminate duplicate literals #[444]): ∀ (a a_1 a_2 a_3 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True)) % 148.62/148.87 Clause #448 (by superposition #[445, 20]): ∀ (a a_1 : Iota), % 148.62/148.87 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.62/148.87 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.90 (Or (Eq True False) % 148.68/148.90 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True)))) % 148.68/148.90 Clause #457 (by clausification #[448]): ∀ (a a_1 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.90 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True))) % 148.68/148.90 Clause #458 (by eliminate duplicate literals #[457]): ∀ (a a_1 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False)) % 148.68/148.90 Clause #1882 (by clausification #[439]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) (skS.0 0 a) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True) % 148.68/148.90 (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) False))) % 148.68/148.90 Clause #1885 (by superposition #[1882, 37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) (skS.0 0 a) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True) % 148.68/148.90 (Or (Eq False True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)))) % 148.68/148.90 Clause #1889 (by clausification #[1885]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) (skS.0 0 a) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True) % 148.68/148.90 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.68/148.90 Clause #1890 (by eliminate duplicate literals #[1889]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) (skS.0 0 a) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True)) % 148.68/148.90 Clause #1891 (by superposition #[1890, 458]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.90 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.90 True) % 148.68/148.90 (Eq True False)))) % 148.68/148.90 Clause #2689 (by clausification #[1891]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5) % 148.68/148.90 (skS.0 0 a)) % 148.68/148.90 True) % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.90 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.90 True))) % 148.68/148.90 Clause #2692 (by superposition #[2689, 33]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.90 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.90 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.90 (Or % 148.68/148.90 (Eq % 148.68/148.90 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.90 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True) % 148.68/148.92 (Or (Eq True False) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) False) % 148.68/148.92 (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True))))) % 148.68/148.92 Clause #3203 (by clausification #[2692]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or % 148.68/148.92 (Eq % 148.68/148.92 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.92 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) False) % 148.68/148.92 (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True)))) % 148.68/148.92 Clause #3204 (by eliminate duplicate literals #[3203]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or % 148.68/148.92 (Eq % 148.68/148.92 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.92 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True) % 148.68/148.92 (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) False))) % 148.68/148.92 Clause #3210 (by superposition #[3204, 37]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or % 148.68/148.92 (Eq % 148.68/148.92 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.92 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True) % 148.68/148.92 (Or (Eq False True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)))) % 148.68/148.92 Clause #3217 (by clausification #[3210]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or % 148.68/148.92 (Eq % 148.68/148.92 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.92 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True) % 148.68/148.92 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.68/148.92 Clause #3218 (by eliminate duplicate literals #[3217]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Eq % 148.68/148.92 (big_f (skS.0 0 a) (skS.0 0 a) % 148.68/148.92 (skS.0 1 (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) a_4 a_5)) % 148.68/148.92 True)) % 148.68/148.92 Clause #3221 (by superposition #[3218, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or (Eq True False) % 148.68/148.92 (Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) False) % 148.68/148.92 (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True)))) % 148.68/148.92 Clause #3235 (by clausification #[3221]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) False) % 148.68/148.92 (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True))) % 148.68/148.92 Clause #3236 (by eliminate duplicate literals #[3235]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.92 (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) False)) % 148.68/148.92 Clause #3238 (by superposition #[3236, 433]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.92 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.92 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq False True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.95 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)))) % 148.68/148.95 Clause #3250 (by clausification #[3238]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.95 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.68/148.95 Clause #3251 (by eliminate duplicate literals #[3250]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.95 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 Clause #3253 (by superposition #[3251, 19]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq True False) % 148.68/148.95 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.68/148.95 Clause #3269 (by clausification #[3253]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)) % 148.68/148.95 Clause #3270 (by eliminate duplicate literals #[3269]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) % 148.68/148.95 Clause #3271 (by superposition #[3270, 153]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) True) (Eq False True))) % 148.68/148.95 Clause #3349 (by clausification #[3271]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.95 (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) True)) % 148.68/148.95 Clause #3350 (by eliminate duplicate literals #[3349]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a)) True) % 148.68/148.95 (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.95 Clause #3354 (by superposition #[3350, 32]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.68/148.95 (Or (Eq True False) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False) (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True))) % 148.68/148.95 Clause #3372 (by clausification #[3354]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False) (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True)) % 148.68/148.95 Clause #3373 (by eliminate duplicate literals #[3372]): ∀ (a a_1 : Iota), Or (Eq (big_f a (skS.0 0 a_1) (skS.0 0 a_1)) True) (Eq (big_f (skS.0 0 a_1) a (skS.0 0 a_1)) False) % 148.68/148.95 Clause #3379 (by superposition #[3373, 37]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq False True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)) % 148.68/148.95 Clause #3384 (by clausification #[3379]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3) (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.95 (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 Clause #3394 (by superposition #[3384, 75]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq True False) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True))) % 148.68/148.95 Clause #3397 (by clausification #[3394]): ∀ (a a_1 : Iota), % 148.68/148.95 Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) % 148.68/148.95 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True)) % 148.68/148.95 Clause #3398 (by eliminate duplicate literals #[3397]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) True) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.95 Clause #3400 (by superposition #[3398, 3373]): ∀ (a a_1 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) True) (Eq True False)) % 148.68/148.98 Clause #3402 (by superposition #[3398, 33]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.98 (Or (Eq True False) % 148.68/148.98 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True))) % 148.68/148.98 Clause #3432 (by clausification #[3400]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) True) % 148.68/148.98 Clause #3571 (by clausification #[3402]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.98 (Or (Eq (big_f (skS.0 0 a) a_1 (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True)) % 148.68/148.98 Clause #3579 (by superposition #[3571, 3398]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.98 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.98 (Or (Eq False True) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True))) % 148.68/148.98 Clause #3587 (by clausification #[3579]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.98 (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True)) % 148.68/148.98 Clause #3588 (by eliminate duplicate literals #[3587]): ∀ (a a_1 a_2 a_3 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) (skS.0 1 (skS.0 0 a) (skS.0 0 a) a_1 a_2 a_3)) True) % 148.68/148.98 (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.98 Clause #3591 (by superposition #[3588, 20]): ∀ (a a_1 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.98 (Or (Eq True False) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True))) % 148.68/148.98 Clause #3605 (by clausification #[3591]): ∀ (a a_1 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True)) % 148.68/148.98 Clause #3606 (by eliminate duplicate literals #[3605]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f a_1 (skS.0 0 a) (skS.0 0 a)) False) % 148.68/148.98 Clause #3611 (by superposition #[3606, 3432]): ∀ (a a_1 : Iota), % 148.68/148.98 Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq False True)) % 148.68/148.98 Clause #3622 (by clausification #[3611]): ∀ (a a_1 : Iota), Or (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) (Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True) % 148.68/148.98 Clause #3623 (by eliminate duplicate literals #[3622]): ∀ (a a_1 : Iota), Eq (big_f (skS.0 0 a) (skS.0 0 a) a_1) True % 148.68/148.98 Clause #3629 (by superposition #[3623, 44]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) % 148.68/148.98 (Or (Eq True False) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) True) (Eq (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) True))) % 148.68/148.98 Clause #3940 (by clausification #[3629]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) True) (Eq (big_f (skS.0 1 a_1 a_2 a a_3 a_4) a_2 a_1) True)) % 148.68/148.98 Clause #3954 (by superposition #[3940, 63]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) True) % 148.68/148.98 (Or (Eq True False) (Or (Eq (big_f a_1 a_2 a) True) (Eq (big_f a a_1 a_2) True)))) % 148.68/148.98 Clause #3966 (by clausification #[3954]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) % 148.68/148.98 (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) True) % 148.68/148.98 (Or (Eq (big_f a_1 a_2 a) True) (Eq (big_f a a_1 a_2) True))) % 148.68/148.98 Clause #3967 (by eliminate duplicate literals #[3966]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) (Or (Eq (big_f a_1 (skS.0 1 a_1 a_2 a a_3 a_4) a_2) True) (Eq (big_f a_1 a_2 a) True)) % 148.68/148.98 Clause #3981 (by superposition #[3967, 33]): ∀ (a a_1 a_2 : Iota), % 148.68/148.98 Or (Eq (big_f a a_1 a_2) True) % 148.68/148.98 (Or (Eq (big_f a_1 a_2 a) True) (Or (Eq True False) (Or (Eq (big_f a_2 a a_1) False) (Eq (big_f a_1 a_2 a) True)))) % 148.80/149.00 Clause #4005 (by clausification #[3981]): ∀ (a a_1 a_2 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 a_2) True) % 148.80/149.00 (Or (Eq (big_f a_1 a_2 a) True) (Or (Eq (big_f a_2 a a_1) False) (Eq (big_f a_1 a_2 a) True))) % 148.80/149.00 Clause #4006 (by eliminate duplicate literals #[4005]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Or (Eq (big_f a_1 a_2 a) True) (Eq (big_f a_2 a a_1) False)) % 148.80/149.00 Clause #4091 (by superposition #[4006, 37]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.00 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 a_2 a_3 a_4)) True) (Or (Eq False True) (Eq (big_f a_1 a_2 a) True))) % 148.80/149.00 Clause #4175 (by clausification #[4091]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.00 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 a_2 a_3 a_4)) True) (Eq (big_f a_1 a_2 a) True)) % 148.80/149.00 Clause #4189 (by superposition #[4175, 68]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1 a) True) % 148.80/149.00 (Or (Eq True False) (Eq (big_f a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a) False)))) % 148.80/149.00 Clause #4757 (by clausification #[4189]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1 a) True) % 148.80/149.00 (Eq (big_f a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a) False))) % 148.80/149.00 Clause #4774 (by superposition #[4757, 37]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1 a) True) % 148.80/149.00 (Or (Eq False True) (Eq (big_f a a_2 a_1) True)))) % 148.80/149.00 Clause #4791 (by clausification #[4774]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1 a) True) (Eq (big_f a a_2 a_1) True))) % 148.80/149.00 Clause #4792 (by eliminate duplicate literals #[4791]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) (Eq (big_f (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1 a) True)) % 148.80/149.00 Clause #4804 (by superposition #[4792, 4006]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.00 (Or (Eq (big_f a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1) True) (Eq True False)))) % 148.80/149.00 Clause #5303 (by clausification #[4804]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.00 (Eq (big_f a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6) a_1) True))) % 148.80/149.00 Clause #5321 (by superposition #[5303, 33]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.00 (Or (Eq True False) % 148.80/149.00 (Or (Eq (big_f a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a) False) % 148.80/149.00 (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True))))) % 148.80/149.00 Clause #5640 (by clausification #[5321]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.00 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.00 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.00 (Or (Eq (big_f a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a) False) (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True)))) % 148.80/149.00 Clause #5641 (by eliminate duplicate literals #[5640]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.00 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.02 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.02 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.02 (Eq (big_f a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a) False))) % 148.80/149.02 Clause #5660 (by superposition #[5641, 37]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.02 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.02 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.02 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) % 148.80/149.02 (Or (Eq False True) (Eq (big_f a a_2 a_1) True)))) % 148.80/149.02 Clause #5680 (by clausification #[5660]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.02 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.02 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.02 (Or (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True) (Eq (big_f a a_2 a_1) True))) % 148.80/149.02 Clause #5681 (by eliminate duplicate literals #[5680]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 148.80/149.02 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.02 (Or (Eq (big_f a a_2 a_1) True) (Eq (big_f a_1 a (skS.0 1 a a_1 (skS.0 1 a_1 a a_2 a_3 a_4) a_5 a_6)) True)) % 148.80/149.03 Clause #5686 (by superposition #[5681, 20]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.03 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.03 (Or (Eq True False) % 148.80/149.03 (Or (Eq (big_f (skS.0 1 a_1 a a_2 a_3 a_4) a a_1) False) (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True)))) % 148.80/149.03 Clause #5714 (by clausification #[5686]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.03 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.03 (Or (Eq (big_f (skS.0 1 a_1 a a_2 a_3 a_4) a a_1) False) (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True))) % 148.80/149.03 Clause #5715 (by eliminate duplicate literals #[5714]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.03 (Or (Eq (big_f a a_2 a_1) True) (Eq (big_f (skS.0 1 a_1 a a_2 a_3 a_4) a a_1) False)) % 148.80/149.03 Clause #5799 (by superposition #[5715, 4175]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.03 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.03 (Or (Eq False True) (Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) (Eq (big_f a a_2 a_1) True)))) % 148.80/149.03 Clause #5806 (by clausification #[5799]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) % 148.80/149.03 (Or (Eq (big_f a a_2 a_1) True) % 148.80/149.03 (Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) (Eq (big_f a a_2 a_1) True))) % 148.80/149.03 Clause #5807 (by eliminate duplicate literals #[5806]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (big_f a a_1 (skS.0 1 a_1 a a_2 a_3 a_4)) True) (Eq (big_f a a_2 a_1) True) % 148.80/149.03 Clause #5820 (by superposition #[5807, 19]): ∀ (a a_1 a_2 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 a_2) True) (Or (Eq True False) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a a_1 a_2) True))) % 148.80/149.03 Clause #5842 (by clausification #[5820]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a a_1 a_2) True)) % 148.80/149.03 Clause #5843 (by eliminate duplicate literals #[5842]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Eq (big_f a_1 a_2 a) False) % 148.80/149.03 Clause #5951 (by superposition #[5843, 5807]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 148.80/149.03 Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) (Or (Eq False True) (Eq (big_f a_1 a_2 a) True)) % 148.80/149.03 Clause #6000 (by clausification #[5951]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (big_f (skS.0 1 a a_1 a_2 a_3 a_4) a_1 a) True) (Eq (big_f a_1 a_2 a) True) % 148.80/149.03 Clause #6020 (by superposition #[6000, 75]): ∀ (a a_1 a_2 : Iota), % 148.80/149.03 Or (Eq (big_f a a_1 a_2) True) (Or (Eq True False) (Or (Eq (big_f a_2 a a_1) True) (Eq (big_f a a_1 a_2) True))) % 148.80/149.03 Clause #6025 (by clausification #[6020]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Or (Eq (big_f a_2 a a_1) True) (Eq (big_f a a_1 a_2) True)) % 148.80/149.03 Clause #6026 (by eliminate duplicate literals #[6025]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Eq (big_f a_2 a a_1) True) % 148.80/149.03 Clause #6071 (by superposition #[6026, 5843]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Or (Eq (big_f a a_1 a_2) True) (Eq True False)) % 148.84/149.12 Clause #6103 (by equality factoring #[6026]): ∀ (a : Iota), Or (Ne True True) (Eq (big_f a a a) True) % 148.84/149.12 Clause #6105 (by clausification #[6103]): ∀ (a : Iota), Or (Eq (big_f a a a) True) (Or (Eq True False) (Eq True False)) % 148.84/149.12 Clause #6107 (by clausification #[6105]): ∀ (a : Iota), Or (Eq (big_f a a a) True) (Eq True False) % 148.84/149.12 Clause #6108 (by clausification #[6107]): ∀ (a : Iota), Eq (big_f a a a) True % 148.84/149.12 Clause #6109 (by superposition #[6108, 115]): ∀ (a a_1 a_2 : Iota), % 148.84/149.12 Or (Eq True False) (Or (Eq (big_f a a_1 a_2) False) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a_2 a a_1) False))) % 148.84/149.12 Clause #6115 (by clausification #[6071]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) True) (Eq (big_f a a_1 a_2) True) % 148.84/149.12 Clause #6116 (by eliminate duplicate literals #[6115]): ∀ (a a_1 a_2 : Iota), Eq (big_f a a_1 a_2) True % 148.84/149.12 Clause #6241 (by clausification #[6109]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) False) (Or (Eq (big_f a_1 a_2 a) False) (Eq (big_f a_2 a a_1) False)) % 148.84/149.12 Clause #6242 (by superposition #[6241, 6116]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) False) (Or (Eq (big_f a_1 a_2 a) False) (Eq False True)) % 148.84/149.12 Clause #6243 (by clausification #[6242]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) False) (Eq (big_f a_1 a_2 a) False) % 148.84/149.12 Clause #6244 (by superposition #[6243, 6116]): ∀ (a a_1 a_2 : Iota), Or (Eq (big_f a a_1 a_2) False) (Eq False True) % 148.84/149.12 Clause #6245 (by clausification #[6244]): ∀ (a a_1 a_2 : Iota), Eq (big_f a a_1 a_2) False % 148.84/149.12 Clause #6246 (by superposition #[6245, 6116]): Eq False True % 148.84/149.12 Clause #6247 (by clausification #[6246]): False % 148.84/149.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------