%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG173+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 07:44:04 PM UTC 2025 % Result : Theorem 6.00s 6.19s % Output : Proof 6.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : ALG173+1 : TPTP v9.2.0. Released v2.7.0. % 0.04/0.13 % Command : duper %s % 0.14/0.34 % Computer : n016.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 09:30:53 EDT 2025 % 0.14/0.35 % CPUTime : % 6.00/6.19 SZS status Theorem for theBenchmark.p % 6.00/6.19 SZS output start Proof for theBenchmark.p % 6.00/6.19 Clause #0 (by assumption #[]): Eq % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (And % 6.00/6.19 (Or % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 6.00/6.19 (Eq (op e0 e0) e3)) % 6.00/6.19 (Eq (op e0 e0) e4)) % 6.00/6.19 (Or % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 6.00/6.19 (Eq (op e0 e1) e3)) % 6.00/6.19 (Eq (op e0 e1) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 6.00/6.19 (Eq (op e0 e2) e3)) % 6.00/6.19 (Eq (op e0 e2) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 6.00/6.19 (Eq (op e0 e3) e3)) % 6.00/6.19 (Eq (op e0 e3) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 6.00/6.19 (Eq (op e0 e4) e3)) % 6.00/6.19 (Eq (op e0 e4) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 6.00/6.19 (Eq (op e1 e0) e3)) % 6.00/6.19 (Eq (op e1 e0) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 6.00/6.19 (Eq (op e1 e1) e3)) % 6.00/6.19 (Eq (op e1 e1) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 6.00/6.19 (Eq (op e1 e2) e3)) % 6.00/6.19 (Eq (op e1 e2) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 6.00/6.19 (Eq (op e1 e3) e3)) % 6.00/6.19 (Eq (op e1 e3) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 6.00/6.19 (Eq (op e1 e4) e3)) % 6.00/6.19 (Eq (op e1 e4) e4))) % 6.00/6.19 (Or % 6.00/6.19 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) % 6.00/6.19 (Eq (op e2 e0) e3)) % 6.00/6.19 (Eq (op e2 e0) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) % 6.08/6.25 (Eq (op e2 e1) e3)) % 6.08/6.25 (Eq (op e2 e1) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 6.08/6.25 (Eq (op e2 e2) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 6.08/6.25 (Eq (op e2 e3) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 6.08/6.25 (Eq (op e2 e4) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 6.08/6.25 (Eq (op e3 e0) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 6.08/6.25 (Eq (op e3 e1) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 6.08/6.25 (Eq (op e3 e2) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 6.08/6.25 (Eq (op e3 e3) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 6.08/6.25 (Eq (op e3 e4) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 6.08/6.25 (Eq (op e4 e0) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 6.08/6.25 (Eq (op e4 e1) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) % 6.08/6.25 (Eq (op e4 e2) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) (Eq (op e4 e3) e3)) % 6.08/6.25 (Eq (op e4 e3) e4))) % 6.08/6.25 (Or (Or (Or (Or (Eq (op e4 e4) e0) (Eq (op e4 e4) e1)) (Eq (op e4 e4) e2)) (Eq (op e4 e4) e3)) (Eq (op e4 e4) e4))) % 6.08/6.25 True % 6.08/6.25 Clause #1 (by assumption #[]): Eq % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (And % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Eq % 6.08/6.25 (op e0 e0) % 6.08/6.25 e0) % 6.08/6.25 (Eq % 6.08/6.25 (op e0 e1) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e0 e2) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e0 e3) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e0 e4) % 6.08/6.25 e0)) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Eq % 6.08/6.25 (op e0 e0) % 6.08/6.25 e0) % 6.08/6.25 (Eq % 6.08/6.25 (op e1 e0) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e2 e0) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e3 e0) % 6.08/6.25 e0)) % 6.08/6.25 (Eq (op e4 e0) % 6.08/6.25 e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Eq (op e0 e0) % 6.08/6.25 e1) % 6.08/6.25 (Eq (op e0 e1) % 6.08/6.25 e1)) % 6.08/6.25 (Eq (op e0 e2) % 6.08/6.25 e1)) % 6.08/6.25 (Eq (op e0 e3) % 6.08/6.25 e1)) % 6.08/6.25 (Eq (op e0 e4) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Eq (op e0 e0) % 6.08/6.25 e1) % 6.08/6.25 (Eq (op e1 e0) % 6.08/6.25 e1)) % 6.08/6.25 (Eq (op e2 e0) % 6.08/6.25 e1)) % 6.08/6.25 (Eq (op e3 e0) e1)) % 6.08/6.25 (Eq (op e4 e0) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Eq (op e0 e0) e2) % 6.08/6.25 (Eq (op e0 e1) % 6.08/6.25 e2)) % 6.08/6.25 (Eq (op e0 e2) e2)) % 6.08/6.25 (Eq (op e0 e3) e2)) % 6.08/6.25 (Eq (op e0 e4) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e0) e2) % 6.08/6.25 (Eq (op e1 e0) e2)) % 6.08/6.25 (Eq (op e2 e0) e2)) % 6.08/6.25 (Eq (op e3 e0) e2)) % 6.08/6.25 (Eq (op e4 e0) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e0) e3) % 6.08/6.25 (Eq (op e0 e1) e3)) % 6.08/6.25 (Eq (op e0 e2) e3)) % 6.08/6.25 (Eq (op e0 e3) e3)) % 6.08/6.25 (Eq (op e0 e4) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e0) e3) % 6.08/6.25 (Eq (op e1 e0) e3)) % 6.08/6.25 (Eq (op e2 e0) e3)) % 6.08/6.25 (Eq (op e3 e0) e3)) % 6.08/6.25 (Eq (op e4 e0) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e0) e4) % 6.08/6.25 (Eq (op e0 e1) e4)) % 6.08/6.25 (Eq (op e0 e2) e4)) % 6.08/6.25 (Eq (op e0 e3) e4)) % 6.08/6.25 (Eq (op e0 e4) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e0) e4) % 6.08/6.25 (Eq (op e1 e0) e4)) % 6.08/6.25 (Eq (op e2 e0) e4)) % 6.08/6.25 (Eq (op e3 e0) e4)) % 6.08/6.25 (Eq (op e4 e0) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e1 e0) e0) % 6.08/6.25 (Eq (op e1 e1) e0)) % 6.08/6.25 (Eq (op e1 e2) e0)) % 6.08/6.25 (Eq (op e1 e3) e0)) % 6.08/6.25 (Eq (op e1 e4) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e1) e0) % 6.08/6.25 (Eq (op e1 e1) e0)) % 6.08/6.25 (Eq (op e2 e1) e0)) % 6.08/6.25 (Eq (op e3 e1) e0)) % 6.08/6.25 (Eq (op e4 e1) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e1 e0) e1) % 6.08/6.25 (Eq (op e1 e1) e1)) % 6.08/6.25 (Eq (op e1 e2) e1)) % 6.08/6.25 (Eq (op e1 e3) e1)) % 6.08/6.25 (Eq (op e1 e4) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e1) e1) % 6.08/6.25 (Eq (op e1 e1) e1)) % 6.08/6.25 (Eq (op e2 e1) e1)) % 6.08/6.25 (Eq (op e3 e1) e1)) % 6.08/6.25 (Eq (op e4 e1) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e1 e0) e2) % 6.08/6.25 (Eq (op e1 e1) e2)) % 6.08/6.25 (Eq (op e1 e2) e2)) % 6.08/6.25 (Eq (op e1 e3) e2)) % 6.08/6.25 (Eq (op e1 e4) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 6.08/6.25 (Eq (op e2 e1) e2)) % 6.08/6.25 (Eq (op e3 e1) e2)) % 6.08/6.25 (Eq (op e4 e1) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 6.08/6.25 (Eq (op e1 e2) e3)) % 6.08/6.25 (Eq (op e1 e3) e3)) % 6.08/6.25 (Eq (op e1 e4) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 6.08/6.25 (Eq (op e2 e1) e3)) % 6.08/6.25 (Eq (op e3 e1) e3)) % 6.08/6.25 (Eq (op e4 e1) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 6.08/6.25 (Eq (op e1 e2) e4)) % 6.08/6.25 (Eq (op e1 e3) e4)) % 6.08/6.25 (Eq (op e1 e4) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 6.08/6.25 (Eq (op e2 e1) e4)) % 6.08/6.25 (Eq (op e3 e1) e4)) % 6.08/6.25 (Eq (op e4 e1) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 6.08/6.25 (Eq (op e2 e2) e0)) % 6.08/6.25 (Eq (op e2 e3) e0)) % 6.08/6.25 (Eq (op e2 e4) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 6.08/6.25 (Eq (op e2 e2) e0)) % 6.08/6.25 (Eq (op e3 e2) e0)) % 6.08/6.25 (Eq (op e4 e2) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 6.08/6.25 (Eq (op e2 e2) e1)) % 6.08/6.25 (Eq (op e2 e3) e1)) % 6.08/6.25 (Eq (op e2 e4) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 6.08/6.25 (Eq (op e2 e2) e1)) % 6.08/6.25 (Eq (op e3 e2) e1)) % 6.08/6.25 (Eq (op e4 e2) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) % 6.08/6.25 (Eq (op e2 e2) e2)) % 6.08/6.25 (Eq (op e2 e3) e2)) % 6.08/6.25 (Eq (op e2 e4) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) % 6.08/6.25 (Eq (op e2 e2) e2)) % 6.08/6.25 (Eq (op e3 e2) e2)) % 6.08/6.25 (Eq (op e4 e2) e2))) % 6.08/6.25 (Or % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 6.08/6.25 (Eq (op e2 e3) e3)) % 6.08/6.25 (Eq (op e2 e4) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 6.08/6.25 (Eq (op e3 e2) e3)) % 6.08/6.25 (Eq (op e4 e2) e3))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 6.08/6.25 (Eq (op e2 e3) e4)) % 6.08/6.25 (Eq (op e2 e4) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 6.08/6.25 (Eq (op e3 e2) e4)) % 6.08/6.25 (Eq (op e4 e2) e4))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 6.08/6.25 (Eq (op e3 e3) e0)) % 6.08/6.25 (Eq (op e3 e4) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 6.08/6.25 (Eq (op e3 e3) e0)) % 6.08/6.25 (Eq (op e4 e3) e0))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 6.08/6.25 (Eq (op e3 e3) e1)) % 6.08/6.25 (Eq (op e3 e4) e1))) % 6.08/6.25 (Or % 6.08/6.25 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 6.08/6.25 (Eq (op e3 e3) e1)) % 6.08/6.25 (Eq (op e4 e3) e1))) % 6.08/6.26 (Or % 6.08/6.26 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 6.08/6.26 (Eq (op e3 e3) e2)) % 6.08/6.26 (Eq (op e3 e4) e2))) % 6.08/6.26 (Or % 6.08/6.26 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) % 6.08/6.26 (Eq (op e3 e3) e2)) % 6.08/6.26 (Eq (op e4 e3) e2))) % 6.08/6.26 (Or % 6.08/6.26 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) % 6.08/6.26 (Eq (op e3 e3) e3)) % 6.08/6.26 (Eq (op e3 e4) e3))) % 6.08/6.26 (Or % 6.08/6.26 (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 6.08/6.26 (Eq (op e4 e3) e3))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 6.08/6.26 (Eq (op e3 e4) e4))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 6.08/6.26 (Eq (op e4 e3) e4))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 6.08/6.26 (Eq (op e4 e4) e0))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 6.08/6.26 (Eq (op e4 e4) e0))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 6.08/6.26 (Eq (op e4 e4) e1))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 6.08/6.26 (Eq (op e4 e4) e1))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 6.08/6.26 (Eq (op e4 e4) e2))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 6.08/6.26 (Eq (op e4 e4) e2))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 6.08/6.26 (Eq (op e4 e4) e3))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) % 6.08/6.26 (Eq (op e4 e4) e3))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) (Eq (op e4 e3) e4)) % 6.08/6.26 (Eq (op e4 e4) e4))) % 6.08/6.26 (Or (Or (Or (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) (Eq (op e2 e4) e4)) (Eq (op e3 e4) e4)) (Eq (op e4 e4) e4))) % 6.08/6.26 True % 6.08/6.26 Clause #2 (by assumption #[]): Eq % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And % 6.08/6.26 (And (Eq (op (op e0 e0) (op e0 e0)) e0) % 6.08/6.26 (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.08/6.26 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.08/6.26 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.08/6.26 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.08/6.26 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.08/6.26 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.08/6.26 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.08/6.29 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.08/6.29 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.08/6.29 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.08/6.29 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.08/6.29 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.08/6.29 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.08/6.29 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.08/6.29 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.08/6.29 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.08/6.29 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.08/6.29 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.08/6.29 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.08/6.29 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 6.08/6.29 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 6.08/6.29 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 6.08/6.29 (Eq (op (op e3 e4) (op e4 e3)) e4)) % 6.08/6.29 (Eq (op (op e4 e4) (op e4 e4)) e4)) % 6.08/6.29 True % 6.08/6.29 Clause #3 (by assumption #[]): Eq % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (And % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e0)) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e0) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e0))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e0 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e1 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e2 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e1))) % 6.08/6.29 (Ne % 6.08/6.29 (op % 6.08/6.29 e3 % 6.08/6.29 e1) % 6.08/6.29 (op % 6.08/6.29 e4 % 6.08/6.29 e1))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e2) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e2))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e3) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e3))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e4) % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e4) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e4) % 6.08/6.30 (op % 6.08/6.30 e3 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e0 % 6.08/6.30 e4) % 6.08/6.30 (op % 6.08/6.30 e4 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op % 6.08/6.30 e1 % 6.08/6.30 e4) % 6.08/6.30 (op % 6.08/6.30 e2 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op e1 % 6.08/6.30 e4) % 6.08/6.30 (op e3 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op e1 % 6.08/6.30 e4) % 6.08/6.30 (op e4 % 6.08/6.30 e4))) % 6.08/6.30 (Ne % 6.08/6.30 (op e2 e4) % 6.08/6.30 (op e3 % 6.08/6.30 e4))) % 6.08/6.30 (Ne (op e2 e4) % 6.08/6.30 (op e4 e4))) % 6.08/6.30 (Ne (op e3 e4) % 6.08/6.30 (op e4 e4))) % 6.08/6.30 (Ne (op e0 e0) % 6.08/6.30 (op e0 e1))) % 6.08/6.30 (Ne (op e0 e0) % 6.08/6.30 (op e0 e2))) % 6.08/6.30 (Ne (op e0 e0) % 6.08/6.30 (op e0 e3))) % 6.08/6.30 (Ne (op e0 e0) % 6.08/6.30 (op e0 e4))) % 6.08/6.30 (Ne (op e0 e1) % 6.08/6.30 (op e0 e2))) % 6.08/6.30 (Ne (op e0 e1) (op e0 e3))) % 6.08/6.30 (Ne (op e0 e1) (op e0 e4))) % 6.08/6.30 (Ne (op e0 e2) (op e0 e3))) % 6.08/6.30 (Ne (op e0 e2) (op e0 e4))) % 6.08/6.30 (Ne (op e0 e3) (op e0 e4))) % 6.08/6.30 (Ne (op e1 e0) (op e1 e1))) % 6.08/6.30 (Ne (op e1 e0) (op e1 e2))) % 6.08/6.30 (Ne (op e1 e0) (op e1 e3))) % 6.08/6.30 (Ne (op e1 e0) (op e1 e4))) % 6.08/6.30 (Ne (op e1 e1) (op e1 e2))) % 6.08/6.30 (Ne (op e1 e1) (op e1 e3))) % 6.08/6.30 (Ne (op e1 e1) (op e1 e4))) % 6.08/6.30 (Ne (op e1 e2) (op e1 e3))) % 6.08/6.30 (Ne (op e1 e2) (op e1 e4))) % 6.08/6.30 (Ne (op e1 e3) (op e1 e4))) % 6.08/6.30 (Ne (op e2 e0) (op e2 e1))) % 6.08/6.30 (Ne (op e2 e0) (op e2 e2))) % 6.08/6.30 (Ne (op e2 e0) (op e2 e3))) % 6.08/6.30 (Ne (op e2 e0) (op e2 e4))) % 6.08/6.30 (Ne (op e2 e1) (op e2 e2))) % 6.08/6.30 (Ne (op e2 e1) (op e2 e3))) % 6.08/6.30 (Ne (op e2 e1) (op e2 e4))) % 6.08/6.30 (Ne (op e2 e2) (op e2 e3))) % 6.08/6.30 (Ne (op e2 e2) (op e2 e4))) % 6.08/6.30 (Ne (op e2 e3) (op e2 e4))) % 6.08/6.30 (Ne (op e3 e0) (op e3 e1))) % 6.08/6.30 (Ne (op e3 e0) (op e3 e2))) % 6.08/6.30 (Ne (op e3 e0) (op e3 e3))) % 6.08/6.30 (Ne (op e3 e0) (op e3 e4))) % 6.08/6.30 (Ne (op e3 e1) (op e3 e2))) % 6.08/6.30 (Ne (op e3 e1) (op e3 e3))) % 6.08/6.30 (Ne (op e3 e1) (op e3 e4))) % 6.08/6.30 (Ne (op e3 e2) (op e3 e3))) % 6.08/6.30 (Ne (op e3 e2) (op e3 e4))) % 6.08/6.30 (Ne (op e3 e3) (op e3 e4))) % 6.08/6.30 (Ne (op e4 e0) (op e4 e1))) % 6.15/6.31 (Ne (op e4 e0) (op e4 e2))) % 6.15/6.31 (Ne (op e4 e0) (op e4 e3))) % 6.15/6.31 (Ne (op e4 e0) (op e4 e4))) % 6.15/6.31 (Ne (op e4 e1) (op e4 e2))) % 6.15/6.31 (Ne (op e4 e1) (op e4 e3))) % 6.15/6.31 (Ne (op e4 e1) (op e4 e4))) % 6.15/6.31 (Ne (op e4 e2) (op e4 e3))) % 6.15/6.31 (Ne (op e4 e2) (op e4 e4))) % 6.15/6.31 (Ne (op e4 e3) (op e4 e4))) % 6.15/6.31 True % 6.15/6.31 Clause #4 (by assumption #[]): Eq % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) (Ne e1 e3)) (Ne e1 e4)) % 6.15/6.31 (Ne e2 e3)) % 6.15/6.31 (Ne e2 e4)) % 6.15/6.31 (Ne e3 e4)) % 6.15/6.31 True % 6.15/6.31 Clause #5 (by assumption #[]): Eq % 6.15/6.31 (And % 6.15/6.31 (And (And (Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3)))) (Eq e1 (op e3 (op e3 (op e3 e3))))) (Eq e2 (op e3 e3))) % 6.15/6.31 (Eq e4 (op e3 (op e3 e3)))) % 6.15/6.31 True % 6.15/6.31 Clause #6 (by assumption #[]): Eq % 6.15/6.31 (Not % 6.15/6.31 (Not % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (Or % 6.15/6.31 (Or % 6.15/6.31 (Or % 6.15/6.31 (Or % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 6.15/6.31 (Ne (op e0 e2) e2)) % 6.15/6.31 (Ne (op e0 e3) e3)) % 6.15/6.31 (Ne (op e0 e4) e4)) % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 6.15/6.31 (Ne (op e1 e2) e2)) % 6.15/6.31 (Ne (op e1 e3) e3)) % 6.15/6.31 (Ne (op e1 e4) e4))) % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 6.15/6.31 (Ne (op e2 e2) e2)) % 6.15/6.31 (Ne (op e2 e3) e3)) % 6.15/6.31 (Ne (op e2 e4) e4))) % 6.15/6.31 (And % 6.15/6.31 (And % 6.15/6.31 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 6.15/6.31 (Ne (op e3 e2) e2)) % 6.15/6.31 (Ne (op e3 e3) e3)) % 6.15/6.31 (Ne (op e3 e4) e4))) % 6.15/6.31 (And % 6.15/6.35 (And % 6.15/6.35 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 6.15/6.35 (Ne (op e4 e2) e2)) % 6.15/6.35 (Ne (op e4 e3) e3)) % 6.15/6.35 (Ne (op e4 e4) e4))) % 6.15/6.35 (Eq (op e0 (op e0 e0)) e0)) % 6.15/6.35 (Eq (op e0 (op e0 e1)) e1)) % 6.15/6.35 (Eq (op e0 (op e0 e2)) e2)) % 6.15/6.35 (Eq (op e0 (op e0 e3)) e3)) % 6.15/6.35 (Eq (op e0 (op e0 e4)) e4)) % 6.15/6.35 (Eq (op e1 (op e1 e0)) e0)) % 6.15/6.35 (Eq (op e1 (op e1 e1)) e1)) % 6.15/6.35 (Eq (op e1 (op e1 e2)) e2)) % 6.15/6.35 (Eq (op e1 (op e1 e3)) e3)) % 6.15/6.35 (Eq (op e1 (op e1 e4)) e4)) % 6.15/6.35 (Eq (op e2 (op e2 e0)) e0)) % 6.15/6.35 (Eq (op e2 (op e2 e1)) e1)) % 6.15/6.35 (Eq (op e2 (op e2 e2)) e2)) % 6.15/6.35 (Eq (op e2 (op e2 e3)) e3)) % 6.15/6.35 (Eq (op e2 (op e2 e4)) e4)) % 6.15/6.35 (Eq (op e3 (op e3 e0)) e0)) % 6.15/6.35 (Eq (op e3 (op e3 e1)) e1)) % 6.15/6.35 (Eq (op e3 (op e3 e2)) e2)) % 6.15/6.35 (Eq (op e3 (op e3 e3)) e3)) % 6.15/6.35 (Eq (op e3 (op e3 e4)) e4)) % 6.15/6.35 (Eq (op e4 (op e4 e0)) e0)) % 6.15/6.35 (Eq (op e4 (op e4 e1)) e1)) % 6.15/6.35 (Eq (op e4 (op e4 e2)) e2)) % 6.15/6.35 (Eq (op e4 (op e4 e3)) e3)) % 6.15/6.35 (Eq (op e4 (op e4 e4)) e4)))) % 6.15/6.35 True % 6.15/6.35 Clause #7 (by clausification #[5]): Eq (Eq e4 (op e3 (op e3 e3))) True % 6.15/6.35 Clause #8 (by clausification #[5]): Eq (And (And (Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3)))) (Eq e1 (op e3 (op e3 (op e3 e3))))) (Eq e2 (op e3 e3))) % 6.15/6.35 True % 6.15/6.35 Clause #9 (by clausification #[7]): Eq e4 (op e3 (op e3 e3)) % 6.15/6.35 Clause #10 (by clausification #[8]): Eq (Eq e2 (op e3 e3)) True % 6.15/6.35 Clause #11 (by clausification #[8]): Eq (And (Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3)))) (Eq e1 (op e3 (op e3 (op e3 e3))))) True % 6.15/6.35 Clause #12 (by clausification #[10]): Eq e2 (op e3 e3) % 6.15/6.35 Clause #13 (by backward demodulation #[12, 9]): Eq e4 (op e3 e2) % 6.15/6.35 Clause #14 (by clausification #[11]): Eq (Eq e1 (op e3 (op e3 (op e3 e3)))) True % 6.15/6.35 Clause #15 (by clausification #[11]): Eq (Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3)))) True % 6.15/6.35 Clause #16 (by clausification #[14]): Eq e1 (op e3 (op e3 (op e3 e3))) % 6.15/6.35 Clause #17 (by forward demodulation #[16, 12]): Eq e1 (op e3 (op e3 e2)) % 6.15/6.35 Clause #18 (by forward demodulation #[17, 13]): Eq e1 (op e3 e4) % 6.15/6.35 Clause #19 (by clausification #[15]): Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3))) % 6.15/6.35 Clause #20 (by forward demodulation #[19, 12]): Eq e0 (op (op e3 (op e3 e3)) (op e3 e2)) % 6.15/6.35 Clause #21 (by forward demodulation #[20, 13]): Eq e0 (op (op e3 (op e3 e3)) e4) % 6.15/6.35 Clause #22 (by forward demodulation #[21, 12]): Eq e0 (op (op e3 e2) e4) % 6.15/6.35 Clause #23 (by forward demodulation #[22, 13]): Eq e0 (op e4 e4) % 6.15/6.35 Clause #25 (by clausification #[0]): Eq % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (And % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 6.15/6.35 (Eq (op e0 e0) e3)) % 6.15/6.35 (Eq (op e0 e0) e4)) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 6.15/6.35 (Eq (op e0 e1) e3)) % 6.15/6.35 (Eq (op e0 e1) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 6.15/6.35 (Eq (op e0 e2) e3)) % 6.15/6.35 (Eq (op e0 e2) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 6.15/6.35 (Eq (op e0 e3) e3)) % 6.15/6.35 (Eq (op e0 e3) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 6.15/6.35 (Eq (op e0 e4) e3)) % 6.15/6.35 (Eq (op e0 e4) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 6.15/6.35 (Eq (op e1 e0) e3)) % 6.15/6.35 (Eq (op e1 e0) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 6.15/6.35 (Eq (op e1 e1) e3)) % 6.15/6.35 (Eq (op e1 e1) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 6.15/6.35 (Eq (op e1 e2) e3)) % 6.15/6.35 (Eq (op e1 e2) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 6.15/6.35 (Eq (op e1 e3) e3)) % 6.15/6.35 (Eq (op e1 e3) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 6.15/6.35 (Eq (op e1 e4) e3)) % 6.15/6.35 (Eq (op e1 e4) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) % 6.15/6.35 (Eq (op e2 e0) e3)) % 6.15/6.35 (Eq (op e2 e0) e4))) % 6.15/6.35 (Or % 6.15/6.35 (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) (Eq (op e2 e1) e3)) % 6.15/6.35 (Eq (op e2 e1) e4))) % 6.15/6.35 (Or (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 6.15/6.35 (Eq (op e2 e2) e4))) % 6.15/6.35 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 6.15/6.35 (Eq (op e2 e3) e4))) % 6.15/6.35 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 6.15/6.35 (Eq (op e2 e4) e4))) % 6.15/6.35 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 6.15/6.35 (Eq (op e3 e0) e4))) % 6.15/6.35 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 6.15/6.35 (Eq (op e3 e1) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 6.20/6.42 (Eq (op e3 e2) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 6.20/6.42 (Eq (op e3 e3) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 6.20/6.42 (Eq (op e3 e4) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 6.20/6.42 (Eq (op e4 e0) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 6.20/6.42 (Eq (op e4 e1) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) % 6.20/6.42 (Eq (op e4 e2) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) (Eq (op e4 e3) e3)) (Eq (op e4 e3) e4))) % 6.20/6.42 True % 6.20/6.42 Clause #39 (by clausification #[4]): Eq (Ne e3 e4) True % 6.20/6.42 Clause #40 (by clausification #[4]): Eq % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) (Ne e1 e3)) (Ne e1 e4)) % 6.20/6.42 (Ne e2 e3)) % 6.20/6.42 (Ne e2 e4)) % 6.20/6.42 True % 6.20/6.42 Clause #41 (by clausification #[39]): Ne e3 e4 % 6.20/6.42 Clause #42 (by clausification #[40]): Eq (Ne e2 e4) True % 6.20/6.42 Clause #43 (by clausification #[40]): Eq % 6.20/6.42 (And (And (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) (Ne e1 e3)) (Ne e1 e4)) % 6.20/6.42 (Ne e2 e3)) % 6.20/6.42 True % 6.20/6.42 Clause #44 (by clausification #[42]): Ne e2 e4 % 6.20/6.42 Clause #45 (by clausification #[43]): Eq (Ne e2 e3) True % 6.20/6.42 Clause #46 (by clausification #[43]): Eq (And (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) (Ne e1 e3)) (Ne e1 e4)) True % 6.20/6.42 Clause #47 (by clausification #[45]): Ne e2 e3 % 6.20/6.42 Clause #48 (by clausification #[46]): Eq (Ne e1 e4) True % 6.20/6.42 Clause #49 (by clausification #[46]): Eq (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) (Ne e1 e3)) True % 6.20/6.42 Clause #50 (by clausification #[48]): Ne e1 e4 % 6.20/6.42 Clause #51 (by clausification #[49]): Eq (Ne e1 e3) True % 6.20/6.42 Clause #52 (by clausification #[49]): Eq (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) (Ne e1 e2)) True % 6.20/6.42 Clause #53 (by clausification #[51]): Ne e1 e3 % 6.20/6.42 Clause #54 (by clausification #[1]): Eq (Or (Or (Or (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) (Eq (op e2 e4) e4)) (Eq (op e3 e4) e4)) (Eq (op e4 e4) e4)) % 6.20/6.42 True % 6.20/6.42 Clause #55 (by clausification #[1]): Eq % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (And % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Eq (op e0 e0) % 6.20/6.42 e0) % 6.20/6.42 (Eq (op e0 e1) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e0 e2) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e0 e3) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e0 e4) e0)) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Eq (op e0 e0) % 6.20/6.42 e0) % 6.20/6.42 (Eq (op e1 e0) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e2 e0) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e3 e0) % 6.20/6.42 e0)) % 6.20/6.42 (Eq (op e4 e0) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Eq (op e0 e0) % 6.20/6.42 e1) % 6.20/6.42 (Eq (op e0 e1) % 6.20/6.42 e1)) % 6.20/6.42 (Eq (op e0 e2) % 6.20/6.42 e1)) % 6.20/6.42 (Eq (op e0 e3) e1)) % 6.20/6.42 (Eq (op e0 e4) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Eq (op e0 e0) e1) % 6.20/6.42 (Eq (op e1 e0) % 6.20/6.42 e1)) % 6.20/6.42 (Eq (op e2 e0) e1)) % 6.20/6.42 (Eq (op e3 e0) e1)) % 6.20/6.42 (Eq (op e4 e0) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e2) % 6.20/6.42 (Eq (op e0 e1) e2)) % 6.20/6.42 (Eq (op e0 e2) e2)) % 6.20/6.42 (Eq (op e0 e3) e2)) % 6.20/6.42 (Eq (op e0 e4) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e2) % 6.20/6.42 (Eq (op e1 e0) e2)) % 6.20/6.42 (Eq (op e2 e0) e2)) % 6.20/6.42 (Eq (op e3 e0) e2)) % 6.20/6.42 (Eq (op e4 e0) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e3) % 6.20/6.42 (Eq (op e0 e1) e3)) % 6.20/6.42 (Eq (op e0 e2) e3)) % 6.20/6.42 (Eq (op e0 e3) e3)) % 6.20/6.42 (Eq (op e0 e4) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e3) % 6.20/6.42 (Eq (op e1 e0) e3)) % 6.20/6.42 (Eq (op e2 e0) e3)) % 6.20/6.42 (Eq (op e3 e0) e3)) % 6.20/6.42 (Eq (op e4 e0) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e4) % 6.20/6.42 (Eq (op e0 e1) e4)) % 6.20/6.42 (Eq (op e0 e2) e4)) % 6.20/6.42 (Eq (op e0 e3) e4)) % 6.20/6.42 (Eq (op e0 e4) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e0) e4) % 6.20/6.42 (Eq (op e1 e0) e4)) % 6.20/6.42 (Eq (op e2 e0) e4)) % 6.20/6.42 (Eq (op e3 e0) e4)) % 6.20/6.42 (Eq (op e4 e0) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e1 e0) e0) % 6.20/6.42 (Eq (op e1 e1) e0)) % 6.20/6.42 (Eq (op e1 e2) e0)) % 6.20/6.42 (Eq (op e1 e3) e0)) % 6.20/6.42 (Eq (op e1 e4) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e1) e0) % 6.20/6.42 (Eq (op e1 e1) e0)) % 6.20/6.42 (Eq (op e2 e1) e0)) % 6.20/6.42 (Eq (op e3 e1) e0)) % 6.20/6.42 (Eq (op e4 e1) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e1 e0) e1) % 6.20/6.42 (Eq (op e1 e1) e1)) % 6.20/6.42 (Eq (op e1 e2) e1)) % 6.20/6.42 (Eq (op e1 e3) e1)) % 6.20/6.42 (Eq (op e1 e4) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e0 e1) e1) % 6.20/6.42 (Eq (op e1 e1) e1)) % 6.20/6.42 (Eq (op e2 e1) e1)) % 6.20/6.42 (Eq (op e3 e1) e1)) % 6.20/6.42 (Eq (op e4 e1) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 6.20/6.42 (Eq (op e1 e2) e2)) % 6.20/6.42 (Eq (op e1 e3) e2)) % 6.20/6.42 (Eq (op e1 e4) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 6.20/6.42 (Eq (op e2 e1) e2)) % 6.20/6.42 (Eq (op e3 e1) e2)) % 6.20/6.42 (Eq (op e4 e1) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 6.20/6.42 (Eq (op e1 e2) e3)) % 6.20/6.42 (Eq (op e1 e3) e3)) % 6.20/6.42 (Eq (op e1 e4) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 6.20/6.42 (Eq (op e2 e1) e3)) % 6.20/6.42 (Eq (op e3 e1) e3)) % 6.20/6.42 (Eq (op e4 e1) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 6.20/6.42 (Eq (op e1 e2) e4)) % 6.20/6.42 (Eq (op e1 e3) e4)) % 6.20/6.42 (Eq (op e1 e4) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 6.20/6.42 (Eq (op e2 e1) e4)) % 6.20/6.42 (Eq (op e3 e1) e4)) % 6.20/6.42 (Eq (op e4 e1) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 6.20/6.42 (Eq (op e2 e2) e0)) % 6.20/6.42 (Eq (op e2 e3) e0)) % 6.20/6.42 (Eq (op e2 e4) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 6.20/6.42 (Eq (op e2 e2) e0)) % 6.20/6.42 (Eq (op e3 e2) e0)) % 6.20/6.42 (Eq (op e4 e2) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 6.20/6.42 (Eq (op e2 e2) e1)) % 6.20/6.42 (Eq (op e2 e3) e1)) % 6.20/6.42 (Eq (op e2 e4) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 6.20/6.42 (Eq (op e2 e2) e1)) % 6.20/6.42 (Eq (op e3 e2) e1)) % 6.20/6.42 (Eq (op e4 e2) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) % 6.20/6.42 (Eq (op e2 e2) e2)) % 6.20/6.42 (Eq (op e2 e3) e2)) % 6.20/6.42 (Eq (op e2 e4) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 6.20/6.42 (Eq (op e3 e2) e2)) % 6.20/6.42 (Eq (op e4 e2) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 6.20/6.42 (Eq (op e2 e3) e3)) % 6.20/6.42 (Eq (op e2 e4) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 6.20/6.42 (Eq (op e3 e2) e3)) % 6.20/6.42 (Eq (op e4 e2) e3))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 6.20/6.42 (Eq (op e2 e3) e4)) % 6.20/6.42 (Eq (op e2 e4) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 6.20/6.42 (Eq (op e3 e2) e4)) % 6.20/6.42 (Eq (op e4 e2) e4))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 6.20/6.42 (Eq (op e3 e3) e0)) % 6.20/6.42 (Eq (op e3 e4) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 6.20/6.42 (Eq (op e3 e3) e0)) % 6.20/6.42 (Eq (op e4 e3) e0))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 6.20/6.42 (Eq (op e3 e3) e1)) % 6.20/6.42 (Eq (op e3 e4) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 6.20/6.42 (Eq (op e3 e3) e1)) % 6.20/6.42 (Eq (op e4 e3) e1))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 6.20/6.42 (Eq (op e3 e3) e2)) % 6.20/6.42 (Eq (op e3 e4) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) % 6.20/6.42 (Eq (op e3 e3) e2)) % 6.20/6.42 (Eq (op e4 e3) e2))) % 6.20/6.42 (Or % 6.20/6.42 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 6.20/6.42 (Eq (op e3 e4) e3))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 6.20/6.42 (Eq (op e4 e3) e3))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 6.20/6.42 (Eq (op e3 e4) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 6.20/6.42 (Eq (op e4 e3) e4))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 6.20/6.42 (Eq (op e4 e4) e0))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 6.20/6.42 (Eq (op e4 e4) e0))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 6.20/6.42 (Eq (op e4 e4) e1))) % 6.20/6.42 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 6.20/6.44 (Eq (op e4 e4) e1))) % 6.20/6.44 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 6.20/6.44 (Eq (op e4 e4) e2))) % 6.20/6.44 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 6.20/6.44 (Eq (op e4 e4) e2))) % 6.20/6.44 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 6.20/6.44 (Eq (op e4 e4) e3))) % 6.20/6.44 (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) % 6.20/6.44 (Eq (op e4 e4) e3))) % 6.20/6.44 (Or (Or (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) (Eq (op e4 e3) e4)) (Eq (op e4 e4) e4))) % 6.20/6.44 True % 6.20/6.44 Clause #56 (by clausification #[54]): Or (Eq (Or (Or (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) (Eq (op e2 e4) e4)) (Eq (op e3 e4) e4)) True) % 6.20/6.44 (Eq (Eq (op e4 e4) e4) True) % 6.20/6.44 Clause #57 (by clausification #[56]): Or (Eq (Eq (op e4 e4) e4) True) % 6.20/6.44 (Or (Eq (Or (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) (Eq (op e2 e4) e4)) True) (Eq (Eq (op e3 e4) e4) True)) % 6.20/6.44 Clause #58 (by clausification #[57]): Or (Eq (Or (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) (Eq (op e2 e4) e4)) True) % 6.20/6.44 (Or (Eq (Eq (op e3 e4) e4) True) (Eq (op e4 e4) e4)) % 6.20/6.44 Clause #59 (by clausification #[58]): Or (Eq (Eq (op e3 e4) e4) True) % 6.20/6.44 (Or (Eq (op e4 e4) e4) (Or (Eq (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) True) (Eq (Eq (op e2 e4) e4) True))) % 6.20/6.44 Clause #60 (by clausification #[59]): Or (Eq (op e4 e4) e4) % 6.20/6.44 (Or (Eq (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) True) (Or (Eq (Eq (op e2 e4) e4) True) (Eq (op e3 e4) e4))) % 6.20/6.44 Clause #61 (by clausification #[60]): Or (Eq (op e4 e4) e4) % 6.20/6.44 (Or (Eq (Eq (op e2 e4) e4) True) % 6.20/6.44 (Or (Eq (op e3 e4) e4) (Or (Eq (Eq (op e0 e4) e4) True) (Eq (Eq (op e1 e4) e4) True)))) % 6.20/6.44 Clause #62 (by clausification #[61]): Or (Eq (op e4 e4) e4) % 6.20/6.44 (Or (Eq (op e3 e4) e4) (Or (Eq (Eq (op e0 e4) e4) True) (Or (Eq (Eq (op e1 e4) e4) True) (Eq (op e2 e4) e4)))) % 6.20/6.44 Clause #63 (by clausification #[62]): Or (Eq (op e4 e4) e4) % 6.20/6.44 (Or (Eq (op e3 e4) e4) (Or (Eq (Eq (op e1 e4) e4) True) (Or (Eq (op e2 e4) e4) (Eq (op e0 e4) e4)))) % 6.20/6.44 Clause #64 (by clausification #[63]): Or (Eq (op e4 e4) e4) (Or (Eq (op e3 e4) e4) (Or (Eq (op e2 e4) e4) (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)))) % 6.20/6.44 Clause #65 (by forward demodulation #[64, 23]): Or (Eq e0 e4) (Or (Eq (op e3 e4) e4) (Or (Eq (op e2 e4) e4) (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)))) % 6.20/6.44 Clause #66 (by forward demodulation #[65, 18]): Or (Eq e0 e4) (Or (Eq e1 e4) (Or (Eq (op e2 e4) e4) (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)))) % 6.20/6.44 Clause #67 (by forward contextual literal cutting #[66, 50]): Or (Eq e0 e4) (Or (Eq (op e2 e4) e4) (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4))) % 6.20/6.44 Clause #69 (by clausification #[52]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) True % 6.20/6.44 Clause #71 (by clausification #[69]): Eq (Ne e0 e4) True % 6.20/6.44 Clause #72 (by clausification #[69]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 6.20/6.44 Clause #73 (by clausification #[71]): Ne e0 e4 % 6.20/6.44 Clause #74 (by backward contextual literal cutting #[73, 67]): Or (Eq (op e2 e4) e4) (Or (Eq (op e0 e4) e4) (Eq (op e1 e4) e4)) % 6.20/6.44 Clause #75 (by clausification #[72]): Eq (Ne e0 e3) True % 6.20/6.44 Clause #77 (by clausification #[75]): Ne e0 e3 % 6.20/6.44 Clause #82 (by clausification #[2]): Eq % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And % 6.20/6.44 (And (Eq (op (op e0 e0) (op e0 e0)) e0) % 6.20/6.44 (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.30/6.46 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.30/6.46 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.30/6.46 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.30/6.46 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.30/6.46 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.30/6.46 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.30/6.46 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.30/6.46 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.30/6.46 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.30/6.46 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.30/6.46 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.30/6.46 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.30/6.46 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.30/6.46 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.30/6.46 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.30/6.46 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.30/6.46 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.30/6.46 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.30/6.46 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 6.30/6.46 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 6.30/6.46 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 6.30/6.46 (Eq (op (op e3 e4) (op e4 e3)) e4)) % 6.30/6.46 True % 6.30/6.46 Clause #88 (by clausification #[82]): Eq % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.30/6.46 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.30/6.46 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.30/6.46 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.30/6.46 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.30/6.46 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.30/6.46 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.30/6.46 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.30/6.46 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.30/6.46 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.30/6.46 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.30/6.46 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.30/6.46 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.30/6.46 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.30/6.46 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.30/6.46 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.30/6.46 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.30/6.46 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.30/6.46 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.30/6.46 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 6.30/6.46 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 6.30/6.46 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 6.30/6.46 True % 6.30/6.46 Clause #91 (by clausification #[88]): Eq (Eq (op (op e2 e4) (op e4 e2)) e4) True % 6.30/6.46 Clause #92 (by clausification #[88]): Eq % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And % 6.30/6.46 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.30/6.46 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.30/6.48 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.30/6.48 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.30/6.48 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.30/6.48 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.30/6.48 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.30/6.48 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.30/6.48 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.30/6.48 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.30/6.48 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.30/6.48 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.30/6.48 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.30/6.48 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.30/6.48 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.30/6.48 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.30/6.48 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.30/6.48 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.30/6.48 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.30/6.48 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 6.30/6.48 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 6.30/6.48 True % 6.30/6.48 Clause #93 (by clausification #[91]): Eq (op (op e2 e4) (op e4 e2)) e4 % 6.30/6.48 Clause #94 (by clausification #[92]): Eq (Eq (op (op e1 e4) (op e4 e1)) e4) True % 6.30/6.48 Clause #95 (by clausification #[92]): Eq % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.30/6.48 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.30/6.48 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.30/6.48 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.30/6.48 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.30/6.48 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.30/6.48 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.30/6.48 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.30/6.48 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.30/6.48 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.30/6.48 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.30/6.48 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.30/6.48 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.30/6.48 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.30/6.48 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.30/6.48 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.30/6.48 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.30/6.48 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.30/6.48 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.30/6.48 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 6.30/6.48 True % 6.30/6.48 Clause #96 (by clausification #[94]): Eq (op (op e1 e4) (op e4 e1)) e4 % 6.30/6.48 Clause #97 (by clausification #[95]): Eq (Eq (op (op e0 e4) (op e4 e0)) e4) True % 6.30/6.48 Clause #98 (by clausification #[95]): Eq % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And % 6.30/6.48 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.30/6.48 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.30/6.48 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.30/6.48 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.30/6.48 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.30/6.48 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.30/6.48 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.34/6.51 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.34/6.51 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.34/6.51 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.34/6.51 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.34/6.51 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.34/6.51 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.34/6.51 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.34/6.51 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.34/6.51 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.34/6.51 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.34/6.51 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.34/6.51 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 6.34/6.51 True % 6.34/6.51 Clause #99 (by clausification #[97]): Eq (op (op e0 e4) (op e4 e0)) e4 % 6.34/6.51 Clause #100 (by superposition #[99, 74]): Or (Eq (op e2 e4) e4) (Or (Eq (op e1 e4) e4) (Eq (op e4 (op e4 e0)) e4)) % 6.34/6.51 Clause #101 (by clausification #[3]): Eq (Ne (op e4 e3) (op e4 e4)) True % 6.34/6.51 Clause #102 (by clausification #[3]): Eq % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (And % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e0)) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e0) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e0))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e1) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e1))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e2) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e2))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e3) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e3))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e4) % 6.34/6.51 (op % 6.34/6.51 e1 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e4) % 6.34/6.51 (op % 6.34/6.51 e2 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e4) % 6.34/6.51 (op % 6.34/6.51 e3 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op % 6.34/6.51 e0 % 6.34/6.51 e4) % 6.34/6.51 (op % 6.34/6.51 e4 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op e1 % 6.34/6.51 e4) % 6.34/6.51 (op e2 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op e1 % 6.34/6.51 e4) % 6.34/6.51 (op e3 % 6.34/6.51 e4))) % 6.34/6.51 (Ne % 6.34/6.51 (op e1 e4) % 6.34/6.51 (op e4 % 6.34/6.51 e4))) % 6.34/6.51 (Ne (op e2 e4) % 6.34/6.51 (op e3 e4))) % 6.34/6.51 (Ne (op e2 e4) % 6.34/6.51 (op e4 e4))) % 6.34/6.51 (Ne (op e3 e4) % 6.34/6.51 (op e4 e4))) % 6.34/6.51 (Ne (op e0 e0) % 6.34/6.51 (op e0 e1))) % 6.34/6.51 (Ne (op e0 e0) % 6.34/6.51 (op e0 e2))) % 6.34/6.51 (Ne (op e0 e0) % 6.34/6.51 (op e0 e3))) % 6.34/6.51 (Ne (op e0 e0) % 6.34/6.51 (op e0 e4))) % 6.34/6.51 (Ne (op e0 e1) (op e0 e2))) % 6.34/6.51 (Ne (op e0 e1) (op e0 e3))) % 6.34/6.51 (Ne (op e0 e1) (op e0 e4))) % 6.34/6.51 (Ne (op e0 e2) (op e0 e3))) % 6.34/6.51 (Ne (op e0 e2) (op e0 e4))) % 6.34/6.51 (Ne (op e0 e3) (op e0 e4))) % 6.34/6.52 (Ne (op e1 e0) (op e1 e1))) % 6.34/6.52 (Ne (op e1 e0) (op e1 e2))) % 6.34/6.52 (Ne (op e1 e0) (op e1 e3))) % 6.34/6.52 (Ne (op e1 e0) (op e1 e4))) % 6.34/6.52 (Ne (op e1 e1) (op e1 e2))) % 6.34/6.52 (Ne (op e1 e1) (op e1 e3))) % 6.34/6.52 (Ne (op e1 e1) (op e1 e4))) % 6.34/6.52 (Ne (op e1 e2) (op e1 e3))) % 6.34/6.52 (Ne (op e1 e2) (op e1 e4))) % 6.34/6.52 (Ne (op e1 e3) (op e1 e4))) % 6.34/6.52 (Ne (op e2 e0) (op e2 e1))) % 6.34/6.52 (Ne (op e2 e0) (op e2 e2))) % 6.34/6.52 (Ne (op e2 e0) (op e2 e3))) % 6.34/6.52 (Ne (op e2 e0) (op e2 e4))) % 6.34/6.52 (Ne (op e2 e1) (op e2 e2))) % 6.34/6.52 (Ne (op e2 e1) (op e2 e3))) % 6.34/6.52 (Ne (op e2 e1) (op e2 e4))) % 6.34/6.52 (Ne (op e2 e2) (op e2 e3))) % 6.34/6.52 (Ne (op e2 e2) (op e2 e4))) % 6.34/6.52 (Ne (op e2 e3) (op e2 e4))) % 6.34/6.52 (Ne (op e3 e0) (op e3 e1))) % 6.34/6.52 (Ne (op e3 e0) (op e3 e2))) % 6.34/6.52 (Ne (op e3 e0) (op e3 e3))) % 6.34/6.52 (Ne (op e3 e0) (op e3 e4))) % 6.34/6.52 (Ne (op e3 e1) (op e3 e2))) % 6.34/6.52 (Ne (op e3 e1) (op e3 e3))) % 6.34/6.52 (Ne (op e3 e1) (op e3 e4))) % 6.34/6.52 (Ne (op e3 e2) (op e3 e3))) % 6.34/6.52 (Ne (op e3 e2) (op e3 e4))) % 6.34/6.52 (Ne (op e3 e3) (op e3 e4))) % 6.34/6.52 (Ne (op e4 e0) (op e4 e1))) % 6.34/6.52 (Ne (op e4 e0) (op e4 e2))) % 6.34/6.52 (Ne (op e4 e0) (op e4 e3))) % 6.34/6.52 (Ne (op e4 e0) (op e4 e4))) % 6.34/6.52 (Ne (op e4 e1) (op e4 e2))) % 6.34/6.52 (Ne (op e4 e1) (op e4 e3))) % 6.34/6.52 (Ne (op e4 e1) (op e4 e4))) % 6.34/6.52 (Ne (op e4 e2) (op e4 e3))) % 6.34/6.52 (Ne (op e4 e2) (op e4 e4))) % 6.34/6.52 True % 6.34/6.52 Clause #103 (by clausification #[101]): Ne (op e4 e3) (op e4 e4) % 6.34/6.52 Clause #104 (by forward demodulation #[103, 23]): Ne (op e4 e3) e0 % 6.34/6.52 Clause #106 (by clausification #[98]): Eq % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And % 6.34/6.52 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.34/6.52 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.34/6.52 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.34/6.52 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.34/6.52 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.34/6.52 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.34/6.52 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.34/6.52 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.34/6.52 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.34/6.52 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.34/6.52 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.34/6.52 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.34/6.52 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.40/6.55 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.40/6.55 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.40/6.55 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.40/6.55 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.40/6.55 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 6.40/6.55 True % 6.40/6.55 Clause #110 (by clausification #[106]): Eq % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.40/6.55 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.40/6.55 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.40/6.55 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.40/6.55 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.40/6.55 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.40/6.55 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.40/6.55 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.40/6.55 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.40/6.55 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.40/6.55 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.40/6.55 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.40/6.55 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.40/6.55 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.40/6.55 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.40/6.55 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.40/6.55 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 6.40/6.55 True % 6.40/6.55 Clause #115 (by clausification #[110]): Eq % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.40/6.55 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.40/6.55 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.40/6.55 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.40/6.55 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.40/6.55 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.40/6.55 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.40/6.55 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.40/6.55 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.40/6.55 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.40/6.55 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.40/6.55 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.40/6.55 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.40/6.55 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.40/6.55 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.40/6.55 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 6.40/6.55 True % 6.40/6.55 Clause #119 (by clausification #[115]): Eq % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.40/6.55 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.40/6.55 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.40/6.55 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.40/6.55 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.40/6.55 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.40/6.55 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.40/6.55 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.40/6.55 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.40/6.55 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.40/6.55 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.40/6.55 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.40/6.55 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.40/6.55 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.40/6.55 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 6.40/6.55 True % 6.40/6.55 Clause #121 (by clausification #[6]): Eq % 6.40/6.55 (Not % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (Or % 6.40/6.55 (Or % 6.40/6.55 (Or % 6.40/6.55 (Or % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 6.40/6.55 (Ne (op e0 e2) e2)) % 6.40/6.55 (Ne (op e0 e3) e3)) % 6.40/6.55 (Ne (op e0 e4) e4)) % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 6.40/6.55 (Ne (op e1 e2) e2)) % 6.40/6.55 (Ne (op e1 e3) e3)) % 6.40/6.55 (Ne (op e1 e4) e4))) % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 6.40/6.55 (Ne (op e2 e2) e2)) % 6.40/6.55 (Ne (op e2 e3) e3)) % 6.40/6.55 (Ne (op e2 e4) e4))) % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 6.40/6.55 (Ne (op e3 e2) e2)) % 6.40/6.55 (Ne (op e3 e3) e3)) % 6.40/6.55 (Ne (op e3 e4) e4))) % 6.40/6.55 (And % 6.40/6.55 (And % 6.40/6.55 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 6.40/6.55 (Ne (op e4 e2) e2)) % 6.40/6.55 (Ne (op e4 e3) e3)) % 6.40/6.55 (Ne (op e4 e4) e4))) % 6.40/6.55 (Eq (op e0 (op e0 e0)) e0)) % 6.40/6.55 (Eq (op e0 (op e0 e1)) e1)) % 6.40/6.55 (Eq (op e0 (op e0 e2)) e2)) % 6.40/6.55 (Eq (op e0 (op e0 e3)) e3)) % 6.40/6.55 (Eq (op e0 (op e0 e4)) e4)) % 6.40/6.55 (Eq (op e1 (op e1 e0)) e0)) % 6.40/6.55 (Eq (op e1 (op e1 e1)) e1)) % 6.40/6.55 (Eq (op e1 (op e1 e2)) e2)) % 6.40/6.57 (Eq (op e1 (op e1 e3)) e3)) % 6.40/6.57 (Eq (op e1 (op e1 e4)) e4)) % 6.40/6.57 (Eq (op e2 (op e2 e0)) e0)) % 6.40/6.57 (Eq (op e2 (op e2 e1)) e1)) % 6.40/6.57 (Eq (op e2 (op e2 e2)) e2)) % 6.40/6.57 (Eq (op e2 (op e2 e3)) e3)) % 6.40/6.57 (Eq (op e2 (op e2 e4)) e4)) % 6.40/6.57 (Eq (op e3 (op e3 e0)) e0)) % 6.40/6.57 (Eq (op e3 (op e3 e1)) e1)) % 6.40/6.57 (Eq (op e3 (op e3 e2)) e2)) % 6.40/6.57 (Eq (op e3 (op e3 e3)) e3)) % 6.40/6.57 (Eq (op e3 (op e3 e4)) e4)) % 6.40/6.57 (Eq (op e4 (op e4 e0)) e0)) % 6.40/6.57 (Eq (op e4 (op e4 e1)) e1)) % 6.40/6.57 (Eq (op e4 (op e4 e2)) e2)) % 6.40/6.57 (Eq (op e4 (op e4 e3)) e3)) % 6.40/6.57 (Eq (op e4 (op e4 e4)) e4))) % 6.40/6.57 False % 6.40/6.57 Clause #122 (by clausification #[121]): Eq % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (Or % 6.40/6.57 (Or % 6.40/6.57 (Or % 6.40/6.57 (Or % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 6.40/6.57 (Ne (op e0 e2) e2)) % 6.40/6.57 (Ne (op e0 e3) e3)) % 6.40/6.57 (Ne (op e0 e4) e4)) % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 6.40/6.57 (Ne (op e1 e2) e2)) % 6.40/6.57 (Ne (op e1 e3) e3)) % 6.40/6.57 (Ne (op e1 e4) e4))) % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 6.40/6.57 (Ne (op e2 e2) e2)) % 6.40/6.57 (Ne (op e2 e3) e3)) % 6.40/6.57 (Ne (op e2 e4) e4))) % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 6.40/6.57 (Ne (op e3 e2) e2)) % 6.40/6.57 (Ne (op e3 e3) e3)) % 6.40/6.57 (Ne (op e3 e4) e4))) % 6.40/6.57 (And % 6.40/6.57 (And % 6.40/6.57 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 6.40/6.58 (Ne (op e4 e2) e2)) % 6.40/6.58 (Ne (op e4 e3) e3)) % 6.40/6.58 (Ne (op e4 e4) e4))) % 6.40/6.58 (Eq (op e0 (op e0 e0)) e0)) % 6.40/6.58 (Eq (op e0 (op e0 e1)) e1)) % 6.40/6.58 (Eq (op e0 (op e0 e2)) e2)) % 6.40/6.58 (Eq (op e0 (op e0 e3)) e3)) % 6.40/6.58 (Eq (op e0 (op e0 e4)) e4)) % 6.40/6.58 (Eq (op e1 (op e1 e0)) e0)) % 6.40/6.58 (Eq (op e1 (op e1 e1)) e1)) % 6.40/6.58 (Eq (op e1 (op e1 e2)) e2)) % 6.40/6.58 (Eq (op e1 (op e1 e3)) e3)) % 6.40/6.58 (Eq (op e1 (op e1 e4)) e4)) % 6.40/6.58 (Eq (op e2 (op e2 e0)) e0)) % 6.40/6.58 (Eq (op e2 (op e2 e1)) e1)) % 6.40/6.58 (Eq (op e2 (op e2 e2)) e2)) % 6.40/6.58 (Eq (op e2 (op e2 e3)) e3)) % 6.40/6.58 (Eq (op e2 (op e2 e4)) e4)) % 6.40/6.58 (Eq (op e3 (op e3 e0)) e0)) % 6.40/6.58 (Eq (op e3 (op e3 e1)) e1)) % 6.40/6.58 (Eq (op e3 (op e3 e2)) e2)) % 6.40/6.58 (Eq (op e3 (op e3 e3)) e3)) % 6.40/6.58 (Eq (op e3 (op e3 e4)) e4)) % 6.40/6.58 (Eq (op e4 (op e4 e0)) e0)) % 6.40/6.58 (Eq (op e4 (op e4 e1)) e1)) % 6.40/6.58 (Eq (op e4 (op e4 e2)) e2)) % 6.40/6.58 (Eq (op e4 (op e4 e3)) e3)) % 6.40/6.58 (Eq (op e4 (op e4 e4)) e4)) % 6.40/6.58 True % 6.40/6.58 Clause #123 (by clausification #[122]): Eq (Eq (op e4 (op e4 e4)) e4) True % 6.40/6.58 Clause #124 (by clausification #[122]): Eq % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (Or % 6.40/6.58 (Or % 6.40/6.58 (Or % 6.40/6.58 (Or % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 6.40/6.58 (Ne (op e0 e2) e2)) % 6.40/6.58 (Ne (op e0 e3) e3)) % 6.40/6.58 (Ne (op e0 e4) e4)) % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 6.40/6.58 (Ne (op e1 e2) e2)) % 6.40/6.58 (Ne (op e1 e3) e3)) % 6.40/6.58 (Ne (op e1 e4) e4))) % 6.40/6.58 (And % 6.40/6.58 (And % 6.40/6.58 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 6.40/6.58 (Ne (op e2 e2) e2)) % 6.40/6.58 (Ne (op e2 e3) e3)) % 6.40/6.58 (Ne (op e2 e4) e4))) % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 6.40/6.59 (Ne (op e3 e2) e2)) % 6.40/6.59 (Ne (op e3 e3) e3)) % 6.40/6.59 (Ne (op e3 e4) e4))) % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 6.40/6.59 (Ne (op e4 e2) e2)) % 6.40/6.59 (Ne (op e4 e3) e3)) % 6.40/6.59 (Ne (op e4 e4) e4))) % 6.40/6.59 (Eq (op e0 (op e0 e0)) e0)) % 6.40/6.59 (Eq (op e0 (op e0 e1)) e1)) % 6.40/6.59 (Eq (op e0 (op e0 e2)) e2)) % 6.40/6.59 (Eq (op e0 (op e0 e3)) e3)) % 6.40/6.59 (Eq (op e0 (op e0 e4)) e4)) % 6.40/6.59 (Eq (op e1 (op e1 e0)) e0)) % 6.40/6.59 (Eq (op e1 (op e1 e1)) e1)) % 6.40/6.59 (Eq (op e1 (op e1 e2)) e2)) % 6.40/6.59 (Eq (op e1 (op e1 e3)) e3)) % 6.40/6.59 (Eq (op e1 (op e1 e4)) e4)) % 6.40/6.59 (Eq (op e2 (op e2 e0)) e0)) % 6.40/6.59 (Eq (op e2 (op e2 e1)) e1)) % 6.40/6.59 (Eq (op e2 (op e2 e2)) e2)) % 6.40/6.59 (Eq (op e2 (op e2 e3)) e3)) % 6.40/6.59 (Eq (op e2 (op e2 e4)) e4)) % 6.40/6.59 (Eq (op e3 (op e3 e0)) e0)) % 6.40/6.59 (Eq (op e3 (op e3 e1)) e1)) % 6.40/6.59 (Eq (op e3 (op e3 e2)) e2)) % 6.40/6.59 (Eq (op e3 (op e3 e3)) e3)) % 6.40/6.59 (Eq (op e3 (op e3 e4)) e4)) % 6.40/6.59 (Eq (op e4 (op e4 e0)) e0)) % 6.40/6.59 (Eq (op e4 (op e4 e1)) e1)) % 6.40/6.59 (Eq (op e4 (op e4 e2)) e2)) % 6.40/6.59 (Eq (op e4 (op e4 e3)) e3)) % 6.40/6.59 True % 6.40/6.59 Clause #125 (by clausification #[123]): Eq (op e4 (op e4 e4)) e4 % 6.40/6.59 Clause #126 (by forward demodulation #[125, 23]): Eq (op e4 e0) e4 % 6.40/6.59 Clause #127 (by backward demodulation #[126, 99]): Eq (op (op e0 e4) e4) e4 % 6.40/6.59 Clause #128 (by backward demodulation #[126, 100]): Or (Eq (op e2 e4) e4) (Or (Eq (op e1 e4) e4) (Eq (op e4 e4) e4)) % 6.40/6.59 Clause #129 (by forward demodulation #[128, 23]): Or (Eq (op e2 e4) e4) (Or (Eq (op e1 e4) e4) (Eq e0 e4)) % 6.40/6.59 Clause #130 (by forward contextual literal cutting #[129, 73]): Or (Eq (op e2 e4) e4) (Eq (op e1 e4) e4) % 6.40/6.59 Clause #131 (by superposition #[130, 93]): Or (Eq (op e1 e4) e4) (Eq (op e4 (op e4 e2)) e4) % 6.40/6.59 Clause #133 (by clausification #[119]): Eq % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And % 6.40/6.59 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 6.40/6.59 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 6.40/6.59 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 6.40/6.59 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 6.40/6.59 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 6.40/6.59 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 6.40/6.59 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 6.40/6.59 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 6.40/6.59 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 6.40/6.59 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 6.40/6.59 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 6.40/6.59 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 6.40/6.59 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 6.40/6.59 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 6.40/6.59 True % 6.40/6.59 Clause #135 (by clausification #[133]): Eq (Eq (op (op e4 e2) (op e2 e4)) e2) True % 6.40/6.59 Clause #137 (by clausification #[135]): Eq (op (op e4 e2) (op e2 e4)) e2 % 6.46/6.62 Clause #139 (by clausification #[25]): Eq (Or (Or (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) (Eq (op e4 e3) e3)) (Eq (op e4 e3) e4)) % 6.46/6.62 True % 6.46/6.62 Clause #140 (by clausification #[25]): Eq % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (And % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 6.46/6.62 (Eq (op e0 e0) e3)) % 6.46/6.62 (Eq (op e0 e0) e4)) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 6.46/6.62 (Eq (op e0 e1) e3)) % 6.46/6.62 (Eq (op e0 e1) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 6.46/6.62 (Eq (op e0 e2) e3)) % 6.46/6.62 (Eq (op e0 e2) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 6.46/6.62 (Eq (op e0 e3) e3)) % 6.46/6.62 (Eq (op e0 e3) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 6.46/6.62 (Eq (op e0 e4) e3)) % 6.46/6.62 (Eq (op e0 e4) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 6.46/6.62 (Eq (op e1 e0) e3)) % 6.46/6.62 (Eq (op e1 e0) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 6.46/6.62 (Eq (op e1 e1) e3)) % 6.46/6.62 (Eq (op e1 e1) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 6.46/6.62 (Eq (op e1 e2) e3)) % 6.46/6.62 (Eq (op e1 e2) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 6.46/6.62 (Eq (op e1 e3) e3)) % 6.46/6.62 (Eq (op e1 e3) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 6.46/6.62 (Eq (op e1 e4) e3)) % 6.46/6.62 (Eq (op e1 e4) e4))) % 6.46/6.62 (Or % 6.46/6.62 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) (Eq (op e2 e0) e3)) % 6.46/6.62 (Eq (op e2 e0) e4))) % 6.46/6.62 (Or (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) (Eq (op e2 e1) e3)) % 6.46/6.62 (Eq (op e2 e1) e4))) % 6.46/6.62 (Or (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 6.52/6.69 (Eq (op e2 e2) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 6.52/6.69 (Eq (op e2 e3) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 6.52/6.69 (Eq (op e2 e4) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 6.52/6.69 (Eq (op e3 e0) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 6.52/6.69 (Eq (op e3 e1) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 6.52/6.69 (Eq (op e3 e2) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 6.52/6.69 (Eq (op e3 e3) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 6.52/6.69 (Eq (op e3 e4) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 6.52/6.69 (Eq (op e4 e0) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 6.52/6.69 (Eq (op e4 e1) e4))) % 6.52/6.69 (Or (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) (Eq (op e4 e2) e4))) % 6.52/6.69 True % 6.52/6.69 Clause #141 (by clausification #[139]): Or (Eq (Or (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) (Eq (op e4 e3) e3)) True) % 6.52/6.69 (Eq (Eq (op e4 e3) e4) True) % 6.52/6.69 Clause #142 (by clausification #[141]): Or (Eq (Eq (op e4 e3) e4) True) % 6.52/6.69 (Or (Eq (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) True) (Eq (Eq (op e4 e3) e3) True)) % 6.52/6.69 Clause #143 (by clausification #[142]): Or (Eq (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) True) % 6.52/6.69 (Or (Eq (Eq (op e4 e3) e3) True) (Eq (op e4 e3) e4)) % 6.52/6.69 Clause #144 (by clausification #[143]): Or (Eq (Eq (op e4 e3) e3) True) % 6.52/6.69 (Or (Eq (op e4 e3) e4) (Or (Eq (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) True) (Eq (Eq (op e4 e3) e2) True))) % 6.52/6.69 Clause #145 (by clausification #[144]): Or (Eq (op e4 e3) e4) % 6.52/6.69 (Or (Eq (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) True) (Or (Eq (Eq (op e4 e3) e2) True) (Eq (op e4 e3) e3))) % 6.52/6.69 Clause #146 (by clausification #[145]): Or (Eq (op e4 e3) e4) % 6.52/6.69 (Or (Eq (Eq (op e4 e3) e2) True) % 6.52/6.69 (Or (Eq (op e4 e3) e3) (Or (Eq (Eq (op e4 e3) e0) True) (Eq (Eq (op e4 e3) e1) True)))) % 6.52/6.69 Clause #147 (by clausification #[146]): Or (Eq (op e4 e3) e4) % 6.52/6.69 (Or (Eq (op e4 e3) e3) (Or (Eq (Eq (op e4 e3) e0) True) (Or (Eq (Eq (op e4 e3) e1) True) (Eq (op e4 e3) e2)))) % 6.52/6.69 Clause #148 (by clausification #[147]): Or (Eq (op e4 e3) e4) % 6.52/6.69 (Or (Eq (op e4 e3) e3) (Or (Eq (Eq (op e4 e3) e1) True) (Or (Eq (op e4 e3) e2) (Eq (op e4 e3) e0)))) % 6.52/6.69 Clause #149 (by clausification #[148]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e2) (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)))) % 6.52/6.69 Clause #150 (by forward contextual literal cutting #[149, 104]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e2) (Eq (op e4 e3) e1))) % 6.52/6.69 Clause #158 (by clausification #[55]): Eq % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (And % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Eq (op e0 e0) % 6.52/6.69 e0) % 6.52/6.69 (Eq (op e0 e1) % 6.52/6.69 e0)) % 6.52/6.69 (Eq (op e0 e2) % 6.52/6.69 e0)) % 6.52/6.69 (Eq (op e0 e3) e0)) % 6.52/6.69 (Eq (op e0 e4) e0)) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Eq (op e0 e0) % 6.52/6.69 e0) % 6.52/6.69 (Eq (op e1 e0) % 6.52/6.69 e0)) % 6.52/6.69 (Eq (op e2 e0) % 6.52/6.69 e0)) % 6.52/6.69 (Eq (op e3 e0) e0)) % 6.52/6.69 (Eq (op e4 e0) e0))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Eq (op e0 e0) e1) % 6.52/6.69 (Eq (op e0 e1) % 6.52/6.69 e1)) % 6.52/6.69 (Eq (op e0 e2) e1)) % 6.52/6.69 (Eq (op e0 e3) e1)) % 6.52/6.69 (Eq (op e0 e4) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e1) % 6.52/6.69 (Eq (op e1 e0) e1)) % 6.52/6.69 (Eq (op e2 e0) e1)) % 6.52/6.69 (Eq (op e3 e0) e1)) % 6.52/6.69 (Eq (op e4 e0) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e2) % 6.52/6.69 (Eq (op e0 e1) e2)) % 6.52/6.69 (Eq (op e0 e2) e2)) % 6.52/6.69 (Eq (op e0 e3) e2)) % 6.52/6.69 (Eq (op e0 e4) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e2) % 6.52/6.69 (Eq (op e1 e0) e2)) % 6.52/6.69 (Eq (op e2 e0) e2)) % 6.52/6.69 (Eq (op e3 e0) e2)) % 6.52/6.69 (Eq (op e4 e0) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e3) % 6.52/6.69 (Eq (op e0 e1) e3)) % 6.52/6.69 (Eq (op e0 e2) e3)) % 6.52/6.69 (Eq (op e0 e3) e3)) % 6.52/6.69 (Eq (op e0 e4) e3))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e3) % 6.52/6.69 (Eq (op e1 e0) e3)) % 6.52/6.69 (Eq (op e2 e0) e3)) % 6.52/6.69 (Eq (op e3 e0) e3)) % 6.52/6.69 (Eq (op e4 e0) e3))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e4) % 6.52/6.69 (Eq (op e0 e1) e4)) % 6.52/6.69 (Eq (op e0 e2) e4)) % 6.52/6.69 (Eq (op e0 e3) e4)) % 6.52/6.69 (Eq (op e0 e4) e4))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e0) e4) % 6.52/6.69 (Eq (op e1 e0) e4)) % 6.52/6.69 (Eq (op e2 e0) e4)) % 6.52/6.69 (Eq (op e3 e0) e4)) % 6.52/6.69 (Eq (op e4 e0) e4))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e1 e0) e0) % 6.52/6.69 (Eq (op e1 e1) e0)) % 6.52/6.69 (Eq (op e1 e2) e0)) % 6.52/6.69 (Eq (op e1 e3) e0)) % 6.52/6.69 (Eq (op e1 e4) e0))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e1) e0) % 6.52/6.69 (Eq (op e1 e1) e0)) % 6.52/6.69 (Eq (op e2 e1) e0)) % 6.52/6.69 (Eq (op e3 e1) e0)) % 6.52/6.69 (Eq (op e4 e1) e0))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e1 e0) e1) % 6.52/6.69 (Eq (op e1 e1) e1)) % 6.52/6.69 (Eq (op e1 e2) e1)) % 6.52/6.69 (Eq (op e1 e3) e1)) % 6.52/6.69 (Eq (op e1 e4) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) % 6.52/6.69 (Eq (op e2 e1) e1)) % 6.52/6.69 (Eq (op e3 e1) e1)) % 6.52/6.69 (Eq (op e4 e1) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 6.52/6.69 (Eq (op e1 e2) e2)) % 6.52/6.69 (Eq (op e1 e3) e2)) % 6.52/6.69 (Eq (op e1 e4) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 6.52/6.69 (Eq (op e2 e1) e2)) % 6.52/6.69 (Eq (op e3 e1) e2)) % 6.52/6.69 (Eq (op e4 e1) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 6.52/6.69 (Eq (op e1 e2) e3)) % 6.52/6.69 (Eq (op e1 e3) e3)) % 6.52/6.69 (Eq (op e1 e4) e3))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 6.52/6.69 (Eq (op e2 e1) e3)) % 6.52/6.69 (Eq (op e3 e1) e3)) % 6.52/6.69 (Eq (op e4 e1) e3))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 6.52/6.69 (Eq (op e1 e2) e4)) % 6.52/6.69 (Eq (op e1 e3) e4)) % 6.52/6.69 (Eq (op e1 e4) e4))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 6.52/6.69 (Eq (op e2 e1) e4)) % 6.52/6.69 (Eq (op e3 e1) e4)) % 6.52/6.69 (Eq (op e4 e1) e4))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 6.52/6.69 (Eq (op e2 e2) e0)) % 6.52/6.69 (Eq (op e2 e3) e0)) % 6.52/6.69 (Eq (op e2 e4) e0))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 6.52/6.69 (Eq (op e2 e2) e0)) % 6.52/6.69 (Eq (op e3 e2) e0)) % 6.52/6.69 (Eq (op e4 e2) e0))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 6.52/6.69 (Eq (op e2 e2) e1)) % 6.52/6.69 (Eq (op e2 e3) e1)) % 6.52/6.69 (Eq (op e2 e4) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 6.52/6.69 (Eq (op e2 e2) e1)) % 6.52/6.69 (Eq (op e3 e2) e1)) % 6.52/6.69 (Eq (op e4 e2) e1))) % 6.52/6.69 (Or % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) % 6.52/6.69 (Eq (op e2 e3) e2)) % 6.52/6.69 (Eq (op e2 e4) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 6.52/6.69 (Eq (op e3 e2) e2)) % 6.52/6.69 (Eq (op e4 e2) e2))) % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 6.52/6.69 (Eq (op e2 e3) e3)) % 6.52/6.69 (Eq (op e2 e4) e3))) % 6.52/6.69 (Or % 6.52/6.69 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 6.52/6.69 (Eq (op e3 e2) e3)) % 6.52/6.72 (Eq (op e4 e2) e3))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 6.52/6.72 (Eq (op e2 e3) e4)) % 6.52/6.72 (Eq (op e2 e4) e4))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 6.52/6.72 (Eq (op e3 e2) e4)) % 6.52/6.72 (Eq (op e4 e2) e4))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 6.52/6.72 (Eq (op e3 e3) e0)) % 6.52/6.72 (Eq (op e3 e4) e0))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 6.52/6.72 (Eq (op e3 e3) e0)) % 6.52/6.72 (Eq (op e4 e3) e0))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 6.52/6.72 (Eq (op e3 e3) e1)) % 6.52/6.72 (Eq (op e3 e4) e1))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 6.52/6.72 (Eq (op e3 e3) e1)) % 6.52/6.72 (Eq (op e4 e3) e1))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 6.52/6.72 (Eq (op e3 e3) e2)) % 6.52/6.72 (Eq (op e3 e4) e2))) % 6.52/6.72 (Or % 6.52/6.72 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2)) % 6.52/6.72 (Eq (op e4 e3) e2))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 6.52/6.72 (Eq (op e3 e4) e3))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 6.52/6.72 (Eq (op e4 e3) e3))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 6.52/6.72 (Eq (op e3 e4) e4))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 6.52/6.72 (Eq (op e4 e3) e4))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 6.52/6.72 (Eq (op e4 e4) e0))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 6.52/6.72 (Eq (op e4 e4) e0))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 6.52/6.72 (Eq (op e4 e4) e1))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 6.52/6.72 (Eq (op e4 e4) e1))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 6.52/6.72 (Eq (op e4 e4) e2))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 6.52/6.72 (Eq (op e4 e4) e2))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 6.52/6.72 (Eq (op e4 e4) e3))) % 6.52/6.72 (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) (Eq (op e4 e4) e3))) % 6.52/6.72 True % 6.52/6.72 Clause #179 (by clausification #[102]): Eq % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (And % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e0)) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e0) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e0))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e1) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e1))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e2) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e2))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e3) % 6.52/6.72 (op % 6.52/6.72 e4 % 6.52/6.72 e3))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e4) % 6.52/6.72 (op % 6.52/6.72 e1 % 6.52/6.72 e4))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e4) % 6.52/6.72 (op % 6.52/6.72 e2 % 6.52/6.72 e4))) % 6.52/6.72 (Ne % 6.52/6.72 (op % 6.52/6.72 e0 % 6.52/6.72 e4) % 6.52/6.72 (op % 6.52/6.72 e3 % 6.52/6.72 e4))) % 6.52/6.72 (Ne % 6.52/6.72 (op e0 % 6.52/6.72 e4) % 6.52/6.72 (op e4 % 6.52/6.72 e4))) % 6.52/6.72 (Ne % 6.52/6.72 (op e1 % 6.52/6.72 e4) % 6.52/6.72 (op e2 % 6.52/6.72 e4))) % 6.52/6.72 (Ne % 6.52/6.72 (op e1 e4) % 6.52/6.72 (op e3 % 6.52/6.72 e4))) % 6.52/6.72 (Ne (op e1 e4) % 6.52/6.72 (op e4 e4))) % 6.52/6.72 (Ne (op e2 e4) % 6.52/6.72 (op e3 e4))) % 6.52/6.72 (Ne (op e2 e4) % 6.52/6.72 (op e4 e4))) % 6.52/6.72 (Ne (op e3 e4) % 6.52/6.72 (op e4 e4))) % 6.52/6.72 (Ne (op e0 e0) % 6.52/6.72 (op e0 e1))) % 6.52/6.72 (Ne (op e0 e0) % 6.52/6.72 (op e0 e2))) % 6.52/6.72 (Ne (op e0 e0) % 6.52/6.72 (op e0 e3))) % 6.52/6.72 (Ne (op e0 e0) (op e0 e4))) % 6.52/6.72 (Ne (op e0 e1) (op e0 e2))) % 6.52/6.72 (Ne (op e0 e1) (op e0 e3))) % 6.52/6.72 (Ne (op e0 e1) (op e0 e4))) % 6.52/6.72 (Ne (op e0 e2) (op e0 e3))) % 6.52/6.72 (Ne (op e0 e2) (op e0 e4))) % 6.52/6.72 (Ne (op e0 e3) (op e0 e4))) % 6.52/6.72 (Ne (op e1 e0) (op e1 e1))) % 6.52/6.72 (Ne (op e1 e0) (op e1 e2))) % 6.52/6.72 (Ne (op e1 e0) (op e1 e3))) % 6.52/6.72 (Ne (op e1 e0) (op e1 e4))) % 6.52/6.72 (Ne (op e1 e1) (op e1 e2))) % 6.52/6.72 (Ne (op e1 e1) (op e1 e3))) % 6.52/6.72 (Ne (op e1 e1) (op e1 e4))) % 6.52/6.72 (Ne (op e1 e2) (op e1 e3))) % 6.52/6.72 (Ne (op e1 e2) (op e1 e4))) % 6.52/6.72 (Ne (op e1 e3) (op e1 e4))) % 6.52/6.72 (Ne (op e2 e0) (op e2 e1))) % 6.52/6.72 (Ne (op e2 e0) (op e2 e2))) % 6.52/6.72 (Ne (op e2 e0) (op e2 e3))) % 6.52/6.72 (Ne (op e2 e0) (op e2 e4))) % 6.52/6.72 (Ne (op e2 e1) (op e2 e2))) % 6.52/6.72 (Ne (op e2 e1) (op e2 e3))) % 6.52/6.72 (Ne (op e2 e1) (op e2 e4))) % 6.52/6.72 (Ne (op e2 e2) (op e2 e3))) % 6.52/6.72 (Ne (op e2 e2) (op e2 e4))) % 6.52/6.72 (Ne (op e2 e3) (op e2 e4))) % 6.52/6.72 (Ne (op e3 e0) (op e3 e1))) % 6.52/6.72 (Ne (op e3 e0) (op e3 e2))) % 6.52/6.72 (Ne (op e3 e0) (op e3 e3))) % 6.52/6.72 (Ne (op e3 e0) (op e3 e4))) % 6.52/6.72 (Ne (op e3 e1) (op e3 e2))) % 6.52/6.72 (Ne (op e3 e1) (op e3 e3))) % 6.52/6.72 (Ne (op e3 e1) (op e3 e4))) % 6.52/6.72 (Ne (op e3 e2) (op e3 e3))) % 6.52/6.72 (Ne (op e3 e2) (op e3 e4))) % 6.52/6.72 (Ne (op e3 e3) (op e3 e4))) % 6.52/6.72 (Ne (op e4 e0) (op e4 e1))) % 6.52/6.72 (Ne (op e4 e0) (op e4 e2))) % 6.52/6.72 (Ne (op e4 e0) (op e4 e3))) % 6.52/6.72 (Ne (op e4 e0) (op e4 e4))) % 6.52/6.72 (Ne (op e4 e1) (op e4 e2))) % 6.52/6.72 (Ne (op e4 e1) (op e4 e3))) % 6.52/6.72 (Ne (op e4 e1) (op e4 e4))) % 6.52/6.74 (Ne (op e4 e2) (op e4 e3))) % 6.52/6.74 True % 6.52/6.74 Clause #185 (by clausification #[124]): Eq (Eq (op e4 (op e4 e3)) e3) True % 6.52/6.74 Clause #186 (by clausification #[124]): Eq % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (Or % 6.52/6.74 (Or % 6.52/6.74 (Or % 6.52/6.74 (Or % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 6.52/6.74 (Ne (op e0 e2) e2)) % 6.52/6.74 (Ne (op e0 e3) e3)) % 6.52/6.74 (Ne (op e0 e4) e4)) % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 6.52/6.74 (Ne (op e1 e2) e2)) % 6.52/6.74 (Ne (op e1 e3) e3)) % 6.52/6.74 (Ne (op e1 e4) e4))) % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 6.52/6.74 (Ne (op e2 e2) e2)) % 6.52/6.74 (Ne (op e2 e3) e3)) % 6.52/6.74 (Ne (op e2 e4) e4))) % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 6.52/6.74 (Ne (op e3 e2) e2)) % 6.52/6.74 (Ne (op e3 e3) e3)) % 6.52/6.74 (Ne (op e3 e4) e4))) % 6.52/6.74 (And % 6.52/6.74 (And % 6.52/6.74 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 6.52/6.74 (Ne (op e4 e2) e2)) % 6.52/6.74 (Ne (op e4 e3) e3)) % 6.52/6.74 (Ne (op e4 e4) e4))) % 6.52/6.74 (Eq (op e0 (op e0 e0)) e0)) % 6.52/6.74 (Eq (op e0 (op e0 e1)) e1)) % 6.52/6.74 (Eq (op e0 (op e0 e2)) e2)) % 6.52/6.74 (Eq (op e0 (op e0 e3)) e3)) % 6.52/6.74 (Eq (op e0 (op e0 e4)) e4)) % 6.52/6.74 (Eq (op e1 (op e1 e0)) e0)) % 6.52/6.74 (Eq (op e1 (op e1 e1)) e1)) % 6.52/6.74 (Eq (op e1 (op e1 e2)) e2)) % 6.52/6.74 (Eq (op e1 (op e1 e3)) e3)) % 6.52/6.74 (Eq (op e1 (op e1 e4)) e4)) % 6.52/6.74 (Eq (op e2 (op e2 e0)) e0)) % 6.52/6.74 (Eq (op e2 (op e2 e1)) e1)) % 6.60/6.76 (Eq (op e2 (op e2 e2)) e2)) % 6.60/6.76 (Eq (op e2 (op e2 e3)) e3)) % 6.60/6.76 (Eq (op e2 (op e2 e4)) e4)) % 6.60/6.76 (Eq (op e3 (op e3 e0)) e0)) % 6.60/6.76 (Eq (op e3 (op e3 e1)) e1)) % 6.60/6.76 (Eq (op e3 (op e3 e2)) e2)) % 6.60/6.76 (Eq (op e3 (op e3 e3)) e3)) % 6.60/6.76 (Eq (op e3 (op e3 e4)) e4)) % 6.60/6.76 (Eq (op e4 (op e4 e0)) e0)) % 6.60/6.76 (Eq (op e4 (op e4 e1)) e1)) % 6.60/6.76 (Eq (op e4 (op e4 e2)) e2)) % 6.60/6.76 True % 6.60/6.76 Clause #187 (by clausification #[185]): Eq (op e4 (op e4 e3)) e3 % 6.60/6.76 Clause #188 (by superposition #[187, 150]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e4 e2) e3))) % 6.60/6.76 Clause #210 (by clausification #[140]): Eq % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (And % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 6.60/6.76 (Eq (op e0 e0) e3)) % 6.60/6.76 (Eq (op e0 e0) e4)) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 6.60/6.76 (Eq (op e0 e1) e3)) % 6.60/6.76 (Eq (op e0 e1) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 6.60/6.76 (Eq (op e0 e2) e3)) % 6.60/6.76 (Eq (op e0 e2) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 6.60/6.76 (Eq (op e0 e3) e3)) % 6.60/6.76 (Eq (op e0 e3) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 6.60/6.76 (Eq (op e0 e4) e3)) % 6.60/6.76 (Eq (op e0 e4) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 6.60/6.76 (Eq (op e1 e0) e3)) % 6.60/6.76 (Eq (op e1 e0) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 6.60/6.76 (Eq (op e1 e1) e3)) % 6.60/6.76 (Eq (op e1 e1) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 6.60/6.76 (Eq (op e1 e2) e3)) % 6.60/6.76 (Eq (op e1 e2) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 6.60/6.76 (Eq (op e1 e3) e3)) % 6.60/6.76 (Eq (op e1 e3) e4))) % 6.60/6.76 (Or % 6.60/6.76 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) (Eq (op e1 e4) e3)) % 6.60/6.76 (Eq (op e1 e4) e4))) % 6.60/6.76 (Or (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) (Eq (op e2 e0) e3)) % 6.62/6.78 (Eq (op e2 e0) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) (Eq (op e2 e1) e3)) % 6.62/6.78 (Eq (op e2 e1) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 6.62/6.78 (Eq (op e2 e2) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 6.62/6.78 (Eq (op e2 e3) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 6.62/6.78 (Eq (op e2 e4) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 6.62/6.78 (Eq (op e3 e0) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 6.62/6.78 (Eq (op e3 e1) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 6.62/6.78 (Eq (op e3 e2) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 6.62/6.78 (Eq (op e3 e3) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 6.62/6.78 (Eq (op e3 e4) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 6.62/6.78 (Eq (op e4 e0) e4))) % 6.62/6.78 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) (Eq (op e4 e1) e4))) % 6.62/6.78 True % 6.62/6.78 Clause #234 (by clausification #[158]): Eq (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) (Eq (op e4 e4) e3)) % 6.62/6.78 True % 6.62/6.78 Clause #236 (by clausification #[234]): Or (Eq (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) True) % 6.62/6.78 (Eq (Eq (op e4 e4) e3) True) % 6.62/6.78 Clause #237 (by clausification #[236]): Or (Eq (Eq (op e4 e4) e3) True) % 6.62/6.78 (Or (Eq (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) True) (Eq (Eq (op e3 e4) e3) True)) % 6.62/6.78 Clause #238 (by clausification #[237]): Or (Eq (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) True) % 6.62/6.78 (Or (Eq (Eq (op e3 e4) e3) True) (Eq (op e4 e4) e3)) % 6.62/6.78 Clause #239 (by clausification #[238]): Or (Eq (Eq (op e3 e4) e3) True) % 6.62/6.78 (Or (Eq (op e4 e4) e3) (Or (Eq (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) True) (Eq (Eq (op e2 e4) e3) True))) % 6.62/6.78 Clause #240 (by clausification #[239]): Or (Eq (op e4 e4) e3) % 6.62/6.78 (Or (Eq (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) True) (Or (Eq (Eq (op e2 e4) e3) True) (Eq (op e3 e4) e3))) % 6.62/6.78 Clause #241 (by clausification #[240]): Or (Eq (op e4 e4) e3) % 6.62/6.78 (Or (Eq (Eq (op e2 e4) e3) True) % 6.62/6.78 (Or (Eq (op e3 e4) e3) (Or (Eq (Eq (op e0 e4) e3) True) (Eq (Eq (op e1 e4) e3) True)))) % 6.62/6.78 Clause #242 (by clausification #[241]): Or (Eq (op e4 e4) e3) % 6.62/6.78 (Or (Eq (op e3 e4) e3) (Or (Eq (Eq (op e0 e4) e3) True) (Or (Eq (Eq (op e1 e4) e3) True) (Eq (op e2 e4) e3)))) % 6.62/6.78 Clause #243 (by clausification #[242]): Or (Eq (op e4 e4) e3) % 6.62/6.78 (Or (Eq (op e3 e4) e3) (Or (Eq (Eq (op e1 e4) e3) True) (Or (Eq (op e2 e4) e3) (Eq (op e0 e4) e3)))) % 6.62/6.78 Clause #244 (by clausification #[243]): Or (Eq (op e4 e4) e3) (Or (Eq (op e3 e4) e3) (Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)))) % 6.62/6.78 Clause #245 (by forward demodulation #[244, 23]): Or (Eq e0 e3) (Or (Eq (op e3 e4) e3) (Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)))) % 6.62/6.78 Clause #246 (by forward demodulation #[245, 18]): Or (Eq e0 e3) (Or (Eq e1 e3) (Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)))) % 6.62/6.78 Clause #247 (by forward contextual literal cutting #[246, 77]): Or (Eq e1 e3) (Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3))) % 6.62/6.78 Clause #248 (by forward contextual literal cutting #[247, 53]): Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) % 6.62/6.78 Clause #249 (by superposition #[248, 127]): Or (Eq (op e2 e4) e3) (Or (Eq (op e1 e4) e3) (Eq (op e3 e4) e4)) % 6.62/6.78 Clause #250 (by forward demodulation #[249, 18]): Or (Eq (op e2 e4) e3) (Or (Eq (op e1 e4) e3) (Eq e1 e4)) % 6.62/6.81 Clause #251 (by forward contextual literal cutting #[250, 50]): Or (Eq (op e2 e4) e3) (Eq (op e1 e4) e3) % 6.62/6.81 Clause #277 (by clausification #[179]): Eq % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.81 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (And % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e0)) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e0) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e0))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e1) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e1))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e2) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e2))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e3 % 6.62/6.82 e3) % 6.62/6.82 (op % 6.62/6.82 e4 % 6.62/6.82 e3))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e4) % 6.62/6.82 (op % 6.62/6.82 e1 % 6.62/6.82 e4))) % 6.62/6.82 (Ne % 6.62/6.82 (op % 6.62/6.82 e0 % 6.62/6.82 e4) % 6.62/6.82 (op % 6.62/6.82 e2 % 6.62/6.82 e4))) % 6.62/6.82 (Ne % 6.62/6.82 (op e0 % 6.62/6.82 e4) % 6.62/6.82 (op e3 % 6.62/6.82 e4))) % 6.62/6.82 (Ne % 6.62/6.82 (op e0 % 6.62/6.82 e4) % 6.62/6.82 (op e4 % 6.62/6.82 e4))) % 6.62/6.82 (Ne % 6.62/6.82 (op e1 e4) % 6.62/6.82 (op e2 % 6.62/6.82 e4))) % 6.62/6.82 (Ne (op e1 e4) % 6.62/6.82 (op e3 e4))) % 6.62/6.82 (Ne (op e1 e4) % 6.62/6.82 (op e4 e4))) % 6.62/6.82 (Ne (op e2 e4) % 6.62/6.82 (op e3 e4))) % 6.62/6.82 (Ne (op e2 e4) % 6.62/6.82 (op e4 e4))) % 6.62/6.82 (Ne (op e3 e4) % 6.62/6.82 (op e4 e4))) % 6.62/6.82 (Ne (op e0 e0) % 6.62/6.82 (op e0 e1))) % 6.62/6.82 (Ne (op e0 e0) % 6.62/6.82 (op e0 e2))) % 6.62/6.82 (Ne (op e0 e0) (op e0 e3))) % 6.62/6.82 (Ne (op e0 e0) (op e0 e4))) % 6.62/6.82 (Ne (op e0 e1) (op e0 e2))) % 6.62/6.82 (Ne (op e0 e1) (op e0 e3))) % 6.62/6.82 (Ne (op e0 e1) (op e0 e4))) % 6.66/6.82 (Ne (op e0 e2) (op e0 e3))) % 6.66/6.82 (Ne (op e0 e2) (op e0 e4))) % 6.66/6.82 (Ne (op e0 e3) (op e0 e4))) % 6.66/6.82 (Ne (op e1 e0) (op e1 e1))) % 6.66/6.82 (Ne (op e1 e0) (op e1 e2))) % 6.66/6.82 (Ne (op e1 e0) (op e1 e3))) % 6.66/6.82 (Ne (op e1 e0) (op e1 e4))) % 6.66/6.82 (Ne (op e1 e1) (op e1 e2))) % 6.66/6.82 (Ne (op e1 e1) (op e1 e3))) % 6.66/6.82 (Ne (op e1 e1) (op e1 e4))) % 6.66/6.82 (Ne (op e1 e2) (op e1 e3))) % 6.66/6.82 (Ne (op e1 e2) (op e1 e4))) % 6.66/6.82 (Ne (op e1 e3) (op e1 e4))) % 6.66/6.82 (Ne (op e2 e0) (op e2 e1))) % 6.66/6.82 (Ne (op e2 e0) (op e2 e2))) % 6.66/6.82 (Ne (op e2 e0) (op e2 e3))) % 6.66/6.82 (Ne (op e2 e0) (op e2 e4))) % 6.66/6.82 (Ne (op e2 e1) (op e2 e2))) % 6.66/6.82 (Ne (op e2 e1) (op e2 e3))) % 6.66/6.82 (Ne (op e2 e1) (op e2 e4))) % 6.66/6.82 (Ne (op e2 e2) (op e2 e3))) % 6.66/6.82 (Ne (op e2 e2) (op e2 e4))) % 6.66/6.82 (Ne (op e2 e3) (op e2 e4))) % 6.66/6.82 (Ne (op e3 e0) (op e3 e1))) % 6.66/6.82 (Ne (op e3 e0) (op e3 e2))) % 6.66/6.82 (Ne (op e3 e0) (op e3 e3))) % 6.66/6.82 (Ne (op e3 e0) (op e3 e4))) % 6.66/6.82 (Ne (op e3 e1) (op e3 e2))) % 6.66/6.82 (Ne (op e3 e1) (op e3 e3))) % 6.66/6.82 (Ne (op e3 e1) (op e3 e4))) % 6.66/6.82 (Ne (op e3 e2) (op e3 e3))) % 6.66/6.82 (Ne (op e3 e2) (op e3 e4))) % 6.66/6.82 (Ne (op e3 e3) (op e3 e4))) % 6.66/6.82 (Ne (op e4 e0) (op e4 e1))) % 6.66/6.82 (Ne (op e4 e0) (op e4 e2))) % 6.66/6.82 (Ne (op e4 e0) (op e4 e3))) % 6.66/6.82 (Ne (op e4 e0) (op e4 e4))) % 6.66/6.82 (Ne (op e4 e1) (op e4 e2))) % 6.66/6.82 (Ne (op e4 e1) (op e4 e3))) % 6.66/6.82 (Ne (op e4 e1) (op e4 e4))) % 6.66/6.82 True % 6.66/6.82 Clause #296 (by clausification #[186]): Eq (Eq (op e4 (op e4 e2)) e2) True % 6.66/6.82 Clause #298 (by clausification #[296]): Eq (op e4 (op e4 e2)) e2 % 6.66/6.82 Clause #299 (by superposition #[298, 131]): Or (Eq (op e1 e4) e4) (Eq e2 e4) % 6.66/6.82 Clause #302 (by forward contextual literal cutting #[299, 44]): Eq (op e1 e4) e4 % 6.66/6.82 Clause #303 (by backward demodulation #[302, 96]): Eq (op e4 (op e4 e1)) e4 % 6.66/6.82 Clause #307 (by backward demodulation #[302, 251]): Or (Eq (op e2 e4) e3) (Eq e4 e3) % 6.66/6.82 Clause #316 (by forward contextual literal cutting #[307, 41]): Eq (op e2 e4) e3 % 6.66/6.82 Clause #317 (by backward demodulation #[316, 93]): Eq (op e3 (op e4 e2)) e4 % 6.66/6.82 Clause #318 (by backward demodulation #[316, 137]): Eq (op (op e4 e2) e3) e2 % 6.66/6.82 Clause #322 (by superposition #[317, 188]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e3 e3) e4))) % 6.66/6.82 Clause #336 (by clausification #[210]): Eq (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) (Eq (op e4 e1) e4)) % 6.66/6.82 True % 6.66/6.82 Clause #338 (by clausification #[336]): Or (Eq (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) True) % 6.66/6.82 (Eq (Eq (op e4 e1) e4) True) % 6.66/6.82 Clause #339 (by clausification #[338]): Or (Eq (Eq (op e4 e1) e4) True) % 6.68/6.85 (Or (Eq (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) True) (Eq (Eq (op e4 e1) e3) True)) % 6.68/6.85 Clause #340 (by clausification #[339]): Or (Eq (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) True) % 6.68/6.85 (Or (Eq (Eq (op e4 e1) e3) True) (Eq (op e4 e1) e4)) % 6.68/6.85 Clause #341 (by clausification #[340]): Or (Eq (Eq (op e4 e1) e3) True) % 6.68/6.85 (Or (Eq (op e4 e1) e4) (Or (Eq (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) True) (Eq (Eq (op e4 e1) e2) True))) % 6.68/6.85 Clause #342 (by clausification #[341]): Or (Eq (op e4 e1) e4) % 6.68/6.85 (Or (Eq (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) True) (Or (Eq (Eq (op e4 e1) e2) True) (Eq (op e4 e1) e3))) % 6.68/6.85 Clause #343 (by clausification #[342]): Or (Eq (op e4 e1) e4) % 6.68/6.85 (Or (Eq (Eq (op e4 e1) e2) True) % 6.68/6.85 (Or (Eq (op e4 e1) e3) (Or (Eq (Eq (op e4 e1) e0) True) (Eq (Eq (op e4 e1) e1) True)))) % 6.68/6.85 Clause #344 (by clausification #[343]): Or (Eq (op e4 e1) e4) % 6.68/6.85 (Or (Eq (op e4 e1) e3) (Or (Eq (Eq (op e4 e1) e0) True) (Or (Eq (Eq (op e4 e1) e1) True) (Eq (op e4 e1) e2)))) % 6.68/6.85 Clause #345 (by clausification #[344]): Or (Eq (op e4 e1) e4) % 6.68/6.85 (Or (Eq (op e4 e1) e3) (Or (Eq (Eq (op e4 e1) e1) True) (Or (Eq (op e4 e1) e2) (Eq (op e4 e1) e0)))) % 6.68/6.85 Clause #346 (by clausification #[345]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e2) (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)))) % 6.68/6.85 Clause #354 (by forward demodulation #[322, 12]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq e2 e4))) % 6.68/6.85 Clause #355 (by forward contextual literal cutting #[354, 44]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Eq (op e4 e3) e1)) % 6.68/6.85 Clause #359 (by superposition #[355, 187]): Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e4 e4) e3)) % 6.68/6.85 Clause #367 (by superposition #[359, 23]): Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq e0 e3)) % 6.68/6.85 Clause #368 (by forward contextual literal cutting #[367, 77]): Or (Eq (op e4 e3) e3) (Eq (op e4 e3) e1) % 6.68/6.85 Clause #372 (by superposition #[368, 187]): Or (Eq (op e4 e3) e3) (Eq (op e4 e1) e3) % 6.68/6.85 Clause #405 (by superposition #[372, 303]): Or (Eq (op e4 e3) e3) (Eq (op e4 e3) e4) % 6.68/6.85 Clause #411 (by superposition #[405, 368]): Or (Eq (op e4 e3) e3) (Or (Eq e4 e3) (Eq e4 e1)) % 6.68/6.85 Clause #416 (by forward contextual literal cutting #[411, 41]): Or (Eq (op e4 e3) e3) (Eq e4 e1) % 6.68/6.85 Clause #417 (by forward contextual literal cutting #[416, 50]): Eq (op e4 e3) e3 % 6.68/6.85 Clause #451 (by clausification #[277]): Eq (Ne (op e4 e1) (op e4 e4)) True % 6.68/6.85 Clause #453 (by clausification #[451]): Ne (op e4 e1) (op e4 e4) % 6.68/6.85 Clause #454 (by forward demodulation #[453, 23]): Ne (op e4 e1) e0 % 6.68/6.85 Clause #455 (by backward contextual literal cutting #[454, 346]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e2) (Eq (op e4 e1) e1))) % 6.68/6.85 Clause #472 (by superposition #[455, 303]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e1) (Eq (op e4 e2) e4))) % 6.68/6.85 Clause #479 (by superposition #[472, 318]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e1) (Eq (op e4 e3) e2))) % 6.68/6.85 Clause #482 (by forward demodulation #[479, 417]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e1) (Eq e3 e2))) % 6.68/6.85 Clause #483 (by forward contextual literal cutting #[482, 47]): Or (Eq (op e4 e1) e4) (Or (Eq (op e4 e1) e3) (Eq (op e4 e1) e1)) % 6.68/6.85 Clause #484 (by superposition #[483, 303]): Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e1) (Eq (op e4 e4) e4)) % 6.68/6.85 Clause #489 (by superposition #[484, 23]): Or (Eq (op e4 e1) e3) (Or (Eq (op e4 e1) e1) (Eq e0 e4)) % 6.68/6.85 Clause #490 (by forward contextual literal cutting #[489, 73]): Or (Eq (op e4 e1) e3) (Eq (op e4 e1) e1) % 6.68/6.85 Clause #491 (by superposition #[490, 303]): Or (Eq (op e4 e1) e3) (Eq (op e4 e1) e4) % 6.68/6.85 Clause #498 (by superposition #[491, 490]): Or (Eq (op e4 e1) e3) (Or (Eq e4 e3) (Eq e4 e1)) % 6.68/6.85 Clause #500 (by forward contextual literal cutting #[498, 41]): Or (Eq (op e4 e1) e3) (Eq e4 e1) % 6.68/6.85 Clause #501 (by forward contextual literal cutting #[500, 50]): Eq (op e4 e1) e3 % 6.68/6.85 Clause #502 (by backward demodulation #[501, 303]): Eq (op e4 e3) e4 % 6.68/6.85 Clause #505 (by superposition #[502, 417]): Eq e4 e3 % 6.68/6.85 Clause #508 (by forward contextual literal cutting #[505, 41]): False % 6.68/6.85 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------