%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO250^5 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n022.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 5.39s 5.62s % Output : Proof 6.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : SYO250^5 : TPTP v9.2.0. Released v4.0.0. % 0.03/0.12 % Command : duper %s % 0.11/0.32 % Computer : n022.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Fri Oct 3 13:28:53 EDT 2025 % 0.11/0.33 % CPUTime : % 5.39/5.62 SZS status Theorem for theBenchmark.p % 5.39/5.62 SZS output start Proof for theBenchmark.p % 5.39/5.62 Clause #0 (by assumption #[]): Eq % 5.39/5.62 (Not % 5.39/5.62 (Exists fun Xa => % 5.39/5.62 Exists fun Xaa => % 5.39/5.62 Exists fun Xb => % 5.39/5.62 Exists fun Xbb => % 5.39/5.62 Exists fun Xc => % 5.39/5.62 Exists fun Xcc => % 5.39/5.62 Exists fun Xd => % 5.39/5.62 Exists fun Xdd => % 5.39/5.62 Exists fun Xe => % 5.39/5.62 Exists fun Xee => % 5.39/5.62 Exists fun Xh => % 5.39/5.62 Exists fun Xhh => % 5.39/5.62 And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (And % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xaa) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xb)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xbb)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xc)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xcc)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xd)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xdd)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xe)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xee)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xh)) % 5.39/5.62 (Ne % 5.39/5.62 Xa % 5.39/5.62 Xhh)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xb)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xbb)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xc)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xcc)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xd)) % 5.39/5.62 (Ne % 5.39/5.62 Xaa % 5.39/5.62 Xdd)) % 5.39/5.62 (Ne Xaa % 5.39/5.62 Xe)) % 5.39/5.62 (Ne Xaa % 5.39/5.62 Xee)) % 5.39/5.62 (Ne Xaa Xh)) % 5.39/5.62 (Ne Xaa Xhh)) % 5.39/5.62 (Ne Xb Xbb)) % 5.39/5.62 (Ne Xb Xc)) % 5.39/5.62 (Ne Xb Xcc)) % 5.39/5.62 (Ne Xb Xd)) % 5.39/5.62 (Ne Xb Xdd)) % 5.39/5.62 (Ne Xb Xe)) % 5.39/5.62 (Ne Xb Xee)) % 5.39/5.62 (Ne Xb Xh)) % 5.39/5.62 (Ne Xb Xhh)) % 5.39/5.62 (Ne Xc Xcc)) % 5.39/5.62 (Ne Xc Xd)) % 5.39/5.62 (Ne Xc Xdd)) % 5.39/5.62 (Ne Xc Xe)) % 5.39/5.62 (Ne Xc Xee)) % 5.39/5.62 (Ne Xc Xh)) % 5.39/5.62 (Ne Xc Xhh)) % 5.39/5.62 (Ne Xcc Xd)) % 5.39/5.62 (Ne Xcc Xdd)) % 5.39/5.62 (Ne Xcc Xe)) % 5.39/5.62 (Ne Xcc Xee)) % 5.39/5.62 (Ne Xcc Xh)) % 5.39/5.62 (Ne Xcc Xhh)) % 5.39/5.62 (Ne Xd Xdd)) % 5.39/5.62 (Ne Xd Xe)) % 5.39/5.62 (Ne Xd Xee)) % 5.39/5.62 (Ne Xd Xh)) % 5.39/5.62 (Ne Xd Xhh)) % 5.39/5.62 (Ne Xdd Xe)) % 5.39/5.62 (Ne Xdd Xee)) % 5.39/5.62 (Ne Xdd Xh)) % 5.39/5.62 (Ne Xdd Xhh)) % 5.39/5.62 (Ne Xe Xee)) % 5.39/5.62 (Ne Xe Xh)) % 5.39/5.62 (Ne Xe Xhh)) % 5.39/5.62 (Ne Xee Xh)) % 5.39/5.62 (Ne Xee Xhh)) % 5.39/5.62 (Ne Xh Xhh) → % 5.39/5.62 ∀ (P : Iota → Iota), % 5.39/5.62 And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xb) (P Xbb))) (Eq (P Xe) (P Xhh)) → % 5.39/5.67 Eq (P Xc) (P Xdd)) % 5.39/5.67 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xh) (P Xhh))) (Eq (P Xb) (P Xcc)) → % 5.39/5.67 Ne (P Xd) (P Xee))) % 5.39/5.67 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.39/5.67 (Ne (P Xa) (P Xbb)) → % 5.39/5.67 Ne (P Xe) (P Xhh))) % 5.39/5.67 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xd) (P Xdd))) (Ne (P Xb) (P Xcc)) → % 5.39/5.67 Eq (P Xe) (P Xhh))) % 5.39/5.67 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.39/5.67 Ne (P Xa) (P Xbb))) % 5.39/5.67 (And (And (And (Eq (P Xb) (P Xbb)) (Eq (P Xbb) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.39/5.67 (Ne (P Xe) (P Xhh)) → % 5.39/5.67 Eq (P Xd) (P Xee)) → % 5.39/5.67 Or % 5.39/5.67 (Or % 5.39/5.67 (Or (Or (Or (Ne (P Xa) (P Xaa)) (Ne (P Xb) (P Xbb))) (Ne (P Xc) (P Xcc))) % 5.39/5.67 (Ne (P Xd) (P Xdd))) % 5.39/5.67 (Ne (P Xe) (P Xee))) % 5.39/5.67 (Ne (P Xh) (P Xhh)))) % 5.39/5.67 True % 5.39/5.67 Clause #1 (by clausification #[0]): Eq % 5.39/5.67 (Exists fun Xa => % 5.39/5.67 Exists fun Xaa => % 5.39/5.67 Exists fun Xb => % 5.39/5.67 Exists fun Xbb => % 5.39/5.67 Exists fun Xc => % 5.39/5.67 Exists fun Xcc => % 5.39/5.67 Exists fun Xd => % 5.39/5.67 Exists fun Xdd => % 5.39/5.67 Exists fun Xe => % 5.39/5.67 Exists fun Xee => % 5.39/5.67 Exists fun Xh => % 5.39/5.67 Exists fun Xhh => % 5.39/5.67 And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (And % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xaa) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xb)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xbb)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xc)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xcc)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xd)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xdd)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xe)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xee)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xh)) % 5.39/5.67 (Ne % 5.39/5.67 Xa % 5.39/5.67 Xhh)) % 5.39/5.67 (Ne % 5.39/5.67 Xaa % 5.39/5.67 Xb)) % 5.39/5.67 (Ne % 5.39/5.67 Xaa % 5.39/5.67 Xbb)) % 5.39/5.67 (Ne % 5.39/5.67 Xaa % 5.39/5.67 Xc)) % 5.39/5.67 (Ne % 5.39/5.67 Xaa % 5.39/5.67 Xcc)) % 5.39/5.67 (Ne % 5.39/5.67 Xaa % 5.39/5.67 Xd)) % 5.39/5.67 (Ne Xaa % 5.39/5.67 Xdd)) % 5.39/5.67 (Ne Xaa % 5.39/5.67 Xe)) % 5.39/5.67 (Ne Xaa % 5.39/5.67 Xee)) % 5.39/5.67 (Ne Xaa Xh)) % 5.39/5.67 (Ne Xaa Xhh)) % 5.39/5.67 (Ne Xb Xbb)) % 5.39/5.67 (Ne Xb Xc)) % 5.39/5.67 (Ne Xb Xcc)) % 5.39/5.67 (Ne Xb Xd)) % 5.39/5.67 (Ne Xb Xdd)) % 5.39/5.67 (Ne Xb Xe)) % 5.39/5.67 (Ne Xb Xee)) % 5.39/5.67 (Ne Xb Xh)) % 5.39/5.67 (Ne Xb Xhh)) % 5.39/5.67 (Ne Xc Xcc)) % 5.39/5.67 (Ne Xc Xd)) % 5.39/5.67 (Ne Xc Xdd)) % 5.39/5.67 (Ne Xc Xe)) % 5.39/5.67 (Ne Xc Xee)) % 5.39/5.67 (Ne Xc Xh)) % 5.39/5.67 (Ne Xc Xhh)) % 5.39/5.67 (Ne Xcc Xd)) % 5.39/5.67 (Ne Xcc Xdd)) % 5.53/5.72 (Ne Xcc Xe)) % 5.53/5.72 (Ne Xcc Xee)) % 5.53/5.72 (Ne Xcc Xh)) % 5.53/5.72 (Ne Xcc Xhh)) % 5.53/5.72 (Ne Xd Xdd)) % 5.53/5.72 (Ne Xd Xe)) % 5.53/5.72 (Ne Xd Xee)) % 5.53/5.72 (Ne Xd Xh)) % 5.53/5.72 (Ne Xd Xhh)) % 5.53/5.72 (Ne Xdd Xe)) % 5.53/5.72 (Ne Xdd Xee)) % 5.53/5.72 (Ne Xdd Xh)) % 5.53/5.72 (Ne Xdd Xhh)) % 5.53/5.72 (Ne Xe Xee)) % 5.53/5.72 (Ne Xe Xh)) % 5.53/5.72 (Ne Xe Xhh)) % 5.53/5.72 (Ne Xee Xh)) % 5.53/5.72 (Ne Xee Xhh)) % 5.53/5.72 (Ne Xh Xhh) → % 5.53/5.72 ∀ (P : Iota → Iota), % 5.53/5.72 And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xb) (P Xbb))) (Eq (P Xe) (P Xhh)) → % 5.53/5.72 Eq (P Xc) (P Xdd)) % 5.53/5.72 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xh) (P Xhh))) (Eq (P Xb) (P Xcc)) → % 5.53/5.72 Ne (P Xd) (P Xee))) % 5.53/5.72 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.53/5.72 (Ne (P Xa) (P Xbb)) → % 5.53/5.72 Ne (P Xe) (P Xhh))) % 5.53/5.72 (And (And (Eq (P Xa) (P Xaa)) (Eq (P Xd) (P Xdd))) (Ne (P Xb) (P Xcc)) → % 5.53/5.72 Eq (P Xe) (P Xhh))) % 5.53/5.72 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.53/5.72 Ne (P Xa) (P Xbb))) % 5.53/5.72 (And (And (And (Eq (P Xb) (P Xbb)) (Eq (P Xbb) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.53/5.72 (Ne (P Xe) (P Xhh)) → % 5.53/5.72 Eq (P Xd) (P Xee)) → % 5.53/5.72 Or % 5.53/5.72 (Or % 5.53/5.72 (Or (Or (Or (Ne (P Xa) (P Xaa)) (Ne (P Xb) (P Xbb))) (Ne (P Xc) (P Xcc))) % 5.53/5.72 (Ne (P Xd) (P Xdd))) % 5.53/5.72 (Ne (P Xe) (P Xee))) % 5.53/5.72 (Ne (P Xh) (P Xhh))) % 5.53/5.72 False % 5.53/5.72 Clause #2 (by clausification #[1]): ∀ (a : Iota), % 5.53/5.72 Eq % 5.53/5.72 (Exists fun Xaa => % 5.53/5.72 Exists fun Xb => % 5.53/5.72 Exists fun Xbb => % 5.53/5.72 Exists fun Xc => % 5.53/5.72 Exists fun Xcc => % 5.53/5.72 Exists fun Xd => % 5.53/5.72 Exists fun Xdd => % 5.53/5.72 Exists fun Xe => % 5.53/5.72 Exists fun Xee => % 5.53/5.72 Exists fun Xh => % 5.53/5.72 Exists fun Xhh => % 5.53/5.72 And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xaa) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xb)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xbb)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xc)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xcc)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xd)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xdd)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xe)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xee)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xh)) % 5.53/5.72 (Ne % 5.53/5.72 a % 5.53/5.72 Xhh)) % 5.53/5.72 (Ne % 5.53/5.72 Xaa % 5.53/5.72 Xb)) % 5.53/5.72 (Ne % 5.53/5.72 Xaa % 5.53/5.72 Xbb)) % 5.53/5.72 (Ne % 5.53/5.72 Xaa % 5.53/5.72 Xc)) % 5.53/5.72 (Ne % 5.53/5.72 Xaa % 5.53/5.72 Xcc)) % 5.53/5.72 (Ne % 5.53/5.72 Xaa % 5.53/5.72 Xd)) % 5.53/5.72 (Ne Xaa % 5.53/5.72 Xdd)) % 5.53/5.72 (Ne Xaa % 5.53/5.72 Xe)) % 5.53/5.72 (Ne Xaa % 5.53/5.72 Xee)) % 5.53/5.72 (Ne Xaa Xh)) % 5.53/5.72 (Ne Xaa Xhh)) % 5.53/5.72 (Ne Xb Xbb)) % 5.53/5.72 (Ne Xb Xc)) % 5.53/5.72 (Ne Xb Xcc)) % 5.53/5.72 (Ne Xb Xd)) % 5.53/5.72 (Ne Xb Xdd)) % 5.53/5.72 (Ne Xb Xe)) % 5.53/5.72 (Ne Xb Xee)) % 5.53/5.72 (Ne Xb Xh)) % 5.53/5.72 (Ne Xb Xhh)) % 5.53/5.72 (Ne Xc Xcc)) % 5.53/5.72 (Ne Xc Xd)) % 5.53/5.72 (Ne Xc Xdd)) % 5.53/5.72 (Ne Xc Xe)) % 5.53/5.72 (Ne Xc Xee)) % 5.53/5.72 (Ne Xc Xh)) % 5.53/5.72 (Ne Xc Xhh)) % 5.53/5.72 (Ne Xcc Xd)) % 5.53/5.72 (Ne Xcc Xdd)) % 5.53/5.72 (Ne Xcc Xe)) % 5.53/5.72 (Ne Xcc Xee)) % 5.53/5.72 (Ne Xcc Xh)) % 5.53/5.72 (Ne Xcc Xhh)) % 5.53/5.72 (Ne Xd Xdd)) % 5.53/5.72 (Ne Xd Xe)) % 5.53/5.72 (Ne Xd Xee)) % 5.53/5.72 (Ne Xd Xh)) % 5.53/5.72 (Ne Xd Xhh)) % 5.53/5.72 (Ne Xdd Xe)) % 5.53/5.72 (Ne Xdd Xee)) % 5.53/5.72 (Ne Xdd Xh)) % 5.53/5.72 (Ne Xdd Xhh)) % 5.53/5.72 (Ne Xe Xee)) % 5.53/5.72 (Ne Xe Xh)) % 5.53/5.72 (Ne Xe Xhh)) % 5.53/5.72 (Ne Xee Xh)) % 5.53/5.72 (Ne Xee Xhh)) % 5.53/5.72 (Ne Xh Xhh) → % 5.53/5.72 ∀ (P : Iota → Iota), % 5.53/5.72 And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And % 5.53/5.72 (And (And (Eq (P a) (P Xaa)) (Eq (P Xb) (P Xbb))) (Eq (P Xe) (P Xhh)) → % 5.53/5.72 Eq (P Xc) (P Xdd)) % 5.53/5.72 (And (And (Eq (P a) (P Xaa)) (Eq (P Xh) (P Xhh))) (Eq (P Xb) (P Xcc)) → % 5.53/5.72 Ne (P Xd) (P Xee))) % 5.53/5.72 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.53/5.72 (Ne (P a) (P Xbb)) → % 5.53/5.72 Ne (P Xe) (P Xhh))) % 5.53/5.72 (And (And (Eq (P a) (P Xaa)) (Eq (P Xd) (P Xdd))) (Ne (P Xb) (P Xcc)) → % 5.53/5.72 Eq (P Xe) (P Xhh))) % 5.53/5.72 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.53/5.72 Ne (P a) (P Xbb))) % 5.53/5.72 (And (And (And (Eq (P Xb) (P Xbb)) (Eq (P Xbb) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.53/5.72 (Ne (P Xe) (P Xhh)) → % 5.53/5.72 Eq (P Xd) (P Xee)) → % 5.53/5.72 Or % 5.53/5.72 (Or % 5.53/5.72 (Or (Or (Or (Ne (P a) (P Xaa)) (Ne (P Xb) (P Xbb))) (Ne (P Xc) (P Xcc))) % 5.53/5.72 (Ne (P Xd) (P Xdd))) % 5.53/5.72 (Ne (P Xe) (P Xee))) % 5.54/5.77 (Ne (P Xh) (P Xhh))) % 5.54/5.77 False % 5.54/5.77 Clause #3 (by clausification #[2]): ∀ (a a_1 : Iota), % 5.54/5.77 Eq % 5.54/5.77 (Exists fun Xb => % 5.54/5.77 Exists fun Xbb => % 5.54/5.77 Exists fun Xc => % 5.54/5.77 Exists fun Xcc => % 5.54/5.77 Exists fun Xd => % 5.54/5.77 Exists fun Xdd => % 5.54/5.77 Exists fun Xe => % 5.54/5.77 Exists fun Xee => % 5.54/5.77 Exists fun Xh => % 5.54/5.77 Exists fun Xhh => % 5.54/5.77 And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 a_1) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xb)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xbb)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xc)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xcc)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xd)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xdd)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xe)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xee)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xh)) % 5.54/5.77 (Ne % 5.54/5.77 a % 5.54/5.77 Xhh)) % 5.54/5.77 (Ne % 5.54/5.77 a_1 % 5.54/5.77 Xb)) % 5.54/5.77 (Ne % 5.54/5.77 a_1 % 5.54/5.77 Xbb)) % 5.54/5.77 (Ne % 5.54/5.77 a_1 % 5.54/5.77 Xc)) % 5.54/5.77 (Ne % 5.54/5.77 a_1 % 5.54/5.77 Xcc)) % 5.54/5.77 (Ne a_1 % 5.54/5.77 Xd)) % 5.54/5.77 (Ne a_1 % 5.54/5.77 Xdd)) % 5.54/5.77 (Ne a_1 Xe)) % 5.54/5.77 (Ne a_1 Xee)) % 5.54/5.77 (Ne a_1 Xh)) % 5.54/5.77 (Ne a_1 Xhh)) % 5.54/5.77 (Ne Xb Xbb)) % 5.54/5.77 (Ne Xb Xc)) % 5.54/5.77 (Ne Xb Xcc)) % 5.54/5.77 (Ne Xb Xd)) % 5.54/5.77 (Ne Xb Xdd)) % 5.54/5.77 (Ne Xb Xe)) % 5.54/5.77 (Ne Xb Xee)) % 5.54/5.77 (Ne Xb Xh)) % 5.54/5.77 (Ne Xb Xhh)) % 5.54/5.77 (Ne Xc Xcc)) % 5.54/5.77 (Ne Xc Xd)) % 5.54/5.77 (Ne Xc Xdd)) % 5.54/5.77 (Ne Xc Xe)) % 5.54/5.77 (Ne Xc Xee)) % 5.54/5.77 (Ne Xc Xh)) % 5.54/5.77 (Ne Xc Xhh)) % 5.54/5.77 (Ne Xcc Xd)) % 5.54/5.77 (Ne Xcc Xdd)) % 5.54/5.77 (Ne Xcc Xe)) % 5.54/5.77 (Ne Xcc Xee)) % 5.54/5.77 (Ne Xcc Xh)) % 5.54/5.77 (Ne Xcc Xhh)) % 5.54/5.77 (Ne Xd Xdd)) % 5.54/5.77 (Ne Xd Xe)) % 5.54/5.77 (Ne Xd Xee)) % 5.54/5.77 (Ne Xd Xh)) % 5.54/5.77 (Ne Xd Xhh)) % 5.54/5.77 (Ne Xdd Xe)) % 5.54/5.77 (Ne Xdd Xee)) % 5.54/5.77 (Ne Xdd Xh)) % 5.54/5.77 (Ne Xdd Xhh)) % 5.54/5.77 (Ne Xe Xee)) % 5.54/5.77 (Ne Xe Xh)) % 5.54/5.77 (Ne Xe Xhh)) % 5.54/5.77 (Ne Xee Xh)) % 5.54/5.77 (Ne Xee Xhh)) % 5.54/5.77 (Ne Xh Xhh) → % 5.54/5.77 ∀ (P : Iota → Iota), % 5.54/5.77 And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And % 5.54/5.77 (And (And (Eq (P a) (P a_1)) (Eq (P Xb) (P Xbb))) (Eq (P Xe) (P Xhh)) → % 5.54/5.77 Eq (P Xc) (P Xdd)) % 5.54/5.77 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P Xb) (P Xcc)) → % 5.54/5.77 Ne (P Xd) (P Xee))) % 5.54/5.77 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.54/5.77 (Ne (P a) (P Xbb)) → % 5.54/5.77 Ne (P Xe) (P Xhh))) % 5.54/5.77 (And (And (Eq (P a) (P a_1)) (Eq (P Xd) (P Xdd))) (Ne (P Xb) (P Xcc)) → % 5.54/5.77 Eq (P Xe) (P Xhh))) % 5.54/5.77 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.54/5.77 Ne (P a) (P Xbb))) % 5.54/5.77 (And (And (And (Eq (P Xb) (P Xbb)) (Eq (P Xbb) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.62/5.81 (Ne (P Xe) (P Xhh)) → % 5.62/5.81 Eq (P Xd) (P Xee)) → % 5.62/5.81 Or % 5.62/5.81 (Or % 5.62/5.81 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P Xb) (P Xbb))) (Ne (P Xc) (P Xcc))) % 5.62/5.81 (Ne (P Xd) (P Xdd))) % 5.62/5.81 (Ne (P Xe) (P Xee))) % 5.62/5.81 (Ne (P Xh) (P Xhh))) % 5.62/5.81 False % 5.62/5.81 Clause #4 (by clausification #[3]): ∀ (a a_1 a_2 : Iota), % 5.62/5.81 Eq % 5.62/5.81 (Exists fun Xbb => % 5.62/5.81 Exists fun Xc => % 5.62/5.81 Exists fun Xcc => % 5.62/5.81 Exists fun Xd => % 5.62/5.81 Exists fun Xdd => % 5.62/5.81 Exists fun Xe => % 5.62/5.81 Exists fun Xee => % 5.62/5.81 Exists fun Xh => % 5.62/5.81 Exists fun Xhh => % 5.62/5.81 And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 a_1) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 a_2)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xbb)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xc)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xcc)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xd)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xdd)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xe)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xee)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xh)) % 5.62/5.81 (Ne % 5.62/5.81 a % 5.62/5.81 Xhh)) % 5.62/5.81 (Ne % 5.62/5.81 a_1 % 5.62/5.81 a_2)) % 5.62/5.81 (Ne % 5.62/5.81 a_1 % 5.62/5.81 Xbb)) % 5.62/5.81 (Ne % 5.62/5.81 a_1 % 5.62/5.81 Xc)) % 5.62/5.81 (Ne a_1 % 5.62/5.81 Xcc)) % 5.62/5.81 (Ne a_1 % 5.62/5.81 Xd)) % 5.62/5.81 (Ne a_1 % 5.62/5.81 Xdd)) % 5.62/5.81 (Ne a_1 Xe)) % 5.62/5.81 (Ne a_1 Xee)) % 5.62/5.81 (Ne a_1 Xh)) % 5.62/5.81 (Ne a_1 Xhh)) % 5.62/5.81 (Ne a_2 Xbb)) % 5.62/5.81 (Ne a_2 Xc)) % 5.62/5.81 (Ne a_2 Xcc)) % 5.62/5.81 (Ne a_2 Xd)) % 5.62/5.81 (Ne a_2 Xdd)) % 5.62/5.81 (Ne a_2 Xe)) % 5.62/5.81 (Ne a_2 Xee)) % 5.62/5.81 (Ne a_2 Xh)) % 5.62/5.81 (Ne a_2 Xhh)) % 5.62/5.81 (Ne Xc Xcc)) % 5.62/5.81 (Ne Xc Xd)) % 5.62/5.81 (Ne Xc Xdd)) % 5.62/5.81 (Ne Xc Xe)) % 5.62/5.81 (Ne Xc Xee)) % 5.62/5.81 (Ne Xc Xh)) % 5.62/5.81 (Ne Xc Xhh)) % 5.62/5.81 (Ne Xcc Xd)) % 5.62/5.81 (Ne Xcc Xdd)) % 5.62/5.81 (Ne Xcc Xe)) % 5.62/5.81 (Ne Xcc Xee)) % 5.62/5.81 (Ne Xcc Xh)) % 5.62/5.81 (Ne Xcc Xhh)) % 5.62/5.81 (Ne Xd Xdd)) % 5.62/5.81 (Ne Xd Xe)) % 5.62/5.81 (Ne Xd Xee)) % 5.62/5.81 (Ne Xd Xh)) % 5.62/5.81 (Ne Xd Xhh)) % 5.62/5.81 (Ne Xdd Xe)) % 5.62/5.81 (Ne Xdd Xee)) % 5.62/5.81 (Ne Xdd Xh)) % 5.62/5.81 (Ne Xdd Xhh)) % 5.62/5.81 (Ne Xe Xee)) % 5.62/5.81 (Ne Xe Xh)) % 5.62/5.81 (Ne Xe Xhh)) % 5.62/5.81 (Ne Xee Xh)) % 5.62/5.81 (Ne Xee Xhh)) % 5.62/5.81 (Ne Xh Xhh) → % 5.62/5.81 ∀ (P : Iota → Iota), % 5.62/5.81 And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And % 5.62/5.81 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P Xbb))) (Eq (P Xe) (P Xhh)) → % 5.62/5.81 Eq (P Xc) (P Xdd)) % 5.62/5.81 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P Xcc)) → % 5.62/5.81 Ne (P Xd) (P Xee))) % 5.62/5.81 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.62/5.81 (Ne (P a) (P Xbb)) → % 5.62/5.81 Ne (P Xe) (P Xhh))) % 5.62/5.81 (And (And (Eq (P a) (P a_1)) (Eq (P Xd) (P Xdd))) (Ne (P a_2) (P Xcc)) → % 5.62/5.81 Eq (P Xe) (P Xhh))) % 5.62/5.81 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.62/5.81 Ne (P a) (P Xbb))) % 5.62/5.86 (And (And (And (Eq (P a_2) (P Xbb)) (Eq (P Xbb) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.62/5.86 (Ne (P Xe) (P Xhh)) → % 5.62/5.86 Eq (P Xd) (P Xee)) → % 5.62/5.86 Or % 5.62/5.86 (Or % 5.62/5.86 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P Xbb))) (Ne (P Xc) (P Xcc))) % 5.62/5.86 (Ne (P Xd) (P Xdd))) % 5.62/5.86 (Ne (P Xe) (P Xee))) % 5.62/5.86 (Ne (P Xh) (P Xhh))) % 5.62/5.86 False % 5.62/5.86 Clause #5 (by clausification #[4]): ∀ (a a_1 a_2 a_3 : Iota), % 5.62/5.86 Eq % 5.62/5.86 (Exists fun Xc => % 5.62/5.86 Exists fun Xcc => % 5.62/5.86 Exists fun Xd => % 5.62/5.86 Exists fun Xdd => % 5.62/5.86 Exists fun Xe => % 5.62/5.86 Exists fun Xee => % 5.62/5.86 Exists fun Xh => % 5.62/5.86 Exists fun Xhh => % 5.62/5.86 And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (And % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 a_1) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 a_2)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 a_3)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xc)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xcc)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xd)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xdd)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xe)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xee)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xh)) % 5.62/5.86 (Ne % 5.62/5.86 a % 5.62/5.86 Xhh)) % 5.62/5.86 (Ne % 5.62/5.86 a_1 % 5.62/5.86 a_2)) % 5.62/5.86 (Ne % 5.62/5.86 a_1 % 5.62/5.86 a_3)) % 5.62/5.86 (Ne a_1 % 5.62/5.86 Xc)) % 5.62/5.86 (Ne a_1 % 5.62/5.86 Xcc)) % 5.62/5.86 (Ne a_1 Xd)) % 5.62/5.86 (Ne a_1 Xdd)) % 5.62/5.86 (Ne a_1 Xe)) % 5.62/5.86 (Ne a_1 Xee)) % 5.62/5.86 (Ne a_1 Xh)) % 5.62/5.86 (Ne a_1 Xhh)) % 5.62/5.86 (Ne a_2 a_3)) % 5.62/5.86 (Ne a_2 Xc)) % 5.62/5.86 (Ne a_2 Xcc)) % 5.62/5.86 (Ne a_2 Xd)) % 5.71/5.91 (Ne a_2 Xdd)) % 5.71/5.91 (Ne a_2 Xe)) % 5.71/5.91 (Ne a_2 Xee)) % 5.71/5.91 (Ne a_2 Xh)) % 5.71/5.91 (Ne a_2 Xhh)) % 5.71/5.91 (Ne Xc Xcc)) % 5.71/5.91 (Ne Xc Xd)) % 5.71/5.91 (Ne Xc Xdd)) % 5.71/5.91 (Ne Xc Xe)) % 5.71/5.91 (Ne Xc Xee)) % 5.71/5.91 (Ne Xc Xh)) % 5.71/5.91 (Ne Xc Xhh)) % 5.71/5.91 (Ne Xcc Xd)) % 5.71/5.91 (Ne Xcc Xdd)) % 5.71/5.91 (Ne Xcc Xe)) % 5.71/5.91 (Ne Xcc Xee)) % 5.71/5.91 (Ne Xcc Xh)) % 5.71/5.91 (Ne Xcc Xhh)) % 5.71/5.91 (Ne Xd Xdd)) % 5.71/5.91 (Ne Xd Xe)) % 5.71/5.91 (Ne Xd Xee)) % 5.71/5.91 (Ne Xd Xh)) % 5.71/5.91 (Ne Xd Xhh)) % 5.71/5.91 (Ne Xdd Xe)) % 5.71/5.91 (Ne Xdd Xee)) % 5.71/5.91 (Ne Xdd Xh)) % 5.71/5.91 (Ne Xdd Xhh)) % 5.71/5.91 (Ne Xe Xee)) % 5.71/5.91 (Ne Xe Xh)) % 5.71/5.91 (Ne Xe Xhh)) % 5.71/5.91 (Ne Xee Xh)) % 5.71/5.91 (Ne Xee Xhh)) % 5.71/5.91 (Ne Xh Xhh) → % 5.71/5.91 ∀ (P : Iota → Iota), % 5.71/5.91 And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P Xe) (P Xhh)) → % 5.71/5.91 Eq (P Xc) (P Xdd)) % 5.71/5.91 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P Xcc)) → % 5.71/5.91 Ne (P Xd) (P Xee))) % 5.71/5.91 (And (And (And (Eq (P Xc) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.71/5.91 (Ne (P a) (P a_3)) → % 5.71/5.91 Ne (P Xe) (P Xhh))) % 5.71/5.91 (And (And (Eq (P a) (P a_1)) (Eq (P Xd) (P Xdd))) (Ne (P a_2) (P Xcc)) → % 5.71/5.91 Eq (P Xe) (P Xhh))) % 5.71/5.91 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P Xc) (P Xdd)) → % 5.71/5.91 Ne (P a) (P a_3))) % 5.71/5.91 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P Xc))) (Eq (P Xc) (P Xcc))) % 5.71/5.91 (Ne (P Xe) (P Xhh)) → % 5.71/5.91 Eq (P Xd) (P Xee)) → % 5.71/5.91 Or % 5.71/5.91 (Or % 5.71/5.91 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P Xc) (P Xcc))) % 5.71/5.91 (Ne (P Xd) (P Xdd))) % 5.71/5.91 (Ne (P Xe) (P Xee))) % 5.71/5.91 (Ne (P Xh) (P Xhh))) % 5.71/5.91 False % 5.71/5.91 Clause #6 (by clausification #[5]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 5.71/5.91 Eq % 5.71/5.91 (Exists fun Xcc => % 5.71/5.91 Exists fun Xd => % 5.71/5.91 Exists fun Xdd => % 5.71/5.91 Exists fun Xe => % 5.71/5.91 Exists fun Xee => % 5.71/5.91 Exists fun Xh => % 5.71/5.91 Exists fun Xhh => % 5.71/5.91 And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (And % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 a_1) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 a_2)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 a_3)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 a_4)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xcc)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xd)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xdd)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xe)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xee)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xh)) % 5.71/5.91 (Ne % 5.71/5.91 a % 5.71/5.91 Xhh)) % 5.71/5.91 (Ne % 5.71/5.91 a_1 % 5.71/5.91 a_2)) % 5.71/5.91 (Ne a_1 % 5.71/5.91 a_3)) % 5.71/5.91 (Ne a_1 % 5.71/5.91 a_4)) % 5.71/5.91 (Ne a_1 % 5.71/5.91 Xcc)) % 5.71/5.91 (Ne a_1 Xd)) % 5.71/5.91 (Ne a_1 Xdd)) % 5.71/5.91 (Ne a_1 Xe)) % 5.71/5.91 (Ne a_1 Xee)) % 5.71/5.91 (Ne a_1 Xh)) % 5.71/5.91 (Ne a_1 Xhh)) % 5.71/5.91 (Ne a_2 a_3)) % 5.71/5.91 (Ne a_2 a_4)) % 5.71/5.91 (Ne a_2 Xcc)) % 5.71/5.91 (Ne a_2 Xd)) % 5.71/5.91 (Ne a_2 Xdd)) % 5.71/5.91 (Ne a_2 Xe)) % 5.71/5.91 (Ne a_2 Xee)) % 5.71/5.91 (Ne a_2 Xh)) % 5.71/5.91 (Ne a_2 Xhh)) % 5.71/5.91 (Ne a_4 Xcc)) % 5.71/5.91 (Ne a_4 Xd)) % 5.71/5.91 (Ne a_4 Xdd)) % 5.71/5.91 (Ne a_4 Xe)) % 5.71/5.91 (Ne a_4 Xee)) % 5.71/5.91 (Ne a_4 Xh)) % 5.71/5.91 (Ne a_4 Xhh)) % 5.71/5.96 (Ne Xcc Xd)) % 5.71/5.96 (Ne Xcc Xdd)) % 5.71/5.96 (Ne Xcc Xe)) % 5.71/5.96 (Ne Xcc Xee)) % 5.71/5.96 (Ne Xcc Xh)) % 5.71/5.96 (Ne Xcc Xhh)) % 5.71/5.96 (Ne Xd Xdd)) % 5.71/5.96 (Ne Xd Xe)) % 5.71/5.96 (Ne Xd Xee)) % 5.71/5.96 (Ne Xd Xh)) % 5.71/5.96 (Ne Xd Xhh)) % 5.71/5.96 (Ne Xdd Xe)) % 5.71/5.96 (Ne Xdd Xee)) % 5.71/5.96 (Ne Xdd Xh)) % 5.71/5.96 (Ne Xdd Xhh)) % 5.71/5.96 (Ne Xe Xee)) % 5.71/5.96 (Ne Xe Xh)) % 5.71/5.96 (Ne Xe Xhh)) % 5.71/5.96 (Ne Xee Xh)) % 5.71/5.96 (Ne Xee Xhh)) % 5.71/5.96 (Ne Xh Xhh) → % 5.71/5.96 ∀ (P : Iota → Iota), % 5.71/5.96 And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P Xe) (P Xhh)) → % 5.71/5.96 Eq (P a_4) (P Xdd)) % 5.71/5.96 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P Xcc)) → % 5.71/5.96 Ne (P Xd) (P Xee))) % 5.71/5.96 (And (And (And (Eq (P a_4) (P Xcc)) (Eq (P Xcc) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.71/5.96 (Ne (P a) (P a_3)) → % 5.71/5.96 Ne (P Xe) (P Xhh))) % 5.71/5.96 (And (And (Eq (P a) (P a_1)) (Eq (P Xd) (P Xdd))) (Ne (P a_2) (P Xcc)) → % 5.71/5.96 Eq (P Xe) (P Xhh))) % 5.71/5.96 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P Xdd)) → Ne (P a) (P a_3))) % 5.71/5.96 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P Xcc))) % 5.71/5.96 (Ne (P Xe) (P Xhh)) → % 5.71/5.96 Eq (P Xd) (P Xee)) → % 5.71/5.96 Or % 5.71/5.96 (Or % 5.71/5.96 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P Xcc))) % 5.71/5.96 (Ne (P Xd) (P Xdd))) % 5.71/5.96 (Ne (P Xe) (P Xee))) % 5.71/5.96 (Ne (P Xh) (P Xhh))) % 5.71/5.96 False % 5.71/5.96 Clause #7 (by clausification #[6]): ∀ (a a_1 a_2 a_3 a_4 a_5 : Iota), % 5.71/5.96 Eq % 5.71/5.96 (Exists fun Xd => % 5.71/5.96 Exists fun Xdd => % 5.71/5.96 Exists fun Xe => % 5.71/5.96 Exists fun Xee => % 5.71/5.96 Exists fun Xh => % 5.71/5.96 Exists fun Xhh => % 5.71/5.96 And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 a_1) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 a_2)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 a_3)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 a_4)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 a_5)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 Xd)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 Xdd)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 Xe)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 Xee)) % 5.71/5.96 (Ne % 5.71/5.96 a % 5.71/5.96 Xh)) % 5.71/5.96 (Ne a % 5.71/5.96 Xhh)) % 5.71/5.96 (Ne a_1 % 5.71/5.96 a_2)) % 5.71/5.96 (Ne a_1 % 5.71/5.96 a_3)) % 5.71/5.96 (Ne a_1 % 5.71/5.96 a_4)) % 5.71/5.96 (Ne a_1 a_5)) % 5.71/5.96 (Ne a_1 Xd)) % 5.71/5.96 (Ne a_1 Xdd)) % 5.71/5.96 (Ne a_1 Xe)) % 5.71/5.96 (Ne a_1 Xee)) % 5.71/5.96 (Ne a_1 Xh)) % 5.71/5.96 (Ne a_1 Xhh)) % 5.71/5.96 (Ne a_2 a_3)) % 5.71/5.96 (Ne a_2 a_4)) % 5.71/5.96 (Ne a_2 a_5)) % 5.71/5.96 (Ne a_2 Xd)) % 5.71/5.96 (Ne a_2 Xdd)) % 5.71/5.96 (Ne a_2 Xe)) % 5.71/5.96 (Ne a_2 Xee)) % 5.71/5.96 (Ne a_2 Xh)) % 5.71/5.96 (Ne a_2 Xhh)) % 5.71/5.96 (Ne a_4 a_5)) % 5.71/5.96 (Ne a_4 Xd)) % 5.71/5.96 (Ne a_4 Xdd)) % 5.71/5.96 (Ne a_4 Xe)) % 5.71/5.96 (Ne a_4 Xee)) % 5.71/5.96 (Ne a_4 Xh)) % 5.71/5.96 (Ne a_4 Xhh)) % 5.71/5.96 (Ne a_5 Xd)) % 5.71/5.96 (Ne a_5 Xdd)) % 5.71/5.96 (Ne a_5 Xe)) % 5.71/5.96 (Ne a_5 Xee)) % 5.71/5.96 (Ne a_5 Xh)) % 5.71/5.96 (Ne a_5 Xhh)) % 5.71/5.96 (Ne Xd Xdd)) % 5.71/5.96 (Ne Xd Xe)) % 5.71/5.96 (Ne Xd Xee)) % 5.71/5.96 (Ne Xd Xh)) % 5.71/5.96 (Ne Xd Xhh)) % 5.71/5.96 (Ne Xdd Xe)) % 5.71/5.96 (Ne Xdd Xee)) % 5.71/5.96 (Ne Xdd Xh)) % 5.71/5.96 (Ne Xdd Xhh)) % 5.71/5.96 (Ne Xe Xee)) % 5.71/5.96 (Ne Xe Xh)) % 5.71/5.96 (Ne Xe Xhh)) % 5.71/5.96 (Ne Xee Xh)) % 5.71/5.96 (Ne Xee Xhh)) % 5.71/5.96 (Ne Xh Xhh) → % 5.71/5.96 ∀ (P : Iota → Iota), % 5.71/5.96 And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And % 5.71/5.96 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P Xe) (P Xhh)) → % 5.71/5.96 Eq (P a_4) (P Xdd)) % 5.71/5.96 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P a_5)) → % 5.71/5.96 Ne (P Xd) (P Xee))) % 5.71/5.96 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P Xd))) (Eq (P Xd) (P Xdd))) % 5.71/5.96 (Ne (P a) (P a_3)) → % 5.71/5.96 Ne (P Xe) (P Xhh))) % 5.81/6.00 (And (And (Eq (P a) (P a_1)) (Eq (P Xd) (P Xdd))) (Ne (P a_2) (P a_5)) → Eq (P Xe) (P Xhh))) % 5.81/6.00 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P Xdd)) → Ne (P a) (P a_3))) % 5.81/6.00 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) % 5.81/6.00 (Ne (P Xe) (P Xhh)) → % 5.81/6.00 Eq (P Xd) (P Xee)) → % 5.81/6.00 Or % 5.81/6.00 (Or % 5.81/6.00 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) % 5.81/6.00 (Ne (P Xd) (P Xdd))) % 5.81/6.00 (Ne (P Xe) (P Xee))) % 5.81/6.00 (Ne (P Xh) (P Xhh))) % 5.81/6.00 False % 5.81/6.00 Clause #8 (by clausification #[7]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 : Iota), % 5.81/6.00 Eq % 5.81/6.00 (Exists fun Xdd => % 5.81/6.00 Exists fun Xe => % 5.81/6.00 Exists fun Xee => % 5.81/6.00 Exists fun Xh => % 5.81/6.00 Exists fun Xhh => % 5.81/6.00 And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (And % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_1) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_2)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_3)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_4)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_5)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 a_6)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 Xdd)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 Xe)) % 5.81/6.00 (Ne % 5.81/6.00 a % 5.81/6.00 Xee)) % 5.81/6.00 (Ne a % 5.81/6.00 Xh)) % 5.81/6.00 (Ne a % 5.81/6.00 Xhh)) % 5.81/6.00 (Ne a_1 % 5.81/6.00 a_2)) % 5.81/6.00 (Ne a_1 % 5.81/6.00 a_3)) % 5.81/6.00 (Ne a_1 a_4)) % 5.81/6.00 (Ne a_1 a_5)) % 5.81/6.00 (Ne a_1 a_6)) % 5.81/6.00 (Ne a_1 Xdd)) % 5.81/6.00 (Ne a_1 Xe)) % 5.81/6.00 (Ne a_1 Xee)) % 5.81/6.00 (Ne a_1 Xh)) % 5.81/6.00 (Ne a_1 Xhh)) % 5.81/6.00 (Ne a_2 a_3)) % 5.81/6.00 (Ne a_2 a_4)) % 5.81/6.00 (Ne a_2 a_5)) % 5.81/6.00 (Ne a_2 a_6)) % 5.81/6.00 (Ne a_2 Xdd)) % 5.81/6.00 (Ne a_2 Xe)) % 5.81/6.00 (Ne a_2 Xee)) % 5.81/6.00 (Ne a_2 Xh)) % 5.81/6.00 (Ne a_2 Xhh)) % 5.81/6.00 (Ne a_4 a_5)) % 5.81/6.00 (Ne a_4 a_6)) % 5.81/6.00 (Ne a_4 Xdd)) % 5.81/6.00 (Ne a_4 Xe)) % 5.81/6.00 (Ne a_4 Xee)) % 5.81/6.00 (Ne a_4 Xh)) % 5.81/6.00 (Ne a_4 Xhh)) % 5.81/6.00 (Ne a_5 a_6)) % 5.81/6.00 (Ne a_5 Xdd)) % 5.81/6.00 (Ne a_5 Xe)) % 5.83/6.05 (Ne a_5 Xee)) % 5.83/6.05 (Ne a_5 Xh)) % 5.83/6.05 (Ne a_5 Xhh)) % 5.83/6.05 (Ne a_6 Xdd)) % 5.83/6.05 (Ne a_6 Xe)) % 5.83/6.05 (Ne a_6 Xee)) % 5.83/6.05 (Ne a_6 Xh)) % 5.83/6.05 (Ne a_6 Xhh)) % 5.83/6.05 (Ne Xdd Xe)) % 5.83/6.05 (Ne Xdd Xee)) % 5.83/6.05 (Ne Xdd Xh)) % 5.83/6.05 (Ne Xdd Xhh)) % 5.83/6.05 (Ne Xe Xee)) % 5.83/6.05 (Ne Xe Xh)) % 5.83/6.05 (Ne Xe Xhh)) % 5.83/6.05 (Ne Xee Xh)) % 5.83/6.05 (Ne Xee Xhh)) % 5.83/6.05 (Ne Xh Xhh) → % 5.83/6.05 ∀ (P : Iota → Iota), % 5.83/6.05 And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P Xe) (P Xhh)) → % 5.83/6.05 Eq (P a_4) (P Xdd)) % 5.83/6.05 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P a_5)) → % 5.83/6.05 Ne (P a_6) (P Xee))) % 5.83/6.05 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P Xdd))) % 5.83/6.05 (Ne (P a) (P a_3)) → % 5.83/6.05 Ne (P Xe) (P Xhh))) % 5.83/6.05 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P Xdd))) (Ne (P a_2) (P a_5)) → Eq (P Xe) (P Xhh))) % 5.83/6.05 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P Xdd)) → Ne (P a) (P a_3))) % 5.83/6.05 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) % 5.83/6.05 (Ne (P Xe) (P Xhh)) → % 5.83/6.05 Eq (P a_6) (P Xee)) → % 5.83/6.05 Or % 5.83/6.05 (Or % 5.83/6.05 (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P Xdd))) % 5.83/6.05 (Ne (P Xe) (P Xee))) % 5.83/6.05 (Ne (P Xh) (P Xhh))) % 5.83/6.05 False % 5.83/6.05 Clause #9 (by clausification #[8]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 : Iota), % 5.83/6.05 Eq % 5.83/6.05 (Exists fun Xe => % 5.83/6.05 Exists fun Xee => % 5.83/6.05 Exists fun Xh => % 5.83/6.05 Exists fun Xhh => % 5.83/6.05 And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (And % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_1) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_2)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_3)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_4)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_5)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_6)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 a_7)) % 5.83/6.05 (Ne % 5.83/6.05 a % 5.83/6.05 Xe)) % 5.83/6.05 (Ne a % 5.83/6.05 Xee)) % 5.83/6.05 (Ne a % 5.83/6.05 Xh)) % 5.83/6.05 (Ne a % 5.83/6.05 Xhh)) % 5.83/6.05 (Ne a_1 % 5.83/6.05 a_2)) % 5.83/6.05 (Ne a_1 a_3)) % 5.83/6.05 (Ne a_1 a_4)) % 5.83/6.05 (Ne a_1 a_5)) % 5.83/6.05 (Ne a_1 a_6)) % 5.83/6.05 (Ne a_1 a_7)) % 5.83/6.05 (Ne a_1 Xe)) % 5.83/6.05 (Ne a_1 Xee)) % 5.83/6.05 (Ne a_1 Xh)) % 5.83/6.05 (Ne a_1 Xhh)) % 5.83/6.05 (Ne a_2 a_3)) % 5.83/6.05 (Ne a_2 a_4)) % 5.83/6.05 (Ne a_2 a_5)) % 5.83/6.05 (Ne a_2 a_6)) % 5.83/6.05 (Ne a_2 a_7)) % 5.83/6.09 (Ne a_2 Xe)) % 5.83/6.09 (Ne a_2 Xee)) % 5.83/6.09 (Ne a_2 Xh)) % 5.83/6.09 (Ne a_2 Xhh)) % 5.83/6.09 (Ne a_4 a_5)) % 5.83/6.09 (Ne a_4 a_6)) % 5.83/6.09 (Ne a_4 a_7)) % 5.83/6.09 (Ne a_4 Xe)) % 5.83/6.09 (Ne a_4 Xee)) % 5.83/6.09 (Ne a_4 Xh)) % 5.83/6.09 (Ne a_4 Xhh)) % 5.83/6.09 (Ne a_5 a_6)) % 5.83/6.09 (Ne a_5 a_7)) % 5.83/6.09 (Ne a_5 Xe)) % 5.83/6.09 (Ne a_5 Xee)) % 5.83/6.09 (Ne a_5 Xh)) % 5.83/6.09 (Ne a_5 Xhh)) % 5.83/6.09 (Ne a_6 a_7)) % 5.83/6.09 (Ne a_6 Xe)) % 5.83/6.09 (Ne a_6 Xee)) % 5.83/6.09 (Ne a_6 Xh)) % 5.83/6.09 (Ne a_6 Xhh)) % 5.83/6.09 (Ne a_7 Xe)) % 5.83/6.09 (Ne a_7 Xee)) % 5.83/6.09 (Ne a_7 Xh)) % 5.83/6.09 (Ne a_7 Xhh)) % 5.83/6.09 (Ne Xe Xee)) % 5.83/6.09 (Ne Xe Xh)) % 5.83/6.09 (Ne Xe Xhh)) % 5.83/6.09 (Ne Xee Xh)) % 5.83/6.09 (Ne Xee Xhh)) % 5.83/6.09 (Ne Xh Xhh) → % 5.83/6.09 ∀ (P : Iota → Iota), % 5.83/6.09 And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P Xe) (P Xhh)) → Eq (P a_4) (P a_7)) % 5.83/6.09 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P a_5)) → % 5.83/6.09 Ne (P a_6) (P Xee))) % 5.83/6.09 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P a_7))) % 5.83/6.09 (Ne (P a) (P a_3)) → % 5.83/6.09 Ne (P Xe) (P Xhh))) % 5.83/6.09 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P a_7))) (Ne (P a_2) (P a_5)) → Eq (P Xe) (P Xhh))) % 5.83/6.09 (And (And (Eq (P Xe) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P a_7)) → Ne (P a) (P a_3))) % 5.83/6.09 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) % 5.83/6.09 (Ne (P Xe) (P Xhh)) → % 5.83/6.09 Eq (P a_6) (P Xee)) → % 5.83/6.09 Or % 5.83/6.09 (Or (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P a_7))) % 5.83/6.09 (Ne (P Xe) (P Xee))) % 5.83/6.09 (Ne (P Xh) (P Xhh))) % 5.83/6.09 False % 5.83/6.09 Clause #10 (by clausification #[9]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 : Iota), % 5.83/6.09 Eq % 5.83/6.09 (Exists fun Xee => % 5.83/6.09 Exists fun Xh => % 5.83/6.09 Exists fun Xhh => % 5.83/6.09 And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (And % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_1) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_2)) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_3)) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_4)) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_5)) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_6)) % 5.83/6.09 (Ne % 5.83/6.09 a % 5.83/6.09 a_7)) % 5.83/6.09 (Ne a % 5.83/6.09 a_8)) % 5.83/6.09 (Ne a % 5.83/6.09 Xee)) % 5.83/6.09 (Ne a Xh)) % 5.83/6.09 (Ne a Xhh)) % 5.83/6.09 (Ne a_1 a_2)) % 5.83/6.09 (Ne a_1 a_3)) % 5.83/6.09 (Ne a_1 a_4)) % 5.83/6.09 (Ne a_1 a_5)) % 5.83/6.09 (Ne a_1 a_6)) % 5.83/6.09 (Ne a_1 a_7)) % 5.83/6.09 (Ne a_1 a_8)) % 5.83/6.09 (Ne a_1 Xee)) % 5.83/6.09 (Ne a_1 Xh)) % 5.83/6.09 (Ne a_1 Xhh)) % 5.83/6.09 (Ne a_2 a_3)) % 5.83/6.09 (Ne a_2 a_4)) % 5.92/6.14 (Ne a_2 a_5)) % 5.92/6.14 (Ne a_2 a_6)) % 5.92/6.14 (Ne a_2 a_7)) % 5.92/6.14 (Ne a_2 a_8)) % 5.92/6.14 (Ne a_2 Xee)) % 5.92/6.14 (Ne a_2 Xh)) % 5.92/6.14 (Ne a_2 Xhh)) % 5.92/6.14 (Ne a_4 a_5)) % 5.92/6.14 (Ne a_4 a_6)) % 5.92/6.14 (Ne a_4 a_7)) % 5.92/6.14 (Ne a_4 a_8)) % 5.92/6.14 (Ne a_4 Xee)) % 5.92/6.14 (Ne a_4 Xh)) % 5.92/6.14 (Ne a_4 Xhh)) % 5.92/6.14 (Ne a_5 a_6)) % 5.92/6.14 (Ne a_5 a_7)) % 5.92/6.14 (Ne a_5 a_8)) % 5.92/6.14 (Ne a_5 Xee)) % 5.92/6.14 (Ne a_5 Xh)) % 5.92/6.14 (Ne a_5 Xhh)) % 5.92/6.14 (Ne a_6 a_7)) % 5.92/6.14 (Ne a_6 a_8)) % 5.92/6.14 (Ne a_6 Xee)) % 5.92/6.14 (Ne a_6 Xh)) % 5.92/6.14 (Ne a_6 Xhh)) % 5.92/6.14 (Ne a_7 a_8)) % 5.92/6.14 (Ne a_7 Xee)) % 5.92/6.14 (Ne a_7 Xh)) % 5.92/6.14 (Ne a_7 Xhh)) % 5.92/6.14 (Ne a_8 Xee)) % 5.92/6.14 (Ne a_8 Xh)) % 5.92/6.14 (Ne a_8 Xhh)) % 5.92/6.14 (Ne Xee Xh)) % 5.92/6.14 (Ne Xee Xhh)) % 5.92/6.14 (Ne Xh Xhh) → % 5.92/6.14 ∀ (P : Iota → Iota), % 5.92/6.14 And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P a_8) (P Xhh)) → Eq (P a_4) (P a_7)) % 5.92/6.14 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P a_5)) → Ne (P a_6) (P Xee))) % 5.92/6.14 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P a_7))) % 5.92/6.14 (Ne (P a) (P a_3)) → % 5.92/6.14 Ne (P a_8) (P Xhh))) % 5.92/6.14 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P a_7))) (Ne (P a_2) (P a_5)) → Eq (P a_8) (P Xhh))) % 5.92/6.14 (And (And (Eq (P a_8) (P Xee)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P a_7)) → Ne (P a) (P a_3))) % 5.92/6.14 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) (Ne (P a_8) (P Xhh)) → % 5.92/6.14 Eq (P a_6) (P Xee)) → % 5.92/6.14 Or % 5.92/6.14 (Or (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P a_7))) % 5.92/6.14 (Ne (P a_8) (P Xee))) % 5.92/6.14 (Ne (P Xh) (P Xhh))) % 5.92/6.14 False % 5.92/6.14 Clause #11 (by clausification #[10]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 : Iota), % 5.92/6.14 Eq % 5.92/6.14 (Exists fun Xh => % 5.92/6.14 Exists fun Xhh => % 5.92/6.14 And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (And % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_1) % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_2)) % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_3)) % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_4)) % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_5)) % 5.92/6.14 (Ne % 5.92/6.14 a % 5.92/6.14 a_6)) % 5.92/6.14 (Ne a % 5.92/6.14 a_7)) % 5.92/6.14 (Ne a % 5.92/6.14 a_8)) % 5.92/6.14 (Ne a % 5.92/6.14 a_9)) % 5.92/6.14 (Ne a Xh)) % 5.92/6.14 (Ne a Xhh)) % 5.92/6.14 (Ne a_1 a_2)) % 5.92/6.14 (Ne a_1 a_3)) % 5.92/6.14 (Ne a_1 a_4)) % 5.92/6.14 (Ne a_1 a_5)) % 5.92/6.14 (Ne a_1 a_6)) % 5.92/6.14 (Ne a_1 a_7)) % 5.92/6.14 (Ne a_1 a_8)) % 5.92/6.14 (Ne a_1 a_9)) % 5.92/6.14 (Ne a_1 Xh)) % 5.92/6.14 (Ne a_1 Xhh)) % 5.92/6.14 (Ne a_2 a_3)) % 5.92/6.14 (Ne a_2 a_4)) % 5.92/6.14 (Ne a_2 a_5)) % 5.92/6.14 (Ne a_2 a_6)) % 5.92/6.18 (Ne a_2 a_7)) % 5.92/6.18 (Ne a_2 a_8)) % 5.92/6.18 (Ne a_2 a_9)) % 5.92/6.18 (Ne a_2 Xh)) % 5.92/6.18 (Ne a_2 Xhh)) % 5.92/6.18 (Ne a_4 a_5)) % 5.92/6.18 (Ne a_4 a_6)) % 5.92/6.18 (Ne a_4 a_7)) % 5.92/6.18 (Ne a_4 a_8)) % 5.92/6.18 (Ne a_4 a_9)) % 5.92/6.18 (Ne a_4 Xh)) % 5.92/6.18 (Ne a_4 Xhh)) % 5.92/6.18 (Ne a_5 a_6)) % 5.92/6.18 (Ne a_5 a_7)) % 5.92/6.18 (Ne a_5 a_8)) % 5.92/6.18 (Ne a_5 a_9)) % 5.92/6.18 (Ne a_5 Xh)) % 5.92/6.18 (Ne a_5 Xhh)) % 5.92/6.18 (Ne a_6 a_7)) % 5.92/6.18 (Ne a_6 a_8)) % 5.92/6.18 (Ne a_6 a_9)) % 5.92/6.18 (Ne a_6 Xh)) % 5.92/6.18 (Ne a_6 Xhh)) % 5.92/6.18 (Ne a_7 a_8)) % 5.92/6.18 (Ne a_7 a_9)) % 5.92/6.18 (Ne a_7 Xh)) % 5.92/6.18 (Ne a_7 Xhh)) % 5.92/6.18 (Ne a_8 a_9)) % 5.92/6.18 (Ne a_8 Xh)) % 5.92/6.18 (Ne a_8 Xhh)) % 5.92/6.18 (Ne a_9 Xh)) % 5.92/6.18 (Ne a_9 Xhh)) % 5.92/6.18 (Ne Xh Xhh) → % 5.92/6.18 ∀ (P : Iota → Iota), % 5.92/6.18 And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P a_8) (P Xhh)) → Eq (P a_4) (P a_7)) % 5.92/6.18 (And (And (Eq (P a) (P a_1)) (Eq (P Xh) (P Xhh))) (Eq (P a_2) (P a_5)) → Ne (P a_6) (P a_9))) % 5.92/6.18 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P a_7))) % 5.92/6.18 (Ne (P a) (P a_3)) → % 5.92/6.18 Ne (P a_8) (P Xhh))) % 5.92/6.18 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P a_7))) (Ne (P a_2) (P a_5)) → Eq (P a_8) (P Xhh))) % 5.92/6.18 (And (And (Eq (P a_8) (P a_9)) (Eq (P Xh) (P Xhh))) (Eq (P a_4) (P a_7)) → Ne (P a) (P a_3))) % 5.92/6.18 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) (Ne (P a_8) (P Xhh)) → % 5.92/6.18 Eq (P a_6) (P a_9)) → % 5.92/6.18 Or % 5.92/6.18 (Or (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P a_7))) % 5.92/6.18 (Ne (P a_8) (P a_9))) % 5.92/6.18 (Ne (P Xh) (P Xhh))) % 5.92/6.18 False % 5.92/6.18 Clause #12 (by clausification #[11]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 : Iota), % 5.92/6.18 Eq % 5.92/6.18 (Exists fun Xhh => % 5.92/6.18 And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (And % 5.92/6.18 (Ne % 5.92/6.18 a % 5.92/6.18 a_1) % 5.92/6.18 (Ne % 5.92/6.18 a % 5.92/6.18 a_2)) % 5.92/6.18 (Ne % 5.92/6.18 a % 5.92/6.18 a_3)) % 5.92/6.18 (Ne % 5.92/6.18 a % 5.92/6.18 a_4)) % 5.92/6.18 (Ne % 5.92/6.18 a % 5.92/6.18 a_5)) % 5.92/6.18 (Ne a % 5.92/6.18 a_6)) % 5.92/6.18 (Ne a % 5.92/6.18 a_7)) % 5.92/6.18 (Ne a % 5.92/6.18 a_8)) % 5.92/6.18 (Ne a a_9)) % 5.92/6.18 (Ne a a_10)) % 5.92/6.18 (Ne a Xhh)) % 5.92/6.18 (Ne a_1 a_2)) % 5.92/6.18 (Ne a_1 a_3)) % 5.92/6.18 (Ne a_1 a_4)) % 5.92/6.18 (Ne a_1 a_5)) % 5.92/6.18 (Ne a_1 a_6)) % 5.92/6.18 (Ne a_1 a_7)) % 5.92/6.18 (Ne a_1 a_8)) % 5.92/6.18 (Ne a_1 a_9)) % 5.92/6.18 (Ne a_1 a_10)) % 5.92/6.18 (Ne a_1 Xhh)) % 5.92/6.18 (Ne a_2 a_3)) % 5.92/6.18 (Ne a_2 a_4)) % 5.92/6.18 (Ne a_2 a_5)) % 5.92/6.18 (Ne a_2 a_6)) % 5.92/6.18 (Ne a_2 a_7)) % 5.92/6.18 (Ne a_2 a_8)) % 5.92/6.18 (Ne a_2 a_9)) % 5.92/6.18 (Ne a_2 a_10)) % 5.92/6.18 (Ne a_2 Xhh)) % 5.92/6.18 (Ne a_4 a_5)) % 5.92/6.18 (Ne a_4 a_6)) % 5.92/6.18 (Ne a_4 a_7)) % 5.92/6.18 (Ne a_4 a_8)) % 5.92/6.18 (Ne a_4 a_9)) % 6.01/6.23 (Ne a_4 a_10)) % 6.01/6.23 (Ne a_4 Xhh)) % 6.01/6.23 (Ne a_5 a_6)) % 6.01/6.23 (Ne a_5 a_7)) % 6.01/6.23 (Ne a_5 a_8)) % 6.01/6.23 (Ne a_5 a_9)) % 6.01/6.23 (Ne a_5 a_10)) % 6.01/6.23 (Ne a_5 Xhh)) % 6.01/6.23 (Ne a_6 a_7)) % 6.01/6.23 (Ne a_6 a_8)) % 6.01/6.23 (Ne a_6 a_9)) % 6.01/6.23 (Ne a_6 a_10)) % 6.01/6.23 (Ne a_6 Xhh)) % 6.01/6.23 (Ne a_7 a_8)) % 6.01/6.23 (Ne a_7 a_9)) % 6.01/6.23 (Ne a_7 a_10)) % 6.01/6.23 (Ne a_7 Xhh)) % 6.01/6.23 (Ne a_8 a_9)) % 6.01/6.23 (Ne a_8 a_10)) % 6.01/6.23 (Ne a_8 Xhh)) % 6.01/6.23 (Ne a_9 a_10)) % 6.01/6.23 (Ne a_9 Xhh)) % 6.01/6.23 (Ne a_10 Xhh) → % 6.01/6.23 ∀ (P : Iota → Iota), % 6.01/6.23 And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P a_8) (P Xhh)) → Eq (P a_4) (P a_7)) % 6.01/6.23 (And (And (Eq (P a) (P a_1)) (Eq (P a_10) (P Xhh))) (Eq (P a_2) (P a_5)) → Ne (P a_6) (P a_9))) % 6.01/6.23 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P a_7))) (Ne (P a) (P a_3)) → % 6.01/6.23 Ne (P a_8) (P Xhh))) % 6.01/6.23 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P a_7))) (Ne (P a_2) (P a_5)) → Eq (P a_8) (P Xhh))) % 6.01/6.23 (And (And (Eq (P a_8) (P a_9)) (Eq (P a_10) (P Xhh))) (Eq (P a_4) (P a_7)) → Ne (P a) (P a_3))) % 6.01/6.23 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) (Ne (P a_8) (P Xhh)) → % 6.01/6.23 Eq (P a_6) (P a_9)) → % 6.01/6.23 Or % 6.01/6.23 (Or (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P a_7))) % 6.01/6.23 (Ne (P a_8) (P a_9))) % 6.01/6.23 (Ne (P a_10) (P Xhh))) % 6.01/6.23 False % 6.01/6.23 Clause #13 (by clausification #[12]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 6.01/6.23 Eq % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (Ne % 6.01/6.23 a % 6.01/6.23 a_1) % 6.01/6.23 (Ne % 6.01/6.23 a % 6.01/6.23 a_2)) % 6.01/6.23 (Ne % 6.01/6.23 a % 6.01/6.23 a_3)) % 6.01/6.23 (Ne % 6.01/6.23 a % 6.01/6.23 a_4)) % 6.01/6.23 (Ne a % 6.01/6.23 a_5)) % 6.01/6.23 (Ne a % 6.01/6.23 a_6)) % 6.01/6.23 (Ne a % 6.01/6.23 a_7)) % 6.01/6.23 (Ne a a_8)) % 6.01/6.23 (Ne a a_9)) % 6.01/6.23 (Ne a a_10)) % 6.01/6.23 (Ne a a_11)) % 6.01/6.23 (Ne a_1 a_2)) % 6.01/6.23 (Ne a_1 a_3)) % 6.01/6.23 (Ne a_1 a_4)) % 6.01/6.23 (Ne a_1 a_5)) % 6.01/6.23 (Ne a_1 a_6)) % 6.01/6.23 (Ne a_1 a_7)) % 6.01/6.23 (Ne a_1 a_8)) % 6.01/6.23 (Ne a_1 a_9)) % 6.01/6.23 (Ne a_1 a_10)) % 6.01/6.23 (Ne a_1 a_11)) % 6.01/6.23 (Ne a_2 a_3)) % 6.01/6.23 (Ne a_2 a_4)) % 6.01/6.23 (Ne a_2 a_5)) % 6.01/6.23 (Ne a_2 a_6)) % 6.01/6.23 (Ne a_2 a_7)) % 6.01/6.23 (Ne a_2 a_8)) % 6.01/6.23 (Ne a_2 a_9)) % 6.01/6.23 (Ne a_2 a_10)) % 6.01/6.23 (Ne a_2 a_11)) % 6.01/6.23 (Ne a_4 a_5)) % 6.01/6.23 (Ne a_4 a_6)) % 6.01/6.23 (Ne a_4 a_7)) % 6.01/6.23 (Ne a_4 a_8)) % 6.01/6.23 (Ne a_4 a_9)) % 6.01/6.23 (Ne a_4 a_10)) % 6.01/6.23 (Ne a_4 a_11)) % 6.01/6.23 (Ne a_5 a_6)) % 6.01/6.23 (Ne a_5 a_7)) % 6.01/6.23 (Ne a_5 a_8)) % 6.01/6.23 (Ne a_5 a_9)) % 6.01/6.23 (Ne a_5 a_10)) % 6.01/6.23 (Ne a_5 a_11)) % 6.01/6.23 (Ne a_6 a_7)) % 6.01/6.23 (Ne a_6 a_8)) % 6.01/6.23 (Ne a_6 a_9)) % 6.01/6.23 (Ne a_6 a_10)) % 6.01/6.23 (Ne a_6 a_11)) % 6.01/6.23 (Ne a_7 a_8)) % 6.01/6.23 (Ne a_7 a_9)) % 6.01/6.23 (Ne a_7 a_10)) % 6.01/6.23 (Ne a_7 a_11)) % 6.01/6.23 (Ne a_8 a_9)) % 6.01/6.23 (Ne a_8 a_10)) % 6.01/6.23 (Ne a_8 a_11)) % 6.01/6.23 (Ne a_9 a_10)) % 6.01/6.23 (Ne a_9 a_11)) % 6.01/6.23 (Ne a_10 a_11) → % 6.01/6.23 ∀ (P : Iota → Iota), % 6.01/6.23 And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And % 6.01/6.23 (And (And (And (Eq (P a) (P a_1)) (Eq (P a_2) (P a_3))) (Eq (P a_8) (P a_11)) → Eq (P a_4) (P a_7)) % 6.01/6.23 (And (And (Eq (P a) (P a_1)) (Eq (P a_10) (P a_11))) (Eq (P a_2) (P a_5)) → Ne (P a_6) (P a_9))) % 6.01/6.25 (And (And (And (Eq (P a_4) (P a_5)) (Eq (P a_5) (P a_6))) (Eq (P a_6) (P a_7))) (Ne (P a) (P a_3)) → % 6.01/6.25 Ne (P a_8) (P a_11))) % 6.01/6.25 (And (And (Eq (P a) (P a_1)) (Eq (P a_6) (P a_7))) (Ne (P a_2) (P a_5)) → Eq (P a_8) (P a_11))) % 6.01/6.25 (And (And (Eq (P a_8) (P a_9)) (Eq (P a_10) (P a_11))) (Eq (P a_4) (P a_7)) → Ne (P a) (P a_3))) % 6.01/6.25 (And (And (And (Eq (P a_2) (P a_3)) (Eq (P a_3) (P a_4))) (Eq (P a_4) (P a_5))) (Ne (P a_8) (P a_11)) → % 6.01/6.25 Eq (P a_6) (P a_9)) → % 6.01/6.25 Or % 6.01/6.25 (Or (Or (Or (Or (Ne (P a) (P a_1)) (Ne (P a_2) (P a_3))) (Ne (P a_4) (P a_5))) (Ne (P a_6) (P a_7))) % 6.01/6.25 (Ne (P a_8) (P a_9))) % 6.01/6.25 (Ne (P a_10) (P a_11))) % 6.01/6.25 False % 6.01/6.25 Clause #14 (by clausification #[13]): ∀ (a a_1 a_2 a_3 a_4 a_5 a_6 a_7 a_8 a_9 a_10 a_11 : Iota), % 6.01/6.25 Eq % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (And % 6.01/6.25 (Ne % 6.01/6.25 a % 6.01/6.25 a_1) % 6.01/6.25 (Ne % 6.01/6.25 a % 6.01/6.25 a_2)) % 6.01/6.25 (Ne % 6.01/6.25 a % 6.01/6.25 a_3)) % 6.01/6.25 (Ne a % 6.01/6.25 a_4)) % 6.01/6.25 (Ne a % 6.01/6.25 a_5)) % 6.01/6.25 (Ne a % 6.01/6.25 a_6)) % 6.01/6.25 (Ne a a_7)) % 6.01/6.25 (Ne a a_8)) % 6.01/6.25 (Ne a a_9)) % 6.01/6.25 (Ne a a_10)) % 6.01/6.25 (Ne a a_11)) % 6.01/6.25 (Ne a_1 a_2)) % 6.01/6.25 (Ne a_1 a_3)) % 6.01/6.25 (Ne a_1 a_4)) % 6.01/6.25 (Ne a_1 a_5)) % 6.01/6.25 (Ne a_1 a_6)) % 6.01/6.25 (Ne a_1 a_7)) % 6.01/6.25 (Ne a_1 a_8)) % 6.01/6.25 (Ne a_1 a_9)) % 6.01/6.25 (Ne a_1 a_10)) % 6.01/6.25 (Ne a_1 a_11)) % 6.01/6.25 (Ne a_2 a_3)) % 6.01/6.25 (Ne a_2 a_4)) % 6.01/6.25 (Ne a_2 a_5)) % 6.01/6.25 (Ne a_2 a_6)) % 6.01/6.25 (Ne a_2 a_7)) % 6.01/6.25 (Ne a_2 a_8)) % 6.01/6.25 (Ne a_2 a_9)) % 6.01/6.25 (Ne a_2 a_10)) % 6.01/6.25 (Ne a_2 a_11)) % 6.01/6.25 (Ne a_4 a_5)) % 6.01/6.25 (Ne a_4 a_6)) % 6.01/6.25 (Ne a_4 a_7)) % 6.01/6.25 (Ne a_4 a_8)) % 6.01/6.25 (Ne a_4 a_9)) % 6.01/6.25 (Ne a_4 a_10)) % 6.01/6.25 (Ne a_4 a_11)) % 6.01/6.25 (Ne a_5 a_6)) % 6.01/6.25 (Ne a_5 a_7)) % 6.01/6.25 (Ne a_5 a_8)) % 6.01/6.25 (Ne a_5 a_9)) % 6.01/6.25 (Ne a_5 a_10)) % 6.01/6.25 (Ne a_5 a_11)) % 6.01/6.25 (Ne a_6 a_7)) % 6.01/6.25 (Ne a_6 a_8)) % 6.01/6.25 (Ne a_6 a_9)) % 6.01/6.25 (Ne a_6 a_10)) % 6.01/6.25 (Ne a_6 a_11)) % 6.01/6.25 (Ne a_7 a_8)) % 6.01/6.25 (Ne a_7 a_9)) % 6.01/6.25 (Ne a_7 a_10)) % 6.01/6.25 (Ne a_7 a_11)) % 6.01/6.25 (Ne a_8 a_9)) % 6.01/6.25 (Ne a_8 a_10)) % 6.01/6.25 (Ne a_8 a_11)) % 6.01/6.25 (Ne a_9 a_10)) % 6.01/6.25 (Ne a_9 a_11)) % 6.01/6.25 (Ne a_10 a_11)) % 6.01/6.25 True % 6.01/6.25 Clause #16 (by clausification #[14]): ∀ (a a_1 : Iota), Eq (Ne a a_1) True % 6.01/6.25 Clause #18 (by clausification #[16]): ∀ (a a_1 : Iota), Ne a a_1 % 6.01/6.25 Clause #19 (by destructive equality resolution #[18]): False % 6.01/6.25 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------