%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU850^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 08:02:33 PM UTC 2025 % Result : Theorem 19.97s 20.18s % Output : Proof 20.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU850^5 : TPTP v9.2.0. Released v4.0.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n005.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 06:24:23 EDT 2025 % 0.13/0.34 % CPUTime : % 19.97/20.18 SZS status Theorem for theBenchmark.p % 19.97/20.18 SZS output start Proof for theBenchmark.p % 19.97/20.18 Clause #0 (by assumption #[]): Eq % 19.97/20.18 (Not % 19.97/20.18 (∀ (S T U : a → Prop), % 19.97/20.18 And (Eq S T) (Eq T U) → And (And (∀ (Xx : a), S Xx → T Xx) (∀ (Xx : a), T Xx → U Xx)) (∀ (Xx : a), U Xx → S Xx))) % 19.97/20.18 True % 19.97/20.18 Clause #1 (by clausification #[0]): Eq % 19.97/20.18 (∀ (S T U : a → Prop), % 19.97/20.18 And (Eq S T) (Eq T U) → And (And (∀ (Xx : a), S Xx → T Xx) (∀ (Xx : a), T Xx → U Xx)) (∀ (Xx : a), U Xx → S Xx)) % 19.97/20.18 False % 19.97/20.18 Clause #2 (by clausification #[1]): ∀ (a_1 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (Not % 19.97/20.18 (∀ (T U : a → Prop), % 19.97/20.18 And (Eq (skS.0 0 a_1) T) (Eq T U) → % 19.97/20.18 And (And (∀ (Xx : a), skS.0 0 a_1 Xx → T Xx) (∀ (Xx : a), T Xx → U Xx)) (∀ (Xx : a), U Xx → skS.0 0 a_1 Xx))) % 19.97/20.18 True % 19.97/20.18 Clause #3 (by clausification #[2]): ∀ (a_1 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (∀ (T U : a → Prop), % 19.97/20.18 And (Eq (skS.0 0 a_1) T) (Eq T U) → % 19.97/20.18 And (And (∀ (Xx : a), skS.0 0 a_1 Xx → T Xx) (∀ (Xx : a), T Xx → U Xx)) (∀ (Xx : a), U Xx → skS.0 0 a_1 Xx)) % 19.97/20.18 False % 19.97/20.18 Clause #4 (by clausification #[3]): ∀ (a_1 a_2 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (Not % 19.97/20.18 (∀ (U : a → Prop), % 19.97/20.18 And (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) (Eq (skS.0 1 a_1 a_2) U) → % 19.97/20.18 And (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → U Xx)) % 19.97/20.18 (∀ (Xx : a), U Xx → skS.0 0 a_1 Xx))) % 19.97/20.18 True % 19.97/20.18 Clause #5 (by clausification #[4]): ∀ (a_1 a_2 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (∀ (U : a → Prop), % 19.97/20.18 And (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) (Eq (skS.0 1 a_1 a_2) U) → % 19.97/20.18 And (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → U Xx)) % 19.97/20.18 (∀ (Xx : a), U Xx → skS.0 0 a_1 Xx)) % 19.97/20.18 False % 19.97/20.18 Clause #6 (by clausification #[5]): ∀ (a_1 a_2 a_3 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (Not % 19.97/20.18 (And (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) (Eq (skS.0 1 a_1 a_2) (skS.0 2 a_1 a_2 a_3)) → % 19.97/20.18 And % 19.97/20.18 (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) % 19.97/20.18 (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx)) % 19.97/20.18 (∀ (Xx : a), skS.0 2 a_1 a_2 a_3 Xx → skS.0 0 a_1 Xx))) % 19.97/20.18 True % 19.97/20.18 Clause #7 (by clausification #[6]): ∀ (a_1 a_2 a_3 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (And (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) (Eq (skS.0 1 a_1 a_2) (skS.0 2 a_1 a_2 a_3)) → % 19.97/20.18 And % 19.97/20.18 (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) % 19.97/20.18 (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx)) % 19.97/20.18 (∀ (Xx : a), skS.0 2 a_1 a_2 a_3 Xx → skS.0 0 a_1 Xx)) % 19.97/20.18 False % 19.97/20.18 Clause #8 (by clausification #[7]): ∀ (a_1 a_2 a_3 : a → Prop), % 19.97/20.18 Eq (And (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) (Eq (skS.0 1 a_1 a_2) (skS.0 2 a_1 a_2 a_3))) True % 19.97/20.18 Clause #9 (by clausification #[7]): ∀ (a_1 a_2 a_3 : a → Prop), % 19.97/20.18 Eq % 19.97/20.18 (And % 19.97/20.18 (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx)) % 19.97/20.18 (∀ (Xx : a), skS.0 2 a_1 a_2 a_3 Xx → skS.0 0 a_1 Xx)) % 19.97/20.18 False % 19.97/20.18 Clause #10 (by clausification #[8]): ∀ (a_1 a_2 a_3 : a → Prop), Eq (Eq (skS.0 1 a_1 a_2) (skS.0 2 a_1 a_2 a_3)) True % 19.97/20.18 Clause #11 (by clausification #[8]): ∀ (a_1 a_2 : a → Prop), Eq (Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2)) True % 19.97/20.18 Clause #12 (by clausification #[10]): ∀ (a_1 a_2 a_3 : a → Prop), Eq (skS.0 1 a_1 a_2) (skS.0 2 a_1 a_2 a_3) % 19.97/20.18 Clause #14 (by clausification #[11]): ∀ (a_1 a_2 : a → Prop), Eq (skS.0 0 a_1) (skS.0 1 a_1 a_2) % 19.97/20.18 Clause #15 (by backward demodulation #[14, 12]): ∀ (a_1 a_2 a_3 : a → Prop), Eq (skS.0 0 a_1) (skS.0 2 a_1 a_2 a_3) % 19.97/20.18 Clause #16 (by argument congruence #[14]): ∀ (a_1 : a → Prop) (a_2 : a) (a_3 : a → Prop), Eq (skS.0 0 a_1 a_2) (skS.0 1 a_1 a_3 a_2) % 19.97/20.18 Clause #18 (by clausify Prop equality #[16]): ∀ (a_1 : a → Prop) (a_2 : a) (a_3 : a → Prop), Or (Eq (skS.0 0 a_1 a_2) False) (Eq (skS.0 1 a_1 a_3 a_2) True) % 19.97/20.18 Clause #19 (by argument congruence #[15]): ∀ (a_1 : a → Prop) (a_2 : a) (a_3 a_4 : a → Prop), Eq (skS.0 0 a_1 a_2) (skS.0 2 a_1 a_3 a_4 a_2) % 19.97/20.18 Clause #21 (by clausify Prop equality #[19]): ∀ (a_1 : a → Prop) (a_2 : a) (a_3 a_4 : a → Prop), Or (Eq (skS.0 0 a_1 a_2) False) (Eq (skS.0 2 a_1 a_3 a_4 a_2) True) % 20.03/20.20 Clause #22 (by clausification #[9]): ∀ (a_1 a_2 a_3 : a → Prop), % 20.03/20.20 Or % 20.03/20.20 (Eq % 20.03/20.20 (And (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx)) % 20.03/20.20 False) % 20.03/20.20 (Eq (∀ (Xx : a), skS.0 2 a_1 a_2 a_3 Xx → skS.0 0 a_1 Xx) False) % 20.03/20.20 Clause #23 (by clausification #[22]): ∀ (a_1 a_2 a_3 : a → Prop), % 20.03/20.20 Or (Eq (∀ (Xx : a), skS.0 2 a_1 a_2 a_3 Xx → skS.0 0 a_1 Xx) False) % 20.03/20.20 (Or (Eq (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) False) % 20.03/20.20 (Eq (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx) False)) % 20.03/20.20 Clause #24 (by clausification #[23]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), % 20.03/20.20 Or (Eq (∀ (Xx : a), skS.0 0 a_1 Xx → skS.0 1 a_1 a_2 Xx) False) % 20.03/20.20 (Or (Eq (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx) False) % 20.03/20.20 (Eq (Not (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4))) True)) % 20.03/20.20 Clause #25 (by clausification #[24]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.03/20.20 Or (Eq (∀ (Xx : a), skS.0 1 a_1 a_2 Xx → skS.0 2 a_1 a_2 a_3 Xx) False) % 20.03/20.20 (Or (Eq (Not (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4))) True) % 20.03/20.20 (Eq (Not (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5))) True)) % 20.03/20.20 Clause #26 (by clausification #[25]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.20 Or (Eq (Not (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4))) True) % 20.03/20.20 (Or (Eq (Not (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5))) True) % 20.03/20.20 (Eq (Not (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6))) True)) % 20.03/20.20 Clause #27 (by clausification #[26]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.03/20.20 Or (Eq (Not (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3))) True) % 20.03/20.20 (Or (Eq (Not (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5) → skS.0 2 a_1 a_2 a_4 (skS.0 5 a_1 a_2 a_4 a_5))) True) % 20.03/20.20 (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 3 a_1 a_2 a_4 a_6) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_6)) False)) % 20.03/20.20 Clause #28 (by clausification #[27]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.20 Or (Eq (Not (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4))) True) % 20.03/20.20 (Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) False) % 20.03/20.20 (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_6)) False)) % 20.03/20.20 Clause #29 (by clausification #[28]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.20 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4) → skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) False) % 20.03/20.20 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5)) False) % 20.03/20.20 (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.20 Clause #30 (by clausification #[29]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.03/20.20 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) % 20.03/20.20 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5) → skS.0 2 a_1 a_2 a_4 (skS.0 5 a_1 a_2 a_4 a_5)) False) % 20.03/20.20 (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 3 a_1 a_2 a_4 a_6)) True)) % 20.03/20.20 Clause #31 (by clausification #[29]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.03/20.20 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3) → skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) % 20.03/20.20 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5) → skS.0 2 a_1 a_2 a_4 (skS.0 5 a_1 a_2 a_4 a_5)) False) % 20.03/20.20 (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_6)) False)) % 20.03/20.20 Clause #32 (by clausification #[30]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.20 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False) % 20.03/20.20 (Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True)) % 20.03/20.23 Clause #33 (by clausification #[30]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_6)) False)) % 20.03/20.23 Clause #34 (by clausification #[32]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6)) True)) % 20.03/20.23 Clause #35 (by clausification #[32]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.23 Clause #36 (by superposition #[34, 19]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.03/20.23 (Or % 20.03/20.23 (Eq (skS.0 1 (fun x => a_1 x) (fun x => a_2 x) (skS.0 5 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_4 x) a_5)) % 20.03/20.23 True) % 20.03/20.23 (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_6)) True)) % 20.03/20.23 Clause #44 (by superposition #[35, 19]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or % 20.03/20.23 (Eq % 20.03/20.23 (skS.0 2 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_3 x) % 20.03/20.23 (skS.0 3 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_3 x) a_4)) % 20.03/20.23 True) % 20.03/20.23 (Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_5)) True) % 20.03/20.23 (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.23 Clause #45 (by clausification #[31]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) False) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True)) % 20.03/20.23 Clause #46 (by clausification #[31]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4) → skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) False) (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_6)) False)) % 20.03/20.23 Clause #47 (by clausification #[45]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6)) True)) % 20.03/20.23 Clause #48 (by clausification #[45]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.23 Clause #49 (by clausification #[46]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5)) False) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6)) True)) % 20.03/20.23 Clause #50 (by clausification #[46]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) False) % 20.03/20.23 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5)) False) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.23 Clause #51 (by clausification #[33]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.03/20.23 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5)) False) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_6)) True)) % 20.03/20.23 Clause #52 (by clausification #[33]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.03/20.23 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_5)) False) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.03/20.23 Clause #74 (by betaEtaReduce #[36]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.03/20.23 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.03/20.23 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5)) True) (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_6)) True)) % 20.10/20.26 Clause #79 (by superposition #[74, 47]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 a_7 : a), % 20.10/20.26 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.10/20.26 (Or % 20.10/20.26 (Eq (skS.0 1 (fun x => a_1 x) (fun x => a_2 x) (skS.0 5 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_4 x) a_5)) % 20.10/20.26 True) % 20.10/20.26 (Or (Eq True False) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_7)) True)))) % 20.10/20.26 Clause #176 (by betaEtaReduce #[44]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 a_6 : a), % 20.10/20.26 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_6)) False)) % 20.10/20.26 Clause #431 (by betaEtaReduce #[79]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 a_7 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5)) True) % 20.10/20.26 (Or (Eq True False) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_7)) True)))) % 20.10/20.26 Clause #432 (by clausification #[431]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 a_7 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_7)) True))) % 20.10/20.26 Clause #444 (by equality factoring #[432]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) % 20.10/20.26 (Or (Ne True True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_5 a_6)) True))) % 20.10/20.26 Clause #445 (by clausification #[444]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) % 20.10/20.26 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_5 a_6)) True) (Or (Eq True False) (Eq True False)))) % 20.10/20.26 Clause #447 (by clausification #[445]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) % 20.10/20.26 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_5 a_6)) True) (Eq True False))) % 20.10/20.26 Clause #448 (by clausification #[447]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_5 a_6)) True)) % 20.10/20.26 Clause #454 (by equality factoring #[448]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.10/20.26 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True) % 20.10/20.26 (Or (Ne True True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True)) % 20.10/20.26 Clause #455 (by clausification #[454]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.10/20.26 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Or (Eq True False) (Eq True False))) % 20.10/20.26 Clause #457 (by clausification #[455]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.10/20.26 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True) % 20.10/20.26 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq True False)) % 20.10/20.26 Clause #458 (by clausification #[457]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.10/20.26 Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) % 20.10/20.26 Clause #459 (by superposition #[458, 16]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.10/20.26 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.10/20.26 (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_4 a_5)) True) % 20.10/20.26 Clause #464 (by betaEtaReduce #[459]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.10/20.26 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_4 a_5)) True) % 20.10/20.26 Clause #468 (by superposition #[464, 176]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.12/20.28 (Or (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 3 a_1 a_2 a_4 a_5)) True) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True) (Eq True False))) % 20.12/20.28 Clause #470 (by superposition #[464, 21]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 a_5 a_6 : a → Prop) (a_7 : a), % 20.12/20.28 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) a_2 a_3)) True) % 20.12/20.28 (Or (Eq True False) (Eq (skS.0 2 a_1 a_4 a_5 (skS.0 5 a_1 a_2 a_6 a_7)) True)) % 20.12/20.28 Clause #525 (by betaEtaReduce #[470]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 a_5 a_6 : a → Prop) (a_7 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.28 (Or (Eq True False) (Eq (skS.0 2 a_1 a_4 a_5 (skS.0 5 a_1 a_2 a_6 a_7)) True)) % 20.12/20.28 Clause #526 (by clausification #[525]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 a_5 a_6 : a → Prop) (a_7 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Eq (skS.0 2 a_1 a_4 a_5 (skS.0 5 a_1 a_2 a_6 a_7)) True) % 20.12/20.28 Clause #575 (by betaEtaReduce #[468]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.28 (Or (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 3 a_1 a_2 a_4 a_5)) True) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True) (Eq True False))) % 20.12/20.28 Clause #576 (by clausification #[575]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.28 (Or (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 3 a_1 a_2 a_4 a_5)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_6)) True)) % 20.12/20.28 Clause #587 (by equality factoring #[576]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.28 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.28 (Or (Ne True True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True)) % 20.12/20.28 Clause #590 (by clausification #[587]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.28 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Or (Eq True False) (Eq True False))) % 20.12/20.28 Clause #592 (by clausification #[590]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.28 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq True False)) % 20.12/20.28 Clause #593 (by clausification #[592]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.28 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) % 20.12/20.28 Clause #594 (by superposition #[593, 19]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.12/20.28 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.12/20.28 (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_5)) True) % 20.12/20.28 Clause #599 (by betaEtaReduce #[594]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_4 a_5)) True) % 20.12/20.28 Clause #603 (by superposition #[599, 48]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.12/20.28 (Or (Eq True False) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq (skS.0 2 a_1 a_2 a_5 (skS.0 5 a_1 a_2 a_5 a_6)) False))) % 20.12/20.28 Clause #702 (by betaEtaReduce #[603]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.28 (Or (Eq True False) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq (skS.0 2 a_1 a_2 a_5 (skS.0 5 a_1 a_2 a_5 a_6)) False))) % 20.12/20.28 Clause #703 (by clausification #[702]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a) (a_5 : a → Prop) (a_6 : a), % 20.12/20.28 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.28 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq (skS.0 2 a_1 a_2 a_5 (skS.0 5 a_1 a_2 a_5 a_6)) False)) % 20.12/20.28 Clause #704 (by superposition #[703, 526]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 a_5 : a), % 20.12/20.28 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_3)) True) % 20.12/20.28 (Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 4 (fun x => a_1 x) (fun x => a_2 x) a_4)) True) % 20.12/20.31 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq False True))) % 20.12/20.31 Clause #710 (by betaEtaReduce #[704]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.31 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) % 20.12/20.31 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True) (Eq False True))) % 20.12/20.31 Clause #711 (by clausification #[710]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.31 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_5)) True)) % 20.12/20.31 Clause #715 (by equality factoring #[711]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Or (Ne True True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True)) % 20.12/20.31 Clause #716 (by clausification #[715]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.31 (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Or (Eq True False) (Eq True False))) % 20.12/20.31 Clause #718 (by clausification #[716]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) (Eq True False)) % 20.12/20.31 Clause #719 (by clausification #[718]): ∀ (a_1 a_2 : a → Prop) (a_3 a_4 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_4)) True) % 20.12/20.31 Clause #723 (by equality factoring #[719]): ∀ (a_1 a_2 : a → Prop) (a_3 : a), Or (Ne True True) (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) % 20.12/20.31 Clause #737 (by clausification #[723]): ∀ (a_1 a_2 : a → Prop) (a_3 : a), Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Or (Eq True False) (Eq True False)) % 20.12/20.31 Clause #739 (by clausification #[737]): ∀ (a_1 a_2 : a → Prop) (a_3 : a), Or (Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True) (Eq True False) % 20.12/20.31 Clause #740 (by clausification #[739]): ∀ (a_1 a_2 : a → Prop) (a_3 : a), Eq (skS.0 0 a_1 (skS.0 4 a_1 a_2 a_3)) True % 20.12/20.31 Clause #742 (by superposition #[740, 18]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Or (Eq True False) (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_3 a_4)) True) % 20.12/20.31 Clause #744 (by clausification #[742]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_3 a_4)) True % 20.12/20.31 Clause #745 (by superposition #[744, 51]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.31 (Or (Eq True False) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_5)) True)) % 20.12/20.31 Clause #746 (by superposition #[744, 52]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.31 (Or (Eq True False) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_5)) False)) % 20.12/20.31 Clause #755 (by clausification #[745]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_5)) True) % 20.12/20.31 Clause #758 (by superposition #[755, 16]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 (fun x => a_1 x) (fun x => a_2 x) a_3 (skS.0 3 (fun x => a_1 x) (fun x => a_2 x) a_3 a_4)) True) % 20.12/20.31 (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_5)) True) % 20.12/20.31 Clause #760 (by clausification #[746]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.12/20.31 (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_5)) False) % 20.12/20.31 Clause #763 (by betaEtaReduce #[758]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_5)) True) % 20.12/20.31 Clause #764 (by superposition #[763, 19]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 5 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_3 x) a_4)) True) % 20.12/20.31 (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) True) % 20.12/20.31 Clause #768 (by betaEtaReduce #[764]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.12/20.31 Or (Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) True) % 20.12/20.31 Clause #770 (by superposition #[768, 21]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a) (a_5 a_6 : a → Prop) (a_7 : a), % 20.18/20.34 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 3 (fun x => a_1 x) a_2 a_3 a_4)) True) % 20.18/20.34 (Or (Eq True False) (Eq (skS.0 2 a_1 a_5 a_6 (skS.0 5 a_1 a_2 a_3 a_7)) True)) % 20.18/20.34 Clause #793 (by betaEtaReduce #[770]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a) (a_5 a_6 : a → Prop) (a_7 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.18/20.34 (Or (Eq True False) (Eq (skS.0 2 a_1 a_5 a_6 (skS.0 5 a_1 a_2 a_3 a_7)) True)) % 20.18/20.34 Clause #794 (by clausification #[793]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a) (a_5 a_6 : a → Prop) (a_7 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 2 a_1 a_5 a_6 (skS.0 5 a_1 a_2 a_3 a_7)) True) % 20.18/20.34 Clause #799 (by superposition #[794, 760]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.18/20.34 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 3 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_3 x) a_4)) True) % 20.18/20.34 (Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5)) True) (Eq True False)) % 20.18/20.34 Clause #842 (by betaEtaReduce #[799]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.18/20.34 (Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5)) True) (Eq True False)) % 20.18/20.34 Clause #843 (by clausification #[842]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 3 a_1 a_2 a_3 a_5)) True) % 20.18/20.34 Clause #848 (by superposition #[843, 19]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.18/20.34 Or (Eq (skS.0 0 (fun x => a_1 x) (skS.0 3 (fun x => a_1 x) (fun x => a_2 x) (fun x => a_3 x) a_4)) True) % 20.18/20.34 (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) True) % 20.18/20.34 Clause #850 (by betaEtaReduce #[848]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 a_5 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_5)) True) % 20.18/20.34 Clause #855 (by equality factoring #[850]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Or (Ne True True) (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) % 20.18/20.34 Clause #856 (by clausification #[855]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), % 20.18/20.34 Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Or (Eq True False) (Eq True False)) % 20.18/20.34 Clause #858 (by clausification #[856]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Or (Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True) (Eq True False) % 20.18/20.34 Clause #859 (by clausification #[858]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Eq (skS.0 0 a_1 (skS.0 3 a_1 a_2 a_3 a_4)) True % 20.18/20.34 Clause #860 (by superposition #[859, 49]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.18/20.34 Or (Eq True False) % 20.18/20.34 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5)) True)) % 20.18/20.34 Clause #861 (by superposition #[859, 50]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.18/20.34 Or (Eq True False) % 20.18/20.34 (Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 5 a_1 a_2 a_4 a_5)) False)) % 20.18/20.34 Clause #868 (by clausification #[860]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.18/20.34 Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_4 a_5)) True) % 20.18/20.34 Clause #869 (by superposition #[868, 744]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), % 20.18/20.34 Or (Eq (skS.0 1 (fun x => a_1 x) (fun x => a_2 x) (skS.0 5 (fun x => a_1 x) (fun x => a_2 x) a_3 a_4)) True) % 20.18/20.34 (Eq False True) % 20.18/20.34 Clause #871 (by betaEtaReduce #[869]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Or (Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True) (Eq False True) % 20.18/20.34 Clause #872 (by clausification #[871]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Eq (skS.0 1 a_1 a_2 (skS.0 5 a_1 a_2 a_3 a_4)) True % 20.18/20.34 Clause #873 (by superposition #[872, 16]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Eq (skS.0 0 a_1 (skS.0 5 a_1 a_2 a_3 a_4)) True % 20.18/20.34 Clause #878 (by superposition #[873, 21]): ∀ (a_1 a_2 a_3 a_4 a_5 : a → Prop) (a_6 : a), % 20.18/20.34 Or (Eq True False) (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_4 a_5 a_6)) True) % 20.18/20.34 Clause #880 (by clausification #[878]): ∀ (a_1 a_2 a_3 a_4 a_5 : a → Prop) (a_6 : a), Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_4 a_5 a_6)) True % 20.18/20.35 Clause #881 (by clausification #[861]): ∀ (a_1 a_2 : a → Prop) (a_3 : a) (a_4 : a → Prop) (a_5 : a), % 20.18/20.35 Or (Eq (skS.0 1 a_1 a_2 (skS.0 4 a_1 a_2 a_3)) False) (Eq (skS.0 2 a_1 a_2 a_4 (skS.0 5 a_1 a_2 a_4 a_5)) False) % 20.18/20.35 Clause #882 (by superposition #[881, 744]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), % 20.18/20.35 Or (Eq (skS.0 2 (fun x => a_1 x) (fun x => a_2 x) a_3 (skS.0 5 (fun x => a_1 x) (fun x => a_2 x) a_3 a_4)) False) % 20.18/20.35 (Eq False True) % 20.18/20.35 Clause #886 (by betaEtaReduce #[882]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Or (Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False) (Eq False True) % 20.18/20.35 Clause #887 (by clausification #[886]): ∀ (a_1 a_2 a_3 : a → Prop) (a_4 : a), Eq (skS.0 2 a_1 a_2 a_3 (skS.0 5 a_1 a_2 a_3 a_4)) False % 20.18/20.35 Clause #888 (by superposition #[887, 880]): Eq False True % 20.18/20.35 Clause #890 (by clausification #[888]): False % 20.18/20.35 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------