%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO248^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n017.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:08:48 PM UTC 2025 % Result : Theorem 4.85s 5.03s % Output : Proof 5.08s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYO248^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.14 % Command : duper %s % 0.14/0.35 % Computer : n017.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 14:13:38 EDT 2025 % 0.14/0.35 % CPUTime : % 4.85/5.03 SZS status Theorem for theBenchmark.p % 4.85/5.03 SZS output start Proof for theBenchmark.p % 4.85/5.03 Clause #0 (by assumption #[]): Eq % 4.85/5.03 (Not % 4.85/5.03 (∀ (P : Iota → Iota → Prop), % 4.85/5.03 And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And (And (And (Eq (P a) (P aa)) (Eq (P b) (P bb))) (Eq (P e) (P hh)) → Eq (P c) (P dd)) % 4.85/5.03 (And (And (Eq (P a) (P aa)) (Eq (P h) (P hh))) (Eq (P b) (P cc)) → Ne (P d) (P ee))) % 4.85/5.03 (And (And (And (Eq (P c) (P cc)) (Eq (P cc) (P d))) (Eq (P d) (P dd))) (Ne (P a) (P bb)) → % 4.85/5.03 Ne (P e) (P hh))) % 4.85/5.03 (And (And (Eq (P a) (P aa)) (Eq (P d) (P dd))) (Ne (P b) (P cc)) → Eq (P e) (P hh))) % 4.85/5.03 (And (And (Eq (P e) (P ee)) (Eq (P h) (P hh))) (Eq (P c) (P dd)) → Ne (P a) (P bb))) % 4.85/5.03 (And (And (And (Eq (P b) (P bb)) (Eq (P bb) (P c))) (Eq (P c) (P cc))) (Ne (P e) (P hh)) → Eq (P d) (P ee)) → % 4.85/5.03 Or (Or (Or (Or (Or (Ne (P a) (P aa)) (Ne (P b) (P bb))) (Ne (P c) (P cc))) (Ne (P d) (P dd))) (Ne (P e) (P ee))) % 4.85/5.03 (Ne (P h) (P hh)))) % 4.85/5.03 True % 4.85/5.03 Clause #1 (by clausification #[0]): Eq % 4.85/5.03 (∀ (P : Iota → Iota → Prop), % 4.85/5.03 And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And (And (And (Eq (P a) (P aa)) (Eq (P b) (P bb))) (Eq (P e) (P hh)) → Eq (P c) (P dd)) % 4.85/5.03 (And (And (Eq (P a) (P aa)) (Eq (P h) (P hh))) (Eq (P b) (P cc)) → Ne (P d) (P ee))) % 4.85/5.03 (And (And (And (Eq (P c) (P cc)) (Eq (P cc) (P d))) (Eq (P d) (P dd))) (Ne (P a) (P bb)) → % 4.85/5.03 Ne (P e) (P hh))) % 4.85/5.03 (And (And (Eq (P a) (P aa)) (Eq (P d) (P dd))) (Ne (P b) (P cc)) → Eq (P e) (P hh))) % 4.85/5.03 (And (And (Eq (P e) (P ee)) (Eq (P h) (P hh))) (Eq (P c) (P dd)) → Ne (P a) (P bb))) % 4.85/5.03 (And (And (And (Eq (P b) (P bb)) (Eq (P bb) (P c))) (Eq (P c) (P cc))) (Ne (P e) (P hh)) → Eq (P d) (P ee)) → % 4.85/5.03 Or (Or (Or (Or (Or (Ne (P a) (P aa)) (Ne (P b) (P bb))) (Ne (P c) (P cc))) (Ne (P d) (P dd))) (Ne (P e) (P ee))) % 4.85/5.03 (Ne (P h) (P hh))) % 4.85/5.03 False % 4.85/5.03 Clause #2 (by clausification #[1]): ∀ (a_1 : Iota → Iota → Prop), % 4.85/5.03 Eq % 4.85/5.03 (Not % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.03 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.03 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.03 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.03 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.85/5.03 (And % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.85/5.03 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.03 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.85/5.03 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.03 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.03 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.03 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) → % 4.85/5.03 Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.85/5.03 (And % 4.85/5.03 (And (And (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) (Eq (skS.0 0 a_1 bb) (skS.0 0 a_1 c))) % 4.85/5.03 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.03 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.03 Eq (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) → % 4.85/5.03 Or % 4.85/5.03 (Or % 4.85/5.03 (Or % 4.85/5.03 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.03 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.03 (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.03 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee))) % 4.85/5.03 (Ne (skS.0 0 a_1 h) (skS.0 0 a_1 hh)))) % 4.85/5.03 True % 4.85/5.03 Clause #3 (by clausification #[2]): ∀ (a_1 : Iota → Iota → Prop), % 4.85/5.03 Eq % 4.85/5.03 (And % 4.85/5.03 (And % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.06 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.06 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.06 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.85/5.06 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.85/5.06 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.06 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) → % 4.85/5.06 Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) (Eq (skS.0 0 a_1 bb) (skS.0 0 a_1 c))) % 4.85/5.06 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.06 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.06 Eq (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) → % 4.85/5.06 Or % 4.85/5.06 (Or % 4.85/5.06 (Or % 4.85/5.06 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.06 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.06 (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee))) % 4.85/5.06 (Ne (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 False % 4.85/5.06 Clause #4 (by clausification #[3]): ∀ (a_1 : Iota → Iota → Prop), % 4.85/5.06 Eq % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.06 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.06 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.06 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.85/5.06 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.85/5.06 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.85/5.06 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) → % 4.85/5.06 Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) (Eq (skS.0 0 a_1 bb) (skS.0 0 a_1 c))) % 4.85/5.06 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.06 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.85/5.06 Eq (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.85/5.06 True % 4.85/5.06 Clause #5 (by clausification #[3]): ∀ (a_1 : Iota → Iota → Prop), % 4.85/5.06 Eq % 4.85/5.06 (Or % 4.85/5.06 (Or % 4.85/5.06 (Or % 4.85/5.06 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.85/5.06 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 4.85/5.06 (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.85/5.06 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee))) % 4.85/5.06 (Ne (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.85/5.06 False % 4.85/5.06 Clause #6 (by clausification #[4]): ∀ (a : Iota → Iota → Prop), % 4.85/5.06 Eq % 4.85/5.06 (And % 4.85/5.06 (And (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) % 4.85/5.06 (Eq (skS.0 0 a c) (skS.0 0 a cc))) % 4.85/5.06 (Ne (skS.0 0 a e) (skS.0 0 a hh)) → % 4.85/5.06 Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.85/5.06 True % 4.85/5.06 Clause #7 (by clausification #[4]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.08 Eq % 4.92/5.08 (And % 4.92/5.08 (And % 4.92/5.08 (And % 4.92/5.08 (And % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.92/5.08 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.92/5.08 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.08 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.08 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.92/5.08 (And % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.08 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.08 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.92/5.08 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.08 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.08 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.08 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) → % 4.92/5.08 Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.92/5.08 True % 4.92/5.08 Clause #8 (by clausification #[6]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or % 4.92/5.08 (Eq % 4.92/5.08 (And % 4.92/5.08 (And (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) % 4.92/5.08 (Eq (skS.0 0 a c) (skS.0 0 a cc))) % 4.92/5.08 (Ne (skS.0 0 a e) (skS.0 0 a hh))) % 4.92/5.08 False) % 4.92/5.08 (Eq (Eq (skS.0 0 a d) (skS.0 0 a ee)) True) % 4.92/5.08 Clause #9 (by clausification #[8]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (Eq (skS.0 0 a d) (skS.0 0 a ee)) True) % 4.92/5.08 (Or % 4.92/5.08 (Eq % 4.92/5.08 (And (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) % 4.92/5.08 (Eq (skS.0 0 a c) (skS.0 0 a cc))) % 4.92/5.08 False) % 4.92/5.08 (Eq (Ne (skS.0 0 a e) (skS.0 0 a hh)) False)) % 4.92/5.08 Clause #10 (by clausification #[9]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or % 4.92/5.08 (Eq % 4.92/5.08 (And (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) (Eq (skS.0 0 a c) (skS.0 0 a cc))) % 4.92/5.08 False) % 4.92/5.08 (Or (Eq (Ne (skS.0 0 a e) (skS.0 0 a hh)) False) (Eq (skS.0 0 a d) (skS.0 0 a ee))) % 4.92/5.08 Clause #11 (by clausification #[10]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (Ne (skS.0 0 a e) (skS.0 0 a hh)) False) % 4.92/5.08 (Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) False) % 4.92/5.08 (Eq (Eq (skS.0 0 a c) (skS.0 0 a cc)) False))) % 4.92/5.08 Clause #12 (by clausification #[11]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (And (Eq (skS.0 0 a b) (skS.0 0 a bb)) (Eq (skS.0 0 a bb) (skS.0 0 a c))) False) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a c) (skS.0 0 a cc)) False) (Eq (skS.0 0 a e) (skS.0 0 a hh)))) % 4.92/5.08 Clause #13 (by clausification #[12]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a c) (skS.0 0 a cc)) False) % 4.92/5.08 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a b) (skS.0 0 a bb)) False) (Eq (Eq (skS.0 0 a bb) (skS.0 0 a c)) False)))) % 4.92/5.08 Clause #14 (by clausification #[13]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a b) (skS.0 0 a bb)) False) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a bb) (skS.0 0 a c)) False) (Ne (skS.0 0 a c) (skS.0 0 a cc))))) % 4.92/5.08 Clause #15 (by clausification #[14]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) % 4.92/5.08 (Or (Eq (Eq (skS.0 0 a bb) (skS.0 0 a c)) False) % 4.92/5.08 (Or (Ne (skS.0 0 a c) (skS.0 0 a cc)) (Ne (skS.0 0 a b) (skS.0 0 a bb))))) % 4.92/5.08 Clause #16 (by clausification #[15]): ∀ (a : Iota → Iota → Prop), % 4.92/5.08 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 4.92/5.08 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) % 4.92/5.08 (Or (Ne (skS.0 0 a c) (skS.0 0 a cc)) (Or (Ne (skS.0 0 a b) (skS.0 0 a bb)) (Ne (skS.0 0 a bb) (skS.0 0 a c))))) % 4.92/5.08 Clause #17 (by clausification #[7]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.08 Eq % 4.92/5.08 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.11 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) → % 4.92/5.11 Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.11 True % 4.92/5.11 Clause #18 (by clausification #[7]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Eq % 4.92/5.11 (And % 4.92/5.11 (And % 4.92/5.11 (And % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.92/5.11 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.92/5.11 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.11 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.11 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.92/5.11 (And % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.11 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.11 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.92/5.11 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.11 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.11 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.11 True % 4.92/5.11 Clause #19 (by clausification #[17]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or % 4.92/5.11 (Eq % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.11 (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd))) % 4.92/5.11 False) % 4.92/5.11 (Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) True) % 4.92/5.11 Clause #20 (by clausification #[19]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) True) % 4.92/5.11 (Or (Eq (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) False) % 4.92/5.11 (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) False)) % 4.92/5.11 Clause #21 (by clausification #[20]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Eq (And (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) False) % 4.92/5.11 (Or (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) False) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.92/5.11 Clause #22 (by clausification #[21]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) False) % 4.92/5.11 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.11 (Or (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) False) (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False))) % 4.92/5.11 Clause #23 (by clausification #[22]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.11 (Or (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) False) % 4.92/5.11 (Or (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False) (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)))) % 4.92/5.11 Clause #24 (by clausification #[23]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.11 (Or (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False) % 4.92/5.11 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee)))) % 4.92/5.11 Clause #25 (by clausification #[24]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.11 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.11 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee)) (Ne (skS.0 0 a_1 h) (skS.0 0 a_1 hh)))) % 4.92/5.11 Clause #26 (by clausification #[18]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Eq % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.11 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.11 Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.11 True % 4.92/5.11 Clause #27 (by clausification #[18]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.11 Eq % 4.92/5.11 (And % 4.92/5.11 (And % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.92/5.11 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.92/5.11 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.11 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.11 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.92/5.11 (And % 4.92/5.11 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.11 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.11 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.92/5.11 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.11 True % 4.92/5.11 Clause #28 (by clausification #[26]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or % 4.92/5.14 (Eq % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.14 (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc))) % 4.92/5.14 False) % 4.92/5.14 (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) True) % 4.92/5.14 Clause #29 (by clausification #[28]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) True) % 4.92/5.14 (Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) False) % 4.92/5.14 (Eq (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False)) % 4.92/5.14 Clause #30 (by clausification #[29]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) False) % 4.92/5.14 (Or (Eq (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False) (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.14 Clause #31 (by clausification #[30]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False) % 4.92/5.14 (Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False))) % 4.92/5.14 Clause #32 (by clausification #[31]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) % 4.92/5.14 (Or (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)))) % 4.92/5.14 Clause #33 (by clausification #[32]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 (Or (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False) % 4.92/5.14 (Or (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)))) % 4.92/5.14 Clause #34 (by clausification #[33]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 (Or (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) % 4.92/5.14 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd)))) % 4.92/5.14 Clause #35 (by clausification #[27]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Eq % 4.92/5.14 (And % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.14 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.14 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) → % 4.92/5.14 Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 True % 4.92/5.14 Clause #36 (by clausification #[27]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Eq % 4.92/5.14 (And % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.92/5.14 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.92/5.14 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.14 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.14 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.92/5.14 True % 4.92/5.14 Clause #37 (by clausification #[35]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or % 4.92/5.14 (Eq % 4.92/5.14 (And % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.14 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.14 (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb))) % 4.92/5.14 False) % 4.92/5.14 (Eq (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) True) % 4.92/5.14 Clause #38 (by clausification #[37]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) True) % 4.92/5.14 (Or % 4.92/5.14 (Eq % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.14 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.14 False) % 4.92/5.14 (Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) False)) % 4.92/5.14 Clause #39 (by clausification #[38]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or % 4.92/5.14 (Eq % 4.92/5.14 (And (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 4.92/5.14 (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 4.92/5.14 False) % 4.92/5.14 (Or (Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) False) (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 4.92/5.14 Clause #40 (by clausification #[39]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.14 Or (Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) False) % 4.92/5.14 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.14 (Or (Eq (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) False) % 4.92/5.14 (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False))) % 4.92/5.14 Clause #41 (by clausification #[40]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.17 (Or (Eq (And (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) False) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False) (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)))) % 4.92/5.17 Clause #42 (by clausification #[41]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) False) % 4.92/5.17 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) False) (Eq (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d)) False)))) % 4.92/5.17 Clause #43 (by clausification #[42]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.17 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) False) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d)) False) (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))))) % 4.92/5.17 Clause #44 (by clausification #[43]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.17 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 cc) (skS.0 0 a_1 d)) False) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))))) % 4.92/5.17 Clause #45 (by clausification #[44]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 4.92/5.17 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd)) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 cc) (skS.0 0 a_1 d))))) % 4.92/5.17 Clause #46 (by clausification #[36]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Eq % 4.92/5.17 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.17 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) → % 4.92/5.17 Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 4.92/5.17 True % 4.92/5.17 Clause #47 (by clausification #[36]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Eq % 4.92/5.17 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 4.92/5.17 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) → % 4.92/5.17 Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 4.92/5.17 True % 4.92/5.17 Clause #48 (by clausification #[46]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or % 4.92/5.17 (Eq % 4.92/5.17 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) % 4.92/5.17 (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc))) % 4.92/5.17 False) % 4.92/5.17 (Eq (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) True) % 4.92/5.17 Clause #49 (by clausification #[48]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Eq (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) True) % 4.92/5.17 (Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) False) % 4.92/5.17 (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False)) % 4.92/5.17 Clause #50 (by clausification #[49]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh))) False) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False) (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee))) % 4.92/5.17 Clause #51 (by clausification #[50]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) False) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False))) % 4.92/5.17 Clause #52 (by clausification #[51]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)))) % 4.92/5.17 Clause #53 (by clausification #[52]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 4.92/5.17 (Or (Eq (Eq (skS.0 0 a_1 h) (skS.0 0 a_1 hh)) False) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)))) % 4.92/5.17 Clause #54 (by clausification #[53]): ∀ (a_1 : Iota → Iota → Prop), % 4.92/5.17 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) % 4.92/5.17 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 h) (skS.0 0 a_1 hh)))) % 4.92/5.17 Clause #55 (by clausification #[5]): ∀ (a : Iota → Iota → Prop), Eq (Ne (skS.0 0 a h) (skS.0 0 a hh)) False % 5.03/5.20 Clause #56 (by clausification #[5]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Eq % 5.03/5.20 (Or % 5.03/5.20 (Or % 5.03/5.20 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 5.03/5.20 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 5.03/5.20 (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 5.03/5.20 (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee))) % 5.03/5.20 False % 5.03/5.20 Clause #57 (by clausification #[55]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a h) (skS.0 0 a hh) % 5.03/5.20 Clause #60 (by backward contextual literal cutting #[57, 25]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 ee))) % 5.03/5.20 Clause #61 (by backward contextual literal cutting #[57, 54]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 ee)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.03/5.20 Clause #66 (by clausification #[47]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or % 5.03/5.20 (Eq % 5.03/5.20 (And (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 5.03/5.20 (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh))) % 5.03/5.20 False) % 5.03/5.20 (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) True) % 5.03/5.20 Clause #67 (by clausification #[66]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) True) % 5.03/5.20 (Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) False) % 5.03/5.20 (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) False)) % 5.03/5.20 Clause #68 (by clausification #[67]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (And (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) False) % 5.03/5.20 (Or (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) False) (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd))) % 5.03/5.20 Clause #69 (by clausification #[68]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) False) % 5.03/5.20 (Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 5.03/5.20 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) False))) % 5.03/5.20 Clause #70 (by clausification #[69]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 5.03/5.20 (Or (Eq (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False) % 5.03/5.20 (Or (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) False) (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)))) % 5.03/5.20 Clause #71 (by clausification #[70]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 5.03/5.20 (Or (Eq (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 bb)) False) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)))) % 5.03/5.20 Clause #72 (by clausification #[71]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb)))) % 5.03/5.20 Clause #74 (by clausification #[56]): ∀ (a : Iota → Iota → Prop), Eq (Ne (skS.0 0 a e) (skS.0 0 a ee)) False % 5.03/5.20 Clause #75 (by clausification #[56]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Eq % 5.03/5.20 (Or % 5.03/5.20 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 5.03/5.20 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 5.03/5.20 (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 dd))) % 5.03/5.20 False % 5.03/5.20 Clause #76 (by clausification #[74]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a e) (skS.0 0 a ee) % 5.03/5.20 Clause #82 (by forward demodulation #[61, 76]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 e)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.03/5.20 Clause #83 (by forward demodulation #[60, 76]): ∀ (a_1 : Iota → Iota → Prop), % 5.03/5.20 Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 5.03/5.20 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 e))) % 5.03/5.20 Clause #84 (by eliminate resolved literals #[83]): ∀ (a_1 : Iota → Iota → Prop), Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 dd)) % 5.03/5.20 Clause #85 (by clausification #[75]): ∀ (a : Iota → Iota → Prop), Eq (Ne (skS.0 0 a d) (skS.0 0 a dd)) False % 5.03/5.20 Clause #86 (by clausification #[75]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Eq % 5.06/5.23 (Or (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) % 5.06/5.23 (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc))) % 5.06/5.23 False % 5.06/5.23 Clause #87 (by clausification #[85]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a d) (skS.0 0 a dd) % 5.06/5.23 Clause #90 (by backward demodulation #[87, 72]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 d)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb)))) % 5.06/5.23 Clause #91 (by backward demodulation #[87, 84]): ∀ (a_1 : Iota → Iota → Prop), Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 d)) % 5.06/5.23 Clause #92 (by backward contextual literal cutting #[87, 34]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.06/5.23 Clause #93 (by backward contextual literal cutting #[87, 45]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 cc)) (Ne (skS.0 0 a_1 cc) (skS.0 0 a_1 d)))) % 5.06/5.23 Clause #98 (by clausification #[86]): ∀ (a : Iota → Iota → Prop), Eq (Ne (skS.0 0 a c) (skS.0 0 a cc)) False % 5.06/5.23 Clause #99 (by clausification #[86]): ∀ (a_1 : Iota → Iota → Prop), Eq (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb))) False % 5.06/5.23 Clause #100 (by clausification #[98]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a c) (skS.0 0 a cc) % 5.06/5.23 Clause #102 (by backward demodulation #[100, 82]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 e)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.06/5.23 Clause #103 (by backward contextual literal cutting #[100, 16]): ∀ (a : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 5.06/5.23 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) (Or (Ne (skS.0 0 a b) (skS.0 0 a bb)) (Ne (skS.0 0 a bb) (skS.0 0 a c)))) % 5.06/5.23 Clause #110 (by forward demodulation #[92, 100]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 b) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.06/5.23 Clause #111 (by clausification #[99]): ∀ (a : Iota → Iota → Prop), Eq (Ne (skS.0 0 a b) (skS.0 0 a bb)) False % 5.06/5.23 Clause #112 (by clausification #[99]): ∀ (a_1 : Iota → Iota → Prop), Eq (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa)) False % 5.06/5.23 Clause #113 (by clausification #[111]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a b) (skS.0 0 a bb) % 5.06/5.23 Clause #114 (by backward demodulation #[113, 110]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 bb) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.06/5.23 Clause #119 (by forward demodulation #[93, 100]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 cc) (skS.0 0 a_1 d)))) % 5.06/5.23 Clause #120 (by eliminate resolved literals #[119]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) (Ne (skS.0 0 a_1 cc) (skS.0 0 a_1 d))) % 5.06/5.23 Clause #121 (by forward demodulation #[120, 100]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Eq (skS.0 0 a_1 a) (skS.0 0 a_1 bb)) (Ne (skS.0 0 a_1 c) (skS.0 0 a_1 d))) % 5.06/5.23 Clause #122 (by forward contextual literal cutting #[121, 91]): ∀ (a : Iota → Iota → Prop), Or (Ne (skS.0 0 a e) (skS.0 0 a hh)) (Ne (skS.0 0 a c) (skS.0 0 a d)) % 5.06/5.23 Clause #123 (by clausification #[112]): ∀ (a_1 : Iota → Iota → Prop), Eq (skS.0 0 a_1 a) (skS.0 0 a_1 aa) % 5.06/5.23 Clause #129 (by forward demodulation #[90, 123]): ∀ (a_1 : Iota → Iota → Prop), % 5.06/5.23 Or (Eq (skS.0 0 a_1 c) (skS.0 0 a_1 d)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.06/5.23 (Or (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 a)) (Ne (skS.0 0 a_1 b) (skS.0 0 a_1 bb)))) % 5.06/5.23 Clause #130 (by eliminate resolved literals #[129]): ∀ (a : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a c) (skS.0 0 a d)) (Or (Ne (skS.0 0 a e) (skS.0 0 a hh)) (Ne (skS.0 0 a b) (skS.0 0 a bb))) % 5.08/5.24 Clause #131 (by forward demodulation #[130, 113]): ∀ (a : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a c) (skS.0 0 a d)) (Or (Ne (skS.0 0 a e) (skS.0 0 a hh)) (Ne (skS.0 0 a bb) (skS.0 0 a bb))) % 5.08/5.24 Clause #132 (by eliminate resolved literals #[131]): ∀ (a : Iota → Iota → Prop), Or (Eq (skS.0 0 a c) (skS.0 0 a d)) (Ne (skS.0 0 a e) (skS.0 0 a hh)) % 5.08/5.24 Clause #133 (by forward contextual literal cutting #[132, 122]): ∀ (a : Iota → Iota → Prop), Ne (skS.0 0 a e) (skS.0 0 a hh) % 5.08/5.24 Clause #135 (by forward demodulation #[102, 113]): ∀ (a_1 : Iota → Iota → Prop), % 5.08/5.24 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 e)) % 5.08/5.24 (Or (Ne (skS.0 0 a_1 bb) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 aa))) % 5.08/5.24 Clause #136 (by forward demodulation #[135, 123]): ∀ (a_1 : Iota → Iota → Prop), % 5.08/5.24 Or (Ne (skS.0 0 a_1 d) (skS.0 0 a_1 e)) % 5.08/5.24 (Or (Ne (skS.0 0 a_1 bb) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 a))) % 5.08/5.24 Clause #137 (by eliminate resolved literals #[136]): ∀ (a : Iota → Iota → Prop), Or (Ne (skS.0 0 a d) (skS.0 0 a e)) (Ne (skS.0 0 a bb) (skS.0 0 a c)) % 5.08/5.24 Clause #138 (by forward demodulation #[114, 123]): ∀ (a_1 : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a_1 e) (skS.0 0 a_1 hh)) % 5.08/5.24 (Or (Eq (skS.0 0 a_1 bb) (skS.0 0 a_1 c)) (Ne (skS.0 0 a_1 a) (skS.0 0 a_1 a))) % 5.08/5.24 Clause #139 (by eliminate resolved literals #[138]): ∀ (a : Iota → Iota → Prop), Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) (Eq (skS.0 0 a bb) (skS.0 0 a c)) % 5.08/5.24 Clause #140 (by forward contextual literal cutting #[139, 133]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a bb) (skS.0 0 a c) % 5.08/5.24 Clause #144 (by backward contextual literal cutting #[140, 137]): ∀ (a : Iota → Iota → Prop), Ne (skS.0 0 a d) (skS.0 0 a e) % 5.08/5.24 Clause #147 (by forward demodulation #[103, 113]): ∀ (a : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) % 5.08/5.24 (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) (Or (Ne (skS.0 0 a bb) (skS.0 0 a bb)) (Ne (skS.0 0 a bb) (skS.0 0 a c)))) % 5.08/5.24 Clause #148 (by eliminate resolved literals #[147]): ∀ (a : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) (Ne (skS.0 0 a bb) (skS.0 0 a c))) % 5.08/5.24 Clause #149 (by forward demodulation #[148, 140]): ∀ (a : Iota → Iota → Prop), % 5.08/5.24 Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) (Or (Eq (skS.0 0 a e) (skS.0 0 a hh)) (Ne (skS.0 0 a bb) (skS.0 0 a bb))) % 5.08/5.24 Clause #150 (by eliminate resolved literals #[149]): ∀ (a : Iota → Iota → Prop), Or (Eq (skS.0 0 a d) (skS.0 0 a ee)) (Eq (skS.0 0 a e) (skS.0 0 a hh)) % 5.08/5.24 Clause #151 (by forward contextual literal cutting #[150, 133]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a d) (skS.0 0 a ee) % 5.08/5.24 Clause #167 (by superposition #[151, 76]): ∀ (a : Iota → Iota → Prop), Eq (skS.0 0 a e) (skS.0 0 a d) % 5.08/5.24 Clause #168 (by forward contextual literal cutting #[167, 144]): False % 5.08/5.24 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------