%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG174+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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 12.11s 12.29s % Output : Proof 12.87s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG174+1 : TPTP v9.2.0. Released v2.7.0. % 0.14/0.14 % Command : duper %s % 0.14/0.35 % Computer : n027.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 09:37:23 EDT 2025 % 0.14/0.35 % CPUTime : % 12.11/12.29 SZS status Theorem for theBenchmark.p % 12.11/12.29 SZS output start Proof for theBenchmark.p % 12.11/12.29 Clause #0 (by assumption #[]): Eq % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (And % 12.11/12.29 (Or % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 12.11/12.29 (Eq (op e0 e0) e3)) % 12.11/12.29 (Eq (op e0 e0) e4)) % 12.11/12.29 (Or % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 12.11/12.29 (Eq (op e0 e1) e3)) % 12.11/12.29 (Eq (op e0 e1) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 12.11/12.29 (Eq (op e0 e2) e3)) % 12.11/12.29 (Eq (op e0 e2) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 12.11/12.29 (Eq (op e0 e3) e3)) % 12.11/12.29 (Eq (op e0 e3) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 12.11/12.29 (Eq (op e0 e4) e3)) % 12.11/12.29 (Eq (op e0 e4) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 12.11/12.29 (Eq (op e1 e0) e3)) % 12.11/12.29 (Eq (op e1 e0) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 12.11/12.29 (Eq (op e1 e1) e3)) % 12.11/12.29 (Eq (op e1 e1) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 12.11/12.29 (Eq (op e1 e2) e3)) % 12.11/12.29 (Eq (op e1 e2) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 12.11/12.29 (Eq (op e1 e3) e3)) % 12.11/12.29 (Eq (op e1 e3) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 12.11/12.29 (Eq (op e1 e4) e3)) % 12.11/12.29 (Eq (op e1 e4) e4))) % 12.11/12.29 (Or % 12.11/12.29 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) % 12.11/12.29 (Eq (op e2 e0) e3)) % 12.11/12.29 (Eq (op e2 e0) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) % 12.17/12.35 (Eq (op e2 e1) e3)) % 12.17/12.35 (Eq (op e2 e1) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 12.17/12.35 (Eq (op e2 e2) e4))) % 12.17/12.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)) % 12.17/12.35 (Eq (op e2 e3) e4))) % 12.17/12.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)) % 12.17/12.35 (Eq (op e2 e4) e4))) % 12.17/12.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)) % 12.17/12.35 (Eq (op e3 e0) e4))) % 12.17/12.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)) % 12.17/12.35 (Eq (op e3 e1) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 12.17/12.35 (Eq (op e3 e2) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 12.17/12.35 (Eq (op e3 e3) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 12.17/12.35 (Eq (op e3 e4) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 12.17/12.35 (Eq (op e4 e0) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 12.17/12.35 (Eq (op e4 e1) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) % 12.17/12.35 (Eq (op e4 e2) e4))) % 12.17/12.35 (Or (Or (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) (Eq (op e4 e3) e3)) % 12.17/12.35 (Eq (op e4 e3) e4))) % 12.17/12.35 (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))) % 12.17/12.35 True % 12.17/12.35 Clause #1 (by assumption #[]): Eq % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (And % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Eq % 12.17/12.35 (op e0 e0) % 12.17/12.35 e0) % 12.17/12.35 (Eq % 12.17/12.35 (op e0 e1) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e0 e2) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e0 e3) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e0 e4) % 12.17/12.35 e0)) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Eq % 12.17/12.35 (op e0 e0) % 12.17/12.35 e0) % 12.17/12.35 (Eq % 12.17/12.35 (op e1 e0) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e2 e0) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e3 e0) % 12.17/12.35 e0)) % 12.17/12.35 (Eq (op e4 e0) % 12.17/12.35 e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Eq (op e0 e0) % 12.17/12.35 e1) % 12.17/12.35 (Eq (op e0 e1) % 12.17/12.35 e1)) % 12.17/12.35 (Eq (op e0 e2) % 12.17/12.35 e1)) % 12.17/12.35 (Eq (op e0 e3) % 12.17/12.35 e1)) % 12.17/12.35 (Eq (op e0 e4) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Eq (op e0 e0) % 12.17/12.35 e1) % 12.17/12.35 (Eq (op e1 e0) % 12.17/12.35 e1)) % 12.17/12.35 (Eq (op e2 e0) % 12.17/12.35 e1)) % 12.17/12.35 (Eq (op e3 e0) e1)) % 12.17/12.35 (Eq (op e4 e0) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Eq (op e0 e0) e2) % 12.17/12.35 (Eq (op e0 e1) % 12.17/12.35 e2)) % 12.17/12.35 (Eq (op e0 e2) e2)) % 12.17/12.35 (Eq (op e0 e3) e2)) % 12.17/12.35 (Eq (op e0 e4) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e0) e2) % 12.17/12.35 (Eq (op e1 e0) e2)) % 12.17/12.35 (Eq (op e2 e0) e2)) % 12.17/12.35 (Eq (op e3 e0) e2)) % 12.17/12.35 (Eq (op e4 e0) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e0) e3) % 12.17/12.35 (Eq (op e0 e1) e3)) % 12.17/12.35 (Eq (op e0 e2) e3)) % 12.17/12.35 (Eq (op e0 e3) e3)) % 12.17/12.35 (Eq (op e0 e4) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e0) e3) % 12.17/12.35 (Eq (op e1 e0) e3)) % 12.17/12.35 (Eq (op e2 e0) e3)) % 12.17/12.35 (Eq (op e3 e0) e3)) % 12.17/12.35 (Eq (op e4 e0) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e0) e4) % 12.17/12.35 (Eq (op e0 e1) e4)) % 12.17/12.35 (Eq (op e0 e2) e4)) % 12.17/12.35 (Eq (op e0 e3) e4)) % 12.17/12.35 (Eq (op e0 e4) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e0) e4) % 12.17/12.35 (Eq (op e1 e0) e4)) % 12.17/12.35 (Eq (op e2 e0) e4)) % 12.17/12.35 (Eq (op e3 e0) e4)) % 12.17/12.35 (Eq (op e4 e0) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e1 e0) e0) % 12.17/12.35 (Eq (op e1 e1) e0)) % 12.17/12.35 (Eq (op e1 e2) e0)) % 12.17/12.35 (Eq (op e1 e3) e0)) % 12.17/12.35 (Eq (op e1 e4) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e1) e0) % 12.17/12.35 (Eq (op e1 e1) e0)) % 12.17/12.35 (Eq (op e2 e1) e0)) % 12.17/12.35 (Eq (op e3 e1) e0)) % 12.17/12.35 (Eq (op e4 e1) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e1 e0) e1) % 12.17/12.35 (Eq (op e1 e1) e1)) % 12.17/12.35 (Eq (op e1 e2) e1)) % 12.17/12.35 (Eq (op e1 e3) e1)) % 12.17/12.35 (Eq (op e1 e4) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e1) e1) % 12.17/12.35 (Eq (op e1 e1) e1)) % 12.17/12.35 (Eq (op e2 e1) e1)) % 12.17/12.35 (Eq (op e3 e1) e1)) % 12.17/12.35 (Eq (op e4 e1) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e1 e0) e2) % 12.17/12.35 (Eq (op e1 e1) e2)) % 12.17/12.35 (Eq (op e1 e2) e2)) % 12.17/12.35 (Eq (op e1 e3) e2)) % 12.17/12.35 (Eq (op e1 e4) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 12.17/12.35 (Eq (op e2 e1) e2)) % 12.17/12.35 (Eq (op e3 e1) e2)) % 12.17/12.35 (Eq (op e4 e1) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 12.17/12.35 (Eq (op e1 e2) e3)) % 12.17/12.35 (Eq (op e1 e3) e3)) % 12.17/12.35 (Eq (op e1 e4) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 12.17/12.35 (Eq (op e2 e1) e3)) % 12.17/12.35 (Eq (op e3 e1) e3)) % 12.17/12.35 (Eq (op e4 e1) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 12.17/12.35 (Eq (op e1 e2) e4)) % 12.17/12.35 (Eq (op e1 e3) e4)) % 12.17/12.35 (Eq (op e1 e4) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 12.17/12.35 (Eq (op e2 e1) e4)) % 12.17/12.35 (Eq (op e3 e1) e4)) % 12.17/12.35 (Eq (op e4 e1) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 12.17/12.35 (Eq (op e2 e2) e0)) % 12.17/12.35 (Eq (op e2 e3) e0)) % 12.17/12.35 (Eq (op e2 e4) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 12.17/12.35 (Eq (op e2 e2) e0)) % 12.17/12.35 (Eq (op e3 e2) e0)) % 12.17/12.35 (Eq (op e4 e2) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 12.17/12.35 (Eq (op e2 e2) e1)) % 12.17/12.35 (Eq (op e2 e3) e1)) % 12.17/12.35 (Eq (op e2 e4) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 12.17/12.35 (Eq (op e2 e2) e1)) % 12.17/12.35 (Eq (op e3 e2) e1)) % 12.17/12.35 (Eq (op e4 e2) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) % 12.17/12.35 (Eq (op e2 e2) e2)) % 12.17/12.35 (Eq (op e2 e3) e2)) % 12.17/12.35 (Eq (op e2 e4) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) % 12.17/12.35 (Eq (op e2 e2) e2)) % 12.17/12.35 (Eq (op e3 e2) e2)) % 12.17/12.35 (Eq (op e4 e2) e2))) % 12.17/12.35 (Or % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 12.17/12.35 (Eq (op e2 e3) e3)) % 12.17/12.35 (Eq (op e2 e4) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 12.17/12.35 (Eq (op e3 e2) e3)) % 12.17/12.35 (Eq (op e4 e2) e3))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 12.17/12.35 (Eq (op e2 e3) e4)) % 12.17/12.35 (Eq (op e2 e4) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 12.17/12.35 (Eq (op e3 e2) e4)) % 12.17/12.35 (Eq (op e4 e2) e4))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 12.17/12.35 (Eq (op e3 e3) e0)) % 12.17/12.35 (Eq (op e3 e4) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 12.17/12.35 (Eq (op e3 e3) e0)) % 12.17/12.35 (Eq (op e4 e3) e0))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 12.17/12.35 (Eq (op e3 e3) e1)) % 12.17/12.35 (Eq (op e3 e4) e1))) % 12.17/12.35 (Or % 12.17/12.35 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 12.17/12.35 (Eq (op e3 e3) e1)) % 12.17/12.35 (Eq (op e4 e3) e1))) % 12.17/12.36 (Or % 12.17/12.36 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 12.17/12.36 (Eq (op e3 e3) e2)) % 12.17/12.36 (Eq (op e3 e4) e2))) % 12.17/12.36 (Or % 12.17/12.36 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) % 12.17/12.36 (Eq (op e3 e3) e2)) % 12.17/12.36 (Eq (op e4 e3) e2))) % 12.17/12.36 (Or % 12.17/12.36 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) % 12.17/12.36 (Eq (op e3 e3) e3)) % 12.17/12.36 (Eq (op e3 e4) e3))) % 12.17/12.36 (Or % 12.17/12.36 (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 12.17/12.36 (Eq (op e4 e3) e3))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 12.17/12.36 (Eq (op e3 e4) e4))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 12.17/12.36 (Eq (op e4 e3) e4))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 12.17/12.36 (Eq (op e4 e4) e0))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 12.17/12.36 (Eq (op e4 e4) e0))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 12.17/12.36 (Eq (op e4 e4) e1))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 12.17/12.36 (Eq (op e4 e4) e1))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 12.17/12.36 (Eq (op e4 e4) e2))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 12.17/12.36 (Eq (op e4 e4) e2))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 12.17/12.36 (Eq (op e4 e4) e3))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) % 12.17/12.36 (Eq (op e4 e4) e3))) % 12.17/12.36 (Or (Or (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) (Eq (op e4 e3) e4)) % 12.17/12.36 (Eq (op e4 e4) e4))) % 12.17/12.36 (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))) % 12.17/12.36 True % 12.17/12.36 Clause #2 (by assumption #[]): Eq % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And % 12.17/12.36 (And (Eq (op (op e0 e0) (op e0 e0)) e0) % 12.17/12.36 (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.17/12.36 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.17/12.36 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.17/12.36 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.17/12.36 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.17/12.36 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.17/12.36 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.17/12.40 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.17/12.40 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.17/12.40 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.17/12.40 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.17/12.40 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.17/12.40 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.17/12.40 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.17/12.40 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.17/12.40 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.17/12.40 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.17/12.40 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.17/12.40 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.17/12.40 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 12.17/12.40 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 12.17/12.40 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 12.17/12.40 (Eq (op (op e3 e4) (op e4 e3)) e4)) % 12.17/12.40 (Eq (op (op e4 e4) (op e4 e4)) e4)) % 12.17/12.40 True % 12.17/12.40 Clause #3 (by assumption #[]): Eq % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (And % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e0)) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e0) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e0))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e1) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e1))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e2) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e2))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e3) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e3))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e4) % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e4) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e4) % 12.17/12.40 (op % 12.17/12.40 e3 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e0 % 12.17/12.40 e4) % 12.17/12.40 (op % 12.17/12.40 e4 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op % 12.17/12.40 e1 % 12.17/12.40 e4) % 12.17/12.40 (op % 12.17/12.40 e2 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op e1 % 12.17/12.40 e4) % 12.17/12.40 (op e3 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op e1 % 12.17/12.40 e4) % 12.17/12.40 (op e4 % 12.17/12.40 e4))) % 12.17/12.40 (Ne % 12.17/12.40 (op e2 e4) % 12.17/12.40 (op e3 % 12.17/12.40 e4))) % 12.17/12.40 (Ne (op e2 e4) % 12.17/12.40 (op e4 e4))) % 12.17/12.40 (Ne (op e3 e4) % 12.17/12.40 (op e4 e4))) % 12.17/12.40 (Ne (op e0 e0) % 12.17/12.40 (op e0 e1))) % 12.17/12.40 (Ne (op e0 e0) % 12.17/12.40 (op e0 e2))) % 12.17/12.40 (Ne (op e0 e0) % 12.17/12.40 (op e0 e3))) % 12.17/12.40 (Ne (op e0 e0) % 12.17/12.40 (op e0 e4))) % 12.17/12.40 (Ne (op e0 e1) % 12.17/12.40 (op e0 e2))) % 12.17/12.40 (Ne (op e0 e1) (op e0 e3))) % 12.17/12.40 (Ne (op e0 e1) (op e0 e4))) % 12.17/12.40 (Ne (op e0 e2) (op e0 e3))) % 12.17/12.40 (Ne (op e0 e2) (op e0 e4))) % 12.17/12.40 (Ne (op e0 e3) (op e0 e4))) % 12.17/12.40 (Ne (op e1 e0) (op e1 e1))) % 12.17/12.40 (Ne (op e1 e0) (op e1 e2))) % 12.17/12.40 (Ne (op e1 e0) (op e1 e3))) % 12.17/12.40 (Ne (op e1 e0) (op e1 e4))) % 12.17/12.40 (Ne (op e1 e1) (op e1 e2))) % 12.17/12.40 (Ne (op e1 e1) (op e1 e3))) % 12.17/12.40 (Ne (op e1 e1) (op e1 e4))) % 12.17/12.40 (Ne (op e1 e2) (op e1 e3))) % 12.17/12.40 (Ne (op e1 e2) (op e1 e4))) % 12.17/12.40 (Ne (op e1 e3) (op e1 e4))) % 12.17/12.40 (Ne (op e2 e0) (op e2 e1))) % 12.17/12.40 (Ne (op e2 e0) (op e2 e2))) % 12.17/12.40 (Ne (op e2 e0) (op e2 e3))) % 12.17/12.40 (Ne (op e2 e0) (op e2 e4))) % 12.17/12.40 (Ne (op e2 e1) (op e2 e2))) % 12.17/12.40 (Ne (op e2 e1) (op e2 e3))) % 12.17/12.40 (Ne (op e2 e1) (op e2 e4))) % 12.17/12.40 (Ne (op e2 e2) (op e2 e3))) % 12.17/12.40 (Ne (op e2 e2) (op e2 e4))) % 12.17/12.40 (Ne (op e2 e3) (op e2 e4))) % 12.17/12.40 (Ne (op e3 e0) (op e3 e1))) % 12.17/12.40 (Ne (op e3 e0) (op e3 e2))) % 12.17/12.40 (Ne (op e3 e0) (op e3 e3))) % 12.17/12.40 (Ne (op e3 e0) (op e3 e4))) % 12.17/12.40 (Ne (op e3 e1) (op e3 e2))) % 12.17/12.40 (Ne (op e3 e1) (op e3 e3))) % 12.17/12.40 (Ne (op e3 e1) (op e3 e4))) % 12.17/12.40 (Ne (op e3 e2) (op e3 e3))) % 12.17/12.40 (Ne (op e3 e2) (op e3 e4))) % 12.17/12.40 (Ne (op e3 e3) (op e3 e4))) % 12.17/12.40 (Ne (op e4 e0) (op e4 e1))) % 12.17/12.41 (Ne (op e4 e0) (op e4 e2))) % 12.17/12.41 (Ne (op e4 e0) (op e4 e3))) % 12.17/12.41 (Ne (op e4 e0) (op e4 e4))) % 12.17/12.41 (Ne (op e4 e1) (op e4 e2))) % 12.17/12.41 (Ne (op e4 e1) (op e4 e3))) % 12.17/12.41 (Ne (op e4 e1) (op e4 e4))) % 12.17/12.41 (Ne (op e4 e2) (op e4 e3))) % 12.17/12.41 (Ne (op e4 e2) (op e4 e4))) % 12.17/12.41 (Ne (op e4 e3) (op e4 e4))) % 12.17/12.41 True % 12.17/12.41 Clause #4 (by assumption #[]): Eq % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (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)) % 12.17/12.41 (Ne e2 e3)) % 12.17/12.41 (Ne e2 e4)) % 12.17/12.41 (Ne e3 e4)) % 12.17/12.41 True % 12.17/12.41 Clause #5 (by assumption #[]): Eq % 12.17/12.41 (And % 12.17/12.41 (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))) % 12.17/12.41 (Eq e4 (op e3 (op e3 e3)))) % 12.17/12.41 True % 12.17/12.41 Clause #6 (by assumption #[]): Eq % 12.17/12.41 (Not % 12.17/12.41 (Not % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (Or % 12.17/12.41 (Or % 12.17/12.41 (Or % 12.17/12.41 (Or % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.17/12.41 (Ne (op e0 e2) e2)) % 12.17/12.41 (Ne (op e0 e3) e3)) % 12.17/12.41 (Ne (op e0 e4) e4)) % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.17/12.41 (Ne (op e1 e2) e2)) % 12.17/12.41 (Ne (op e1 e3) e3)) % 12.17/12.41 (Ne (op e1 e4) e4))) % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.17/12.41 (Ne (op e2 e2) e2)) % 12.17/12.41 (Ne (op e2 e3) e3)) % 12.17/12.41 (Ne (op e2 e4) e4))) % 12.17/12.41 (And % 12.17/12.41 (And % 12.17/12.41 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.17/12.41 (Ne (op e3 e2) e2)) % 12.17/12.41 (Ne (op e3 e3) e3)) % 12.17/12.41 (Ne (op e3 e4) e4))) % 12.17/12.41 (And % 12.26/12.45 (And % 12.26/12.45 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 12.26/12.45 (Ne (op e4 e2) e2)) % 12.26/12.45 (Ne (op e4 e3) e3)) % 12.26/12.45 (Ne (op e4 e4) e4))) % 12.26/12.45 (Eq (op (op e0 e0) e0) e0)) % 12.26/12.45 (Eq (op (op e0 e1) e1) e0)) % 12.26/12.45 (Eq (op (op e0 e2) e2) e0)) % 12.26/12.45 (Eq (op (op e0 e3) e3) e0)) % 12.26/12.45 (Eq (op (op e0 e4) e4) e0)) % 12.26/12.45 (Eq (op (op e1 e0) e0) e1)) % 12.26/12.45 (Eq (op (op e1 e1) e1) e1)) % 12.26/12.45 (Eq (op (op e1 e2) e2) e1)) % 12.26/12.45 (Eq (op (op e1 e3) e3) e1)) % 12.26/12.45 (Eq (op (op e1 e4) e4) e1)) % 12.26/12.45 (Eq (op (op e2 e0) e0) e2)) % 12.26/12.45 (Eq (op (op e2 e1) e1) e2)) % 12.26/12.45 (Eq (op (op e2 e2) e2) e2)) % 12.26/12.45 (Eq (op (op e2 e3) e3) e2)) % 12.26/12.45 (Eq (op (op e2 e4) e4) e2)) % 12.26/12.45 (Eq (op (op e3 e0) e0) e3)) % 12.26/12.45 (Eq (op (op e3 e1) e1) e3)) % 12.26/12.45 (Eq (op (op e3 e2) e2) e3)) % 12.26/12.45 (Eq (op (op e3 e3) e3) e3)) % 12.26/12.45 (Eq (op (op e3 e4) e4) e3)) % 12.26/12.45 (Eq (op (op e4 e0) e0) e4)) % 12.26/12.45 (Eq (op (op e4 e1) e1) e4)) % 12.26/12.45 (Eq (op (op e4 e2) e2) e4)) % 12.26/12.45 (Eq (op (op e4 e3) e3) e4)) % 12.26/12.45 (Eq (op (op e4 e4) e4) e4)))) % 12.26/12.45 True % 12.26/12.45 Clause #7 (by clausification #[5]): Eq (Eq e4 (op e3 (op e3 e3))) True % 12.26/12.45 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))) % 12.26/12.45 True % 12.26/12.45 Clause #9 (by clausification #[7]): Eq e4 (op e3 (op e3 e3)) % 12.26/12.45 Clause #10 (by clausification #[8]): Eq (Eq e2 (op e3 e3)) True % 12.26/12.45 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 % 12.26/12.45 Clause #12 (by clausification #[10]): Eq e2 (op e3 e3) % 12.26/12.45 Clause #13 (by backward demodulation #[12, 9]): Eq e4 (op e3 e2) % 12.26/12.45 Clause #14 (by clausification #[11]): Eq (Eq e1 (op e3 (op e3 (op e3 e3)))) True % 12.26/12.45 Clause #15 (by clausification #[11]): Eq (Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3)))) True % 12.26/12.45 Clause #16 (by clausification #[14]): Eq e1 (op e3 (op e3 (op e3 e3))) % 12.26/12.45 Clause #17 (by forward demodulation #[16, 12]): Eq e1 (op e3 (op e3 e2)) % 12.26/12.45 Clause #18 (by forward demodulation #[17, 13]): Eq e1 (op e3 e4) % 12.26/12.45 Clause #19 (by clausification #[15]): Eq e0 (op (op e3 (op e3 e3)) (op e3 (op e3 e3))) % 12.26/12.45 Clause #20 (by forward demodulation #[19, 12]): Eq e0 (op (op e3 (op e3 e3)) (op e3 e2)) % 12.26/12.45 Clause #21 (by forward demodulation #[20, 13]): Eq e0 (op (op e3 (op e3 e3)) e4) % 12.26/12.45 Clause #22 (by forward demodulation #[21, 12]): Eq e0 (op (op e3 e2) e4) % 12.26/12.45 Clause #23 (by forward demodulation #[22, 13]): Eq e0 (op e4 e4) % 12.26/12.45 Clause #25 (by clausification #[0]): Eq % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (And % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 12.26/12.45 (Eq (op e0 e0) e3)) % 12.26/12.45 (Eq (op e0 e0) e4)) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 12.26/12.45 (Eq (op e0 e1) e3)) % 12.26/12.45 (Eq (op e0 e1) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 12.26/12.45 (Eq (op e0 e2) e3)) % 12.26/12.45 (Eq (op e0 e2) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 12.26/12.45 (Eq (op e0 e3) e3)) % 12.26/12.45 (Eq (op e0 e3) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 12.26/12.45 (Eq (op e0 e4) e3)) % 12.26/12.45 (Eq (op e0 e4) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 12.26/12.45 (Eq (op e1 e0) e3)) % 12.26/12.45 (Eq (op e1 e0) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 12.26/12.45 (Eq (op e1 e1) e3)) % 12.26/12.45 (Eq (op e1 e1) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 12.26/12.45 (Eq (op e1 e2) e3)) % 12.26/12.45 (Eq (op e1 e2) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 12.26/12.45 (Eq (op e1 e3) e3)) % 12.26/12.45 (Eq (op e1 e3) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 12.26/12.45 (Eq (op e1 e4) e3)) % 12.26/12.45 (Eq (op e1 e4) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) % 12.26/12.45 (Eq (op e2 e0) e3)) % 12.26/12.45 (Eq (op e2 e0) e4))) % 12.26/12.45 (Or % 12.26/12.45 (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) (Eq (op e2 e1) e3)) % 12.26/12.45 (Eq (op e2 e1) e4))) % 12.26/12.45 (Or (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 12.26/12.45 (Eq (op e2 e2) e4))) % 12.26/12.45 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 12.26/12.45 (Eq (op e2 e3) e4))) % 12.26/12.45 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 12.26/12.45 (Eq (op e2 e4) e4))) % 12.26/12.45 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 12.26/12.45 (Eq (op e3 e0) e4))) % 12.26/12.45 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 12.26/12.45 (Eq (op e3 e1) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 12.32/12.52 (Eq (op e3 e2) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 12.32/12.52 (Eq (op e3 e3) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 12.32/12.52 (Eq (op e3 e4) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 12.32/12.52 (Eq (op e4 e0) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 12.32/12.52 (Eq (op e4 e1) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) % 12.32/12.52 (Eq (op e4 e2) e4))) % 12.32/12.52 (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))) % 12.32/12.52 True % 12.32/12.52 Clause #39 (by clausification #[4]): Eq (Ne e3 e4) True % 12.32/12.52 Clause #40 (by clausification #[4]): Eq % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (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)) % 12.32/12.52 (Ne e2 e3)) % 12.32/12.52 (Ne e2 e4)) % 12.32/12.52 True % 12.32/12.52 Clause #41 (by clausification #[39]): Ne e3 e4 % 12.32/12.52 Clause #42 (by clausification #[40]): Eq (Ne e2 e4) True % 12.32/12.52 Clause #43 (by clausification #[40]): Eq % 12.32/12.52 (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)) % 12.32/12.52 (Ne e2 e3)) % 12.32/12.52 True % 12.32/12.52 Clause #44 (by clausification #[42]): Ne e2 e4 % 12.32/12.52 Clause #45 (by clausification #[43]): Eq (Ne e2 e3) True % 12.32/12.52 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 % 12.32/12.52 Clause #47 (by clausification #[45]): Ne e2 e3 % 12.32/12.52 Clause #48 (by clausification #[46]): Eq (Ne e1 e4) True % 12.32/12.52 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 % 12.32/12.52 Clause #50 (by clausification #[48]): Ne e1 e4 % 12.32/12.52 Clause #51 (by clausification #[49]): Eq (Ne e1 e3) True % 12.32/12.52 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 % 12.32/12.52 Clause #53 (by clausification #[51]): Ne e1 e3 % 12.32/12.52 Clause #55 (by clausification #[1]): Eq % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (And % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Eq (op e0 e0) % 12.32/12.52 e0) % 12.32/12.52 (Eq (op e0 e1) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e0 e2) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e0 e3) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e0 e4) e0)) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Eq (op e0 e0) % 12.32/12.52 e0) % 12.32/12.52 (Eq (op e1 e0) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e2 e0) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e3 e0) % 12.32/12.52 e0)) % 12.32/12.52 (Eq (op e4 e0) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Eq (op e0 e0) % 12.32/12.52 e1) % 12.32/12.52 (Eq (op e0 e1) % 12.32/12.52 e1)) % 12.32/12.52 (Eq (op e0 e2) % 12.32/12.52 e1)) % 12.32/12.52 (Eq (op e0 e3) e1)) % 12.32/12.52 (Eq (op e0 e4) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Eq (op e0 e0) e1) % 12.32/12.52 (Eq (op e1 e0) % 12.32/12.52 e1)) % 12.32/12.52 (Eq (op e2 e0) e1)) % 12.32/12.52 (Eq (op e3 e0) e1)) % 12.32/12.52 (Eq (op e4 e0) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e2) % 12.32/12.52 (Eq (op e0 e1) e2)) % 12.32/12.52 (Eq (op e0 e2) e2)) % 12.32/12.52 (Eq (op e0 e3) e2)) % 12.32/12.52 (Eq (op e0 e4) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e2) % 12.32/12.52 (Eq (op e1 e0) e2)) % 12.32/12.52 (Eq (op e2 e0) e2)) % 12.32/12.52 (Eq (op e3 e0) e2)) % 12.32/12.52 (Eq (op e4 e0) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e3) % 12.32/12.52 (Eq (op e0 e1) e3)) % 12.32/12.52 (Eq (op e0 e2) e3)) % 12.32/12.52 (Eq (op e0 e3) e3)) % 12.32/12.52 (Eq (op e0 e4) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e3) % 12.32/12.52 (Eq (op e1 e0) e3)) % 12.32/12.52 (Eq (op e2 e0) e3)) % 12.32/12.52 (Eq (op e3 e0) e3)) % 12.32/12.52 (Eq (op e4 e0) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e4) % 12.32/12.52 (Eq (op e0 e1) e4)) % 12.32/12.52 (Eq (op e0 e2) e4)) % 12.32/12.52 (Eq (op e0 e3) e4)) % 12.32/12.52 (Eq (op e0 e4) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e0) e4) % 12.32/12.52 (Eq (op e1 e0) e4)) % 12.32/12.52 (Eq (op e2 e0) e4)) % 12.32/12.52 (Eq (op e3 e0) e4)) % 12.32/12.52 (Eq (op e4 e0) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e1 e0) e0) % 12.32/12.52 (Eq (op e1 e1) e0)) % 12.32/12.52 (Eq (op e1 e2) e0)) % 12.32/12.52 (Eq (op e1 e3) e0)) % 12.32/12.52 (Eq (op e1 e4) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e1) e0) % 12.32/12.52 (Eq (op e1 e1) e0)) % 12.32/12.52 (Eq (op e2 e1) e0)) % 12.32/12.52 (Eq (op e3 e1) e0)) % 12.32/12.52 (Eq (op e4 e1) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e1 e0) e1) % 12.32/12.52 (Eq (op e1 e1) e1)) % 12.32/12.52 (Eq (op e1 e2) e1)) % 12.32/12.52 (Eq (op e1 e3) e1)) % 12.32/12.52 (Eq (op e1 e4) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e0 e1) e1) % 12.32/12.52 (Eq (op e1 e1) e1)) % 12.32/12.52 (Eq (op e2 e1) e1)) % 12.32/12.52 (Eq (op e3 e1) e1)) % 12.32/12.52 (Eq (op e4 e1) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 12.32/12.52 (Eq (op e1 e2) e2)) % 12.32/12.52 (Eq (op e1 e3) e2)) % 12.32/12.52 (Eq (op e1 e4) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 12.32/12.52 (Eq (op e2 e1) e2)) % 12.32/12.52 (Eq (op e3 e1) e2)) % 12.32/12.52 (Eq (op e4 e1) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 12.32/12.52 (Eq (op e1 e2) e3)) % 12.32/12.52 (Eq (op e1 e3) e3)) % 12.32/12.52 (Eq (op e1 e4) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 12.32/12.52 (Eq (op e2 e1) e3)) % 12.32/12.52 (Eq (op e3 e1) e3)) % 12.32/12.52 (Eq (op e4 e1) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 12.32/12.52 (Eq (op e1 e2) e4)) % 12.32/12.52 (Eq (op e1 e3) e4)) % 12.32/12.52 (Eq (op e1 e4) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 12.32/12.52 (Eq (op e2 e1) e4)) % 12.32/12.52 (Eq (op e3 e1) e4)) % 12.32/12.52 (Eq (op e4 e1) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 12.32/12.52 (Eq (op e2 e2) e0)) % 12.32/12.52 (Eq (op e2 e3) e0)) % 12.32/12.52 (Eq (op e2 e4) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 12.32/12.52 (Eq (op e2 e2) e0)) % 12.32/12.52 (Eq (op e3 e2) e0)) % 12.32/12.52 (Eq (op e4 e2) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 12.32/12.52 (Eq (op e2 e2) e1)) % 12.32/12.52 (Eq (op e2 e3) e1)) % 12.32/12.52 (Eq (op e2 e4) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 12.32/12.52 (Eq (op e2 e2) e1)) % 12.32/12.52 (Eq (op e3 e2) e1)) % 12.32/12.52 (Eq (op e4 e2) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) % 12.32/12.52 (Eq (op e2 e2) e2)) % 12.32/12.52 (Eq (op e2 e3) e2)) % 12.32/12.52 (Eq (op e2 e4) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 12.32/12.52 (Eq (op e3 e2) e2)) % 12.32/12.52 (Eq (op e4 e2) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 12.32/12.52 (Eq (op e2 e3) e3)) % 12.32/12.52 (Eq (op e2 e4) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 12.32/12.52 (Eq (op e3 e2) e3)) % 12.32/12.52 (Eq (op e4 e2) e3))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 12.32/12.52 (Eq (op e2 e3) e4)) % 12.32/12.52 (Eq (op e2 e4) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 12.32/12.52 (Eq (op e3 e2) e4)) % 12.32/12.52 (Eq (op e4 e2) e4))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 12.32/12.52 (Eq (op e3 e3) e0)) % 12.32/12.52 (Eq (op e3 e4) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 12.32/12.52 (Eq (op e3 e3) e0)) % 12.32/12.52 (Eq (op e4 e3) e0))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 12.32/12.52 (Eq (op e3 e3) e1)) % 12.32/12.52 (Eq (op e3 e4) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 12.32/12.52 (Eq (op e3 e3) e1)) % 12.32/12.52 (Eq (op e4 e3) e1))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 12.32/12.52 (Eq (op e3 e3) e2)) % 12.32/12.52 (Eq (op e3 e4) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) % 12.32/12.52 (Eq (op e3 e3) e2)) % 12.32/12.52 (Eq (op e4 e3) e2))) % 12.32/12.52 (Or % 12.32/12.52 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 12.32/12.52 (Eq (op e3 e4) e3))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 12.32/12.52 (Eq (op e4 e3) e3))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 12.32/12.52 (Eq (op e3 e4) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 12.32/12.52 (Eq (op e4 e3) e4))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 12.32/12.52 (Eq (op e4 e4) e0))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 12.32/12.52 (Eq (op e4 e4) e0))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 12.32/12.52 (Eq (op e4 e4) e1))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 12.32/12.52 (Eq (op e4 e4) e1))) % 12.32/12.52 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 12.32/12.54 (Eq (op e4 e4) e2))) % 12.32/12.54 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 12.32/12.54 (Eq (op e4 e4) e2))) % 12.32/12.54 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 12.32/12.54 (Eq (op e4 e4) e3))) % 12.32/12.54 (Or (Or (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) (Eq (op e3 e4) e3)) % 12.32/12.54 (Eq (op e4 e4) e3))) % 12.32/12.54 (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))) % 12.32/12.54 True % 12.32/12.54 Clause #68 (by clausification #[52]): Eq (Ne e1 e2) True % 12.32/12.54 Clause #69 (by clausification #[52]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e0 e4)) True % 12.32/12.54 Clause #70 (by clausification #[68]): Ne e1 e2 % 12.32/12.54 Clause #71 (by clausification #[69]): Eq (Ne e0 e4) True % 12.32/12.54 Clause #72 (by clausification #[69]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 12.32/12.54 Clause #73 (by clausification #[71]): Ne e0 e4 % 12.32/12.54 Clause #75 (by clausification #[72]): Eq (Ne e0 e3) True % 12.32/12.54 Clause #76 (by clausification #[72]): Eq (And (Ne e0 e1) (Ne e0 e2)) True % 12.32/12.54 Clause #77 (by clausification #[75]): Ne e0 e3 % 12.32/12.54 Clause #78 (by clausification #[76]): Eq (Ne e0 e2) True % 12.32/12.54 Clause #80 (by clausification #[78]): Ne e0 e2 % 12.32/12.54 Clause #82 (by clausification #[2]): Eq % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And (Eq (op (op e0 e0) (op e0 e0)) e0) % 12.32/12.54 (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.32/12.54 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.32/12.54 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.32/12.54 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.32/12.54 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.32/12.54 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.32/12.54 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.32/12.54 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.32/12.54 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.32/12.54 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.32/12.54 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.32/12.54 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.32/12.54 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.32/12.54 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.32/12.54 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.32/12.54 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.32/12.54 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.32/12.54 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.32/12.54 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.32/12.54 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 12.32/12.54 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 12.32/12.54 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 12.32/12.54 (Eq (op (op e3 e4) (op e4 e3)) e4)) % 12.32/12.54 True % 12.32/12.54 Clause #87 (by clausification #[82]): Eq (Eq (op (op e3 e4) (op e4 e3)) e4) True % 12.32/12.54 Clause #88 (by clausification #[82]): Eq % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.54 (And % 12.32/12.56 (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.32/12.56 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.32/12.56 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.32/12.56 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.32/12.56 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.32/12.56 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.32/12.56 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.32/12.56 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.32/12.56 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.32/12.56 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.32/12.56 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.32/12.56 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.32/12.56 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.32/12.56 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.32/12.56 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.32/12.56 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.32/12.56 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.32/12.56 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.32/12.56 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.32/12.56 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 12.32/12.56 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 12.32/12.56 (Eq (op (op e2 e4) (op e4 e2)) e4)) % 12.32/12.56 True % 12.32/12.56 Clause #89 (by clausification #[87]): Eq (op (op e3 e4) (op e4 e3)) e4 % 12.32/12.56 Clause #90 (by forward demodulation #[89, 18]): Eq (op e1 (op e4 e3)) e4 % 12.32/12.56 Clause #91 (by clausification #[88]): Eq (Eq (op (op e2 e4) (op e4 e2)) e4) True % 12.32/12.56 Clause #92 (by clausification #[88]): Eq % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.32/12.56 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.32/12.56 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.32/12.56 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.32/12.56 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.32/12.56 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.32/12.56 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.32/12.56 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.32/12.56 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.32/12.56 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.32/12.56 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.32/12.56 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.32/12.56 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.32/12.56 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.32/12.56 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.32/12.56 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.32/12.56 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.32/12.56 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.32/12.56 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.32/12.56 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 12.32/12.56 (Eq (op (op e1 e4) (op e4 e1)) e4)) % 12.32/12.56 True % 12.32/12.56 Clause #93 (by clausification #[91]): Eq (op (op e2 e4) (op e4 e2)) e4 % 12.32/12.56 Clause #94 (by clausification #[92]): Eq (Eq (op (op e1 e4) (op e4 e1)) e4) True % 12.32/12.56 Clause #95 (by clausification #[92]): Eq % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.32/12.56 (And % 12.41/12.60 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.41/12.60 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.41/12.60 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.41/12.60 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.41/12.60 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.41/12.60 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.41/12.60 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.41/12.60 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.41/12.60 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.41/12.60 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.41/12.60 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.41/12.60 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.41/12.60 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.41/12.60 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.41/12.60 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.41/12.60 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.41/12.60 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.41/12.60 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.41/12.60 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.41/12.60 (Eq (op (op e0 e4) (op e4 e0)) e4)) % 12.41/12.60 True % 12.41/12.60 Clause #96 (by clausification #[94]): Eq (op (op e1 e4) (op e4 e1)) e4 % 12.41/12.60 Clause #97 (by clausification #[95]): Eq (Eq (op (op e0 e4) (op e4 e0)) e4) True % 12.41/12.60 Clause #98 (by clausification #[95]): Eq % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.41/12.60 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.41/12.60 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.41/12.60 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.41/12.60 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.41/12.60 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.41/12.60 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.41/12.60 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.41/12.60 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.41/12.60 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.41/12.60 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.41/12.60 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.41/12.60 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.41/12.60 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.41/12.60 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.41/12.60 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.41/12.60 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.41/12.60 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.41/12.60 (Eq (op (op e4 e3) (op e3 e4)) e3)) % 12.41/12.60 True % 12.41/12.60 Clause #99 (by clausification #[97]): Eq (op (op e0 e4) (op e4 e0)) e4 % 12.41/12.60 Clause #101 (by clausification #[3]): Eq (Ne (op e4 e3) (op e4 e4)) True % 12.41/12.60 Clause #102 (by clausification #[3]): Eq % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (And % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e0)) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e0) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e0))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e1) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e1))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e2) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e2))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e3) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e3))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e4) % 12.41/12.60 (op % 12.41/12.60 e1 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e4) % 12.41/12.60 (op % 12.41/12.60 e2 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e4) % 12.41/12.60 (op % 12.41/12.60 e3 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op % 12.41/12.60 e0 % 12.41/12.60 e4) % 12.41/12.60 (op % 12.41/12.60 e4 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op e1 % 12.41/12.60 e4) % 12.41/12.60 (op e2 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op e1 % 12.41/12.60 e4) % 12.41/12.60 (op e3 % 12.41/12.60 e4))) % 12.41/12.60 (Ne % 12.41/12.60 (op e1 e4) % 12.41/12.60 (op e4 % 12.41/12.60 e4))) % 12.41/12.60 (Ne (op e2 e4) % 12.41/12.60 (op e3 e4))) % 12.41/12.60 (Ne (op e2 e4) % 12.41/12.60 (op e4 e4))) % 12.41/12.60 (Ne (op e3 e4) % 12.41/12.60 (op e4 e4))) % 12.41/12.60 (Ne (op e0 e0) % 12.41/12.60 (op e0 e1))) % 12.41/12.60 (Ne (op e0 e0) % 12.41/12.60 (op e0 e2))) % 12.41/12.60 (Ne (op e0 e0) % 12.41/12.60 (op e0 e3))) % 12.41/12.60 (Ne (op e0 e0) % 12.41/12.60 (op e0 e4))) % 12.41/12.60 (Ne (op e0 e1) (op e0 e2))) % 12.41/12.60 (Ne (op e0 e1) (op e0 e3))) % 12.41/12.60 (Ne (op e0 e1) (op e0 e4))) % 12.41/12.60 (Ne (op e0 e2) (op e0 e3))) % 12.41/12.60 (Ne (op e0 e2) (op e0 e4))) % 12.41/12.60 (Ne (op e0 e3) (op e0 e4))) % 12.41/12.60 (Ne (op e1 e0) (op e1 e1))) % 12.41/12.60 (Ne (op e1 e0) (op e1 e2))) % 12.41/12.60 (Ne (op e1 e0) (op e1 e3))) % 12.41/12.60 (Ne (op e1 e0) (op e1 e4))) % 12.41/12.60 (Ne (op e1 e1) (op e1 e2))) % 12.41/12.60 (Ne (op e1 e1) (op e1 e3))) % 12.41/12.60 (Ne (op e1 e1) (op e1 e4))) % 12.41/12.60 (Ne (op e1 e2) (op e1 e3))) % 12.41/12.60 (Ne (op e1 e2) (op e1 e4))) % 12.41/12.60 (Ne (op e1 e3) (op e1 e4))) % 12.41/12.60 (Ne (op e2 e0) (op e2 e1))) % 12.41/12.60 (Ne (op e2 e0) (op e2 e2))) % 12.41/12.60 (Ne (op e2 e0) (op e2 e3))) % 12.41/12.60 (Ne (op e2 e0) (op e2 e4))) % 12.41/12.60 (Ne (op e2 e1) (op e2 e2))) % 12.41/12.60 (Ne (op e2 e1) (op e2 e3))) % 12.41/12.60 (Ne (op e2 e1) (op e2 e4))) % 12.41/12.60 (Ne (op e2 e2) (op e2 e3))) % 12.41/12.60 (Ne (op e2 e2) (op e2 e4))) % 12.41/12.60 (Ne (op e2 e3) (op e2 e4))) % 12.41/12.60 (Ne (op e3 e0) (op e3 e1))) % 12.41/12.60 (Ne (op e3 e0) (op e3 e2))) % 12.41/12.62 (Ne (op e3 e0) (op e3 e3))) % 12.41/12.62 (Ne (op e3 e0) (op e3 e4))) % 12.41/12.62 (Ne (op e3 e1) (op e3 e2))) % 12.41/12.62 (Ne (op e3 e1) (op e3 e3))) % 12.41/12.62 (Ne (op e3 e1) (op e3 e4))) % 12.41/12.62 (Ne (op e3 e2) (op e3 e3))) % 12.41/12.62 (Ne (op e3 e2) (op e3 e4))) % 12.41/12.62 (Ne (op e3 e3) (op e3 e4))) % 12.41/12.62 (Ne (op e4 e0) (op e4 e1))) % 12.41/12.62 (Ne (op e4 e0) (op e4 e2))) % 12.41/12.62 (Ne (op e4 e0) (op e4 e3))) % 12.41/12.62 (Ne (op e4 e0) (op e4 e4))) % 12.41/12.62 (Ne (op e4 e1) (op e4 e2))) % 12.41/12.62 (Ne (op e4 e1) (op e4 e3))) % 12.41/12.62 (Ne (op e4 e1) (op e4 e4))) % 12.41/12.62 (Ne (op e4 e2) (op e4 e3))) % 12.41/12.62 (Ne (op e4 e2) (op e4 e4))) % 12.41/12.62 True % 12.41/12.62 Clause #103 (by clausification #[101]): Ne (op e4 e3) (op e4 e4) % 12.41/12.62 Clause #104 (by forward demodulation #[103, 23]): Ne (op e4 e3) e0 % 12.41/12.62 Clause #105 (by clausification #[98]): Eq (Eq (op (op e4 e3) (op e3 e4)) e3) True % 12.41/12.62 Clause #106 (by clausification #[98]): Eq % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.41/12.62 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.41/12.62 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.41/12.62 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.41/12.62 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.41/12.62 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.41/12.62 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.41/12.62 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.41/12.62 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.41/12.62 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.41/12.62 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.41/12.62 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.41/12.62 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.41/12.62 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.41/12.62 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.41/12.62 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.41/12.62 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.41/12.62 (Eq (op (op e3 e3) (op e3 e3)) e3)) % 12.41/12.62 True % 12.41/12.62 Clause #107 (by clausification #[105]): Eq (op (op e4 e3) (op e3 e4)) e3 % 12.41/12.62 Clause #108 (by forward demodulation #[107, 18]): Eq (op (op e4 e3) e1) e3 % 12.41/12.62 Clause #109 (by clausification #[106]): Eq (Eq (op (op e3 e3) (op e3 e3)) e3) True % 12.41/12.62 Clause #110 (by clausification #[106]): Eq % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And % 12.41/12.62 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.41/12.62 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.41/12.62 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.41/12.62 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.41/12.62 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.41/12.62 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.41/12.62 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.41/12.62 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.41/12.62 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.41/12.62 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.41/12.62 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.41/12.62 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.41/12.62 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.41/12.62 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.41/12.62 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.41/12.62 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.41/12.62 (Eq (op (op e2 e3) (op e3 e2)) e3)) % 12.48/12.65 True % 12.48/12.65 Clause #111 (by clausification #[109]): Eq (op (op e3 e3) (op e3 e3)) e3 % 12.48/12.65 Clause #112 (by forward demodulation #[111, 12]): Eq (op (op e3 e3) e2) e3 % 12.48/12.65 Clause #113 (by forward demodulation #[112, 12]): Eq (op e2 e2) e3 % 12.48/12.65 Clause #114 (by clausification #[110]): Eq (Eq (op (op e2 e3) (op e3 e2)) e3) True % 12.48/12.65 Clause #115 (by clausification #[110]): Eq % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.48/12.65 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.48/12.65 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.48/12.65 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.48/12.65 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.48/12.65 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.48/12.65 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.48/12.65 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.48/12.65 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.48/12.65 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.48/12.65 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.48/12.65 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.48/12.65 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.48/12.65 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.48/12.65 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.48/12.65 (Eq (op (op e1 e3) (op e3 e1)) e3)) % 12.48/12.65 True % 12.48/12.65 Clause #116 (by clausification #[114]): Eq (op (op e2 e3) (op e3 e2)) e3 % 12.48/12.65 Clause #117 (by forward demodulation #[116, 13]): Eq (op (op e2 e3) e4) e3 % 12.48/12.65 Clause #118 (by clausification #[115]): Eq (Eq (op (op e1 e3) (op e3 e1)) e3) True % 12.48/12.65 Clause #119 (by clausification #[115]): Eq % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.48/12.65 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.48/12.65 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.48/12.65 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.48/12.65 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.48/12.65 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.48/12.65 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.48/12.65 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.48/12.65 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.48/12.65 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.48/12.65 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.48/12.65 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.48/12.65 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.48/12.65 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.48/12.65 (Eq (op (op e0 e3) (op e3 e0)) e3)) % 12.48/12.65 True % 12.48/12.65 Clause #120 (by clausification #[118]): Eq (op (op e1 e3) (op e3 e1)) e3 % 12.48/12.65 Clause #121 (by clausification #[6]): Eq % 12.48/12.65 (Not % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (And % 12.48/12.65 (Or % 12.48/12.65 (Or % 12.48/12.65 (Or % 12.48/12.65 (Or % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.48/12.66 (Ne (op e0 e2) e2)) % 12.48/12.66 (Ne (op e0 e3) e3)) % 12.48/12.66 (Ne (op e0 e4) e4)) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.48/12.66 (Ne (op e1 e2) e2)) % 12.48/12.66 (Ne (op e1 e3) e3)) % 12.48/12.66 (Ne (op e1 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.48/12.66 (Ne (op e2 e2) e2)) % 12.48/12.66 (Ne (op e2 e3) e3)) % 12.48/12.66 (Ne (op e2 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.48/12.66 (Ne (op e3 e2) e2)) % 12.48/12.66 (Ne (op e3 e3) e3)) % 12.48/12.66 (Ne (op e3 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 12.48/12.66 (Ne (op e4 e2) e2)) % 12.48/12.66 (Ne (op e4 e3) e3)) % 12.48/12.66 (Ne (op e4 e4) e4))) % 12.48/12.66 (Eq (op (op e0 e0) e0) e0)) % 12.48/12.66 (Eq (op (op e0 e1) e1) e0)) % 12.48/12.66 (Eq (op (op e0 e2) e2) e0)) % 12.48/12.66 (Eq (op (op e0 e3) e3) e0)) % 12.48/12.66 (Eq (op (op e0 e4) e4) e0)) % 12.48/12.66 (Eq (op (op e1 e0) e0) e1)) % 12.48/12.66 (Eq (op (op e1 e1) e1) e1)) % 12.48/12.66 (Eq (op (op e1 e2) e2) e1)) % 12.48/12.66 (Eq (op (op e1 e3) e3) e1)) % 12.48/12.66 (Eq (op (op e1 e4) e4) e1)) % 12.48/12.66 (Eq (op (op e2 e0) e0) e2)) % 12.48/12.66 (Eq (op (op e2 e1) e1) e2)) % 12.48/12.66 (Eq (op (op e2 e2) e2) e2)) % 12.48/12.66 (Eq (op (op e2 e3) e3) e2)) % 12.48/12.66 (Eq (op (op e2 e4) e4) e2)) % 12.48/12.66 (Eq (op (op e3 e0) e0) e3)) % 12.48/12.66 (Eq (op (op e3 e1) e1) e3)) % 12.48/12.66 (Eq (op (op e3 e2) e2) e3)) % 12.48/12.66 (Eq (op (op e3 e3) e3) e3)) % 12.48/12.66 (Eq (op (op e3 e4) e4) e3)) % 12.48/12.66 (Eq (op (op e4 e0) e0) e4)) % 12.48/12.66 (Eq (op (op e4 e1) e1) e4)) % 12.48/12.66 (Eq (op (op e4 e2) e2) e4)) % 12.48/12.66 (Eq (op (op e4 e3) e3) e4)) % 12.48/12.66 (Eq (op (op e4 e4) e4) e4))) % 12.48/12.66 False % 12.48/12.66 Clause #122 (by clausification #[121]): Eq % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (Or % 12.48/12.66 (Or % 12.48/12.66 (Or % 12.48/12.66 (Or % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.48/12.66 (Ne (op e0 e2) e2)) % 12.48/12.66 (Ne (op e0 e3) e3)) % 12.48/12.66 (Ne (op e0 e4) e4)) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.48/12.66 (Ne (op e1 e2) e2)) % 12.48/12.66 (Ne (op e1 e3) e3)) % 12.48/12.66 (Ne (op e1 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.48/12.66 (Ne (op e2 e2) e2)) % 12.48/12.66 (Ne (op e2 e3) e3)) % 12.48/12.66 (Ne (op e2 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.48/12.66 (Ne (op e3 e2) e2)) % 12.48/12.66 (Ne (op e3 e3) e3)) % 12.48/12.66 (Ne (op e3 e4) e4))) % 12.48/12.66 (And % 12.48/12.66 (And % 12.48/12.66 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 12.48/12.66 (Ne (op e4 e2) e2)) % 12.48/12.66 (Ne (op e4 e3) e3)) % 12.48/12.66 (Ne (op e4 e4) e4))) % 12.48/12.66 (Eq (op (op e0 e0) e0) e0)) % 12.48/12.66 (Eq (op (op e0 e1) e1) e0)) % 12.48/12.66 (Eq (op (op e0 e2) e2) e0)) % 12.48/12.66 (Eq (op (op e0 e3) e3) e0)) % 12.48/12.66 (Eq (op (op e0 e4) e4) e0)) % 12.48/12.66 (Eq (op (op e1 e0) e0) e1)) % 12.48/12.66 (Eq (op (op e1 e1) e1) e1)) % 12.48/12.66 (Eq (op (op e1 e2) e2) e1)) % 12.48/12.66 (Eq (op (op e1 e3) e3) e1)) % 12.48/12.66 (Eq (op (op e1 e4) e4) e1)) % 12.48/12.66 (Eq (op (op e2 e0) e0) e2)) % 12.48/12.68 (Eq (op (op e2 e1) e1) e2)) % 12.48/12.68 (Eq (op (op e2 e2) e2) e2)) % 12.48/12.68 (Eq (op (op e2 e3) e3) e2)) % 12.48/12.68 (Eq (op (op e2 e4) e4) e2)) % 12.48/12.68 (Eq (op (op e3 e0) e0) e3)) % 12.48/12.68 (Eq (op (op e3 e1) e1) e3)) % 12.48/12.68 (Eq (op (op e3 e2) e2) e3)) % 12.48/12.68 (Eq (op (op e3 e3) e3) e3)) % 12.48/12.68 (Eq (op (op e3 e4) e4) e3)) % 12.48/12.68 (Eq (op (op e4 e0) e0) e4)) % 12.48/12.68 (Eq (op (op e4 e1) e1) e4)) % 12.48/12.68 (Eq (op (op e4 e2) e2) e4)) % 12.48/12.68 (Eq (op (op e4 e3) e3) e4)) % 12.48/12.68 (Eq (op (op e4 e4) e4) e4)) % 12.48/12.68 True % 12.48/12.68 Clause #123 (by clausification #[122]): Eq (Eq (op (op e4 e4) e4) e4) True % 12.48/12.68 Clause #124 (by clausification #[122]): Eq % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (Or % 12.48/12.68 (Or % 12.48/12.68 (Or % 12.48/12.68 (Or % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.48/12.68 (Ne (op e0 e2) e2)) % 12.48/12.68 (Ne (op e0 e3) e3)) % 12.48/12.68 (Ne (op e0 e4) e4)) % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.48/12.68 (Ne (op e1 e2) e2)) % 12.48/12.68 (Ne (op e1 e3) e3)) % 12.48/12.68 (Ne (op e1 e4) e4))) % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.48/12.68 (Ne (op e2 e2) e2)) % 12.48/12.68 (Ne (op e2 e3) e3)) % 12.48/12.68 (Ne (op e2 e4) e4))) % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.48/12.68 (Ne (op e3 e2) e2)) % 12.48/12.68 (Ne (op e3 e3) e3)) % 12.48/12.68 (Ne (op e3 e4) e4))) % 12.48/12.68 (And % 12.48/12.68 (And % 12.48/12.68 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 12.48/12.68 (Ne (op e4 e2) e2)) % 12.48/12.68 (Ne (op e4 e3) e3)) % 12.48/12.68 (Ne (op e4 e4) e4))) % 12.48/12.71 (Eq (op (op e0 e0) e0) e0)) % 12.48/12.71 (Eq (op (op e0 e1) e1) e0)) % 12.48/12.71 (Eq (op (op e0 e2) e2) e0)) % 12.48/12.71 (Eq (op (op e0 e3) e3) e0)) % 12.48/12.71 (Eq (op (op e0 e4) e4) e0)) % 12.48/12.71 (Eq (op (op e1 e0) e0) e1)) % 12.48/12.71 (Eq (op (op e1 e1) e1) e1)) % 12.48/12.71 (Eq (op (op e1 e2) e2) e1)) % 12.48/12.71 (Eq (op (op e1 e3) e3) e1)) % 12.48/12.71 (Eq (op (op e1 e4) e4) e1)) % 12.48/12.71 (Eq (op (op e2 e0) e0) e2)) % 12.48/12.71 (Eq (op (op e2 e1) e1) e2)) % 12.48/12.71 (Eq (op (op e2 e2) e2) e2)) % 12.48/12.71 (Eq (op (op e2 e3) e3) e2)) % 12.48/12.71 (Eq (op (op e2 e4) e4) e2)) % 12.48/12.71 (Eq (op (op e3 e0) e0) e3)) % 12.48/12.71 (Eq (op (op e3 e1) e1) e3)) % 12.48/12.71 (Eq (op (op e3 e2) e2) e3)) % 12.48/12.71 (Eq (op (op e3 e3) e3) e3)) % 12.48/12.71 (Eq (op (op e3 e4) e4) e3)) % 12.48/12.71 (Eq (op (op e4 e0) e0) e4)) % 12.48/12.71 (Eq (op (op e4 e1) e1) e4)) % 12.48/12.71 (Eq (op (op e4 e2) e2) e4)) % 12.48/12.71 (Eq (op (op e4 e3) e3) e4)) % 12.48/12.71 True % 12.48/12.71 Clause #125 (by clausification #[123]): Eq (op (op e4 e4) e4) e4 % 12.48/12.71 Clause #126 (by forward demodulation #[125, 23]): Eq (op e0 e4) e4 % 12.48/12.71 Clause #127 (by backward demodulation #[126, 99]): Eq (op e4 (op e4 e0)) e4 % 12.48/12.71 Clause #129 (by clausification #[119]): Eq % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And (And (Eq (op (op e0 e0) (op e0 e0)) e0) (Eq (op (op e1 e0) (op e0 e1)) e0)) % 12.48/12.71 (Eq (op (op e2 e0) (op e0 e2)) e0)) % 12.48/12.71 (Eq (op (op e3 e0) (op e0 e3)) e0)) % 12.48/12.71 (Eq (op (op e4 e0) (op e0 e4)) e0)) % 12.48/12.71 (Eq (op (op e0 e1) (op e1 e0)) e1)) % 12.48/12.71 (Eq (op (op e1 e1) (op e1 e1)) e1)) % 12.48/12.71 (Eq (op (op e2 e1) (op e1 e2)) e1)) % 12.48/12.71 (Eq (op (op e3 e1) (op e1 e3)) e1)) % 12.48/12.71 (Eq (op (op e4 e1) (op e1 e4)) e1)) % 12.48/12.71 (Eq (op (op e0 e2) (op e2 e0)) e2)) % 12.48/12.71 (Eq (op (op e1 e2) (op e2 e1)) e2)) % 12.48/12.71 (Eq (op (op e2 e2) (op e2 e2)) e2)) % 12.48/12.71 (Eq (op (op e3 e2) (op e2 e3)) e2)) % 12.48/12.71 (Eq (op (op e4 e2) (op e2 e4)) e2)) % 12.48/12.71 True % 12.48/12.71 Clause #131 (by clausification #[129]): Eq (Eq (op (op e4 e2) (op e2 e4)) e2) True % 12.48/12.71 Clause #133 (by clausification #[131]): Eq (op (op e4 e2) (op e2 e4)) e2 % 12.48/12.71 Clause #143 (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)) % 12.48/12.71 True % 12.48/12.71 Clause #144 (by clausification #[25]): Eq % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (And % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e0) e1)) (Eq (op e0 e0) e2)) % 12.48/12.71 (Eq (op e0 e0) e3)) % 12.48/12.71 (Eq (op e0 e0) e4)) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e0 e1) e1)) (Eq (op e0 e1) e2)) % 12.48/12.71 (Eq (op e0 e1) e3)) % 12.48/12.71 (Eq (op e0 e1) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e0 e2) e1)) (Eq (op e0 e2) e2)) % 12.48/12.71 (Eq (op e0 e2) e3)) % 12.48/12.71 (Eq (op e0 e2) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e0 e3) e1)) (Eq (op e0 e3) e2)) % 12.48/12.71 (Eq (op e0 e3) e3)) % 12.48/12.71 (Eq (op e0 e3) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e0 e4) e1)) (Eq (op e0 e4) e2)) % 12.48/12.71 (Eq (op e0 e4) e3)) % 12.48/12.71 (Eq (op e0 e4) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e0) e1)) (Eq (op e1 e0) e2)) % 12.48/12.71 (Eq (op e1 e0) e3)) % 12.48/12.71 (Eq (op e1 e0) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e1 e1) e0) (Eq (op e1 e1) e1)) (Eq (op e1 e1) e2)) % 12.48/12.71 (Eq (op e1 e1) e3)) % 12.48/12.71 (Eq (op e1 e1) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e1 e2) e0) (Eq (op e1 e2) e1)) (Eq (op e1 e2) e2)) % 12.48/12.71 (Eq (op e1 e2) e3)) % 12.48/12.71 (Eq (op e1 e2) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e1 e3) e0) (Eq (op e1 e3) e1)) (Eq (op e1 e3) e2)) % 12.48/12.71 (Eq (op e1 e3) e3)) % 12.48/12.71 (Eq (op e1 e3) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e1 e4) e0) (Eq (op e1 e4) e1)) (Eq (op e1 e4) e2)) % 12.48/12.71 (Eq (op e1 e4) e3)) % 12.48/12.71 (Eq (op e1 e4) e4))) % 12.48/12.71 (Or % 12.48/12.71 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e0) e1)) (Eq (op e2 e0) e2)) (Eq (op e2 e0) e3)) % 12.48/12.71 (Eq (op e2 e0) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e2 e1) e0) (Eq (op e2 e1) e1)) (Eq (op e2 e1) e2)) (Eq (op e2 e1) e3)) % 12.48/12.71 (Eq (op e2 e1) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e2 e2) e0) (Eq (op e2 e2) e1)) (Eq (op e2 e2) e2)) (Eq (op e2 e2) e3)) % 12.48/12.71 (Eq (op e2 e2) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e2 e3) e0) (Eq (op e2 e3) e1)) (Eq (op e2 e3) e2)) (Eq (op e2 e3) e3)) % 12.48/12.71 (Eq (op e2 e3) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e2 e4) e0) (Eq (op e2 e4) e1)) (Eq (op e2 e4) e2)) (Eq (op e2 e4) e3)) % 12.48/12.71 (Eq (op e2 e4) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e0) e1)) (Eq (op e3 e0) e2)) (Eq (op e3 e0) e3)) % 12.48/12.71 (Eq (op e3 e0) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e3 e1) e0) (Eq (op e3 e1) e1)) (Eq (op e3 e1) e2)) (Eq (op e3 e1) e3)) % 12.48/12.71 (Eq (op e3 e1) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e3 e2) e0) (Eq (op e3 e2) e1)) (Eq (op e3 e2) e2)) (Eq (op e3 e2) e3)) % 12.48/12.71 (Eq (op e3 e2) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e3 e3) e0) (Eq (op e3 e3) e1)) (Eq (op e3 e3) e2)) (Eq (op e3 e3) e3)) % 12.48/12.71 (Eq (op e3 e3) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e3 e4) e0) (Eq (op e3 e4) e1)) (Eq (op e3 e4) e2)) (Eq (op e3 e4) e3)) % 12.48/12.71 (Eq (op e3 e4) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e0) e1)) (Eq (op e4 e0) e2)) (Eq (op e4 e0) e3)) % 12.48/12.71 (Eq (op e4 e0) e4))) % 12.48/12.71 (Or (Or (Or (Or (Eq (op e4 e1) e0) (Eq (op e4 e1) e1)) (Eq (op e4 e1) e2)) (Eq (op e4 e1) e3)) % 12.48/12.71 (Eq (op e4 e1) e4))) % 12.57/12.78 (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))) % 12.57/12.78 True % 12.57/12.78 Clause #145 (by clausification #[143]): 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) % 12.57/12.78 (Eq (Eq (op e4 e3) e4) True) % 12.57/12.78 Clause #146 (by clausification #[145]): Or (Eq (Eq (op e4 e3) e4) True) % 12.57/12.78 (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)) % 12.57/12.78 Clause #147 (by clausification #[146]): Or (Eq (Or (Or (Eq (op e4 e3) e0) (Eq (op e4 e3) e1)) (Eq (op e4 e3) e2)) True) % 12.57/12.78 (Or (Eq (Eq (op e4 e3) e3) True) (Eq (op e4 e3) e4)) % 12.57/12.78 Clause #148 (by clausification #[147]): Or (Eq (Eq (op e4 e3) e3) True) % 12.57/12.78 (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))) % 12.57/12.78 Clause #149 (by clausification #[148]): Or (Eq (op e4 e3) e4) % 12.57/12.78 (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))) % 12.57/12.78 Clause #150 (by clausification #[149]): Or (Eq (op e4 e3) e4) % 12.57/12.78 (Or (Eq (Eq (op e4 e3) e2) True) % 12.57/12.78 (Or (Eq (op e4 e3) e3) (Or (Eq (Eq (op e4 e3) e0) True) (Eq (Eq (op e4 e3) e1) True)))) % 12.57/12.78 Clause #151 (by clausification #[150]): Or (Eq (op e4 e3) e4) % 12.57/12.78 (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)))) % 12.57/12.78 Clause #152 (by clausification #[151]): Or (Eq (op e4 e3) e4) % 12.57/12.78 (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)))) % 12.57/12.78 Clause #153 (by clausification #[152]): 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)))) % 12.57/12.78 Clause #154 (by forward contextual literal cutting #[153, 104]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e2) (Eq (op e4 e3) e1))) % 12.57/12.78 Clause #161 (by clausification #[55]): Eq (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)) % 12.57/12.78 True % 12.57/12.78 Clause #162 (by clausification #[55]): Eq % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (And % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Eq (op e0 e0) % 12.57/12.78 e0) % 12.57/12.78 (Eq (op e0 e1) % 12.57/12.78 e0)) % 12.57/12.78 (Eq (op e0 e2) % 12.57/12.78 e0)) % 12.57/12.78 (Eq (op e0 e3) e0)) % 12.57/12.78 (Eq (op e0 e4) e0)) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Eq (op e0 e0) % 12.57/12.78 e0) % 12.57/12.78 (Eq (op e1 e0) % 12.57/12.78 e0)) % 12.57/12.78 (Eq (op e2 e0) % 12.57/12.78 e0)) % 12.57/12.78 (Eq (op e3 e0) e0)) % 12.57/12.78 (Eq (op e4 e0) e0))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Eq (op e0 e0) e1) % 12.57/12.78 (Eq (op e0 e1) % 12.57/12.78 e1)) % 12.57/12.78 (Eq (op e0 e2) e1)) % 12.57/12.78 (Eq (op e0 e3) e1)) % 12.57/12.78 (Eq (op e0 e4) e1))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or (Eq (op e0 e0) e1) % 12.57/12.78 (Eq (op e1 e0) e1)) % 12.57/12.78 (Eq (op e2 e0) e1)) % 12.57/12.78 (Eq (op e3 e0) e1)) % 12.57/12.78 (Eq (op e4 e0) e1))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or (Eq (op e0 e0) e2) % 12.57/12.78 (Eq (op e0 e1) e2)) % 12.57/12.78 (Eq (op e0 e2) e2)) % 12.57/12.78 (Eq (op e0 e3) e2)) % 12.57/12.78 (Eq (op e0 e4) e2))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or (Eq (op e0 e0) e2) % 12.57/12.78 (Eq (op e1 e0) e2)) % 12.57/12.78 (Eq (op e2 e0) e2)) % 12.57/12.78 (Eq (op e3 e0) e2)) % 12.57/12.78 (Eq (op e4 e0) e2))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or (Eq (op e0 e0) e3) % 12.57/12.78 (Eq (op e0 e1) e3)) % 12.57/12.78 (Eq (op e0 e2) e3)) % 12.57/12.78 (Eq (op e0 e3) e3)) % 12.57/12.78 (Eq (op e0 e4) e3))) % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or % 12.57/12.78 (Or (Eq (op e0 e0) e3) % 12.57/12.78 (Eq (op e1 e0) e3)) % 12.62/12.78 (Eq (op e2 e0) e3)) % 12.62/12.78 (Eq (op e3 e0) e3)) % 12.62/12.78 (Eq (op e4 e0) e3))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e0 e0) e4) % 12.62/12.78 (Eq (op e0 e1) e4)) % 12.62/12.78 (Eq (op e0 e2) e4)) % 12.62/12.78 (Eq (op e0 e3) e4)) % 12.62/12.78 (Eq (op e0 e4) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e0 e0) e4) % 12.62/12.78 (Eq (op e1 e0) e4)) % 12.62/12.78 (Eq (op e2 e0) e4)) % 12.62/12.78 (Eq (op e3 e0) e4)) % 12.62/12.78 (Eq (op e4 e0) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e1 e0) e0) % 12.62/12.78 (Eq (op e1 e1) e0)) % 12.62/12.78 (Eq (op e1 e2) e0)) % 12.62/12.78 (Eq (op e1 e3) e0)) % 12.62/12.78 (Eq (op e1 e4) e0))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e0 e1) e0) % 12.62/12.78 (Eq (op e1 e1) e0)) % 12.62/12.78 (Eq (op e2 e1) e0)) % 12.62/12.78 (Eq (op e3 e1) e0)) % 12.62/12.78 (Eq (op e4 e1) e0))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e1 e0) e1) % 12.62/12.78 (Eq (op e1 e1) e1)) % 12.62/12.78 (Eq (op e1 e2) e1)) % 12.62/12.78 (Eq (op e1 e3) e1)) % 12.62/12.78 (Eq (op e1 e4) e1))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) % 12.62/12.78 (Eq (op e2 e1) e1)) % 12.62/12.78 (Eq (op e3 e1) e1)) % 12.62/12.78 (Eq (op e4 e1) e1))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 12.62/12.78 (Eq (op e1 e2) e2)) % 12.62/12.78 (Eq (op e1 e3) e2)) % 12.62/12.78 (Eq (op e1 e4) e2))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 12.62/12.78 (Eq (op e2 e1) e2)) % 12.62/12.78 (Eq (op e3 e1) e2)) % 12.62/12.78 (Eq (op e4 e1) e2))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 12.62/12.78 (Eq (op e1 e2) e3)) % 12.62/12.78 (Eq (op e1 e3) e3)) % 12.62/12.78 (Eq (op e1 e4) e3))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 12.62/12.78 (Eq (op e2 e1) e3)) % 12.62/12.78 (Eq (op e3 e1) e3)) % 12.62/12.78 (Eq (op e4 e1) e3))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 12.62/12.78 (Eq (op e1 e2) e4)) % 12.62/12.78 (Eq (op e1 e3) e4)) % 12.62/12.78 (Eq (op e1 e4) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 12.62/12.78 (Eq (op e2 e1) e4)) % 12.62/12.78 (Eq (op e3 e1) e4)) % 12.62/12.78 (Eq (op e4 e1) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 12.62/12.78 (Eq (op e2 e2) e0)) % 12.62/12.78 (Eq (op e2 e3) e0)) % 12.62/12.78 (Eq (op e2 e4) e0))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 12.62/12.78 (Eq (op e2 e2) e0)) % 12.62/12.78 (Eq (op e3 e2) e0)) % 12.62/12.78 (Eq (op e4 e2) e0))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 12.62/12.78 (Eq (op e2 e2) e1)) % 12.62/12.78 (Eq (op e2 e3) e1)) % 12.62/12.78 (Eq (op e2 e4) e1))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 12.62/12.78 (Eq (op e2 e2) e1)) % 12.62/12.78 (Eq (op e3 e2) e1)) % 12.62/12.78 (Eq (op e4 e2) e1))) % 12.62/12.78 (Or % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) % 12.62/12.78 (Eq (op e2 e3) e2)) % 12.62/12.78 (Eq (op e2 e4) e2))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 12.62/12.78 (Eq (op e3 e2) e2)) % 12.62/12.78 (Eq (op e4 e2) e2))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 12.62/12.78 (Eq (op e2 e3) e3)) % 12.62/12.78 (Eq (op e2 e4) e3))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 12.62/12.78 (Eq (op e3 e2) e3)) % 12.62/12.78 (Eq (op e4 e2) e3))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 12.62/12.78 (Eq (op e2 e3) e4)) % 12.62/12.78 (Eq (op e2 e4) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 12.62/12.78 (Eq (op e3 e2) e4)) % 12.62/12.78 (Eq (op e4 e2) e4))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 12.62/12.78 (Eq (op e3 e3) e0)) % 12.62/12.78 (Eq (op e3 e4) e0))) % 12.62/12.78 (Or % 12.62/12.78 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 12.62/12.78 (Eq (op e3 e3) e0)) % 12.62/12.78 (Eq (op e4 e3) e0))) % 12.62/12.78 (Or % 12.62/12.79 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 12.62/12.79 (Eq (op e3 e3) e1)) % 12.62/12.79 (Eq (op e3 e4) e1))) % 12.62/12.79 (Or % 12.62/12.79 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 12.62/12.79 (Eq (op e3 e3) e1)) % 12.62/12.79 (Eq (op e4 e3) e1))) % 12.62/12.79 (Or % 12.62/12.79 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) % 12.62/12.79 (Eq (op e3 e3) e2)) % 12.62/12.79 (Eq (op e3 e4) e2))) % 12.62/12.79 (Or % 12.62/12.79 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2)) % 12.62/12.79 (Eq (op e4 e3) e2))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 12.62/12.79 (Eq (op e3 e4) e3))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 12.62/12.79 (Eq (op e4 e3) e3))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 12.62/12.79 (Eq (op e3 e4) e4))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 12.62/12.79 (Eq (op e4 e3) e4))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 12.62/12.79 (Eq (op e4 e4) e0))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 12.62/12.79 (Eq (op e4 e4) e0))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 12.62/12.79 (Eq (op e4 e4) e1))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 12.62/12.79 (Eq (op e4 e4) e1))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 12.62/12.79 (Eq (op e4 e4) e2))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 12.62/12.79 (Eq (op e4 e4) e2))) % 12.62/12.79 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) % 12.62/12.79 (Eq (op e4 e4) e3))) % 12.62/12.79 (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))) % 12.62/12.79 True % 12.62/12.79 Clause #163 (by clausification #[161]): Or (Eq (Or (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) (Eq (op e4 e3) e4)) True) % 12.62/12.79 (Eq (Eq (op e4 e4) e4) True) % 12.62/12.79 Clause #164 (by clausification #[163]): Or (Eq (Eq (op e4 e4) e4) True) % 12.62/12.79 (Or (Eq (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) True) (Eq (Eq (op e4 e3) e4) True)) % 12.62/12.79 Clause #165 (by clausification #[164]): Or (Eq (Or (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) (Eq (op e4 e2) e4)) True) % 12.62/12.79 (Or (Eq (Eq (op e4 e3) e4) True) (Eq (op e4 e4) e4)) % 12.62/12.79 Clause #166 (by clausification #[165]): Or (Eq (Eq (op e4 e3) e4) True) % 12.62/12.79 (Or (Eq (op e4 e4) e4) (Or (Eq (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) True) (Eq (Eq (op e4 e2) e4) True))) % 12.62/12.79 Clause #167 (by clausification #[166]): Or (Eq (op e4 e4) e4) % 12.62/12.79 (Or (Eq (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)) True) (Or (Eq (Eq (op e4 e2) e4) True) (Eq (op e4 e3) e4))) % 12.62/12.79 Clause #168 (by clausification #[167]): Or (Eq (op e4 e4) e4) % 12.62/12.79 (Or (Eq (Eq (op e4 e2) e4) True) % 12.62/12.79 (Or (Eq (op e4 e3) e4) (Or (Eq (Eq (op e4 e0) e4) True) (Eq (Eq (op e4 e1) e4) True)))) % 12.62/12.79 Clause #169 (by clausification #[168]): Or (Eq (op e4 e4) e4) % 12.62/12.79 (Or (Eq (op e4 e3) e4) (Or (Eq (Eq (op e4 e0) e4) True) (Or (Eq (Eq (op e4 e1) e4) True) (Eq (op e4 e2) e4)))) % 12.62/12.79 Clause #170 (by clausification #[169]): Or (Eq (op e4 e4) e4) % 12.62/12.79 (Or (Eq (op e4 e3) e4) (Or (Eq (Eq (op e4 e1) e4) True) (Or (Eq (op e4 e2) e4) (Eq (op e4 e0) e4)))) % 12.62/12.81 Clause #171 (by clausification #[170]): Or (Eq (op e4 e4) e4) (Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)))) % 12.62/12.81 Clause #172 (by forward demodulation #[171, 23]): Or (Eq e0 e4) (Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4)))) % 12.62/12.81 Clause #173 (by forward contextual literal cutting #[172, 73]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e0) e4) (Eq (op e4 e1) e4))) % 12.62/12.81 Clause #174 (by superposition #[173, 127]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e1) e4) (Eq (op e4 e4) e4))) % 12.62/12.81 Clause #175 (by forward demodulation #[174, 23]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e1) e4) (Eq e0 e4))) % 12.62/12.81 Clause #176 (by forward contextual literal cutting #[175, 73]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e2) e4) (Eq (op e4 e1) e4)) % 12.62/12.81 Clause #184 (by clausification #[102]): Eq (Ne (op e4 e2) (op e4 e4)) True % 12.62/12.81 Clause #186 (by clausification #[184]): Ne (op e4 e2) (op e4 e4) % 12.62/12.81 Clause #187 (by forward demodulation #[186, 23]): Ne (op e4 e2) e0 % 12.62/12.81 Clause #193 (by clausification #[124]): Eq (Eq (op (op e4 e3) e3) e4) True % 12.62/12.81 Clause #194 (by clausification #[124]): Eq % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (Or % 12.62/12.81 (Or % 12.62/12.81 (Or % 12.62/12.81 (Or % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.62/12.81 (Ne (op e0 e2) e2)) % 12.62/12.81 (Ne (op e0 e3) e3)) % 12.62/12.81 (Ne (op e0 e4) e4)) % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.62/12.81 (Ne (op e1 e2) e2)) % 12.62/12.81 (Ne (op e1 e3) e3)) % 12.62/12.81 (Ne (op e1 e4) e4))) % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.62/12.81 (Ne (op e2 e2) e2)) % 12.62/12.81 (Ne (op e2 e3) e3)) % 12.62/12.81 (Ne (op e2 e4) e4))) % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.62/12.81 (Ne (op e3 e2) e2)) % 12.62/12.81 (Ne (op e3 e3) e3)) % 12.62/12.81 (Ne (op e3 e4) e4))) % 12.62/12.81 (And % 12.62/12.81 (And % 12.62/12.81 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) % 12.70/12.89 (Ne (op e4 e2) e2)) % 12.70/12.89 (Ne (op e4 e3) e3)) % 12.70/12.89 (Ne (op e4 e4) e4))) % 12.70/12.89 (Eq (op (op e0 e0) e0) e0)) % 12.70/12.89 (Eq (op (op e0 e1) e1) e0)) % 12.70/12.89 (Eq (op (op e0 e2) e2) e0)) % 12.70/12.89 (Eq (op (op e0 e3) e3) e0)) % 12.70/12.89 (Eq (op (op e0 e4) e4) e0)) % 12.70/12.89 (Eq (op (op e1 e0) e0) e1)) % 12.70/12.89 (Eq (op (op e1 e1) e1) e1)) % 12.70/12.89 (Eq (op (op e1 e2) e2) e1)) % 12.70/12.89 (Eq (op (op e1 e3) e3) e1)) % 12.70/12.89 (Eq (op (op e1 e4) e4) e1)) % 12.70/12.89 (Eq (op (op e2 e0) e0) e2)) % 12.70/12.89 (Eq (op (op e2 e1) e1) e2)) % 12.70/12.89 (Eq (op (op e2 e2) e2) e2)) % 12.70/12.89 (Eq (op (op e2 e3) e3) e2)) % 12.70/12.89 (Eq (op (op e2 e4) e4) e2)) % 12.70/12.89 (Eq (op (op e3 e0) e0) e3)) % 12.70/12.89 (Eq (op (op e3 e1) e1) e3)) % 12.70/12.89 (Eq (op (op e3 e2) e2) e3)) % 12.70/12.89 (Eq (op (op e3 e3) e3) e3)) % 12.70/12.89 (Eq (op (op e3 e4) e4) e3)) % 12.70/12.89 (Eq (op (op e4 e0) e0) e4)) % 12.70/12.89 (Eq (op (op e4 e1) e1) e4)) % 12.70/12.89 (Eq (op (op e4 e2) e2) e4)) % 12.70/12.89 True % 12.70/12.89 Clause #195 (by clausification #[193]): Eq (op (op e4 e3) e3) e4 % 12.70/12.89 Clause #196 (by superposition #[195, 154]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e2 e3) e4))) % 12.70/12.89 Clause #218 (by clausification #[144]): Eq (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)) % 12.70/12.89 True % 12.70/12.89 Clause #220 (by clausification #[218]): Or (Eq (Or (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) (Eq (op e4 e2) e3)) True) % 12.70/12.89 (Eq (Eq (op e4 e2) e4) True) % 12.70/12.89 Clause #221 (by clausification #[220]): Or (Eq (Eq (op e4 e2) e4) True) % 12.70/12.89 (Or (Eq (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) True) (Eq (Eq (op e4 e2) e3) True)) % 12.70/12.89 Clause #222 (by clausification #[221]): Or (Eq (Or (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) (Eq (op e4 e2) e2)) True) % 12.70/12.89 (Or (Eq (Eq (op e4 e2) e3) True) (Eq (op e4 e2) e4)) % 12.70/12.89 Clause #223 (by clausification #[222]): Or (Eq (Eq (op e4 e2) e3) True) % 12.70/12.89 (Or (Eq (op e4 e2) e4) (Or (Eq (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) True) (Eq (Eq (op e4 e2) e2) True))) % 12.70/12.89 Clause #224 (by clausification #[223]): Or (Eq (op e4 e2) e4) % 12.70/12.89 (Or (Eq (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)) True) (Or (Eq (Eq (op e4 e2) e2) True) (Eq (op e4 e2) e3))) % 12.70/12.89 Clause #225 (by clausification #[224]): Or (Eq (op e4 e2) e4) % 12.70/12.89 (Or (Eq (Eq (op e4 e2) e2) True) % 12.70/12.89 (Or (Eq (op e4 e2) e3) (Or (Eq (Eq (op e4 e2) e0) True) (Eq (Eq (op e4 e2) e1) True)))) % 12.70/12.89 Clause #226 (by clausification #[225]): Or (Eq (op e4 e2) e4) % 12.70/12.89 (Or (Eq (op e4 e2) e3) (Or (Eq (Eq (op e4 e2) e0) True) (Or (Eq (Eq (op e4 e2) e1) True) (Eq (op e4 e2) e2)))) % 12.70/12.89 Clause #227 (by clausification #[226]): Or (Eq (op e4 e2) e4) % 12.70/12.89 (Or (Eq (op e4 e2) e3) (Or (Eq (Eq (op e4 e2) e1) True) (Or (Eq (op e4 e2) e2) (Eq (op e4 e2) e0)))) % 12.70/12.89 Clause #228 (by clausification #[227]): Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e2) (Or (Eq (op e4 e2) e0) (Eq (op e4 e2) e1)))) % 12.70/12.89 Clause #229 (by forward contextual literal cutting #[228, 187]): Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e2) (Eq (op e4 e2) e1))) % 12.70/12.89 Clause #240 (by clausification #[162]): 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)) % 12.70/12.89 True % 12.70/12.89 Clause #241 (by clausification #[162]): Eq % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (And % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Eq (op e0 e0) e0) % 12.70/12.89 (Eq (op e0 e1) % 12.70/12.89 e0)) % 12.70/12.89 (Eq (op e0 e2) e0)) % 12.70/12.89 (Eq (op e0 e3) e0)) % 12.70/12.89 (Eq (op e0 e4) e0)) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Eq (op e0 e0) e0) % 12.70/12.89 (Eq (op e1 e0) % 12.70/12.89 e0)) % 12.70/12.89 (Eq (op e2 e0) e0)) % 12.70/12.89 (Eq (op e3 e0) e0)) % 12.70/12.89 (Eq (op e4 e0) e0))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e1) % 12.70/12.89 (Eq (op e0 e1) e1)) % 12.70/12.89 (Eq (op e0 e2) e1)) % 12.70/12.89 (Eq (op e0 e3) e1)) % 12.70/12.89 (Eq (op e0 e4) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e1) % 12.70/12.89 (Eq (op e1 e0) e1)) % 12.70/12.89 (Eq (op e2 e0) e1)) % 12.70/12.89 (Eq (op e3 e0) e1)) % 12.70/12.89 (Eq (op e4 e0) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e2) % 12.70/12.89 (Eq (op e0 e1) e2)) % 12.70/12.89 (Eq (op e0 e2) e2)) % 12.70/12.89 (Eq (op e0 e3) e2)) % 12.70/12.89 (Eq (op e0 e4) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e2) % 12.70/12.89 (Eq (op e1 e0) e2)) % 12.70/12.89 (Eq (op e2 e0) e2)) % 12.70/12.89 (Eq (op e3 e0) e2)) % 12.70/12.89 (Eq (op e4 e0) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e3) % 12.70/12.89 (Eq (op e0 e1) e3)) % 12.70/12.89 (Eq (op e0 e2) e3)) % 12.70/12.89 (Eq (op e0 e3) e3)) % 12.70/12.89 (Eq (op e0 e4) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e3) % 12.70/12.89 (Eq (op e1 e0) e3)) % 12.70/12.89 (Eq (op e2 e0) e3)) % 12.70/12.89 (Eq (op e3 e0) e3)) % 12.70/12.89 (Eq (op e4 e0) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e4) % 12.70/12.89 (Eq (op e0 e1) e4)) % 12.70/12.89 (Eq (op e0 e2) e4)) % 12.70/12.89 (Eq (op e0 e3) e4)) % 12.70/12.89 (Eq (op e0 e4) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e0) e4) % 12.70/12.89 (Eq (op e1 e0) e4)) % 12.70/12.89 (Eq (op e2 e0) e4)) % 12.70/12.89 (Eq (op e3 e0) e4)) % 12.70/12.89 (Eq (op e4 e0) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e1 e0) e0) % 12.70/12.89 (Eq (op e1 e1) e0)) % 12.70/12.89 (Eq (op e1 e2) e0)) % 12.70/12.89 (Eq (op e1 e3) e0)) % 12.70/12.89 (Eq (op e1 e4) e0))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e0 e1) e0) % 12.70/12.89 (Eq (op e1 e1) e0)) % 12.70/12.89 (Eq (op e2 e1) e0)) % 12.70/12.89 (Eq (op e3 e1) e0)) % 12.70/12.89 (Eq (op e4 e1) e0))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) % 12.70/12.89 (Eq (op e1 e2) e1)) % 12.70/12.89 (Eq (op e1 e3) e1)) % 12.70/12.89 (Eq (op e1 e4) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) % 12.70/12.89 (Eq (op e2 e1) e1)) % 12.70/12.89 (Eq (op e3 e1) e1)) % 12.70/12.89 (Eq (op e4 e1) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 12.70/12.89 (Eq (op e1 e2) e2)) % 12.70/12.89 (Eq (op e1 e3) e2)) % 12.70/12.89 (Eq (op e1 e4) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 12.70/12.89 (Eq (op e2 e1) e2)) % 12.70/12.89 (Eq (op e3 e1) e2)) % 12.70/12.89 (Eq (op e4 e1) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 12.70/12.89 (Eq (op e1 e2) e3)) % 12.70/12.89 (Eq (op e1 e3) e3)) % 12.70/12.89 (Eq (op e1 e4) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 12.70/12.89 (Eq (op e2 e1) e3)) % 12.70/12.89 (Eq (op e3 e1) e3)) % 12.70/12.89 (Eq (op e4 e1) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 12.70/12.89 (Eq (op e1 e2) e4)) % 12.70/12.89 (Eq (op e1 e3) e4)) % 12.70/12.89 (Eq (op e1 e4) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 12.70/12.89 (Eq (op e2 e1) e4)) % 12.70/12.89 (Eq (op e3 e1) e4)) % 12.70/12.89 (Eq (op e4 e1) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 12.70/12.89 (Eq (op e2 e2) e0)) % 12.70/12.89 (Eq (op e2 e3) e0)) % 12.70/12.89 (Eq (op e2 e4) e0))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 12.70/12.89 (Eq (op e2 e2) e0)) % 12.70/12.89 (Eq (op e3 e2) e0)) % 12.70/12.89 (Eq (op e4 e2) e0))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) % 12.70/12.89 (Eq (op e2 e2) e1)) % 12.70/12.89 (Eq (op e2 e3) e1)) % 12.70/12.89 (Eq (op e2 e4) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) % 12.70/12.89 (Eq (op e3 e2) e1)) % 12.70/12.89 (Eq (op e4 e2) e1))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) % 12.70/12.89 (Eq (op e2 e3) e2)) % 12.70/12.89 (Eq (op e2 e4) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 12.70/12.89 (Eq (op e3 e2) e2)) % 12.70/12.89 (Eq (op e4 e2) e2))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 12.70/12.89 (Eq (op e2 e3) e3)) % 12.70/12.89 (Eq (op e2 e4) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 12.70/12.89 (Eq (op e3 e2) e3)) % 12.70/12.89 (Eq (op e4 e2) e3))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 12.70/12.89 (Eq (op e2 e3) e4)) % 12.70/12.89 (Eq (op e2 e4) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 12.70/12.89 (Eq (op e3 e2) e4)) % 12.70/12.89 (Eq (op e4 e2) e4))) % 12.70/12.89 (Or % 12.70/12.89 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 12.70/12.89 (Eq (op e3 e3) e0)) % 12.70/12.90 (Eq (op e3 e4) e0))) % 12.70/12.90 (Or % 12.70/12.90 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 12.70/12.90 (Eq (op e3 e3) e0)) % 12.70/12.90 (Eq (op e4 e3) e0))) % 12.70/12.90 (Or % 12.70/12.90 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 12.70/12.90 (Eq (op e3 e3) e1)) % 12.70/12.90 (Eq (op e3 e4) e1))) % 12.70/12.90 (Or % 12.70/12.90 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) % 12.70/12.90 (Eq (op e3 e3) e1)) % 12.70/12.90 (Eq (op e4 e3) e1))) % 12.70/12.90 (Or % 12.70/12.90 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2)) % 12.70/12.90 (Eq (op e3 e4) e2))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2)) % 12.70/12.90 (Eq (op e4 e3) e2))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 12.70/12.90 (Eq (op e3 e4) e3))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 12.70/12.90 (Eq (op e4 e3) e3))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 12.70/12.90 (Eq (op e3 e4) e4))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 12.70/12.90 (Eq (op e4 e3) e4))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 12.70/12.90 (Eq (op e4 e4) e0))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 12.70/12.90 (Eq (op e4 e4) e0))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 12.70/12.90 (Eq (op e4 e4) e1))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 12.70/12.90 (Eq (op e4 e4) e1))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 12.70/12.90 (Eq (op e4 e4) e2))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) % 12.70/12.90 (Eq (op e4 e4) e2))) % 12.70/12.90 (Or (Or (Or (Or (Eq (op e4 e0) e3) (Eq (op e4 e1) e3)) (Eq (op e4 e2) e3)) (Eq (op e4 e3) e3)) (Eq (op e4 e4) e3))) % 12.70/12.90 True % 12.70/12.90 Clause #242 (by clausification #[240]): 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) % 12.70/12.90 (Eq (Eq (op e4 e4) e3) True) % 12.70/12.90 Clause #243 (by clausification #[242]): Or (Eq (Eq (op e4 e4) e3) True) % 12.70/12.90 (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)) % 12.70/12.90 Clause #244 (by clausification #[243]): Or (Eq (Or (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) (Eq (op e2 e4) e3)) True) % 12.70/12.90 (Or (Eq (Eq (op e3 e4) e3) True) (Eq (op e4 e4) e3)) % 12.70/12.90 Clause #245 (by clausification #[244]): Or (Eq (Eq (op e3 e4) e3) True) % 12.70/12.90 (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))) % 12.70/12.90 Clause #246 (by clausification #[245]): Or (Eq (op e4 e4) e3) % 12.70/12.90 (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))) % 12.70/12.90 Clause #247 (by clausification #[246]): Or (Eq (op e4 e4) e3) % 12.70/12.90 (Or (Eq (Eq (op e2 e4) e3) True) % 12.70/12.90 (Or (Eq (op e3 e4) e3) (Or (Eq (Eq (op e0 e4) e3) True) (Eq (Eq (op e1 e4) e3) True)))) % 12.70/12.90 Clause #248 (by clausification #[247]): Or (Eq (op e4 e4) e3) % 12.70/12.90 (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)))) % 12.70/12.90 Clause #249 (by clausification #[248]): Or (Eq (op e4 e4) e3) % 12.74/12.92 (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)))) % 12.74/12.92 Clause #250 (by clausification #[249]): 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)))) % 12.74/12.92 Clause #251 (by forward demodulation #[250, 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)))) % 12.74/12.92 Clause #252 (by forward demodulation #[251, 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)))) % 12.74/12.92 Clause #253 (by forward contextual literal cutting #[252, 77]): Or (Eq e1 e3) (Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3))) % 12.74/12.92 Clause #254 (by forward contextual literal cutting #[253, 53]): Or (Eq (op e2 e4) e3) (Or (Eq (op e0 e4) e3) (Eq (op e1 e4) e3)) % 12.74/12.92 Clause #255 (by superposition #[254, 126]): Or (Eq (op e2 e4) e3) (Or (Eq (op e1 e4) e3) (Eq e3 e4)) % 12.74/12.92 Clause #256 (by forward contextual literal cutting #[255, 41]): Or (Eq (op e2 e4) e3) (Eq (op e1 e4) e3) % 12.74/12.92 Clause #257 (by superposition #[256, 93]): Or (Eq (op e1 e4) e3) (Eq (op e3 (op e4 e2)) e4) % 12.74/12.92 Clause #258 (by superposition #[256, 133]): Or (Eq (op e1 e4) e3) (Eq (op (op e4 e2) e3) e2) % 12.74/12.92 Clause #263 (by superposition #[257, 176]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e1) e4) (Or (Eq (op e1 e4) e3) (Eq (op e3 e4) e4))) % 12.74/12.92 Clause #266 (by forward demodulation #[263, 18]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e1) e4) (Or (Eq (op e1 e4) e3) (Eq e1 e4))) % 12.74/12.92 Clause #267 (by forward contextual literal cutting #[266, 50]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e1) e4) (Eq (op e1 e4) e3)) % 12.74/12.92 Clause #268 (by superposition #[267, 96]): Or (Eq (op e4 e3) e4) (Or (Eq (op e1 e4) e3) (Eq (op (op e1 e4) e4) e4)) % 12.74/12.92 Clause #287 (by clausification #[194]): Eq (Eq (op (op e4 e2) e2) e4) True % 12.74/12.92 Clause #288 (by clausification #[194]): Eq % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (Or % 12.74/12.92 (Or % 12.74/12.92 (Or % 12.74/12.92 (Or % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And (And (Ne (op e0 e0) e0) (Ne (op e0 e1) e1)) % 12.74/12.92 (Ne (op e0 e2) e2)) % 12.74/12.92 (Ne (op e0 e3) e3)) % 12.74/12.92 (Ne (op e0 e4) e4)) % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And (And (Ne (op e1 e0) e0) (Ne (op e1 e1) e1)) % 12.74/12.92 (Ne (op e1 e2) e2)) % 12.74/12.92 (Ne (op e1 e3) e3)) % 12.74/12.92 (Ne (op e1 e4) e4))) % 12.74/12.92 (And % 12.74/12.92 (And % 12.74/12.92 (And (And (Ne (op e2 e0) e0) (Ne (op e2 e1) e1)) % 12.74/12.92 (Ne (op e2 e2) e2)) % 12.74/12.92 (Ne (op e2 e3) e3)) % 12.74/12.92 (Ne (op e2 e4) e4))) % 12.74/12.92 (And % 12.74/12.94 (And % 12.74/12.94 (And (And (Ne (op e3 e0) e0) (Ne (op e3 e1) e1)) % 12.74/12.94 (Ne (op e3 e2) e2)) % 12.74/12.94 (Ne (op e3 e3) e3)) % 12.74/12.94 (Ne (op e3 e4) e4))) % 12.74/12.94 (And % 12.74/12.94 (And % 12.74/12.94 (And (And (Ne (op e4 e0) e0) (Ne (op e4 e1) e1)) (Ne (op e4 e2) e2)) % 12.74/12.94 (Ne (op e4 e3) e3)) % 12.74/12.94 (Ne (op e4 e4) e4))) % 12.74/12.94 (Eq (op (op e0 e0) e0) e0)) % 12.74/12.94 (Eq (op (op e0 e1) e1) e0)) % 12.74/12.94 (Eq (op (op e0 e2) e2) e0)) % 12.74/12.94 (Eq (op (op e0 e3) e3) e0)) % 12.74/12.94 (Eq (op (op e0 e4) e4) e0)) % 12.74/12.94 (Eq (op (op e1 e0) e0) e1)) % 12.74/12.94 (Eq (op (op e1 e1) e1) e1)) % 12.74/12.94 (Eq (op (op e1 e2) e2) e1)) % 12.74/12.94 (Eq (op (op e1 e3) e3) e1)) % 12.74/12.94 (Eq (op (op e1 e4) e4) e1)) % 12.74/12.94 (Eq (op (op e2 e0) e0) e2)) % 12.74/12.94 (Eq (op (op e2 e1) e1) e2)) % 12.74/12.94 (Eq (op (op e2 e2) e2) e2)) % 12.74/12.94 (Eq (op (op e2 e3) e3) e2)) % 12.74/12.94 (Eq (op (op e2 e4) e4) e2)) % 12.74/12.94 (Eq (op (op e3 e0) e0) e3)) % 12.74/12.94 (Eq (op (op e3 e1) e1) e3)) % 12.74/12.94 (Eq (op (op e3 e2) e2) e3)) % 12.74/12.94 (Eq (op (op e3 e3) e3) e3)) % 12.74/12.94 (Eq (op (op e3 e4) e4) e3)) % 12.74/12.94 (Eq (op (op e4 e0) e0) e4)) % 12.74/12.94 (Eq (op (op e4 e1) e1) e4)) % 12.74/12.94 True % 12.74/12.94 Clause #289 (by clausification #[287]): Eq (op (op e4 e2) e2) e4 % 12.74/12.94 Clause #291 (by superposition #[289, 229]): Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e1) (Eq (op e2 e2) e4))) % 12.74/12.94 Clause #294 (by superposition #[291, 113]): Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e1) (Eq e4 e3))) % 12.74/12.94 Clause #295 (by forward contextual literal cutting #[294, 41]): Or (Eq (op e4 e2) e4) (Or (Eq (op e4 e2) e3) (Eq (op e4 e2) e1)) % 12.74/12.94 Clause #300 (by superposition #[295, 257]): Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e1) (Or (Eq (op e1 e4) e3) (Eq (op e3 e4) e4))) % 12.74/12.94 Clause #305 (by superposition #[196, 117]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e4 e4) e3))) % 12.74/12.94 Clause #325 (by superposition #[305, 23]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq e0 e3))) % 12.74/12.94 Clause #326 (by forward contextual literal cutting #[325, 77]): Or (Eq (op e4 e3) e4) (Or (Eq (op e4 e3) e3) (Eq (op e4 e3) e1)) % 12.74/12.94 Clause #327 (by superposition #[326, 90]): Or (Eq (op e4 e3) e3) (Or (Eq (op e4 e3) e1) (Eq (op e1 e4) e4)) % 12.74/12.94 Clause #340 (by superposition #[327, 90]): Or (Eq (op e4 e3) e3) (Or (Eq (op e1 e4) e4) (Eq (op e1 e1) e4)) % 12.74/12.94 Clause #342 (by superposition #[327, 108]): Or (Eq (op e4 e3) e3) (Or (Eq (op e1 e4) e4) (Eq (op e1 e1) e3)) % 12.74/12.94 Clause #343 (by superposition #[327, 195]): Or (Eq (op e4 e3) e3) (Or (Eq (op e1 e4) e4) (Eq (op e1 e3) e4)) % 12.74/12.94 Clause #349 (by superposition #[342, 195]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e1) e3) (Eq (op e3 e3) e4)) % 12.74/12.94 Clause #355 (by forward demodulation #[349, 12]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e1) e3) (Eq e2 e4)) % 12.74/12.94 Clause #356 (by forward contextual literal cutting #[355, 44]): Or (Eq (op e1 e4) e4) (Eq (op e1 e1) e3) % 12.74/12.94 Clause #358 (by superposition #[356, 268]): Or (Eq (op e1 e1) e3) (Or (Eq (op e4 e3) e4) (Or (Eq e4 e3) (Eq (op e4 e4) e4))) % 12.74/12.94 Clause #365 (by superposition #[340, 195]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e1) e4) (Eq (op e3 e3) e4)) % 12.74/12.94 Clause #369 (by forward demodulation #[365, 12]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e1) e4) (Eq e2 e4)) % 12.74/12.94 Clause #370 (by forward contextual literal cutting #[369, 44]): Or (Eq (op e1 e4) e4) (Eq (op e1 e1) e4) % 12.78/13.00 Clause #372 (by superposition #[370, 268]): Or (Eq (op e1 e1) e4) (Or (Eq (op e4 e3) e4) (Or (Eq e4 e3) (Eq (op e4 e4) e4))) % 12.78/13.00 Clause #378 (by superposition #[343, 195]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e3) e4) (Eq (op e3 e3) e4)) % 12.78/13.00 Clause #380 (by forward demodulation #[378, 12]): Or (Eq (op e1 e4) e4) (Or (Eq (op e1 e3) e4) (Eq e2 e4)) % 12.78/13.00 Clause #381 (by forward contextual literal cutting #[380, 44]): Or (Eq (op e1 e4) e4) (Eq (op e1 e3) e4) % 12.78/13.00 Clause #383 (by superposition #[381, 268]): Or (Eq (op e1 e3) e4) (Or (Eq (op e4 e3) e4) (Or (Eq e4 e3) (Eq (op e4 e4) e4))) % 12.78/13.00 Clause #386 (by forward contextual literal cutting #[383, 41]): Or (Eq (op e1 e3) e4) (Or (Eq (op e4 e3) e4) (Eq (op e4 e4) e4)) % 12.78/13.00 Clause #387 (by superposition #[386, 23]): Or (Eq (op e1 e3) e4) (Or (Eq (op e4 e3) e4) (Eq e0 e4)) % 12.78/13.00 Clause #409 (by forward contextual literal cutting #[387, 73]): Or (Eq (op e1 e3) e4) (Eq (op e4 e3) e4) % 12.78/13.00 Clause #449 (by clausification #[241]): Eq % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (And % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e0) % 12.78/13.00 (Eq (op e0 e1) e0)) % 12.78/13.00 (Eq (op e0 e2) e0)) % 12.78/13.00 (Eq (op e0 e3) e0)) % 12.78/13.00 (Eq (op e0 e4) e0)) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e0) % 12.78/13.00 (Eq (op e1 e0) e0)) % 12.78/13.00 (Eq (op e2 e0) e0)) % 12.78/13.00 (Eq (op e3 e0) e0)) % 12.78/13.00 (Eq (op e4 e0) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e1) % 12.78/13.00 (Eq (op e0 e1) e1)) % 12.78/13.00 (Eq (op e0 e2) e1)) % 12.78/13.00 (Eq (op e0 e3) e1)) % 12.78/13.00 (Eq (op e0 e4) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e1) % 12.78/13.00 (Eq (op e1 e0) e1)) % 12.78/13.00 (Eq (op e2 e0) e1)) % 12.78/13.00 (Eq (op e3 e0) e1)) % 12.78/13.00 (Eq (op e4 e0) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e2) % 12.78/13.00 (Eq (op e0 e1) e2)) % 12.78/13.00 (Eq (op e0 e2) e2)) % 12.78/13.00 (Eq (op e0 e3) e2)) % 12.78/13.00 (Eq (op e0 e4) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e2) % 12.78/13.00 (Eq (op e1 e0) e2)) % 12.78/13.00 (Eq (op e2 e0) e2)) % 12.78/13.00 (Eq (op e3 e0) e2)) % 12.78/13.00 (Eq (op e4 e0) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e3) % 12.78/13.00 (Eq (op e0 e1) e3)) % 12.78/13.00 (Eq (op e0 e2) e3)) % 12.78/13.00 (Eq (op e0 e3) e3)) % 12.78/13.00 (Eq (op e0 e4) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e3) % 12.78/13.00 (Eq (op e1 e0) e3)) % 12.78/13.00 (Eq (op e2 e0) e3)) % 12.78/13.00 (Eq (op e3 e0) e3)) % 12.78/13.00 (Eq (op e4 e0) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e4) % 12.78/13.00 (Eq (op e0 e1) e4)) % 12.78/13.00 (Eq (op e0 e2) e4)) % 12.78/13.00 (Eq (op e0 e3) e4)) % 12.78/13.00 (Eq (op e0 e4) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e0) e4) % 12.78/13.00 (Eq (op e1 e0) e4)) % 12.78/13.00 (Eq (op e2 e0) e4)) % 12.78/13.00 (Eq (op e3 e0) e4)) % 12.78/13.00 (Eq (op e4 e0) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e1 e0) e0) % 12.78/13.00 (Eq (op e1 e1) e0)) % 12.78/13.00 (Eq (op e1 e2) e0)) % 12.78/13.00 (Eq (op e1 e3) e0)) % 12.78/13.00 (Eq (op e1 e4) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) % 12.78/13.00 (Eq (op e2 e1) e0)) % 12.78/13.00 (Eq (op e3 e1) e0)) % 12.78/13.00 (Eq (op e4 e1) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) % 12.78/13.00 (Eq (op e1 e2) e1)) % 12.78/13.00 (Eq (op e1 e3) e1)) % 12.78/13.00 (Eq (op e1 e4) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) % 12.78/13.00 (Eq (op e2 e1) e1)) % 12.78/13.00 (Eq (op e3 e1) e1)) % 12.78/13.00 (Eq (op e4 e1) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) % 12.78/13.00 (Eq (op e1 e2) e2)) % 12.78/13.00 (Eq (op e1 e3) e2)) % 12.78/13.00 (Eq (op e1 e4) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) % 12.78/13.00 (Eq (op e2 e1) e2)) % 12.78/13.00 (Eq (op e3 e1) e2)) % 12.78/13.00 (Eq (op e4 e1) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) % 12.78/13.00 (Eq (op e1 e2) e3)) % 12.78/13.00 (Eq (op e1 e3) e3)) % 12.78/13.00 (Eq (op e1 e4) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) % 12.78/13.00 (Eq (op e2 e1) e3)) % 12.78/13.00 (Eq (op e3 e1) e3)) % 12.78/13.00 (Eq (op e4 e1) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e1 e0) e4) (Eq (op e1 e1) e4)) % 12.78/13.00 (Eq (op e1 e2) e4)) % 12.78/13.00 (Eq (op e1 e3) e4)) % 12.78/13.00 (Eq (op e1 e4) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e0 e1) e4) (Eq (op e1 e1) e4)) % 12.78/13.00 (Eq (op e2 e1) e4)) % 12.78/13.00 (Eq (op e3 e1) e4)) % 12.78/13.00 (Eq (op e4 e1) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) % 12.78/13.00 (Eq (op e2 e2) e0)) % 12.78/13.00 (Eq (op e2 e3) e0)) % 12.78/13.00 (Eq (op e2 e4) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 12.78/13.00 (Eq (op e2 e2) e0)) % 12.78/13.00 (Eq (op e3 e2) e0)) % 12.78/13.00 (Eq (op e4 e2) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) % 12.78/13.00 (Eq (op e2 e3) e1)) % 12.78/13.00 (Eq (op e2 e4) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) % 12.78/13.00 (Eq (op e3 e2) e1)) % 12.78/13.00 (Eq (op e4 e2) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) % 12.78/13.00 (Eq (op e2 e3) e2)) % 12.78/13.00 (Eq (op e2 e4) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) % 12.78/13.00 (Eq (op e3 e2) e2)) % 12.78/13.00 (Eq (op e4 e2) e2))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) % 12.78/13.00 (Eq (op e2 e3) e3)) % 12.78/13.00 (Eq (op e2 e4) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) % 12.78/13.00 (Eq (op e3 e2) e3)) % 12.78/13.00 (Eq (op e4 e2) e3))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e2 e0) e4) (Eq (op e2 e1) e4)) (Eq (op e2 e2) e4)) % 12.78/13.00 (Eq (op e2 e3) e4)) % 12.78/13.00 (Eq (op e2 e4) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e2) e4) (Eq (op e1 e2) e4)) (Eq (op e2 e2) e4)) % 12.78/13.00 (Eq (op e3 e2) e4)) % 12.78/13.00 (Eq (op e4 e2) e4))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) % 12.78/13.00 (Eq (op e3 e3) e0)) % 12.78/13.00 (Eq (op e3 e4) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) % 12.78/13.00 (Eq (op e3 e3) e0)) % 12.78/13.00 (Eq (op e4 e3) e0))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) % 12.78/13.00 (Eq (op e3 e3) e1)) % 12.78/13.00 (Eq (op e3 e4) e1))) % 12.78/13.00 (Or % 12.78/13.00 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1)) % 12.78/13.00 (Eq (op e4 e3) e1))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2)) % 12.78/13.00 (Eq (op e3 e4) e2))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2)) % 12.78/13.00 (Eq (op e4 e3) e2))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3)) % 12.78/13.00 (Eq (op e3 e4) e3))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3)) % 12.78/13.00 (Eq (op e4 e3) e3))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e3 e0) e4) (Eq (op e3 e1) e4)) (Eq (op e3 e2) e4)) (Eq (op e3 e3) e4)) % 12.78/13.00 (Eq (op e3 e4) e4))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e3) e4) (Eq (op e1 e3) e4)) (Eq (op e2 e3) e4)) (Eq (op e3 e3) e4)) % 12.78/13.00 (Eq (op e4 e3) e4))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e4 e0) e0) (Eq (op e4 e1) e0)) (Eq (op e4 e2) e0)) (Eq (op e4 e3) e0)) % 12.78/13.00 (Eq (op e4 e4) e0))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e4) e0) (Eq (op e1 e4) e0)) (Eq (op e2 e4) e0)) (Eq (op e3 e4) e0)) % 12.78/13.00 (Eq (op e4 e4) e0))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e4 e0) e1) (Eq (op e4 e1) e1)) (Eq (op e4 e2) e1)) (Eq (op e4 e3) e1)) % 12.78/13.00 (Eq (op e4 e4) e1))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e4) e1) (Eq (op e1 e4) e1)) (Eq (op e2 e4) e1)) (Eq (op e3 e4) e1)) % 12.78/13.00 (Eq (op e4 e4) e1))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e4 e0) e2) (Eq (op e4 e1) e2)) (Eq (op e4 e2) e2)) (Eq (op e4 e3) e2)) % 12.78/13.00 (Eq (op e4 e4) e2))) % 12.78/13.00 (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) (Eq (op e4 e4) e2))) % 12.78/13.00 True % 12.78/13.00 Clause #467 (by forward contextual literal cutting #[358, 41]): Or (Eq (op e1 e1) e3) (Or (Eq (op e4 e3) e4) (Eq (op e4 e4) e4)) % 12.78/13.00 Clause #468 (by superposition #[467, 23]): Or (Eq (op e1 e1) e3) (Or (Eq (op e4 e3) e4) (Eq e0 e4)) % 12.78/13.00 Clause #469 (by forward contextual literal cutting #[468, 73]): Or (Eq (op e1 e1) e3) (Eq (op e4 e3) e4) % 12.78/13.00 Clause #472 (by superposition #[469, 108]): Or (Eq (op e1 e1) e3) (Eq (op e4 e1) e3) % 12.78/13.00 Clause #533 (by forward contextual literal cutting #[372, 41]): Or (Eq (op e1 e1) e4) (Or (Eq (op e4 e3) e4) (Eq (op e4 e4) e4)) % 12.78/13.00 Clause #534 (by superposition #[533, 23]): Or (Eq (op e1 e1) e4) (Or (Eq (op e4 e3) e4) (Eq e0 e4)) % 12.78/13.00 Clause #535 (by forward contextual literal cutting #[534, 73]): Or (Eq (op e1 e1) e4) (Eq (op e4 e3) e4) % 12.78/13.00 Clause #538 (by superposition #[535, 108]): Or (Eq (op e1 e1) e4) (Eq (op e4 e1) e3) % 12.78/13.00 Clause #561 (by clausification #[288]): Eq (Eq (op (op e4 e1) e1) e4) True % 12.78/13.00 Clause #563 (by clausification #[561]): Eq (op (op e4 e1) e1) e4 % 12.78/13.00 Clause #567 (by superposition #[563, 472]): Or (Eq (op e1 e1) e3) (Eq (op e3 e1) e4) % 12.78/13.00 Clause #568 (by superposition #[563, 538]): Or (Eq (op e1 e1) e4) (Eq (op e3 e1) e4) % 12.78/13.00 Clause #569 (by superposition #[567, 568]): Or (Eq (op e3 e1) e4) (Or (Eq e4 e3) (Eq (op e3 e1) e4)) % 12.78/13.00 Clause #571 (by eliminate duplicate literals #[569]): Or (Eq (op e3 e1) e4) (Eq e4 e3) % 12.78/13.00 Clause #572 (by forward contextual literal cutting #[571, 41]): Eq (op e3 e1) e4 % 12.78/13.00 Clause #573 (by backward demodulation #[572, 120]): Eq (op (op e1 e3) e4) e3 % 12.78/13.03 Clause #579 (by forward demodulation #[300, 18]): Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e1) (Or (Eq (op e1 e4) e3) (Eq e1 e4))) % 12.78/13.03 Clause #580 (by forward contextual literal cutting #[579, 50]): Or (Eq (op e4 e2) e3) (Or (Eq (op e4 e2) e1) (Eq (op e1 e4) e3)) % 12.78/13.03 Clause #585 (by superposition #[580, 258]): Or (Eq (op e4 e2) e3) (Or (Eq (op e1 e4) e3) (Or (Eq (op e1 e4) e3) (Eq (op e1 e3) e2))) % 12.78/13.03 Clause #872 (by eliminate duplicate literals #[585]): Or (Eq (op e4 e2) e3) (Or (Eq (op e1 e4) e3) (Eq (op e1 e3) e2)) % 12.78/13.03 Clause #878 (by superposition #[872, 257]): Or (Eq (op e1 e4) e3) (Or (Eq (op e1 e3) e2) (Or (Eq (op e1 e4) e3) (Eq (op e3 e3) e4))) % 12.78/13.03 Clause #906 (by eliminate duplicate literals #[878]): Or (Eq (op e1 e4) e3) (Or (Eq (op e1 e3) e2) (Eq (op e3 e3) e4)) % 12.78/13.03 Clause #907 (by forward demodulation #[906, 12]): Or (Eq (op e1 e4) e3) (Or (Eq (op e1 e3) e2) (Eq e2 e4)) % 12.78/13.03 Clause #908 (by forward contextual literal cutting #[907, 44]): Or (Eq (op e1 e4) e3) (Eq (op e1 e3) e2) % 12.78/13.03 Clause #910 (by superposition #[908, 356]): Or (Eq (op e1 e3) e2) (Or (Eq e3 e4) (Eq (op e1 e1) e3)) % 12.78/13.03 Clause #911 (by superposition #[908, 370]): Or (Eq (op e1 e3) e2) (Or (Eq e3 e4) (Eq (op e1 e1) e4)) % 12.78/13.03 Clause #979 (by forward contextual literal cutting #[911, 41]): Or (Eq (op e1 e3) e2) (Eq (op e1 e1) e4) % 12.78/13.03 Clause #980 (by forward contextual literal cutting #[910, 41]): Or (Eq (op e1 e3) e2) (Eq (op e1 e1) e3) % 12.78/13.03 Clause #981 (by superposition #[980, 979]): Or (Eq (op e1 e3) e2) (Or (Eq (op e1 e3) e2) (Eq e3 e4)) % 12.78/13.03 Clause #982 (by eliminate duplicate literals #[981]): Or (Eq (op e1 e3) e2) (Eq e3 e4) % 12.78/13.03 Clause #983 (by forward contextual literal cutting #[982, 41]): Eq (op e1 e3) e2 % 12.78/13.03 Clause #986 (by backward demodulation #[983, 409]): Or (Eq e2 e4) (Eq (op e4 e3) e4) % 12.78/13.03 Clause #997 (by backward demodulation #[983, 573]): Eq (op e2 e4) e3 % 12.78/13.03 Clause #1035 (by forward contextual literal cutting #[986, 44]): Eq (op e4 e3) e4 % 12.78/13.03 Clause #1036 (by backward demodulation #[1035, 90]): Eq (op e1 e4) e4 % 12.78/13.03 Clause #1125 (by clausification #[449]): Eq (Or (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) (Eq (op e4 e4) e2)) % 12.78/13.03 True % 12.78/13.03 Clause #1127 (by clausification #[1125]): Or (Eq (Or (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) (Eq (op e3 e4) e2)) True) % 12.78/13.03 (Eq (Eq (op e4 e4) e2) True) % 12.78/13.03 Clause #1128 (by clausification #[1127]): Or (Eq (Eq (op e4 e4) e2) True) % 12.78/13.03 (Or (Eq (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) True) (Eq (Eq (op e3 e4) e2) True)) % 12.78/13.03 Clause #1129 (by clausification #[1128]): Or (Eq (Or (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) (Eq (op e2 e4) e2)) True) % 12.78/13.03 (Or (Eq (Eq (op e3 e4) e2) True) (Eq (op e4 e4) e2)) % 12.78/13.03 Clause #1130 (by clausification #[1129]): Or (Eq (Eq (op e3 e4) e2) True) % 12.78/13.03 (Or (Eq (op e4 e4) e2) (Or (Eq (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) True) (Eq (Eq (op e2 e4) e2) True))) % 12.78/13.03 Clause #1131 (by clausification #[1130]): Or (Eq (op e4 e4) e2) % 12.78/13.03 (Or (Eq (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)) True) (Or (Eq (Eq (op e2 e4) e2) True) (Eq (op e3 e4) e2))) % 12.78/13.03 Clause #1132 (by clausification #[1131]): Or (Eq (op e4 e4) e2) % 12.78/13.03 (Or (Eq (Eq (op e2 e4) e2) True) % 12.78/13.03 (Or (Eq (op e3 e4) e2) (Or (Eq (Eq (op e0 e4) e2) True) (Eq (Eq (op e1 e4) e2) True)))) % 12.78/13.03 Clause #1133 (by clausification #[1132]): Or (Eq (op e4 e4) e2) % 12.78/13.03 (Or (Eq (op e3 e4) e2) (Or (Eq (Eq (op e0 e4) e2) True) (Or (Eq (Eq (op e1 e4) e2) True) (Eq (op e2 e4) e2)))) % 12.78/13.03 Clause #1134 (by clausification #[1133]): Or (Eq (op e4 e4) e2) % 12.78/13.03 (Or (Eq (op e3 e4) e2) (Or (Eq (Eq (op e1 e4) e2) True) (Or (Eq (op e2 e4) e2) (Eq (op e0 e4) e2)))) % 12.78/13.03 Clause #1135 (by clausification #[1134]): Or (Eq (op e4 e4) e2) (Or (Eq (op e3 e4) e2) (Or (Eq (op e2 e4) e2) (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)))) % 12.78/13.03 Clause #1136 (by forward demodulation #[1135, 23]): Or (Eq e0 e2) (Or (Eq (op e3 e4) e2) (Or (Eq (op e2 e4) e2) (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)))) % 12.78/13.03 Clause #1137 (by forward demodulation #[1136, 18]): Or (Eq e0 e2) (Or (Eq e1 e2) (Or (Eq (op e2 e4) e2) (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)))) % 12.78/13.03 Clause #1138 (by forward demodulation #[1137, 997]): Or (Eq e0 e2) (Or (Eq e1 e2) (Or (Eq e3 e2) (Or (Eq (op e0 e4) e2) (Eq (op e1 e4) e2)))) % 12.87/13.04 Clause #1139 (by forward demodulation #[1138, 1036]): Or (Eq e0 e2) (Or (Eq e1 e2) (Or (Eq e3 e2) (Or (Eq (op e0 e4) e2) (Eq e4 e2)))) % 12.87/13.04 Clause #1140 (by forward contextual literal cutting #[1139, 80]): Or (Eq e1 e2) (Or (Eq e3 e2) (Or (Eq (op e0 e4) e2) (Eq e4 e2))) % 12.87/13.04 Clause #1141 (by forward contextual literal cutting #[1140, 70]): Or (Eq e3 e2) (Or (Eq (op e0 e4) e2) (Eq e4 e2)) % 12.87/13.04 Clause #1142 (by forward contextual literal cutting #[1141, 47]): Or (Eq (op e0 e4) e2) (Eq e4 e2) % 12.87/13.04 Clause #1143 (by forward contextual literal cutting #[1142, 44]): Eq (op e0 e4) e2 % 12.87/13.04 Clause #1144 (by superposition #[1143, 126]): Eq e2 e4 % 12.87/13.04 Clause #1145 (by forward contextual literal cutting #[1144, 44]): False % 12.87/13.04 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------