%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG054+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:43:57 PM UTC 2025 % Result : Theorem 8.76s 9.00s % Output : Proof 9.33s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG054+1 : TPTP v9.2.0. Released v2.7.0. % 0.12/0.12 % Command : duper %s % 0.12/0.32 % Computer : n001.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Fri Oct 3 09:48:08 EDT 2025 % 0.12/0.32 % CPUTime : % 8.76/9.00 SZS status Theorem for theBenchmark.p % 8.76/9.00 SZS output start Proof for theBenchmark.p % 8.76/9.00 Clause #1 (by assumption #[]): Eq % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 8.76/9.00 (Eq (op unit e2) e2)) % 8.76/9.00 (Eq (op e2 unit) e2)) % 8.76/9.00 (Eq (op unit e3) e3)) % 8.76/9.00 (Eq (op e3 unit) e3)) % 8.76/9.00 (Eq (op unit e4) e4)) % 8.76/9.00 (Eq (op e4 unit) e4)) % 8.76/9.00 (Or (Or (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) (Eq unit e3)) (Eq unit e4))) % 8.76/9.00 True % 8.76/9.00 Clause #3 (by assumption #[]): Eq % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (And % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e0)) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e0) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e0))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e1) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e1))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e2) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e2))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e3) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e3))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e4) % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e4) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e4) % 8.76/9.00 (op % 8.76/9.00 e3 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e0 % 8.76/9.00 e4) % 8.76/9.00 (op % 8.76/9.00 e4 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op % 8.76/9.00 e1 % 8.76/9.00 e4) % 8.76/9.00 (op % 8.76/9.00 e2 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op e1 % 8.76/9.00 e4) % 8.76/9.00 (op e3 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op e1 % 8.76/9.00 e4) % 8.76/9.00 (op e4 % 8.76/9.00 e4))) % 8.76/9.00 (Ne % 8.76/9.00 (op e2 e4) % 8.76/9.00 (op e3 % 8.76/9.00 e4))) % 8.76/9.00 (Ne (op e2 e4) % 8.76/9.00 (op e4 e4))) % 8.76/9.00 (Ne (op e3 e4) % 8.76/9.00 (op e4 e4))) % 8.76/9.00 (Ne (op e0 e0) % 8.76/9.00 (op e0 e1))) % 8.76/9.00 (Ne (op e0 e0) % 8.76/9.00 (op e0 e2))) % 8.76/9.00 (Ne (op e0 e0) % 8.76/9.00 (op e0 e3))) % 8.76/9.00 (Ne (op e0 e0) % 8.76/9.00 (op e0 e4))) % 8.76/9.00 (Ne (op e0 e1) % 8.76/9.00 (op e0 e2))) % 8.76/9.00 (Ne (op e0 e1) (op e0 e3))) % 8.76/9.00 (Ne (op e0 e1) (op e0 e4))) % 8.76/9.00 (Ne (op e0 e2) (op e0 e3))) % 8.76/9.00 (Ne (op e0 e2) (op e0 e4))) % 8.76/9.00 (Ne (op e0 e3) (op e0 e4))) % 8.76/9.00 (Ne (op e1 e0) (op e1 e1))) % 8.76/9.00 (Ne (op e1 e0) (op e1 e2))) % 8.76/9.00 (Ne (op e1 e0) (op e1 e3))) % 8.76/9.00 (Ne (op e1 e0) (op e1 e4))) % 8.76/9.00 (Ne (op e1 e1) (op e1 e2))) % 8.76/9.00 (Ne (op e1 e1) (op e1 e3))) % 8.76/9.00 (Ne (op e1 e1) (op e1 e4))) % 8.76/9.00 (Ne (op e1 e2) (op e1 e3))) % 8.76/9.00 (Ne (op e1 e2) (op e1 e4))) % 8.76/9.00 (Ne (op e1 e3) (op e1 e4))) % 8.76/9.00 (Ne (op e2 e0) (op e2 e1))) % 8.76/9.00 (Ne (op e2 e0) (op e2 e2))) % 8.76/9.00 (Ne (op e2 e0) (op e2 e3))) % 8.76/9.00 (Ne (op e2 e0) (op e2 e4))) % 8.76/9.00 (Ne (op e2 e1) (op e2 e2))) % 8.76/9.00 (Ne (op e2 e1) (op e2 e3))) % 8.76/9.00 (Ne (op e2 e1) (op e2 e4))) % 8.76/9.00 (Ne (op e2 e2) (op e2 e3))) % 8.76/9.00 (Ne (op e2 e2) (op e2 e4))) % 8.76/9.00 (Ne (op e2 e3) (op e2 e4))) % 8.76/9.00 (Ne (op e3 e0) (op e3 e1))) % 8.76/9.00 (Ne (op e3 e0) (op e3 e2))) % 8.76/9.00 (Ne (op e3 e0) (op e3 e3))) % 8.76/9.00 (Ne (op e3 e0) (op e3 e4))) % 8.76/9.00 (Ne (op e3 e1) (op e3 e2))) % 8.76/9.00 (Ne (op e3 e1) (op e3 e3))) % 8.76/9.00 (Ne (op e3 e1) (op e3 e4))) % 8.76/9.00 (Ne (op e3 e2) (op e3 e3))) % 8.76/9.00 (Ne (op e3 e2) (op e3 e4))) % 8.76/9.00 (Ne (op e3 e3) (op e3 e4))) % 8.76/9.00 (Ne (op e4 e0) (op e4 e1))) % 8.76/9.00 (Ne (op e4 e0) (op e4 e2))) % 8.76/9.00 (Ne (op e4 e0) (op e4 e3))) % 8.76/9.00 (Ne (op e4 e0) (op e4 e4))) % 8.76/9.00 (Ne (op e4 e1) (op e4 e2))) % 8.76/9.00 (Ne (op e4 e1) (op e4 e3))) % 8.76/9.00 (Ne (op e4 e1) (op e4 e4))) % 8.76/9.00 (Ne (op e4 e2) (op e4 e3))) % 8.76/9.00 (Ne (op e4 e2) (op e4 e4))) % 8.76/9.00 (Ne (op e4 e3) (op e4 e4))) % 8.86/9.03 True % 8.86/9.03 Clause #4 (by assumption #[]): Eq % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (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)) % 8.86/9.03 (Ne e2 e3)) % 8.86/9.03 (Ne e2 e4)) % 8.86/9.03 (Ne e3 e4)) % 8.86/9.03 True % 8.86/9.03 Clause #5 (by assumption #[]): Eq % 8.86/9.03 (And % 8.86/9.03 (And (And (Eq e0 (op e1 (op (op e1 e1) (op e1 e1)))) (Eq e2 (op (op e1 e1) (op e1 e1)))) % 8.86/9.03 (Eq e3 (op (op (op e1 e1) (op e1 e1)) (op (op e1 e1) (op e1 e1))))) % 8.86/9.03 (Eq e4 (op e1 e1))) % 8.86/9.03 True % 8.86/9.03 Clause #6 (by assumption #[]): Eq % 8.86/9.03 (Not % 8.86/9.03 (Not % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (And % 8.86/9.03 (Or % 8.86/9.03 (Or % 8.86/9.03 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) % 8.86/9.03 (Eq (op e2 e2) e0)) % 8.86/9.03 (Eq (op e3 e3) e0)) % 8.86/9.03 (Eq (op e4 e4) e0)) % 8.86/9.03 (Or % 8.86/9.03 (Or % 8.86/9.03 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) % 8.86/9.03 (Eq (op e2 e2) e1)) % 8.86/9.03 (Eq (op e3 e3) e1)) % 8.86/9.03 (Eq (op e4 e4) e1))) % 8.86/9.03 (Or % 8.86/9.03 (Or % 8.86/9.03 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) % 8.86/9.03 (Eq (op e2 e2) e2)) % 8.86/9.03 (Eq (op e3 e3) e2)) % 8.86/9.03 (Eq (op e4 e4) e2))) % 8.86/9.03 (Or % 8.86/9.03 (Or % 8.86/9.03 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) % 8.86/9.03 (Eq (op e2 e2) e3)) % 8.86/9.03 (Eq (op e3 e3) e3)) % 8.86/9.03 (Eq (op e4 e4) e3))) % 8.86/9.03 (Or % 8.86/9.03 (Or % 8.86/9.03 (Or (Or (Eq (op e0 e0) e4) (Eq (op e1 e1) e4)) % 8.86/9.03 (Eq (op e2 e2) e4)) % 8.86/9.03 (Eq (op e3 e3) e4)) % 8.86/9.04 (Eq (op e4 e4) e4))) % 8.86/9.04 (Or (Ne (op e0 e0) e0) (Eq (op e0 e0) e0))) % 8.86/9.04 (Or (Ne (op e0 e0) e1) (Eq (op e0 e1) e0))) % 8.86/9.04 (Or (Ne (op e0 e0) e2) (Eq (op e0 e2) e0))) % 8.86/9.04 (Or (Ne (op e0 e0) e3) (Eq (op e0 e3) e0))) % 8.86/9.04 (Or (Ne (op e0 e0) e4) (Eq (op e0 e4) e0))) % 8.86/9.04 (Or (Ne (op e1 e1) e0) (Eq (op e1 e0) e1))) % 8.86/9.04 (Or (Ne (op e1 e1) e1) (Eq (op e1 e1) e1))) % 8.86/9.04 (Or (Ne (op e1 e1) e2) (Eq (op e1 e2) e1))) % 8.86/9.04 (Or (Ne (op e1 e1) e3) (Eq (op e1 e3) e1))) % 8.86/9.04 (Or (Ne (op e1 e1) e4) (Eq (op e1 e4) e1))) % 8.86/9.04 (Or (Ne (op e2 e2) e0) (Eq (op e2 e0) e2))) % 8.86/9.04 (Or (Ne (op e2 e2) e1) (Eq (op e2 e1) e2))) % 8.86/9.04 (Or (Ne (op e2 e2) e2) (Eq (op e2 e2) e2))) % 8.86/9.04 (Or (Ne (op e2 e2) e3) (Eq (op e2 e3) e2))) % 8.86/9.04 (Or (Ne (op e2 e2) e4) (Eq (op e2 e4) e2))) % 8.86/9.04 (Or (Ne (op e3 e3) e0) (Eq (op e3 e0) e3))) % 8.86/9.04 (Or (Ne (op e3 e3) e1) (Eq (op e3 e1) e3))) % 8.86/9.04 (Or (Ne (op e3 e3) e2) (Eq (op e3 e2) e3))) % 8.86/9.04 (Or (Ne (op e3 e3) e3) (Eq (op e3 e3) e3))) % 8.86/9.04 (Or (Ne (op e3 e3) e4) (Eq (op e3 e4) e3))) % 8.86/9.04 (Or (Ne (op e4 e4) e0) (Eq (op e4 e0) e4))) % 8.86/9.04 (Or (Ne (op e4 e4) e1) (Eq (op e4 e1) e4))) % 8.86/9.04 (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4))) % 8.86/9.04 (Or (Ne (op e4 e4) e3) (Eq (op e4 e3) e4))) % 8.86/9.04 (Or (Ne (op e4 e4) e4) (Eq (op e4 e4) e4))))) % 8.86/9.04 True % 8.86/9.04 Clause #7 (by clausification #[5]): Eq (Eq e4 (op e1 e1)) True % 8.86/9.04 Clause #8 (by clausification #[5]): Eq % 8.86/9.04 (And (And (Eq e0 (op e1 (op (op e1 e1) (op e1 e1)))) (Eq e2 (op (op e1 e1) (op e1 e1)))) % 8.86/9.04 (Eq e3 (op (op (op e1 e1) (op e1 e1)) (op (op e1 e1) (op e1 e1))))) % 8.86/9.04 True % 8.86/9.04 Clause #9 (by clausification #[7]): Eq e4 (op e1 e1) % 8.86/9.04 Clause #10 (by clausification #[8]): Eq (Eq e3 (op (op (op e1 e1) (op e1 e1)) (op (op e1 e1) (op e1 e1)))) True % 8.86/9.04 Clause #11 (by clausification #[8]): Eq (And (Eq e0 (op e1 (op (op e1 e1) (op e1 e1)))) (Eq e2 (op (op e1 e1) (op e1 e1)))) True % 8.86/9.04 Clause #12 (by clausification #[10]): Eq e3 (op (op (op e1 e1) (op e1 e1)) (op (op e1 e1) (op e1 e1))) % 8.86/9.04 Clause #13 (by forward demodulation #[12, 9]): Eq e3 (op (op (op e1 e1) (op e1 e1)) (op (op e1 e1) e4)) % 8.86/9.04 Clause #14 (by forward demodulation #[13, 9]): Eq e3 (op (op (op e1 e1) (op e1 e1)) (op e4 e4)) % 8.86/9.04 Clause #15 (by forward demodulation #[14, 9]): Eq e3 (op (op (op e1 e1) e4) (op e4 e4)) % 8.86/9.04 Clause #16 (by forward demodulation #[15, 9]): Eq e3 (op (op e4 e4) (op e4 e4)) % 8.86/9.04 Clause #17 (by clausification #[11]): Eq (Eq e2 (op (op e1 e1) (op e1 e1))) True % 8.86/9.04 Clause #19 (by clausification #[17]): Eq e2 (op (op e1 e1) (op e1 e1)) % 8.86/9.04 Clause #20 (by forward demodulation #[19, 9]): Eq e2 (op (op e1 e1) e4) % 8.86/9.04 Clause #21 (by forward demodulation #[20, 9]): Eq e2 (op e4 e4) % 8.86/9.04 Clause #22 (by backward demodulation #[21, 16]): Eq e3 (op (op e4 e4) e2) % 8.86/9.04 Clause #23 (by forward demodulation #[22, 21]): Eq e3 (op e2 e2) % 8.86/9.04 Clause #43 (by clausification #[4]): Eq % 8.86/9.04 (And % 8.86/9.04 (And % 8.86/9.04 (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)) % 8.86/9.04 (Ne e2 e3)) % 8.86/9.04 (Ne e2 e4)) % 8.86/9.04 True % 8.86/9.04 Clause #45 (by clausification #[43]): Eq (Ne e2 e4) True % 8.86/9.04 Clause #46 (by clausification #[43]): Eq % 8.86/9.04 (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)) % 8.86/9.04 (Ne e2 e3)) % 8.86/9.04 True % 8.86/9.04 Clause #47 (by clausification #[45]): Ne e2 e4 % 8.86/9.04 Clause #48 (by clausification #[46]): Eq (Ne e2 e3) True % 8.86/9.04 Clause #49 (by clausification #[46]): 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 % 8.95/9.11 Clause #50 (by clausification #[48]): Ne e2 e3 % 8.95/9.11 Clause #51 (by clausification #[49]): Eq (Ne e1 e4) True % 8.95/9.11 Clause #53 (by clausification #[51]): Ne e1 e4 % 8.95/9.11 Clause #57 (by clausification #[1]): Eq (Or (Or (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) (Eq unit e3)) (Eq unit e4)) True % 8.95/9.11 Clause #58 (by clausification #[1]): Eq % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 8.95/9.11 (Eq (op unit e2) e2)) % 8.95/9.11 (Eq (op e2 unit) e2)) % 8.95/9.11 (Eq (op unit e3) e3)) % 8.95/9.11 (Eq (op e3 unit) e3)) % 8.95/9.11 (Eq (op unit e4) e4)) % 8.95/9.11 (Eq (op e4 unit) e4)) % 8.95/9.11 True % 8.95/9.11 Clause #59 (by clausification #[57]): Or (Eq (Or (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) (Eq unit e3)) True) (Eq (Eq unit e4) True) % 8.95/9.11 Clause #60 (by clausification #[59]): Or (Eq (Eq unit e4) True) (Or (Eq (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) True) (Eq (Eq unit e3) True)) % 8.95/9.11 Clause #61 (by clausification #[60]): Or (Eq (Or (Or (Eq unit e0) (Eq unit e1)) (Eq unit e2)) True) (Or (Eq (Eq unit e3) True) (Eq unit e4)) % 8.95/9.11 Clause #62 (by clausification #[61]): Or (Eq (Eq unit e3) True) (Or (Eq unit e4) (Or (Eq (Or (Eq unit e0) (Eq unit e1)) True) (Eq (Eq unit e2) True))) % 8.95/9.11 Clause #63 (by clausification #[62]): Or (Eq unit e4) (Or (Eq (Or (Eq unit e0) (Eq unit e1)) True) (Or (Eq (Eq unit e2) True) (Eq unit e3))) % 8.95/9.11 Clause #64 (by clausification #[63]): Or (Eq unit e4) (Or (Eq (Eq unit e2) True) (Or (Eq unit e3) (Or (Eq (Eq unit e0) True) (Eq (Eq unit e1) True)))) % 8.95/9.11 Clause #65 (by clausification #[64]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq (Eq unit e0) True) (Or (Eq (Eq unit e1) True) (Eq unit e2)))) % 8.95/9.11 Clause #66 (by clausification #[65]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq (Eq unit e1) True) (Or (Eq unit e2) (Eq unit e0)))) % 8.95/9.11 Clause #67 (by clausification #[66]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq unit e2) (Or (Eq unit e0) (Eq unit e1)))) % 8.95/9.11 Clause #98 (by clausification #[58]): Eq (Eq (op e4 unit) e4) True % 8.95/9.11 Clause #99 (by clausification #[58]): Eq % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 8.95/9.11 (Eq (op unit e2) e2)) % 8.95/9.11 (Eq (op e2 unit) e2)) % 8.95/9.11 (Eq (op unit e3) e3)) % 8.95/9.11 (Eq (op e3 unit) e3)) % 8.95/9.11 (Eq (op unit e4) e4)) % 8.95/9.11 True % 8.95/9.11 Clause #100 (by clausification #[98]): Eq (op e4 unit) e4 % 8.95/9.11 Clause #101 (by superposition #[100, 67]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq unit e2) (Or (Eq unit e1) (Eq (op e4 e0) e4)))) % 8.95/9.11 Clause #103 (by clausification #[3]): Eq % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (And % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e0)) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e0) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e0))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e1) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e1))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e2) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e2))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e3) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e3))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e4) % 8.95/9.11 (op % 8.95/9.11 e1 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e4) % 8.95/9.11 (op % 8.95/9.11 e2 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e4) % 8.95/9.11 (op % 8.95/9.11 e3 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op % 8.95/9.11 e0 % 8.95/9.11 e4) % 8.95/9.11 (op % 8.95/9.11 e4 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op e1 % 8.95/9.11 e4) % 8.95/9.11 (op e2 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op e1 % 8.95/9.11 e4) % 8.95/9.11 (op e3 % 8.95/9.11 e4))) % 8.95/9.11 (Ne % 8.95/9.11 (op e1 e4) % 8.95/9.11 (op e4 % 8.95/9.11 e4))) % 8.95/9.11 (Ne (op e2 e4) % 8.95/9.11 (op e3 e4))) % 8.95/9.11 (Ne (op e2 e4) % 8.95/9.11 (op e4 e4))) % 8.95/9.11 (Ne (op e3 e4) % 8.95/9.11 (op e4 e4))) % 8.95/9.11 (Ne (op e0 e0) % 8.95/9.11 (op e0 e1))) % 8.95/9.11 (Ne (op e0 e0) % 8.95/9.11 (op e0 e2))) % 8.95/9.11 (Ne (op e0 e0) % 8.95/9.11 (op e0 e3))) % 8.95/9.11 (Ne (op e0 e0) % 8.95/9.11 (op e0 e4))) % 8.95/9.11 (Ne (op e0 e1) (op e0 e2))) % 8.95/9.11 (Ne (op e0 e1) (op e0 e3))) % 8.95/9.11 (Ne (op e0 e1) (op e0 e4))) % 8.95/9.11 (Ne (op e0 e2) (op e0 e3))) % 8.95/9.11 (Ne (op e0 e2) (op e0 e4))) % 8.95/9.11 (Ne (op e0 e3) (op e0 e4))) % 8.95/9.11 (Ne (op e1 e0) (op e1 e1))) % 8.95/9.11 (Ne (op e1 e0) (op e1 e2))) % 8.95/9.11 (Ne (op e1 e0) (op e1 e3))) % 8.95/9.11 (Ne (op e1 e0) (op e1 e4))) % 8.95/9.11 (Ne (op e1 e1) (op e1 e2))) % 8.95/9.11 (Ne (op e1 e1) (op e1 e3))) % 8.95/9.11 (Ne (op e1 e1) (op e1 e4))) % 8.95/9.11 (Ne (op e1 e2) (op e1 e3))) % 8.95/9.11 (Ne (op e1 e2) (op e1 e4))) % 8.95/9.11 (Ne (op e1 e3) (op e1 e4))) % 8.95/9.11 (Ne (op e2 e0) (op e2 e1))) % 8.95/9.11 (Ne (op e2 e0) (op e2 e2))) % 8.95/9.11 (Ne (op e2 e0) (op e2 e3))) % 8.95/9.11 (Ne (op e2 e0) (op e2 e4))) % 8.95/9.11 (Ne (op e2 e1) (op e2 e2))) % 8.95/9.11 (Ne (op e2 e1) (op e2 e3))) % 8.95/9.11 (Ne (op e2 e1) (op e2 e4))) % 8.95/9.11 (Ne (op e2 e2) (op e2 e3))) % 8.95/9.11 (Ne (op e2 e2) (op e2 e4))) % 8.95/9.11 (Ne (op e2 e3) (op e2 e4))) % 8.95/9.11 (Ne (op e3 e0) (op e3 e1))) % 8.95/9.11 (Ne (op e3 e0) (op e3 e2))) % 8.95/9.11 (Ne (op e3 e0) (op e3 e3))) % 8.95/9.11 (Ne (op e3 e0) (op e3 e4))) % 8.95/9.11 (Ne (op e3 e1) (op e3 e2))) % 8.95/9.11 (Ne (op e3 e1) (op e3 e3))) % 8.95/9.11 (Ne (op e3 e1) (op e3 e4))) % 8.95/9.11 (Ne (op e3 e2) (op e3 e3))) % 8.95/9.11 (Ne (op e3 e2) (op e3 e4))) % 8.95/9.11 (Ne (op e3 e3) (op e3 e4))) % 8.95/9.14 (Ne (op e4 e0) (op e4 e1))) % 8.95/9.14 (Ne (op e4 e0) (op e4 e2))) % 8.95/9.14 (Ne (op e4 e0) (op e4 e3))) % 8.95/9.14 (Ne (op e4 e0) (op e4 e4))) % 8.95/9.14 (Ne (op e4 e1) (op e4 e2))) % 8.95/9.14 (Ne (op e4 e1) (op e4 e3))) % 8.95/9.14 (Ne (op e4 e1) (op e4 e4))) % 8.95/9.14 (Ne (op e4 e2) (op e4 e3))) % 8.95/9.14 (Ne (op e4 e2) (op e4 e4))) % 8.95/9.14 True % 8.95/9.14 Clause #107 (by clausification #[99]): Eq % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 8.95/9.14 (Eq (op unit e2) e2)) % 8.95/9.14 (Eq (op e2 unit) e2)) % 8.95/9.14 (Eq (op unit e3) e3)) % 8.95/9.14 (Eq (op e3 unit) e3)) % 8.95/9.14 True % 8.95/9.14 Clause #111 (by clausification #[107]): Eq % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 8.95/9.14 (Eq (op unit e2) e2)) % 8.95/9.14 (Eq (op e2 unit) e2)) % 8.95/9.14 (Eq (op unit e3) e3)) % 8.95/9.14 True % 8.95/9.14 Clause #114 (by clausification #[6]): Eq % 8.95/9.14 (Not % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (And % 8.95/9.14 (Or % 8.95/9.14 (Or % 8.95/9.14 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) % 8.95/9.14 (Eq (op e2 e2) e0)) % 8.95/9.14 (Eq (op e3 e3) e0)) % 8.95/9.14 (Eq (op e4 e4) e0)) % 8.95/9.14 (Or % 8.95/9.14 (Or % 8.95/9.14 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) % 8.95/9.14 (Eq (op e2 e2) e1)) % 8.95/9.14 (Eq (op e3 e3) e1)) % 8.95/9.14 (Eq (op e4 e4) e1))) % 8.95/9.14 (Or % 8.95/9.14 (Or % 8.95/9.14 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) % 8.95/9.14 (Eq (op e2 e2) e2)) % 8.95/9.14 (Eq (op e3 e3) e2)) % 8.95/9.14 (Eq (op e4 e4) e2))) % 8.95/9.14 (Or % 8.95/9.14 (Or % 8.95/9.14 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) % 8.95/9.14 (Eq (op e2 e2) e3)) % 8.95/9.14 (Eq (op e3 e3) e3)) % 8.95/9.14 (Eq (op e4 e4) e3))) % 8.95/9.14 (Or % 8.95/9.16 (Or % 8.95/9.16 (Or (Or (Eq (op e0 e0) e4) (Eq (op e1 e1) e4)) % 8.95/9.16 (Eq (op e2 e2) e4)) % 8.95/9.16 (Eq (op e3 e3) e4)) % 8.95/9.16 (Eq (op e4 e4) e4))) % 8.95/9.16 (Or (Ne (op e0 e0) e0) (Eq (op e0 e0) e0))) % 8.95/9.16 (Or (Ne (op e0 e0) e1) (Eq (op e0 e1) e0))) % 8.95/9.16 (Or (Ne (op e0 e0) e2) (Eq (op e0 e2) e0))) % 8.95/9.16 (Or (Ne (op e0 e0) e3) (Eq (op e0 e3) e0))) % 8.95/9.16 (Or (Ne (op e0 e0) e4) (Eq (op e0 e4) e0))) % 8.95/9.16 (Or (Ne (op e1 e1) e0) (Eq (op e1 e0) e1))) % 8.95/9.16 (Or (Ne (op e1 e1) e1) (Eq (op e1 e1) e1))) % 8.95/9.16 (Or (Ne (op e1 e1) e2) (Eq (op e1 e2) e1))) % 8.95/9.16 (Or (Ne (op e1 e1) e3) (Eq (op e1 e3) e1))) % 8.95/9.16 (Or (Ne (op e1 e1) e4) (Eq (op e1 e4) e1))) % 8.95/9.16 (Or (Ne (op e2 e2) e0) (Eq (op e2 e0) e2))) % 8.95/9.16 (Or (Ne (op e2 e2) e1) (Eq (op e2 e1) e2))) % 8.95/9.16 (Or (Ne (op e2 e2) e2) (Eq (op e2 e2) e2))) % 8.95/9.16 (Or (Ne (op e2 e2) e3) (Eq (op e2 e3) e2))) % 8.95/9.16 (Or (Ne (op e2 e2) e4) (Eq (op e2 e4) e2))) % 8.95/9.16 (Or (Ne (op e3 e3) e0) (Eq (op e3 e0) e3))) % 8.95/9.16 (Or (Ne (op e3 e3) e1) (Eq (op e3 e1) e3))) % 8.95/9.16 (Or (Ne (op e3 e3) e2) (Eq (op e3 e2) e3))) % 8.95/9.16 (Or (Ne (op e3 e3) e3) (Eq (op e3 e3) e3))) % 8.95/9.16 (Or (Ne (op e3 e3) e4) (Eq (op e3 e4) e3))) % 8.95/9.16 (Or (Ne (op e4 e4) e0) (Eq (op e4 e0) e4))) % 8.95/9.16 (Or (Ne (op e4 e4) e1) (Eq (op e4 e1) e4))) % 8.95/9.16 (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4))) % 8.95/9.16 (Or (Ne (op e4 e4) e3) (Eq (op e4 e3) e4))) % 8.95/9.16 (Or (Ne (op e4 e4) e4) (Eq (op e4 e4) e4)))) % 8.95/9.16 False % 8.95/9.16 Clause #115 (by clausification #[114]): Eq % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (And % 8.95/9.16 (Or % 8.95/9.16 (Or % 8.95/9.16 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) % 8.95/9.16 (Eq (op e2 e2) e0)) % 8.95/9.16 (Eq (op e3 e3) e0)) % 8.95/9.16 (Eq (op e4 e4) e0)) % 8.95/9.16 (Or % 8.95/9.16 (Or % 8.95/9.16 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) % 8.95/9.18 (Eq (op e2 e2) e1)) % 8.95/9.18 (Eq (op e3 e3) e1)) % 8.95/9.18 (Eq (op e4 e4) e1))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) % 8.95/9.18 (Eq (op e2 e2) e2)) % 8.95/9.18 (Eq (op e3 e3) e2)) % 8.95/9.18 (Eq (op e4 e4) e2))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) % 8.95/9.18 (Eq (op e2 e2) e3)) % 8.95/9.18 (Eq (op e3 e3) e3)) % 8.95/9.18 (Eq (op e4 e4) e3))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e4) (Eq (op e1 e1) e4)) % 8.95/9.18 (Eq (op e2 e2) e4)) % 8.95/9.18 (Eq (op e3 e3) e4)) % 8.95/9.18 (Eq (op e4 e4) e4))) % 8.95/9.18 (Or (Ne (op e0 e0) e0) (Eq (op e0 e0) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e1) (Eq (op e0 e1) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e2) (Eq (op e0 e2) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e3) (Eq (op e0 e3) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e4) (Eq (op e0 e4) e0))) % 8.95/9.18 (Or (Ne (op e1 e1) e0) (Eq (op e1 e0) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e1) (Eq (op e1 e1) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e2) (Eq (op e1 e2) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e3) (Eq (op e1 e3) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e4) (Eq (op e1 e4) e1))) % 8.95/9.18 (Or (Ne (op e2 e2) e0) (Eq (op e2 e0) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e1) (Eq (op e2 e1) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e2) (Eq (op e2 e2) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e3) (Eq (op e2 e3) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e4) (Eq (op e2 e4) e2))) % 8.95/9.18 (Or (Ne (op e3 e3) e0) (Eq (op e3 e0) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e1) (Eq (op e3 e1) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e2) (Eq (op e3 e2) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e3) (Eq (op e3 e3) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e4) (Eq (op e3 e4) e3))) % 8.95/9.18 (Or (Ne (op e4 e4) e0) (Eq (op e4 e0) e4))) % 8.95/9.18 (Or (Ne (op e4 e4) e1) (Eq (op e4 e1) e4))) % 8.95/9.18 (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4))) % 8.95/9.18 (Or (Ne (op e4 e4) e3) (Eq (op e4 e3) e4))) % 8.95/9.18 (Or (Ne (op e4 e4) e4) (Eq (op e4 e4) e4))) % 8.95/9.18 True % 8.95/9.18 Clause #117 (by clausification #[115]): Eq % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (And % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) % 8.95/9.18 (Eq (op e2 e2) e0)) % 8.95/9.18 (Eq (op e3 e3) e0)) % 8.95/9.18 (Eq (op e4 e4) e0)) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) % 8.95/9.18 (Eq (op e2 e2) e1)) % 8.95/9.18 (Eq (op e3 e3) e1)) % 8.95/9.18 (Eq (op e4 e4) e1))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) % 8.95/9.18 (Eq (op e2 e2) e2)) % 8.95/9.18 (Eq (op e3 e3) e2)) % 8.95/9.18 (Eq (op e4 e4) e2))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) % 8.95/9.18 (Eq (op e2 e2) e3)) % 8.95/9.18 (Eq (op e3 e3) e3)) % 8.95/9.18 (Eq (op e4 e4) e3))) % 8.95/9.18 (Or % 8.95/9.18 (Or % 8.95/9.18 (Or (Or (Eq (op e0 e0) e4) (Eq (op e1 e1) e4)) % 8.95/9.18 (Eq (op e2 e2) e4)) % 8.95/9.18 (Eq (op e3 e3) e4)) % 8.95/9.18 (Eq (op e4 e4) e4))) % 8.95/9.18 (Or (Ne (op e0 e0) e0) (Eq (op e0 e0) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e1) (Eq (op e0 e1) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e2) (Eq (op e0 e2) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e3) (Eq (op e0 e3) e0))) % 8.95/9.18 (Or (Ne (op e0 e0) e4) (Eq (op e0 e4) e0))) % 8.95/9.18 (Or (Ne (op e1 e1) e0) (Eq (op e1 e0) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e1) (Eq (op e1 e1) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e2) (Eq (op e1 e2) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e3) (Eq (op e1 e3) e1))) % 8.95/9.18 (Or (Ne (op e1 e1) e4) (Eq (op e1 e4) e1))) % 8.95/9.18 (Or (Ne (op e2 e2) e0) (Eq (op e2 e0) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e1) (Eq (op e2 e1) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e2) (Eq (op e2 e2) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e3) (Eq (op e2 e3) e2))) % 8.95/9.18 (Or (Ne (op e2 e2) e4) (Eq (op e2 e4) e2))) % 8.95/9.18 (Or (Ne (op e3 e3) e0) (Eq (op e3 e0) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e1) (Eq (op e3 e1) e3))) % 8.95/9.18 (Or (Ne (op e3 e3) e2) (Eq (op e3 e2) e3))) % 9.03/9.26 (Or (Ne (op e3 e3) e3) (Eq (op e3 e3) e3))) % 9.03/9.26 (Or (Ne (op e3 e3) e4) (Eq (op e3 e4) e3))) % 9.03/9.26 (Or (Ne (op e4 e4) e0) (Eq (op e4 e0) e4))) % 9.03/9.26 (Or (Ne (op e4 e4) e1) (Eq (op e4 e1) e4))) % 9.03/9.26 (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4))) % 9.03/9.26 (Or (Ne (op e4 e4) e3) (Eq (op e4 e3) e4))) % 9.03/9.26 True % 9.03/9.26 Clause #122 (by clausification #[111]): Eq % 9.03/9.26 (And % 9.03/9.26 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 9.03/9.26 (Eq (op unit e2) e2)) % 9.03/9.26 (Eq (op e2 unit) e2)) % 9.03/9.26 True % 9.03/9.26 Clause #125 (by clausification #[122]): Eq (Eq (op e2 unit) e2) True % 9.03/9.26 Clause #126 (by clausification #[122]): Eq % 9.03/9.26 (And (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) % 9.03/9.26 (Eq (op unit e2) e2)) % 9.03/9.26 True % 9.03/9.26 Clause #127 (by clausification #[125]): Eq (op e2 unit) e2 % 9.03/9.26 Clause #129 (by clausification #[126]): Eq (Eq (op unit e2) e2) True % 9.03/9.26 Clause #130 (by clausification #[126]): Eq (And (And (And (Eq (op unit e0) e0) (Eq (op e0 unit) e0)) (Eq (op unit e1) e1)) (Eq (op e1 unit) e1)) True % 9.03/9.26 Clause #131 (by clausification #[129]): Eq (op unit e2) e2 % 9.03/9.26 Clause #162 (by clausification #[130]): Eq (Eq (op e1 unit) e1) True % 9.03/9.26 Clause #164 (by clausification #[162]): Eq (op e1 unit) e1 % 9.03/9.26 Clause #175 (by clausification #[103]): Eq % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (And % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e0)) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e0) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e0))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e1) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e1))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e2) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e2))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e3) % 9.03/9.26 (op % 9.03/9.26 e4 % 9.03/9.26 e3))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e4) % 9.03/9.26 (op % 9.03/9.26 e1 % 9.03/9.26 e4))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e4) % 9.03/9.26 (op % 9.03/9.26 e2 % 9.03/9.26 e4))) % 9.03/9.26 (Ne % 9.03/9.26 (op % 9.03/9.26 e0 % 9.03/9.26 e4) % 9.03/9.26 (op % 9.03/9.26 e3 % 9.03/9.26 e4))) % 9.03/9.26 (Ne % 9.03/9.26 (op e0 % 9.03/9.26 e4) % 9.03/9.26 (op e4 % 9.03/9.26 e4))) % 9.03/9.26 (Ne % 9.03/9.26 (op e1 % 9.03/9.26 e4) % 9.03/9.26 (op e2 % 9.03/9.26 e4))) % 9.03/9.26 (Ne % 9.03/9.26 (op e1 e4) % 9.03/9.26 (op e3 % 9.03/9.26 e4))) % 9.03/9.26 (Ne (op e1 e4) % 9.03/9.26 (op e4 e4))) % 9.03/9.26 (Ne (op e2 e4) % 9.03/9.26 (op e3 e4))) % 9.03/9.26 (Ne (op e2 e4) % 9.03/9.26 (op e4 e4))) % 9.03/9.26 (Ne (op e3 e4) % 9.03/9.26 (op e4 e4))) % 9.03/9.26 (Ne (op e0 e0) % 9.03/9.26 (op e0 e1))) % 9.03/9.26 (Ne (op e0 e0) % 9.03/9.26 (op e0 e2))) % 9.03/9.26 (Ne (op e0 e0) % 9.03/9.26 (op e0 e3))) % 9.03/9.26 (Ne (op e0 e0) (op e0 e4))) % 9.03/9.26 (Ne (op e0 e1) (op e0 e2))) % 9.03/9.26 (Ne (op e0 e1) (op e0 e3))) % 9.03/9.26 (Ne (op e0 e1) (op e0 e4))) % 9.03/9.26 (Ne (op e0 e2) (op e0 e3))) % 9.03/9.26 (Ne (op e0 e2) (op e0 e4))) % 9.03/9.26 (Ne (op e0 e3) (op e0 e4))) % 9.03/9.26 (Ne (op e1 e0) (op e1 e1))) % 9.03/9.26 (Ne (op e1 e0) (op e1 e2))) % 9.03/9.26 (Ne (op e1 e0) (op e1 e3))) % 9.03/9.26 (Ne (op e1 e0) (op e1 e4))) % 9.03/9.26 (Ne (op e1 e1) (op e1 e2))) % 9.03/9.26 (Ne (op e1 e1) (op e1 e3))) % 9.03/9.26 (Ne (op e1 e1) (op e1 e4))) % 9.03/9.26 (Ne (op e1 e2) (op e1 e3))) % 9.03/9.26 (Ne (op e1 e2) (op e1 e4))) % 9.03/9.26 (Ne (op e1 e3) (op e1 e4))) % 9.03/9.26 (Ne (op e2 e0) (op e2 e1))) % 9.03/9.26 (Ne (op e2 e0) (op e2 e2))) % 9.03/9.26 (Ne (op e2 e0) (op e2 e3))) % 9.13/9.29 (Ne (op e2 e0) (op e2 e4))) % 9.13/9.29 (Ne (op e2 e1) (op e2 e2))) % 9.13/9.29 (Ne (op e2 e1) (op e2 e3))) % 9.13/9.29 (Ne (op e2 e1) (op e2 e4))) % 9.13/9.29 (Ne (op e2 e2) (op e2 e3))) % 9.13/9.29 (Ne (op e2 e2) (op e2 e4))) % 9.13/9.29 (Ne (op e2 e3) (op e2 e4))) % 9.13/9.29 (Ne (op e3 e0) (op e3 e1))) % 9.13/9.29 (Ne (op e3 e0) (op e3 e2))) % 9.13/9.29 (Ne (op e3 e0) (op e3 e3))) % 9.13/9.29 (Ne (op e3 e0) (op e3 e4))) % 9.13/9.29 (Ne (op e3 e1) (op e3 e2))) % 9.13/9.29 (Ne (op e3 e1) (op e3 e3))) % 9.13/9.29 (Ne (op e3 e1) (op e3 e4))) % 9.13/9.29 (Ne (op e3 e2) (op e3 e3))) % 9.13/9.29 (Ne (op e3 e2) (op e3 e4))) % 9.13/9.29 (Ne (op e3 e3) (op e3 e4))) % 9.13/9.29 (Ne (op e4 e0) (op e4 e1))) % 9.13/9.29 (Ne (op e4 e0) (op e4 e2))) % 9.13/9.29 (Ne (op e4 e0) (op e4 e3))) % 9.13/9.29 (Ne (op e4 e0) (op e4 e4))) % 9.13/9.29 (Ne (op e4 e1) (op e4 e2))) % 9.13/9.29 (Ne (op e4 e1) (op e4 e3))) % 9.13/9.29 (Ne (op e4 e1) (op e4 e4))) % 9.13/9.29 (Ne (op e4 e2) (op e4 e3))) % 9.13/9.29 True % 9.13/9.29 Clause #180 (by clausification #[117]): Eq % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (And % 9.13/9.29 (Or % 9.13/9.29 (Or % 9.13/9.29 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) % 9.13/9.29 (Eq (op e2 e2) e0)) % 9.13/9.29 (Eq (op e3 e3) e0)) % 9.13/9.29 (Eq (op e4 e4) e0)) % 9.13/9.29 (Or % 9.13/9.29 (Or % 9.13/9.29 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) % 9.13/9.29 (Eq (op e2 e2) e1)) % 9.13/9.29 (Eq (op e3 e3) e1)) % 9.13/9.29 (Eq (op e4 e4) e1))) % 9.13/9.29 (Or % 9.13/9.29 (Or % 9.13/9.29 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) % 9.13/9.29 (Eq (op e2 e2) e2)) % 9.13/9.29 (Eq (op e3 e3) e2)) % 9.13/9.29 (Eq (op e4 e4) e2))) % 9.13/9.29 (Or % 9.13/9.29 (Or % 9.13/9.29 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) % 9.13/9.29 (Eq (op e2 e2) e3)) % 9.15/9.33 (Eq (op e3 e3) e3)) % 9.15/9.33 (Eq (op e4 e4) e3))) % 9.15/9.33 (Or % 9.15/9.33 (Or % 9.15/9.33 (Or (Or (Eq (op e0 e0) e4) (Eq (op e1 e1) e4)) (Eq (op e2 e2) e4)) % 9.15/9.33 (Eq (op e3 e3) e4)) % 9.15/9.33 (Eq (op e4 e4) e4))) % 9.15/9.33 (Or (Ne (op e0 e0) e0) (Eq (op e0 e0) e0))) % 9.15/9.33 (Or (Ne (op e0 e0) e1) (Eq (op e0 e1) e0))) % 9.15/9.33 (Or (Ne (op e0 e0) e2) (Eq (op e0 e2) e0))) % 9.15/9.33 (Or (Ne (op e0 e0) e3) (Eq (op e0 e3) e0))) % 9.15/9.33 (Or (Ne (op e0 e0) e4) (Eq (op e0 e4) e0))) % 9.15/9.33 (Or (Ne (op e1 e1) e0) (Eq (op e1 e0) e1))) % 9.15/9.33 (Or (Ne (op e1 e1) e1) (Eq (op e1 e1) e1))) % 9.15/9.33 (Or (Ne (op e1 e1) e2) (Eq (op e1 e2) e1))) % 9.15/9.33 (Or (Ne (op e1 e1) e3) (Eq (op e1 e3) e1))) % 9.15/9.33 (Or (Ne (op e1 e1) e4) (Eq (op e1 e4) e1))) % 9.15/9.33 (Or (Ne (op e2 e2) e0) (Eq (op e2 e0) e2))) % 9.15/9.33 (Or (Ne (op e2 e2) e1) (Eq (op e2 e1) e2))) % 9.15/9.33 (Or (Ne (op e2 e2) e2) (Eq (op e2 e2) e2))) % 9.15/9.33 (Or (Ne (op e2 e2) e3) (Eq (op e2 e3) e2))) % 9.15/9.33 (Or (Ne (op e2 e2) e4) (Eq (op e2 e4) e2))) % 9.15/9.33 (Or (Ne (op e3 e3) e0) (Eq (op e3 e0) e3))) % 9.15/9.33 (Or (Ne (op e3 e3) e1) (Eq (op e3 e1) e3))) % 9.15/9.33 (Or (Ne (op e3 e3) e2) (Eq (op e3 e2) e3))) % 9.15/9.33 (Or (Ne (op e3 e3) e3) (Eq (op e3 e3) e3))) % 9.15/9.33 (Or (Ne (op e3 e3) e4) (Eq (op e3 e4) e3))) % 9.15/9.33 (Or (Ne (op e4 e4) e0) (Eq (op e4 e0) e4))) % 9.15/9.33 (Or (Ne (op e4 e4) e1) (Eq (op e4 e1) e4))) % 9.15/9.33 (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4))) % 9.15/9.33 True % 9.15/9.33 Clause #185 (by clausification #[180]): Eq (Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4)) True % 9.15/9.33 Clause #187 (by clausification #[185]): Or (Eq (Ne (op e4 e4) e2) True) (Eq (Eq (op e4 e2) e4) True) % 9.15/9.33 Clause #188 (by clausification #[187]): Or (Eq (Eq (op e4 e2) e4) True) (Ne (op e4 e4) e2) % 9.15/9.33 Clause #189 (by clausification #[188]): Or (Ne (op e4 e4) e2) (Eq (op e4 e2) e4) % 9.15/9.33 Clause #190 (by forward demodulation #[189, 21]): Or (Ne e2 e2) (Eq (op e4 e2) e4) % 9.15/9.33 Clause #191 (by eliminate resolved literals #[190]): Eq (op e4 e2) e4 % 9.15/9.33 Clause #253 (by clausification #[175]): Eq (Ne (op e4 e2) (op e4 e3)) True % 9.15/9.33 Clause #254 (by clausification #[175]): Eq % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (And % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e0)) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e0) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e0))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e1) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e1))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e2) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e2))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e3 % 9.15/9.33 e3) % 9.15/9.33 (op % 9.15/9.33 e4 % 9.15/9.33 e3))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e4) % 9.15/9.33 (op % 9.15/9.33 e1 % 9.15/9.33 e4))) % 9.15/9.33 (Ne % 9.15/9.33 (op % 9.15/9.33 e0 % 9.15/9.33 e4) % 9.15/9.33 (op % 9.15/9.33 e2 % 9.15/9.33 e4))) % 9.15/9.33 (Ne % 9.15/9.33 (op e0 % 9.15/9.33 e4) % 9.15/9.33 (op e3 % 9.15/9.33 e4))) % 9.15/9.33 (Ne % 9.15/9.33 (op e0 % 9.15/9.33 e4) % 9.15/9.33 (op e4 % 9.15/9.33 e4))) % 9.15/9.33 (Ne % 9.15/9.33 (op e1 e4) % 9.15/9.33 (op e2 % 9.15/9.33 e4))) % 9.15/9.33 (Ne (op e1 e4) % 9.15/9.33 (op e3 e4))) % 9.15/9.33 (Ne (op e1 e4) % 9.15/9.33 (op e4 e4))) % 9.15/9.33 (Ne (op e2 e4) % 9.15/9.33 (op e3 e4))) % 9.15/9.33 (Ne (op e2 e4) % 9.15/9.33 (op e4 e4))) % 9.15/9.33 (Ne (op e3 e4) % 9.15/9.33 (op e4 e4))) % 9.15/9.33 (Ne (op e0 e0) % 9.15/9.33 (op e0 e1))) % 9.15/9.33 (Ne (op e0 e0) % 9.15/9.33 (op e0 e2))) % 9.15/9.33 (Ne (op e0 e0) (op e0 e3))) % 9.15/9.33 (Ne (op e0 e0) (op e0 e4))) % 9.15/9.33 (Ne (op e0 e1) (op e0 e2))) % 9.15/9.33 (Ne (op e0 e1) (op e0 e3))) % 9.15/9.33 (Ne (op e0 e1) (op e0 e4))) % 9.15/9.33 (Ne (op e0 e2) (op e0 e3))) % 9.15/9.33 (Ne (op e0 e2) (op e0 e4))) % 9.15/9.33 (Ne (op e0 e3) (op e0 e4))) % 9.15/9.33 (Ne (op e1 e0) (op e1 e1))) % 9.15/9.33 (Ne (op e1 e0) (op e1 e2))) % 9.15/9.33 (Ne (op e1 e0) (op e1 e3))) % 9.15/9.33 (Ne (op e1 e0) (op e1 e4))) % 9.15/9.33 (Ne (op e1 e1) (op e1 e2))) % 9.15/9.33 (Ne (op e1 e1) (op e1 e3))) % 9.15/9.33 (Ne (op e1 e1) (op e1 e4))) % 9.15/9.33 (Ne (op e1 e2) (op e1 e3))) % 9.15/9.33 (Ne (op e1 e2) (op e1 e4))) % 9.15/9.33 (Ne (op e1 e3) (op e1 e4))) % 9.15/9.33 (Ne (op e2 e0) (op e2 e1))) % 9.15/9.33 (Ne (op e2 e0) (op e2 e2))) % 9.15/9.33 (Ne (op e2 e0) (op e2 e3))) % 9.15/9.33 (Ne (op e2 e0) (op e2 e4))) % 9.15/9.39 (Ne (op e2 e1) (op e2 e2))) % 9.15/9.39 (Ne (op e2 e1) (op e2 e3))) % 9.15/9.39 (Ne (op e2 e1) (op e2 e4))) % 9.15/9.39 (Ne (op e2 e2) (op e2 e3))) % 9.15/9.39 (Ne (op e2 e2) (op e2 e4))) % 9.15/9.39 (Ne (op e2 e3) (op e2 e4))) % 9.15/9.39 (Ne (op e3 e0) (op e3 e1))) % 9.15/9.39 (Ne (op e3 e0) (op e3 e2))) % 9.15/9.39 (Ne (op e3 e0) (op e3 e3))) % 9.15/9.39 (Ne (op e3 e0) (op e3 e4))) % 9.15/9.39 (Ne (op e3 e1) (op e3 e2))) % 9.15/9.39 (Ne (op e3 e1) (op e3 e3))) % 9.15/9.39 (Ne (op e3 e1) (op e3 e4))) % 9.15/9.39 (Ne (op e3 e2) (op e3 e3))) % 9.15/9.39 (Ne (op e3 e2) (op e3 e4))) % 9.15/9.39 (Ne (op e3 e3) (op e3 e4))) % 9.15/9.39 (Ne (op e4 e0) (op e4 e1))) % 9.15/9.39 (Ne (op e4 e0) (op e4 e2))) % 9.15/9.39 (Ne (op e4 e0) (op e4 e3))) % 9.15/9.39 (Ne (op e4 e0) (op e4 e4))) % 9.15/9.39 (Ne (op e4 e1) (op e4 e2))) % 9.15/9.39 (Ne (op e4 e1) (op e4 e3))) % 9.15/9.39 (Ne (op e4 e1) (op e4 e4))) % 9.15/9.39 True % 9.15/9.39 Clause #255 (by clausification #[253]): Ne (op e4 e2) (op e4 e3) % 9.15/9.39 Clause #256 (by forward demodulation #[255, 191]): Ne e4 (op e4 e3) % 9.15/9.39 Clause #313 (by clausification #[254]): Eq % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (And % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e0)) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e0) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e0))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e1) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e1))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e2) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e2))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e2 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e3 % 9.15/9.39 e3) % 9.15/9.39 (op % 9.15/9.39 e4 % 9.15/9.39 e3))) % 9.15/9.39 (Ne % 9.15/9.39 (op % 9.15/9.39 e0 % 9.15/9.39 e4) % 9.15/9.39 (op % 9.15/9.39 e1 % 9.15/9.39 e4))) % 9.15/9.39 (Ne % 9.15/9.39 (op e0 % 9.15/9.39 e4) % 9.15/9.39 (op e2 % 9.15/9.39 e4))) % 9.15/9.39 (Ne % 9.15/9.39 (op e0 % 9.15/9.39 e4) % 9.15/9.39 (op e3 % 9.15/9.39 e4))) % 9.15/9.39 (Ne % 9.15/9.39 (op e0 e4) % 9.15/9.39 (op e4 % 9.15/9.39 e4))) % 9.15/9.39 (Ne (op e1 e4) % 9.15/9.39 (op e2 e4))) % 9.15/9.39 (Ne (op e1 e4) % 9.15/9.39 (op e3 e4))) % 9.15/9.39 (Ne (op e1 e4) % 9.15/9.39 (op e4 e4))) % 9.15/9.39 (Ne (op e2 e4) % 9.15/9.39 (op e3 e4))) % 9.15/9.39 (Ne (op e2 e4) % 9.15/9.39 (op e4 e4))) % 9.15/9.39 (Ne (op e3 e4) % 9.15/9.39 (op e4 e4))) % 9.15/9.39 (Ne (op e0 e0) % 9.15/9.39 (op e0 e1))) % 9.15/9.39 (Ne (op e0 e0) (op e0 e2))) % 9.15/9.39 (Ne (op e0 e0) (op e0 e3))) % 9.15/9.39 (Ne (op e0 e0) (op e0 e4))) % 9.15/9.39 (Ne (op e0 e1) (op e0 e2))) % 9.15/9.39 (Ne (op e0 e1) (op e0 e3))) % 9.15/9.39 (Ne (op e0 e1) (op e0 e4))) % 9.15/9.39 (Ne (op e0 e2) (op e0 e3))) % 9.15/9.39 (Ne (op e0 e2) (op e0 e4))) % 9.15/9.39 (Ne (op e0 e3) (op e0 e4))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e1))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e2))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e3))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e4))) % 9.25/9.43 (Ne (op e1 e1) (op e1 e2))) % 9.25/9.43 (Ne (op e1 e1) (op e1 e3))) % 9.25/9.43 (Ne (op e1 e1) (op e1 e4))) % 9.25/9.43 (Ne (op e1 e2) (op e1 e3))) % 9.25/9.43 (Ne (op e1 e2) (op e1 e4))) % 9.25/9.43 (Ne (op e1 e3) (op e1 e4))) % 9.25/9.43 (Ne (op e2 e0) (op e2 e1))) % 9.25/9.43 (Ne (op e2 e0) (op e2 e2))) % 9.25/9.43 (Ne (op e2 e0) (op e2 e3))) % 9.25/9.43 (Ne (op e2 e0) (op e2 e4))) % 9.25/9.43 (Ne (op e2 e1) (op e2 e2))) % 9.25/9.43 (Ne (op e2 e1) (op e2 e3))) % 9.25/9.43 (Ne (op e2 e1) (op e2 e4))) % 9.25/9.43 (Ne (op e2 e2) (op e2 e3))) % 9.25/9.43 (Ne (op e2 e2) (op e2 e4))) % 9.25/9.43 (Ne (op e2 e3) (op e2 e4))) % 9.25/9.43 (Ne (op e3 e0) (op e3 e1))) % 9.25/9.43 (Ne (op e3 e0) (op e3 e2))) % 9.25/9.43 (Ne (op e3 e0) (op e3 e3))) % 9.25/9.43 (Ne (op e3 e0) (op e3 e4))) % 9.25/9.43 (Ne (op e3 e1) (op e3 e2))) % 9.25/9.43 (Ne (op e3 e1) (op e3 e3))) % 9.25/9.43 (Ne (op e3 e1) (op e3 e4))) % 9.25/9.43 (Ne (op e3 e2) (op e3 e3))) % 9.25/9.43 (Ne (op e3 e2) (op e3 e4))) % 9.25/9.43 (Ne (op e3 e3) (op e3 e4))) % 9.25/9.43 (Ne (op e4 e0) (op e4 e1))) % 9.25/9.43 (Ne (op e4 e0) (op e4 e2))) % 9.25/9.43 (Ne (op e4 e0) (op e4 e3))) % 9.25/9.43 (Ne (op e4 e0) (op e4 e4))) % 9.25/9.43 (Ne (op e4 e1) (op e4 e2))) % 9.25/9.43 (Ne (op e4 e1) (op e4 e3))) % 9.25/9.43 True % 9.25/9.43 Clause #375 (by clausification #[313]): Eq % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (And % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e0)) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e0) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e0))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e1) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e1))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e2) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e2))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e0 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e1 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e2 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op % 9.25/9.43 e3 % 9.25/9.43 e3) % 9.25/9.43 (op % 9.25/9.43 e4 % 9.25/9.43 e3))) % 9.25/9.43 (Ne % 9.25/9.43 (op e0 % 9.25/9.43 e4) % 9.25/9.43 (op e1 % 9.25/9.43 e4))) % 9.25/9.43 (Ne % 9.25/9.43 (op e0 % 9.25/9.43 e4) % 9.25/9.43 (op e2 % 9.25/9.43 e4))) % 9.25/9.43 (Ne % 9.25/9.43 (op e0 e4) % 9.25/9.43 (op e3 % 9.25/9.43 e4))) % 9.25/9.43 (Ne (op e0 e4) % 9.25/9.43 (op e4 e4))) % 9.25/9.43 (Ne (op e1 e4) % 9.25/9.43 (op e2 e4))) % 9.25/9.43 (Ne (op e1 e4) % 9.25/9.43 (op e3 e4))) % 9.25/9.43 (Ne (op e1 e4) % 9.25/9.43 (op e4 e4))) % 9.25/9.43 (Ne (op e2 e4) % 9.25/9.43 (op e3 e4))) % 9.25/9.43 (Ne (op e2 e4) % 9.25/9.43 (op e4 e4))) % 9.25/9.43 (Ne (op e3 e4) % 9.25/9.43 (op e4 e4))) % 9.25/9.43 (Ne (op e0 e0) (op e0 e1))) % 9.25/9.43 (Ne (op e0 e0) (op e0 e2))) % 9.25/9.43 (Ne (op e0 e0) (op e0 e3))) % 9.25/9.43 (Ne (op e0 e0) (op e0 e4))) % 9.25/9.43 (Ne (op e0 e1) (op e0 e2))) % 9.25/9.43 (Ne (op e0 e1) (op e0 e3))) % 9.25/9.43 (Ne (op e0 e1) (op e0 e4))) % 9.25/9.43 (Ne (op e0 e2) (op e0 e3))) % 9.25/9.43 (Ne (op e0 e2) (op e0 e4))) % 9.25/9.43 (Ne (op e0 e3) (op e0 e4))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e1))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e2))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e3))) % 9.25/9.43 (Ne (op e1 e0) (op e1 e4))) % 9.25/9.43 (Ne (op e1 e1) (op e1 e2))) % 9.25/9.47 (Ne (op e1 e1) (op e1 e3))) % 9.25/9.47 (Ne (op e1 e1) (op e1 e4))) % 9.25/9.47 (Ne (op e1 e2) (op e1 e3))) % 9.25/9.47 (Ne (op e1 e2) (op e1 e4))) % 9.25/9.47 (Ne (op e1 e3) (op e1 e4))) % 9.25/9.47 (Ne (op e2 e0) (op e2 e1))) % 9.25/9.47 (Ne (op e2 e0) (op e2 e2))) % 9.25/9.47 (Ne (op e2 e0) (op e2 e3))) % 9.25/9.47 (Ne (op e2 e0) (op e2 e4))) % 9.25/9.47 (Ne (op e2 e1) (op e2 e2))) % 9.25/9.47 (Ne (op e2 e1) (op e2 e3))) % 9.25/9.47 (Ne (op e2 e1) (op e2 e4))) % 9.25/9.47 (Ne (op e2 e2) (op e2 e3))) % 9.25/9.47 (Ne (op e2 e2) (op e2 e4))) % 9.25/9.47 (Ne (op e2 e3) (op e2 e4))) % 9.25/9.47 (Ne (op e3 e0) (op e3 e1))) % 9.25/9.47 (Ne (op e3 e0) (op e3 e2))) % 9.25/9.47 (Ne (op e3 e0) (op e3 e3))) % 9.25/9.47 (Ne (op e3 e0) (op e3 e4))) % 9.25/9.47 (Ne (op e3 e1) (op e3 e2))) % 9.25/9.47 (Ne (op e3 e1) (op e3 e3))) % 9.25/9.47 (Ne (op e3 e1) (op e3 e4))) % 9.25/9.47 (Ne (op e3 e2) (op e3 e3))) % 9.25/9.47 (Ne (op e3 e2) (op e3 e4))) % 9.25/9.47 (Ne (op e3 e3) (op e3 e4))) % 9.25/9.47 (Ne (op e4 e0) (op e4 e1))) % 9.25/9.47 (Ne (op e4 e0) (op e4 e2))) % 9.25/9.47 (Ne (op e4 e0) (op e4 e3))) % 9.25/9.47 (Ne (op e4 e0) (op e4 e4))) % 9.25/9.47 (Ne (op e4 e1) (op e4 e2))) % 9.25/9.47 True % 9.25/9.47 Clause #429 (by clausification #[375]): Eq % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (And % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e0)) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e0) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e0))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e1) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e1))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e2) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e2))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e0 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e1 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e3 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op % 9.25/9.47 e2 % 9.25/9.47 e3) % 9.25/9.47 (op % 9.25/9.47 e4 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op e3 % 9.25/9.47 e3) % 9.25/9.47 (op e4 % 9.25/9.47 e3))) % 9.25/9.47 (Ne % 9.25/9.47 (op e0 % 9.25/9.47 e4) % 9.25/9.47 (op e1 % 9.25/9.47 e4))) % 9.25/9.47 (Ne % 9.25/9.47 (op e0 e4) % 9.25/9.47 (op e2 % 9.25/9.47 e4))) % 9.25/9.47 (Ne (op e0 e4) % 9.25/9.47 (op e3 e4))) % 9.25/9.47 (Ne (op e0 e4) % 9.25/9.47 (op e4 e4))) % 9.25/9.47 (Ne (op e1 e4) % 9.25/9.47 (op e2 e4))) % 9.25/9.47 (Ne (op e1 e4) % 9.25/9.47 (op e3 e4))) % 9.25/9.47 (Ne (op e1 e4) % 9.25/9.47 (op e4 e4))) % 9.33/9.50 (Ne (op e2 e4) % 9.33/9.50 (op e3 e4))) % 9.33/9.50 (Ne (op e2 e4) % 9.33/9.50 (op e4 e4))) % 9.33/9.50 (Ne (op e3 e4) (op e4 e4))) % 9.33/9.50 (Ne (op e0 e0) (op e0 e1))) % 9.33/9.50 (Ne (op e0 e0) (op e0 e2))) % 9.33/9.50 (Ne (op e0 e0) (op e0 e3))) % 9.33/9.50 (Ne (op e0 e0) (op e0 e4))) % 9.33/9.50 (Ne (op e0 e1) (op e0 e2))) % 9.33/9.50 (Ne (op e0 e1) (op e0 e3))) % 9.33/9.50 (Ne (op e0 e1) (op e0 e4))) % 9.33/9.50 (Ne (op e0 e2) (op e0 e3))) % 9.33/9.50 (Ne (op e0 e2) (op e0 e4))) % 9.33/9.50 (Ne (op e0 e3) (op e0 e4))) % 9.33/9.50 (Ne (op e1 e0) (op e1 e1))) % 9.33/9.50 (Ne (op e1 e0) (op e1 e2))) % 9.33/9.50 (Ne (op e1 e0) (op e1 e3))) % 9.33/9.50 (Ne (op e1 e0) (op e1 e4))) % 9.33/9.50 (Ne (op e1 e1) (op e1 e2))) % 9.33/9.50 (Ne (op e1 e1) (op e1 e3))) % 9.33/9.50 (Ne (op e1 e1) (op e1 e4))) % 9.33/9.50 (Ne (op e1 e2) (op e1 e3))) % 9.33/9.50 (Ne (op e1 e2) (op e1 e4))) % 9.33/9.50 (Ne (op e1 e3) (op e1 e4))) % 9.33/9.50 (Ne (op e2 e0) (op e2 e1))) % 9.33/9.50 (Ne (op e2 e0) (op e2 e2))) % 9.33/9.50 (Ne (op e2 e0) (op e2 e3))) % 9.33/9.50 (Ne (op e2 e0) (op e2 e4))) % 9.33/9.50 (Ne (op e2 e1) (op e2 e2))) % 9.33/9.50 (Ne (op e2 e1) (op e2 e3))) % 9.33/9.50 (Ne (op e2 e1) (op e2 e4))) % 9.33/9.50 (Ne (op e2 e2) (op e2 e3))) % 9.33/9.50 (Ne (op e2 e2) (op e2 e4))) % 9.33/9.50 (Ne (op e2 e3) (op e2 e4))) % 9.33/9.50 (Ne (op e3 e0) (op e3 e1))) % 9.33/9.50 (Ne (op e3 e0) (op e3 e2))) % 9.33/9.50 (Ne (op e3 e0) (op e3 e3))) % 9.33/9.50 (Ne (op e3 e0) (op e3 e4))) % 9.33/9.50 (Ne (op e3 e1) (op e3 e2))) % 9.33/9.50 (Ne (op e3 e1) (op e3 e3))) % 9.33/9.50 (Ne (op e3 e1) (op e3 e4))) % 9.33/9.50 (Ne (op e3 e2) (op e3 e3))) % 9.33/9.50 (Ne (op e3 e2) (op e3 e4))) % 9.33/9.50 (Ne (op e3 e3) (op e3 e4))) % 9.33/9.50 (Ne (op e4 e0) (op e4 e1))) % 9.33/9.50 (Ne (op e4 e0) (op e4 e2))) % 9.33/9.50 (Ne (op e4 e0) (op e4 e3))) % 9.33/9.50 (Ne (op e4 e0) (op e4 e4))) % 9.33/9.50 True % 9.33/9.50 Clause #499 (by clausification #[429]): Eq % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (And % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e1 % 9.33/9.50 e0)) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e2 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e3 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e4 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e1 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e2 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e1 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e3 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e1 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e4 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e2 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e3 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e2 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e4 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e3 % 9.33/9.50 e0) % 9.33/9.50 (op % 9.33/9.50 e4 % 9.33/9.50 e0))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.50 e1) % 9.33/9.50 (op % 9.33/9.50 e1 % 9.33/9.50 e1))) % 9.33/9.50 (Ne % 9.33/9.50 (op % 9.33/9.50 e0 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e1) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e1))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e2) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e2))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e0 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e1 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e4 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op % 9.33/9.51 e2 % 9.33/9.51 e3) % 9.33/9.51 (op % 9.33/9.51 e3 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op e2 % 9.33/9.51 e3) % 9.33/9.51 (op e4 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op e3 % 9.33/9.51 e3) % 9.33/9.51 (op e4 % 9.33/9.51 e3))) % 9.33/9.51 (Ne % 9.33/9.51 (op e0 e4) % 9.33/9.51 (op e1 % 9.33/9.51 e4))) % 9.33/9.51 (Ne (op e0 e4) % 9.33/9.51 (op e2 e4))) % 9.33/9.51 (Ne (op e0 e4) % 9.33/9.51 (op e3 e4))) % 9.33/9.51 (Ne (op e0 e4) % 9.33/9.51 (op e4 e4))) % 9.33/9.51 (Ne (op e1 e4) % 9.33/9.51 (op e2 e4))) % 9.33/9.51 (Ne (op e1 e4) % 9.33/9.51 (op e3 e4))) % 9.33/9.51 (Ne (op e1 e4) % 9.33/9.51 (op e4 e4))) % 9.33/9.51 (Ne (op e2 e4) % 9.33/9.51 (op e3 e4))) % 9.33/9.51 (Ne (op e2 e4) (op e4 e4))) % 9.33/9.51 (Ne (op e3 e4) (op e4 e4))) % 9.33/9.51 (Ne (op e0 e0) (op e0 e1))) % 9.33/9.51 (Ne (op e0 e0) (op e0 e2))) % 9.33/9.51 (Ne (op e0 e0) (op e0 e3))) % 9.33/9.51 (Ne (op e0 e0) (op e0 e4))) % 9.33/9.51 (Ne (op e0 e1) (op e0 e2))) % 9.33/9.51 (Ne (op e0 e1) (op e0 e3))) % 9.33/9.51 (Ne (op e0 e1) (op e0 e4))) % 9.33/9.51 (Ne (op e0 e2) (op e0 e3))) % 9.33/9.51 (Ne (op e0 e2) (op e0 e4))) % 9.33/9.51 (Ne (op e0 e3) (op e0 e4))) % 9.33/9.51 (Ne (op e1 e0) (op e1 e1))) % 9.33/9.51 (Ne (op e1 e0) (op e1 e2))) % 9.33/9.51 (Ne (op e1 e0) (op e1 e3))) % 9.33/9.51 (Ne (op e1 e0) (op e1 e4))) % 9.33/9.51 (Ne (op e1 e1) (op e1 e2))) % 9.33/9.51 (Ne (op e1 e1) (op e1 e3))) % 9.33/9.51 (Ne (op e1 e1) (op e1 e4))) % 9.33/9.51 (Ne (op e1 e2) (op e1 e3))) % 9.33/9.51 (Ne (op e1 e2) (op e1 e4))) % 9.33/9.51 (Ne (op e1 e3) (op e1 e4))) % 9.33/9.51 (Ne (op e2 e0) (op e2 e1))) % 9.33/9.51 (Ne (op e2 e0) (op e2 e2))) % 9.33/9.51 (Ne (op e2 e0) (op e2 e3))) % 9.33/9.51 (Ne (op e2 e0) (op e2 e4))) % 9.33/9.51 (Ne (op e2 e1) (op e2 e2))) % 9.33/9.51 (Ne (op e2 e1) (op e2 e3))) % 9.33/9.51 (Ne (op e2 e1) (op e2 e4))) % 9.33/9.51 (Ne (op e2 e2) (op e2 e3))) % 9.33/9.51 (Ne (op e2 e2) (op e2 e4))) % 9.33/9.51 (Ne (op e2 e3) (op e2 e4))) % 9.33/9.51 (Ne (op e3 e0) (op e3 e1))) % 9.33/9.51 (Ne (op e3 e0) (op e3 e2))) % 9.33/9.51 (Ne (op e3 e0) (op e3 e3))) % 9.33/9.51 (Ne (op e3 e0) (op e3 e4))) % 9.33/9.51 (Ne (op e3 e1) (op e3 e2))) % 9.33/9.51 (Ne (op e3 e1) (op e3 e3))) % 9.33/9.51 (Ne (op e3 e1) (op e3 e4))) % 9.33/9.51 (Ne (op e3 e2) (op e3 e3))) % 9.33/9.51 (Ne (op e3 e2) (op e3 e4))) % 9.33/9.54 (Ne (op e3 e3) (op e3 e4))) % 9.33/9.54 (Ne (op e4 e0) (op e4 e1))) % 9.33/9.54 (Ne (op e4 e0) (op e4 e2))) % 9.33/9.54 (Ne (op e4 e0) (op e4 e3))) % 9.33/9.54 True % 9.33/9.54 Clause #562 (by clausification #[499]): Eq % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (And % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e0)) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e0) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e0))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e1) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e1))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e2) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e2))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e0 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e2 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e3 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op % 9.33/9.54 e1 % 9.33/9.54 e3) % 9.33/9.54 (op % 9.33/9.54 e4 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op e2 % 9.33/9.54 e3) % 9.33/9.54 (op e3 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op e2 % 9.33/9.54 e3) % 9.33/9.54 (op e4 % 9.33/9.54 e3))) % 9.33/9.54 (Ne % 9.33/9.54 (op e3 e3) % 9.33/9.54 (op e4 % 9.33/9.54 e3))) % 9.33/9.54 (Ne (op e0 e4) % 9.33/9.54 (op e1 e4))) % 9.33/9.54 (Ne (op e0 e4) % 9.33/9.54 (op e2 e4))) % 9.33/9.54 (Ne (op e0 e4) % 9.33/9.54 (op e3 e4))) % 9.33/9.54 (Ne (op e0 e4) % 9.33/9.54 (op e4 e4))) % 9.33/9.54 (Ne (op e1 e4) % 9.33/9.54 (op e2 e4))) % 9.33/9.54 (Ne (op e1 e4) % 9.33/9.54 (op e3 e4))) % 9.33/9.54 (Ne (op e1 e4) % 9.33/9.54 (op e4 e4))) % 9.33/9.54 (Ne (op e2 e4) (op e3 e4))) % 9.33/9.54 (Ne (op e2 e4) (op e4 e4))) % 9.33/9.54 (Ne (op e3 e4) (op e4 e4))) % 9.33/9.55 (Ne (op e0 e0) (op e0 e1))) % 9.33/9.55 (Ne (op e0 e0) (op e0 e2))) % 9.33/9.55 (Ne (op e0 e0) (op e0 e3))) % 9.33/9.55 (Ne (op e0 e0) (op e0 e4))) % 9.33/9.55 (Ne (op e0 e1) (op e0 e2))) % 9.33/9.55 (Ne (op e0 e1) (op e0 e3))) % 9.33/9.55 (Ne (op e0 e1) (op e0 e4))) % 9.33/9.55 (Ne (op e0 e2) (op e0 e3))) % 9.33/9.55 (Ne (op e0 e2) (op e0 e4))) % 9.33/9.55 (Ne (op e0 e3) (op e0 e4))) % 9.33/9.55 (Ne (op e1 e0) (op e1 e1))) % 9.33/9.55 (Ne (op e1 e0) (op e1 e2))) % 9.33/9.55 (Ne (op e1 e0) (op e1 e3))) % 9.33/9.55 (Ne (op e1 e0) (op e1 e4))) % 9.33/9.55 (Ne (op e1 e1) (op e1 e2))) % 9.33/9.55 (Ne (op e1 e1) (op e1 e3))) % 9.33/9.55 (Ne (op e1 e1) (op e1 e4))) % 9.33/9.55 (Ne (op e1 e2) (op e1 e3))) % 9.33/9.55 (Ne (op e1 e2) (op e1 e4))) % 9.33/9.55 (Ne (op e1 e3) (op e1 e4))) % 9.33/9.55 (Ne (op e2 e0) (op e2 e1))) % 9.33/9.55 (Ne (op e2 e0) (op e2 e2))) % 9.33/9.55 (Ne (op e2 e0) (op e2 e3))) % 9.33/9.55 (Ne (op e2 e0) (op e2 e4))) % 9.33/9.55 (Ne (op e2 e1) (op e2 e2))) % 9.33/9.55 (Ne (op e2 e1) (op e2 e3))) % 9.33/9.55 (Ne (op e2 e1) (op e2 e4))) % 9.33/9.55 (Ne (op e2 e2) (op e2 e3))) % 9.33/9.55 (Ne (op e2 e2) (op e2 e4))) % 9.33/9.55 (Ne (op e2 e3) (op e2 e4))) % 9.33/9.55 (Ne (op e3 e0) (op e3 e1))) % 9.33/9.55 (Ne (op e3 e0) (op e3 e2))) % 9.33/9.55 (Ne (op e3 e0) (op e3 e3))) % 9.33/9.55 (Ne (op e3 e0) (op e3 e4))) % 9.33/9.55 (Ne (op e3 e1) (op e3 e2))) % 9.33/9.55 (Ne (op e3 e1) (op e3 e3))) % 9.33/9.55 (Ne (op e3 e1) (op e3 e4))) % 9.33/9.55 (Ne (op e3 e2) (op e3 e3))) % 9.33/9.55 (Ne (op e3 e2) (op e3 e4))) % 9.33/9.55 (Ne (op e3 e3) (op e3 e4))) % 9.33/9.55 (Ne (op e4 e0) (op e4 e1))) % 9.33/9.55 (Ne (op e4 e0) (op e4 e2))) % 9.33/9.55 True % 9.33/9.55 Clause #629 (by clausification #[562]): Eq (Ne (op e4 e0) (op e4 e2)) True % 9.33/9.55 Clause #631 (by clausification #[629]): Ne (op e4 e0) (op e4 e2) % 9.33/9.55 Clause #632 (by forward demodulation #[631, 191]): Ne (op e4 e0) e4 % 9.33/9.55 Clause #633 (by backward contextual literal cutting #[632, 101]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq unit e2) (Eq unit e1))) % 9.33/9.55 Clause #643 (by superposition #[633, 127]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq unit e1) (Eq (op e2 e2) e2))) % 9.33/9.55 Clause #651 (by superposition #[643, 23]): Or (Eq unit e4) (Or (Eq unit e3) (Or (Eq unit e1) (Eq e3 e2))) % 9.33/9.55 Clause #668 (by forward contextual literal cutting #[651, 50]): Or (Eq unit e4) (Or (Eq unit e3) (Eq unit e1)) % 9.33/9.55 Clause #673 (by superposition #[668, 131]): Or (Eq unit e3) (Or (Eq unit e1) (Eq (op e4 e2) e2)) % 9.33/9.55 Clause #692 (by superposition #[673, 191]): Or (Eq unit e3) (Or (Eq unit e1) (Eq e2 e4)) % 9.33/9.55 Clause #693 (by forward contextual literal cutting #[692, 47]): Or (Eq unit e3) (Eq unit e1) % 9.33/9.55 Clause #694 (by superposition #[693, 100]): Or (Eq unit e1) (Eq (op e4 e3) e4) % 9.33/9.55 Clause #705 (by forward contextual literal cutting #[694, 256]): Eq unit e1 % 9.33/9.55 Clause #712 (by backward demodulation #[705, 164]): Eq (op e1 e1) e1 % 9.33/9.55 Clause #737 (by superposition #[712, 9]): Eq e4 e1 % 9.33/9.55 Clause #738 (by forward contextual literal cutting #[737, 53]): False % 9.33/9.55 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------