%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG138+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:44:02 PM UTC 2025 % Result : Unsatisfiable 10.73s 10.95s % Output : Proof 11.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : ALG138+1 : TPTP v9.2.0. Released v2.7.0. % 0.08/0.15 % Command : duper %s % 0.15/0.36 % Computer : n016.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Fri Oct 3 09:41:53 EDT 2025 % 0.15/0.36 % CPUTime : % 10.73/10.95 SZS status Theorem for theBenchmark.p % 10.73/10.95 SZS output start Proof for theBenchmark.p % 10.73/10.95 Clause #1 (by assumption #[]): Eq % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (And % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 10.73/10.95 (Eq (op e0 e2) e0)) % 10.73/10.95 (Eq (op e0 e3) e0)) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 10.73/10.95 (Eq (op e2 e0) e0)) % 10.73/10.95 (Eq (op e3 e0) e0))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) % 10.73/10.95 (Eq (op e0 e2) e1)) % 10.73/10.95 (Eq (op e0 e3) e1))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) % 10.73/10.95 (Eq (op e2 e0) e1)) % 10.73/10.95 (Eq (op e3 e0) e1))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) % 10.73/10.95 (Eq (op e0 e2) e2)) % 10.73/10.95 (Eq (op e0 e3) e2))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) % 10.73/10.95 (Eq (op e2 e0) e2)) % 10.73/10.95 (Eq (op e3 e0) e2))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) % 10.73/10.95 (Eq (op e0 e2) e3)) % 10.73/10.95 (Eq (op e0 e3) e3))) % 10.73/10.95 (Or % 10.73/10.95 (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 10.73/10.95 (Eq (op e3 e0) e3))) % 10.73/10.95 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 10.73/10.95 (Eq (op e1 e3) e0))) % 10.73/10.95 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 10.80/10.96 (Eq (op e3 e1) e0))) % 10.80/10.96 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 10.80/10.96 (Eq (op e1 e3) e1))) % 10.80/10.96 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 10.80/10.96 (Eq (op e3 e1) e1))) % 10.80/10.96 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 10.80/10.96 (Eq (op e1 e3) e2))) % 10.80/10.96 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 10.80/10.96 (Eq (op e3 e1) e2))) % 10.80/10.96 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) % 10.80/10.96 (Eq (op e1 e3) e3))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) % 10.80/10.97 (Eq (op e3 e1) e3))) % 10.80/10.97 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) % 10.80/10.97 (Eq (op e2 e3) e0))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) % 10.80/10.97 (Eq (op e3 e2) e0))) % 10.80/10.97 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) % 10.80/10.97 (Eq (op e2 e3) e1))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 10.80/10.97 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 10.80/10.97 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 10.80/10.97 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 10.80/10.97 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1))) % 10.80/10.97 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2))) % 10.80/10.97 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3))) % 10.80/10.97 (Or (Or (Or (Eq (op e0 e3) e3) (Eq (op e1 e3) e3)) (Eq (op e2 e3) e3)) (Eq (op e3 e3) e3))) % 10.80/10.97 True % 10.80/10.97 Clause #2 (by assumption #[]): Eq % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (And % 10.80/10.97 (Ne (op e0 e0) % 10.80/10.97 (op e1 e0)) % 10.80/10.97 (Ne (op e0 e0) % 10.80/10.97 (op e2 e0))) % 10.80/10.97 (Ne (op e0 e0) % 10.80/10.97 (op e3 e0))) % 10.80/10.97 (Ne (op e1 e0) (op e2 e0))) % 10.80/10.97 (Ne (op e1 e0) (op e3 e0))) % 10.80/10.97 (Ne (op e2 e0) (op e3 e0))) % 10.80/10.97 (Ne (op e0 e1) (op e1 e1))) % 10.80/10.97 (Ne (op e0 e1) (op e2 e1))) % 10.80/10.97 (Ne (op e0 e1) (op e3 e1))) % 10.80/10.97 (Ne (op e1 e1) (op e2 e1))) % 10.80/10.97 (Ne (op e1 e1) (op e3 e1))) % 10.80/10.97 (Ne (op e2 e1) (op e3 e1))) % 10.80/10.97 (Ne (op e0 e2) (op e1 e2))) % 10.80/10.97 (Ne (op e0 e2) (op e2 e2))) % 10.80/10.97 (Ne (op e0 e2) (op e3 e2))) % 10.80/10.97 (Ne (op e1 e2) (op e2 e2))) % 10.80/10.97 (Ne (op e1 e2) (op e3 e2))) % 10.80/10.97 (Ne (op e2 e2) (op e3 e2))) % 10.80/10.97 (Ne (op e0 e3) (op e1 e3))) % 10.80/10.97 (Ne (op e0 e3) (op e2 e3))) % 10.80/10.97 (Ne (op e0 e3) (op e3 e3))) % 10.80/10.97 (Ne (op e1 e3) (op e2 e3))) % 10.82/11.00 (Ne (op e1 e3) (op e3 e3))) % 10.82/11.00 (Ne (op e2 e3) (op e3 e3))) % 10.82/11.00 (Ne (op e0 e0) (op e0 e1))) % 10.82/11.00 (Ne (op e0 e0) (op e0 e2))) % 10.82/11.00 (Ne (op e0 e0) (op e0 e3))) % 10.82/11.00 (Ne (op e0 e1) (op e0 e2))) % 10.82/11.00 (Ne (op e0 e1) (op e0 e3))) % 10.82/11.00 (Ne (op e0 e2) (op e0 e3))) % 10.82/11.00 (Ne (op e1 e0) (op e1 e1))) % 10.82/11.00 (Ne (op e1 e0) (op e1 e2))) % 10.82/11.00 (Ne (op e1 e0) (op e1 e3))) % 10.82/11.00 (Ne (op e1 e1) (op e1 e2))) % 10.82/11.00 (Ne (op e1 e1) (op e1 e3))) % 10.82/11.00 (Ne (op e1 e2) (op e1 e3))) % 10.82/11.00 (Ne (op e2 e0) (op e2 e1))) % 10.82/11.00 (Ne (op e2 e0) (op e2 e2))) % 10.82/11.00 (Ne (op e2 e0) (op e2 e3))) % 10.82/11.00 (Ne (op e2 e1) (op e2 e2))) % 10.82/11.00 (Ne (op e2 e1) (op e2 e3))) % 10.82/11.00 (Ne (op e2 e2) (op e2 e3))) % 10.82/11.00 (Ne (op e3 e0) (op e3 e1))) % 10.82/11.00 (Ne (op e3 e0) (op e3 e2))) % 10.82/11.00 (Ne (op e3 e0) (op e3 e3))) % 10.82/11.00 (Ne (op e3 e1) (op e3 e2))) % 10.82/11.00 (Ne (op e3 e1) (op e3 e3))) % 10.82/11.00 (Ne (op e3 e2) (op e3 e3))) % 10.82/11.00 True % 10.82/11.00 Clause #3 (by assumption #[]): Eq (And (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) (Ne e2 e3)) True % 10.82/11.00 Clause #4 (by assumption #[]): Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) True % 10.82/11.00 Clause #13 (by assumption #[]): Eq (Not (And (Eq e1 (op e0 e3)) (Eq e2 (op (op e0 e3) e3)))) True % 10.82/11.00 Clause #15 (by assumption #[]): Eq (Not (And (Eq e1 (op e0 e2)) (Eq e3 (op (op e0 e2) e2)))) True % 10.82/11.00 Clause #19 (by assumption #[]): Eq (Not (And (Eq e2 (op e0 e3)) (Eq e1 (op (op e0 e3) e3)))) True % 10.82/11.00 Clause #25 (by assumption #[]): Eq (Not (And (Eq e3 (op e0 e2)) (Eq e1 (op (op e0 e2) e2)))) True % 10.82/11.00 Clause #41 (by clausification #[25]): Eq (And (Eq e3 (op e0 e2)) (Eq e1 (op (op e0 e2) e2))) False % 10.82/11.00 Clause #42 (by clausification #[41]): Or (Eq (Eq e3 (op e0 e2)) False) (Eq (Eq e1 (op (op e0 e2) e2)) False) % 10.82/11.00 Clause #43 (by clausification #[42]): Or (Eq (Eq e1 (op (op e0 e2) e2)) False) (Ne e3 (op e0 e2)) % 10.82/11.00 Clause #44 (by clausification #[43]): Or (Ne e3 (op e0 e2)) (Ne e1 (op (op e0 e2) e2)) % 10.82/11.00 Clause #65 (by clausification #[19]): Eq (And (Eq e2 (op e0 e3)) (Eq e1 (op (op e0 e3) e3))) False % 10.82/11.00 Clause #66 (by clausification #[65]): Or (Eq (Eq e2 (op e0 e3)) False) (Eq (Eq e1 (op (op e0 e3) e3)) False) % 10.82/11.00 Clause #67 (by clausification #[66]): Or (Eq (Eq e1 (op (op e0 e3) e3)) False) (Ne e2 (op e0 e3)) % 10.82/11.00 Clause #68 (by clausification #[67]): Or (Ne e2 (op e0 e3)) (Ne e1 (op (op e0 e3) e3)) % 10.82/11.00 Clause #70 (by clausification #[1]): Eq % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (And % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 10.82/11.00 (Eq (op e0 e2) e0)) % 10.82/11.00 (Eq (op e0 e3) e0)) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 10.82/11.00 (Eq (op e2 e0) e0)) % 10.82/11.00 (Eq (op e3 e0) e0))) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) % 10.82/11.00 (Eq (op e0 e2) e1)) % 10.82/11.00 (Eq (op e0 e3) e1))) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) % 10.82/11.00 (Eq (op e2 e0) e1)) % 10.82/11.00 (Eq (op e3 e0) e1))) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) % 10.82/11.00 (Eq (op e0 e2) e2)) % 10.82/11.00 (Eq (op e0 e3) e2))) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) % 10.82/11.00 (Eq (op e2 e0) e2)) % 10.82/11.00 (Eq (op e3 e0) e2))) % 10.82/11.00 (Or % 10.82/11.00 (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 10.82/11.00 (Eq (op e0 e3) e3))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 10.82/11.00 (Eq (op e3 e0) e3))) % 10.82/11.00 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 10.82/11.00 (Eq (op e1 e3) e0))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 10.82/11.00 (Eq (op e3 e1) e0))) % 10.82/11.00 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 10.82/11.00 (Eq (op e1 e3) e1))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 10.82/11.00 (Eq (op e3 e1) e1))) % 10.82/11.00 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 10.82/11.00 (Eq (op e1 e3) e2))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 10.82/11.00 (Eq (op e3 e1) e2))) % 10.82/11.00 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) % 10.82/11.00 (Eq (op e1 e3) e3))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) % 10.82/11.00 (Eq (op e3 e1) e3))) % 10.82/11.00 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) % 10.82/11.00 (Eq (op e2 e3) e0))) % 10.82/11.00 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) % 10.86/11.02 (Eq (op e3 e2) e0))) % 10.86/11.02 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 10.86/11.02 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 10.86/11.02 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 10.86/11.02 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 10.86/11.02 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1))) % 10.86/11.02 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2))) % 10.86/11.02 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2))) % 10.86/11.02 (Or (Or (Or (Eq (op e3 e0) e3) (Eq (op e3 e1) e3)) (Eq (op e3 e2) e3)) (Eq (op e3 e3) e3))) % 10.86/11.02 True % 10.86/11.02 Clause #99 (by clausification #[2]): Eq (Ne (op e3 e2) (op e3 e3)) True % 10.86/11.02 Clause #100 (by clausification #[2]): Eq % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (And % 10.86/11.02 (Ne (op e0 e0) (op e1 e0)) % 10.86/11.02 (Ne (op e0 e0) % 10.86/11.02 (op e2 e0))) % 10.86/11.02 (Ne (op e0 e0) (op e3 e0))) % 10.86/11.02 (Ne (op e1 e0) (op e2 e0))) % 10.86/11.02 (Ne (op e1 e0) (op e3 e0))) % 10.86/11.02 (Ne (op e2 e0) (op e3 e0))) % 10.86/11.02 (Ne (op e0 e1) (op e1 e1))) % 10.86/11.02 (Ne (op e0 e1) (op e2 e1))) % 10.86/11.02 (Ne (op e0 e1) (op e3 e1))) % 10.86/11.02 (Ne (op e1 e1) (op e2 e1))) % 10.86/11.02 (Ne (op e1 e1) (op e3 e1))) % 10.86/11.02 (Ne (op e2 e1) (op e3 e1))) % 10.86/11.02 (Ne (op e0 e2) (op e1 e2))) % 10.86/11.02 (Ne (op e0 e2) (op e2 e2))) % 10.86/11.02 (Ne (op e0 e2) (op e3 e2))) % 10.86/11.02 (Ne (op e1 e2) (op e2 e2))) % 10.86/11.02 (Ne (op e1 e2) (op e3 e2))) % 10.86/11.02 (Ne (op e2 e2) (op e3 e2))) % 10.86/11.02 (Ne (op e0 e3) (op e1 e3))) % 10.86/11.02 (Ne (op e0 e3) (op e2 e3))) % 10.86/11.02 (Ne (op e0 e3) (op e3 e3))) % 10.86/11.02 (Ne (op e1 e3) (op e2 e3))) % 10.86/11.02 (Ne (op e1 e3) (op e3 e3))) % 10.86/11.02 (Ne (op e2 e3) (op e3 e3))) % 10.86/11.02 (Ne (op e0 e0) (op e0 e1))) % 10.86/11.02 (Ne (op e0 e0) (op e0 e2))) % 10.86/11.02 (Ne (op e0 e0) (op e0 e3))) % 10.86/11.02 (Ne (op e0 e1) (op e0 e2))) % 10.86/11.02 (Ne (op e0 e1) (op e0 e3))) % 10.86/11.02 (Ne (op e0 e2) (op e0 e3))) % 10.86/11.02 (Ne (op e1 e0) (op e1 e1))) % 10.86/11.02 (Ne (op e1 e0) (op e1 e2))) % 10.86/11.02 (Ne (op e1 e0) (op e1 e3))) % 10.86/11.02 (Ne (op e1 e1) (op e1 e2))) % 10.86/11.02 (Ne (op e1 e1) (op e1 e3))) % 10.86/11.02 (Ne (op e1 e2) (op e1 e3))) % 10.86/11.02 (Ne (op e2 e0) (op e2 e1))) % 10.86/11.02 (Ne (op e2 e0) (op e2 e2))) % 10.86/11.02 (Ne (op e2 e0) (op e2 e3))) % 10.86/11.02 (Ne (op e2 e1) (op e2 e2))) % 10.86/11.02 (Ne (op e2 e1) (op e2 e3))) % 10.86/11.02 (Ne (op e2 e2) (op e2 e3))) % 10.86/11.02 (Ne (op e3 e0) (op e3 e1))) % 10.86/11.02 (Ne (op e3 e0) (op e3 e2))) % 10.86/11.02 (Ne (op e3 e0) (op e3 e3))) % 10.86/11.02 (Ne (op e3 e1) (op e3 e2))) % 10.86/11.02 (Ne (op e3 e1) (op e3 e3))) % 10.86/11.02 True % 10.86/11.02 Clause #101 (by clausification #[99]): Ne (op e3 e2) (op e3 e3) % 10.86/11.02 Clause #106 (by clausification #[15]): Eq (And (Eq e1 (op e0 e2)) (Eq e3 (op (op e0 e2) e2))) False % 10.86/11.02 Clause #107 (by clausification #[106]): Or (Eq (Eq e1 (op e0 e2)) False) (Eq (Eq e3 (op (op e0 e2) e2)) False) % 10.86/11.02 Clause #108 (by clausification #[107]): Or (Eq (Eq e3 (op (op e0 e2) e2)) False) (Ne e1 (op e0 e2)) % 10.86/11.02 Clause #109 (by clausification #[108]): Or (Ne e1 (op e0 e2)) (Ne e3 (op (op e0 e2) e2)) % 10.89/11.06 Clause #114 (by clausification #[13]): Eq (And (Eq e1 (op e0 e3)) (Eq e2 (op (op e0 e3) e3))) False % 10.89/11.06 Clause #115 (by clausification #[114]): Or (Eq (Eq e1 (op e0 e3)) False) (Eq (Eq e2 (op (op e0 e3) e3)) False) % 10.89/11.06 Clause #116 (by clausification #[115]): Or (Eq (Eq e2 (op (op e0 e3) e3)) False) (Ne e1 (op e0 e3)) % 10.89/11.06 Clause #117 (by clausification #[116]): Or (Ne e1 (op e0 e3)) (Ne e2 (op (op e0 e3) e3)) % 10.89/11.06 Clause #123 (by clausification #[3]): Eq (Ne e2 e3) True % 10.89/11.06 Clause #124 (by clausification #[3]): Eq (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) True % 10.89/11.06 Clause #125 (by clausification #[123]): Ne e2 e3 % 10.89/11.06 Clause #146 (by clausification #[4]): Eq (Eq (op e3 e3) e3) True % 10.89/11.06 Clause #147 (by clausification #[4]): Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) True % 10.89/11.06 Clause #148 (by clausification #[146]): Eq (op e3 e3) e3 % 10.89/11.06 Clause #154 (by backward demodulation #[148, 101]): Ne (op e3 e2) e3 % 10.89/11.06 Clause #166 (by clausification #[147]): Eq (Eq (op e2 e2) e2) True % 10.89/11.06 Clause #167 (by clausification #[147]): Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) True % 10.89/11.06 Clause #168 (by clausification #[166]): Eq (op e2 e2) e2 % 10.89/11.06 Clause #186 (by clausification #[70]): Eq % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (And % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 10.89/11.06 (Eq (op e0 e2) e0)) % 10.89/11.06 (Eq (op e0 e3) e0)) % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 10.89/11.06 (Eq (op e2 e0) e0)) % 10.89/11.06 (Eq (op e3 e0) e0))) % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) % 10.89/11.06 (Eq (op e0 e2) e1)) % 10.89/11.06 (Eq (op e0 e3) e1))) % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) % 10.89/11.06 (Eq (op e2 e0) e1)) % 10.89/11.06 (Eq (op e3 e0) e1))) % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) % 10.89/11.06 (Eq (op e0 e2) e2)) % 10.89/11.06 (Eq (op e0 e3) e2))) % 10.89/11.06 (Or % 10.89/11.06 (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 10.89/11.06 (Eq (op e3 e0) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 10.89/11.06 (Eq (op e0 e3) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 10.89/11.06 (Eq (op e3 e0) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 10.89/11.06 (Eq (op e1 e3) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 10.89/11.06 (Eq (op e3 e1) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 10.89/11.06 (Eq (op e1 e3) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 10.89/11.06 (Eq (op e3 e1) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 10.89/11.06 (Eq (op e1 e3) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 10.89/11.06 (Eq (op e3 e1) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) % 10.89/11.06 (Eq (op e1 e3) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) % 10.89/11.06 (Eq (op e3 e1) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) % 10.89/11.06 (Eq (op e2 e3) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 10.89/11.06 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 10.89/11.06 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1))) % 10.89/11.06 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2))) % 10.89/11.06 (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2))) % 10.89/11.06 True % 10.89/11.06 Clause #195 (by clausification #[167]): Eq (Eq (op e1 e1) e1) True % 10.89/11.06 Clause #197 (by clausification #[195]): Eq (op e1 e1) e1 % 10.89/11.06 Clause #199 (by clausification #[124]): Eq (Ne e1 e3) True % 10.89/11.06 Clause #200 (by clausification #[124]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) True % 10.89/11.06 Clause #201 (by clausification #[199]): Ne e1 e3 % 10.89/11.06 Clause #202 (by clausification #[200]): Eq (Ne e1 e2) True % 10.89/11.06 Clause #203 (by clausification #[200]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 10.89/11.06 Clause #204 (by clausification #[202]): Ne e1 e2 % 10.89/11.06 Clause #205 (by clausification #[203]): Eq (Ne e0 e3) True % 10.89/11.06 Clause #206 (by clausification #[203]): Eq (And (Ne e0 e1) (Ne e0 e2)) True % 10.89/11.06 Clause #207 (by clausification #[205]): Ne e0 e3 % 10.89/11.07 Clause #209 (by clausification #[100]): Eq % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.07 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (And % 10.89/11.08 (Ne (op e0 e0) (op e1 e0)) % 10.89/11.08 (Ne (op e0 e0) (op e2 e0))) % 10.89/11.08 (Ne (op e0 e0) (op e3 e0))) % 10.89/11.08 (Ne (op e1 e0) (op e2 e0))) % 10.89/11.08 (Ne (op e1 e0) (op e3 e0))) % 10.89/11.08 (Ne (op e2 e0) (op e3 e0))) % 10.89/11.08 (Ne (op e0 e1) (op e1 e1))) % 10.89/11.08 (Ne (op e0 e1) (op e2 e1))) % 10.89/11.08 (Ne (op e0 e1) (op e3 e1))) % 10.89/11.08 (Ne (op e1 e1) (op e2 e1))) % 10.89/11.08 (Ne (op e1 e1) (op e3 e1))) % 10.89/11.08 (Ne (op e2 e1) (op e3 e1))) % 10.89/11.08 (Ne (op e0 e2) (op e1 e2))) % 10.89/11.08 (Ne (op e0 e2) (op e2 e2))) % 10.89/11.08 (Ne (op e0 e2) (op e3 e2))) % 10.89/11.08 (Ne (op e1 e2) (op e2 e2))) % 10.89/11.08 (Ne (op e1 e2) (op e3 e2))) % 10.89/11.10 (Ne (op e2 e2) (op e3 e2))) % 10.89/11.10 (Ne (op e0 e3) (op e1 e3))) % 10.89/11.10 (Ne (op e0 e3) (op e2 e3))) % 10.89/11.10 (Ne (op e0 e3) (op e3 e3))) % 10.89/11.10 (Ne (op e1 e3) (op e2 e3))) % 10.89/11.10 (Ne (op e1 e3) (op e3 e3))) % 10.89/11.10 (Ne (op e2 e3) (op e3 e3))) % 10.89/11.10 (Ne (op e0 e0) (op e0 e1))) % 10.89/11.10 (Ne (op e0 e0) (op e0 e2))) % 10.89/11.10 (Ne (op e0 e0) (op e0 e3))) % 10.89/11.10 (Ne (op e0 e1) (op e0 e2))) % 10.89/11.10 (Ne (op e0 e1) (op e0 e3))) % 10.89/11.10 (Ne (op e0 e2) (op e0 e3))) % 10.89/11.10 (Ne (op e1 e0) (op e1 e1))) % 10.89/11.10 (Ne (op e1 e0) (op e1 e2))) % 10.89/11.10 (Ne (op e1 e0) (op e1 e3))) % 10.89/11.10 (Ne (op e1 e1) (op e1 e2))) % 10.89/11.10 (Ne (op e1 e1) (op e1 e3))) % 10.89/11.10 (Ne (op e1 e2) (op e1 e3))) % 10.89/11.10 (Ne (op e2 e0) (op e2 e1))) % 10.89/11.10 (Ne (op e2 e0) (op e2 e2))) % 10.89/11.10 (Ne (op e2 e0) (op e2 e3))) % 10.89/11.10 (Ne (op e2 e1) (op e2 e2))) % 10.89/11.10 (Ne (op e2 e1) (op e2 e3))) % 10.89/11.10 (Ne (op e2 e2) (op e2 e3))) % 10.89/11.10 (Ne (op e3 e0) (op e3 e1))) % 10.89/11.10 (Ne (op e3 e0) (op e3 e2))) % 10.89/11.10 (Ne (op e3 e0) (op e3 e3))) % 10.89/11.10 (Ne (op e3 e1) (op e3 e2))) % 10.89/11.10 True % 10.89/11.10 Clause #212 (by clausification #[206]): Eq (Ne e0 e2) True % 10.89/11.10 Clause #213 (by clausification #[206]): Eq (Ne e0 e1) True % 10.89/11.10 Clause #214 (by clausification #[212]): Ne e0 e2 % 10.89/11.10 Clause #215 (by clausification #[213]): Ne e0 e1 % 10.89/11.10 Clause #231 (by clausification #[186]): Eq (Or (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) (Eq (op e3 e3) e2)) True % 10.89/11.10 Clause #232 (by clausification #[186]): Eq % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (And % 10.89/11.10 (Or % 10.89/11.10 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 10.89/11.10 (Eq (op e0 e2) e0)) % 10.89/11.10 (Eq (op e0 e3) e0)) % 10.89/11.10 (Or % 10.89/11.10 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 10.89/11.10 (Eq (op e2 e0) e0)) % 10.89/11.10 (Eq (op e3 e0) e0))) % 10.89/11.10 (Or % 10.89/11.10 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) % 10.89/11.10 (Eq (op e0 e2) e1)) % 10.89/11.10 (Eq (op e0 e3) e1))) % 10.89/11.11 (Or % 10.89/11.11 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) % 10.89/11.11 (Eq (op e2 e0) e1)) % 10.89/11.11 (Eq (op e3 e0) e1))) % 10.89/11.11 (Or % 10.89/11.11 (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 10.89/11.11 (Eq (op e0 e3) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 10.89/11.11 (Eq (op e3 e0) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 10.89/11.11 (Eq (op e0 e3) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 10.89/11.11 (Eq (op e3 e0) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 10.89/11.11 (Eq (op e1 e3) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 10.89/11.11 (Eq (op e3 e1) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 10.89/11.11 (Eq (op e1 e3) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 10.89/11.11 (Eq (op e3 e1) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 10.89/11.11 (Eq (op e1 e3) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 10.89/11.11 (Eq (op e3 e1) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) % 10.89/11.11 (Eq (op e1 e3) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) % 10.89/11.11 (Eq (op e3 e1) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 10.89/11.11 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 10.89/11.11 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 10.89/11.11 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1))) % 10.89/11.11 (Or (Or (Or (Eq (op e3 e0) e2) (Eq (op e3 e1) e2)) (Eq (op e3 e2) e2)) (Eq (op e3 e3) e2))) % 10.89/11.11 True % 10.89/11.11 Clause #233 (by clausification #[231]): Or (Eq (Or (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) (Eq (op e2 e3) e2)) True) (Eq (Eq (op e3 e3) e2) True) % 10.89/11.11 Clause #234 (by clausification #[233]): Or (Eq (Eq (op e3 e3) e2) True) (Or (Eq (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) True) (Eq (Eq (op e2 e3) e2) True)) % 10.97/11.13 Clause #235 (by clausification #[234]): Or (Eq (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) True) (Or (Eq (Eq (op e2 e3) e2) True) (Eq (op e3 e3) e2)) % 10.97/11.13 Clause #236 (by clausification #[235]): Or (Eq (Eq (op e2 e3) e2) True) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e0 e3) e2) True) (Eq (Eq (op e1 e3) e2) True))) % 10.97/11.13 Clause #237 (by clausification #[236]): Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e0 e3) e2) True) (Or (Eq (Eq (op e1 e3) e2) True) (Eq (op e2 e3) e2))) % 10.97/11.13 Clause #238 (by clausification #[237]): Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e1 e3) e2) True) (Or (Eq (op e2 e3) e2) (Eq (op e0 e3) e2))) % 10.97/11.13 Clause #239 (by clausification #[238]): Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e3) e2) (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2))) % 10.97/11.13 Clause #240 (by forward demodulation #[239, 148]): Or (Eq e3 e2) (Or (Eq (op e2 e3) e2) (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2))) % 10.97/11.13 Clause #241 (by forward contextual literal cutting #[240, 125]): Or (Eq (op e2 e3) e2) (Or (Eq (op e0 e3) e2) (Eq (op e1 e3) e2)) % 10.97/11.13 Clause #242 (by superposition #[241, 68]): Or (Eq (op e2 e3) e2) (Or (Eq (op e1 e3) e2) (Or (Ne e2 e2) (Ne e1 (op e2 e3)))) % 10.97/11.13 Clause #244 (by eliminate resolved literals #[242]): Or (Eq (op e2 e3) e2) (Or (Eq (op e1 e3) e2) (Ne e1 (op e2 e3))) % 10.97/11.13 Clause #247 (by clausification #[209]): Eq % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And % 10.97/11.13 (And (Ne (op e0 e0) (op e1 e0)) % 10.97/11.13 (Ne (op e0 e0) (op e2 e0))) % 10.97/11.13 (Ne (op e0 e0) (op e3 e0))) % 10.97/11.13 (Ne (op e1 e0) (op e2 e0))) % 10.97/11.13 (Ne (op e1 e0) (op e3 e0))) % 10.97/11.15 (Ne (op e2 e0) (op e3 e0))) % 10.97/11.15 (Ne (op e0 e1) (op e1 e1))) % 10.97/11.15 (Ne (op e0 e1) (op e2 e1))) % 10.97/11.15 (Ne (op e0 e1) (op e3 e1))) % 10.97/11.15 (Ne (op e1 e1) (op e2 e1))) % 10.97/11.15 (Ne (op e1 e1) (op e3 e1))) % 10.97/11.15 (Ne (op e2 e1) (op e3 e1))) % 10.97/11.15 (Ne (op e0 e2) (op e1 e2))) % 10.97/11.15 (Ne (op e0 e2) (op e2 e2))) % 10.97/11.15 (Ne (op e0 e2) (op e3 e2))) % 10.97/11.15 (Ne (op e1 e2) (op e2 e2))) % 10.97/11.15 (Ne (op e1 e2) (op e3 e2))) % 10.97/11.15 (Ne (op e2 e2) (op e3 e2))) % 10.97/11.15 (Ne (op e0 e3) (op e1 e3))) % 10.97/11.15 (Ne (op e0 e3) (op e2 e3))) % 10.97/11.15 (Ne (op e0 e3) (op e3 e3))) % 10.97/11.15 (Ne (op e1 e3) (op e2 e3))) % 10.97/11.15 (Ne (op e1 e3) (op e3 e3))) % 10.97/11.15 (Ne (op e2 e3) (op e3 e3))) % 10.97/11.15 (Ne (op e0 e0) (op e0 e1))) % 10.97/11.15 (Ne (op e0 e0) (op e0 e2))) % 10.97/11.15 (Ne (op e0 e0) (op e0 e3))) % 10.97/11.15 (Ne (op e0 e1) (op e0 e2))) % 10.97/11.15 (Ne (op e0 e1) (op e0 e3))) % 10.97/11.15 (Ne (op e0 e2) (op e0 e3))) % 10.97/11.15 (Ne (op e1 e0) (op e1 e1))) % 10.97/11.15 (Ne (op e1 e0) (op e1 e2))) % 10.97/11.15 (Ne (op e1 e0) (op e1 e3))) % 10.97/11.15 (Ne (op e1 e1) (op e1 e2))) % 10.97/11.15 (Ne (op e1 e1) (op e1 e3))) % 10.97/11.15 (Ne (op e1 e2) (op e1 e3))) % 10.97/11.15 (Ne (op e2 e0) (op e2 e1))) % 10.97/11.15 (Ne (op e2 e0) (op e2 e2))) % 10.97/11.15 (Ne (op e2 e0) (op e2 e3))) % 10.97/11.15 (Ne (op e2 e1) (op e2 e2))) % 10.97/11.15 (Ne (op e2 e1) (op e2 e3))) % 10.97/11.15 (Ne (op e2 e2) (op e2 e3))) % 10.97/11.15 (Ne (op e3 e0) (op e3 e1))) % 10.97/11.15 (Ne (op e3 e0) (op e3 e2))) % 10.97/11.15 (Ne (op e3 e0) (op e3 e3))) % 10.97/11.15 True % 10.97/11.15 Clause #274 (by clausification #[232]): Eq % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (And % 10.97/11.15 (Or % 10.97/11.15 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 10.97/11.15 (Eq (op e0 e2) e0)) % 10.97/11.15 (Eq (op e0 e3) e0)) % 10.97/11.15 (Or % 10.97/11.15 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 10.97/11.15 (Eq (op e2 e0) e0)) % 10.97/11.15 (Eq (op e3 e0) e0))) % 10.97/11.15 (Or % 10.97/11.15 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) % 10.97/11.15 (Eq (op e0 e2) e1)) % 10.97/11.15 (Eq (op e0 e3) e1))) % 10.97/11.15 (Or % 10.97/11.15 (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 10.97/11.15 (Eq (op e3 e0) e1))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 10.97/11.15 (Eq (op e0 e3) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 10.97/11.15 (Eq (op e3 e0) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 10.97/11.15 (Eq (op e0 e3) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 10.97/11.15 (Eq (op e3 e0) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 10.97/11.15 (Eq (op e1 e3) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 10.97/11.15 (Eq (op e3 e1) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 10.97/11.15 (Eq (op e1 e3) e1))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 10.97/11.15 (Eq (op e3 e1) e1))) % 10.97/11.15 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 10.97/11.15 (Eq (op e1 e3) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 10.97/11.15 (Eq (op e3 e1) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) % 10.97/11.15 (Eq (op e1 e3) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 10.97/11.15 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 10.97/11.15 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 10.97/11.15 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 10.97/11.15 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 10.97/11.17 (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1))) % 10.97/11.17 True % 10.97/11.17 Clause #305 (by clausification #[247]): Eq % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And % 10.97/11.17 (And (Ne (op e0 e0) (op e1 e0)) % 10.97/11.17 (Ne (op e0 e0) (op e2 e0))) % 10.97/11.17 (Ne (op e0 e0) (op e3 e0))) % 10.97/11.17 (Ne (op e1 e0) (op e2 e0))) % 10.97/11.17 (Ne (op e1 e0) (op e3 e0))) % 10.97/11.17 (Ne (op e2 e0) (op e3 e0))) % 10.97/11.17 (Ne (op e0 e1) (op e1 e1))) % 10.97/11.17 (Ne (op e0 e1) (op e2 e1))) % 10.97/11.17 (Ne (op e0 e1) (op e3 e1))) % 10.97/11.17 (Ne (op e1 e1) (op e2 e1))) % 10.97/11.17 (Ne (op e1 e1) (op e3 e1))) % 10.97/11.17 (Ne (op e2 e1) (op e3 e1))) % 10.97/11.17 (Ne (op e0 e2) (op e1 e2))) % 10.97/11.17 (Ne (op e0 e2) (op e2 e2))) % 10.97/11.17 (Ne (op e0 e2) (op e3 e2))) % 10.97/11.17 (Ne (op e1 e2) (op e2 e2))) % 10.97/11.17 (Ne (op e1 e2) (op e3 e2))) % 10.97/11.17 (Ne (op e2 e2) (op e3 e2))) % 10.97/11.17 (Ne (op e0 e3) (op e1 e3))) % 10.97/11.17 (Ne (op e0 e3) (op e2 e3))) % 11.03/11.19 (Ne (op e0 e3) (op e3 e3))) % 11.03/11.19 (Ne (op e1 e3) (op e2 e3))) % 11.03/11.19 (Ne (op e1 e3) (op e3 e3))) % 11.03/11.19 (Ne (op e2 e3) (op e3 e3))) % 11.03/11.19 (Ne (op e0 e0) (op e0 e1))) % 11.03/11.19 (Ne (op e0 e0) (op e0 e2))) % 11.03/11.19 (Ne (op e0 e0) (op e0 e3))) % 11.03/11.19 (Ne (op e0 e1) (op e0 e2))) % 11.03/11.19 (Ne (op e0 e1) (op e0 e3))) % 11.03/11.19 (Ne (op e0 e2) (op e0 e3))) % 11.03/11.19 (Ne (op e1 e0) (op e1 e1))) % 11.03/11.19 (Ne (op e1 e0) (op e1 e2))) % 11.03/11.19 (Ne (op e1 e0) (op e1 e3))) % 11.03/11.19 (Ne (op e1 e1) (op e1 e2))) % 11.03/11.19 (Ne (op e1 e1) (op e1 e3))) % 11.03/11.19 (Ne (op e1 e2) (op e1 e3))) % 11.03/11.19 (Ne (op e2 e0) (op e2 e1))) % 11.03/11.19 (Ne (op e2 e0) (op e2 e2))) % 11.03/11.19 (Ne (op e2 e0) (op e2 e3))) % 11.03/11.19 (Ne (op e2 e1) (op e2 e2))) % 11.03/11.19 (Ne (op e2 e1) (op e2 e3))) % 11.03/11.19 (Ne (op e2 e2) (op e2 e3))) % 11.03/11.19 (Ne (op e3 e0) (op e3 e1))) % 11.03/11.19 (Ne (op e3 e0) (op e3 e2))) % 11.03/11.19 True % 11.03/11.19 Clause #316 (by clausification #[274]): Eq (Or (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) (Eq (op e3 e3) e1)) True % 11.03/11.19 Clause #317 (by clausification #[274]): Eq % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.19 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (And % 11.03/11.20 (Or % 11.03/11.20 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) % 11.03/11.20 (Eq (op e0 e2) e0)) % 11.03/11.20 (Eq (op e0 e3) e0)) % 11.03/11.20 (Or % 11.03/11.20 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) % 11.03/11.20 (Eq (op e2 e0) e0)) % 11.03/11.20 (Eq (op e3 e0) e0))) % 11.03/11.20 (Or % 11.03/11.20 (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.03/11.20 (Eq (op e0 e3) e1))) % 11.03/11.20 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.03/11.20 (Eq (op e3 e0) e1))) % 11.03/11.20 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.03/11.20 (Eq (op e0 e3) e2))) % 11.03/11.20 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.03/11.20 (Eq (op e3 e0) e2))) % 11.03/11.20 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.03/11.20 (Eq (op e0 e3) e3))) % 11.03/11.20 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.03/11.21 (Eq (op e3 e0) e3))) % 11.03/11.21 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.03/11.21 (Eq (op e1 e3) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 11.03/11.21 (Eq (op e3 e1) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 11.03/11.21 (Eq (op e1 e3) e1))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 11.03/11.21 (Eq (op e3 e1) e1))) % 11.03/11.21 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 11.03/11.21 (Eq (op e1 e3) e2))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) % 11.03/11.21 (Eq (op e3 e1) e2))) % 11.03/11.21 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.03/11.21 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.03/11.21 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.03/11.21 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 11.03/11.21 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 11.03/11.21 (Or (Or (Or (Eq (op e3 e0) e1) (Eq (op e3 e1) e1)) (Eq (op e3 e2) e1)) (Eq (op e3 e3) e1))) % 11.03/11.21 True % 11.03/11.21 Clause #318 (by clausification #[316]): Or (Eq (Or (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) (Eq (op e2 e3) e1)) True) (Eq (Eq (op e3 e3) e1) True) % 11.03/11.21 Clause #319 (by clausification #[318]): Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) True) (Eq (Eq (op e2 e3) e1) True)) % 11.03/11.21 Clause #320 (by clausification #[319]): Or (Eq (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) True) (Or (Eq (Eq (op e2 e3) e1) True) (Eq (op e3 e3) e1)) % 11.03/11.21 Clause #321 (by clausification #[320]): Or (Eq (Eq (op e2 e3) e1) True) (Or (Eq (op e3 e3) e1) (Or (Eq (Eq (op e0 e3) e1) True) (Eq (Eq (op e1 e3) e1) True))) % 11.03/11.21 Clause #322 (by clausification #[321]): Or (Eq (op e3 e3) e1) (Or (Eq (Eq (op e0 e3) e1) True) (Or (Eq (Eq (op e1 e3) e1) True) (Eq (op e2 e3) e1))) % 11.03/11.21 Clause #323 (by clausification #[322]): Or (Eq (op e3 e3) e1) (Or (Eq (Eq (op e1 e3) e1) True) (Or (Eq (op e2 e3) e1) (Eq (op e0 e3) e1))) % 11.03/11.21 Clause #324 (by clausification #[323]): Or (Eq (op e3 e3) e1) (Or (Eq (op e2 e3) e1) (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1))) % 11.03/11.21 Clause #325 (by forward demodulation #[324, 148]): Or (Eq e3 e1) (Or (Eq (op e2 e3) e1) (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1))) % 11.03/11.21 Clause #326 (by forward contextual literal cutting #[325, 201]): Or (Eq (op e2 e3) e1) (Or (Eq (op e0 e3) e1) (Eq (op e1 e3) e1)) % 11.03/11.21 Clause #328 (by superposition #[326, 117]): Or (Eq (op e2 e3) e1) (Or (Eq (op e1 e3) e1) (Or (Ne e1 e1) (Ne e2 (op e1 e3)))) % 11.03/11.21 Clause #329 (by superposition #[326, 241]): Or (Eq (op e2 e3) e1) (Or (Eq (op e1 e3) e1) (Or (Eq (op e2 e3) e2) (Or (Eq e1 e2) (Eq (op e1 e3) e2)))) % 11.03/11.22 Clause #343 (by eliminate resolved literals #[328]): Or (Eq (op e2 e3) e1) (Or (Eq (op e1 e3) e1) (Ne e2 (op e1 e3))) % 11.03/11.22 Clause #347 (by forward contextual literal cutting #[329, 244]): Or (Eq (op e1 e3) e1) (Or (Eq (op e2 e3) e2) (Or (Eq e1 e2) (Eq (op e1 e3) e2))) % 11.03/11.22 Clause #348 (by forward contextual literal cutting #[347, 204]): Or (Eq (op e1 e3) e1) (Or (Eq (op e2 e3) e2) (Eq (op e1 e3) e2)) % 11.03/11.22 Clause #358 (by clausification #[305]): Eq % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And % 11.03/11.22 (And (Ne (op e0 e0) (op e1 e0)) % 11.03/11.22 (Ne (op e0 e0) (op e2 e0))) % 11.03/11.22 (Ne (op e0 e0) (op e3 e0))) % 11.03/11.22 (Ne (op e1 e0) (op e2 e0))) % 11.03/11.22 (Ne (op e1 e0) (op e3 e0))) % 11.03/11.22 (Ne (op e2 e0) (op e3 e0))) % 11.03/11.22 (Ne (op e0 e1) (op e1 e1))) % 11.03/11.22 (Ne (op e0 e1) (op e2 e1))) % 11.03/11.22 (Ne (op e0 e1) (op e3 e1))) % 11.03/11.22 (Ne (op e1 e1) (op e2 e1))) % 11.03/11.22 (Ne (op e1 e1) (op e3 e1))) % 11.03/11.22 (Ne (op e2 e1) (op e3 e1))) % 11.03/11.22 (Ne (op e0 e2) (op e1 e2))) % 11.03/11.22 (Ne (op e0 e2) (op e2 e2))) % 11.03/11.22 (Ne (op e0 e2) (op e3 e2))) % 11.03/11.22 (Ne (op e1 e2) (op e2 e2))) % 11.03/11.22 (Ne (op e1 e2) (op e3 e2))) % 11.03/11.22 (Ne (op e2 e2) (op e3 e2))) % 11.03/11.25 (Ne (op e0 e3) (op e1 e3))) % 11.03/11.25 (Ne (op e0 e3) (op e2 e3))) % 11.03/11.25 (Ne (op e0 e3) (op e3 e3))) % 11.03/11.25 (Ne (op e1 e3) (op e2 e3))) % 11.03/11.25 (Ne (op e1 e3) (op e3 e3))) % 11.03/11.25 (Ne (op e2 e3) (op e3 e3))) % 11.03/11.25 (Ne (op e0 e0) (op e0 e1))) % 11.03/11.25 (Ne (op e0 e0) (op e0 e2))) % 11.03/11.25 (Ne (op e0 e0) (op e0 e3))) % 11.03/11.25 (Ne (op e0 e1) (op e0 e2))) % 11.03/11.25 (Ne (op e0 e1) (op e0 e3))) % 11.03/11.25 (Ne (op e0 e2) (op e0 e3))) % 11.03/11.25 (Ne (op e1 e0) (op e1 e1))) % 11.03/11.25 (Ne (op e1 e0) (op e1 e2))) % 11.03/11.25 (Ne (op e1 e0) (op e1 e3))) % 11.03/11.25 (Ne (op e1 e1) (op e1 e2))) % 11.03/11.25 (Ne (op e1 e1) (op e1 e3))) % 11.03/11.25 (Ne (op e1 e2) (op e1 e3))) % 11.03/11.25 (Ne (op e2 e0) (op e2 e1))) % 11.03/11.25 (Ne (op e2 e0) (op e2 e2))) % 11.03/11.25 (Ne (op e2 e0) (op e2 e3))) % 11.03/11.25 (Ne (op e2 e1) (op e2 e2))) % 11.03/11.25 (Ne (op e2 e1) (op e2 e3))) % 11.03/11.25 (Ne (op e2 e2) (op e2 e3))) % 11.03/11.25 (Ne (op e3 e0) (op e3 e1))) % 11.03/11.25 True % 11.03/11.25 Clause #371 (by clausification #[317]): Eq % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (And % 11.03/11.25 (Or % 11.03/11.25 (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.03/11.25 (Eq (op e0 e3) e0)) % 11.03/11.25 (Or % 11.03/11.25 (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.03/11.25 (Eq (op e3 e0) e0))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.03/11.25 (Eq (op e0 e3) e1))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.03/11.25 (Eq (op e3 e0) e1))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.03/11.25 (Eq (op e0 e3) e2))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.03/11.25 (Eq (op e3 e0) e2))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.03/11.25 (Eq (op e0 e3) e3))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.03/11.25 (Eq (op e3 e0) e3))) % 11.03/11.25 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.03/11.25 (Eq (op e1 e3) e0))) % 11.03/11.25 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 11.10/11.26 (Eq (op e3 e1) e0))) % 11.10/11.26 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 11.10/11.26 (Eq (op e1 e3) e1))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 11.10/11.26 (Eq (op e3 e1) e1))) % 11.10/11.26 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) % 11.10/11.26 (Eq (op e1 e3) e2))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.10/11.26 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.10/11.26 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.10/11.26 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.10/11.26 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.10/11.26 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 11.10/11.26 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 11.10/11.26 (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0))) % 11.10/11.26 True % 11.10/11.26 Clause #421 (by clausification #[358]): Eq % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And % 11.10/11.26 (And (Ne (op e0 e0) (op e1 e0)) % 11.10/11.26 (Ne (op e0 e0) (op e2 e0))) % 11.10/11.28 (Ne (op e0 e0) (op e3 e0))) % 11.10/11.28 (Ne (op e1 e0) (op e2 e0))) % 11.10/11.28 (Ne (op e1 e0) (op e3 e0))) % 11.10/11.28 (Ne (op e2 e0) (op e3 e0))) % 11.10/11.28 (Ne (op e0 e1) (op e1 e1))) % 11.10/11.28 (Ne (op e0 e1) (op e2 e1))) % 11.10/11.28 (Ne (op e0 e1) (op e3 e1))) % 11.10/11.28 (Ne (op e1 e1) (op e2 e1))) % 11.10/11.28 (Ne (op e1 e1) (op e3 e1))) % 11.10/11.28 (Ne (op e2 e1) (op e3 e1))) % 11.10/11.28 (Ne (op e0 e2) (op e1 e2))) % 11.10/11.28 (Ne (op e0 e2) (op e2 e2))) % 11.10/11.28 (Ne (op e0 e2) (op e3 e2))) % 11.10/11.28 (Ne (op e1 e2) (op e2 e2))) % 11.10/11.28 (Ne (op e1 e2) (op e3 e2))) % 11.10/11.28 (Ne (op e2 e2) (op e3 e2))) % 11.10/11.28 (Ne (op e0 e3) (op e1 e3))) % 11.10/11.28 (Ne (op e0 e3) (op e2 e3))) % 11.10/11.28 (Ne (op e0 e3) (op e3 e3))) % 11.10/11.28 (Ne (op e1 e3) (op e2 e3))) % 11.10/11.28 (Ne (op e1 e3) (op e3 e3))) % 11.10/11.28 (Ne (op e2 e3) (op e3 e3))) % 11.10/11.28 (Ne (op e0 e0) (op e0 e1))) % 11.10/11.28 (Ne (op e0 e0) (op e0 e2))) % 11.10/11.28 (Ne (op e0 e0) (op e0 e3))) % 11.10/11.28 (Ne (op e0 e1) (op e0 e2))) % 11.10/11.28 (Ne (op e0 e1) (op e0 e3))) % 11.10/11.28 (Ne (op e0 e2) (op e0 e3))) % 11.10/11.28 (Ne (op e1 e0) (op e1 e1))) % 11.10/11.28 (Ne (op e1 e0) (op e1 e2))) % 11.10/11.28 (Ne (op e1 e0) (op e1 e3))) % 11.10/11.28 (Ne (op e1 e1) (op e1 e2))) % 11.10/11.28 (Ne (op e1 e1) (op e1 e3))) % 11.10/11.28 (Ne (op e1 e2) (op e1 e3))) % 11.10/11.28 (Ne (op e2 e0) (op e2 e1))) % 11.10/11.28 (Ne (op e2 e0) (op e2 e2))) % 11.10/11.28 (Ne (op e2 e0) (op e2 e3))) % 11.10/11.28 (Ne (op e2 e1) (op e2 e2))) % 11.10/11.28 (Ne (op e2 e1) (op e2 e3))) % 11.10/11.28 (Ne (op e2 e2) (op e2 e3))) % 11.10/11.28 True % 11.10/11.28 Clause #437 (by clausification #[371]): Eq (Or (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) (Eq (op e3 e3) e0)) True % 11.10/11.28 Clause #438 (by clausification #[371]): Eq % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (And % 11.10/11.28 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.10/11.28 (Eq (op e0 e3) e0)) % 11.10/11.28 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.10/11.28 (Eq (op e3 e0) e0))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.14/11.29 (Eq (op e0 e3) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.14/11.29 (Eq (op e3 e0) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.14/11.29 (Eq (op e0 e3) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.14/11.29 (Eq (op e3 e0) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.14/11.29 (Eq (op e0 e3) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.14/11.29 (Eq (op e3 e0) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.14/11.29 (Eq (op e1 e3) e0))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 11.14/11.29 (Eq (op e3 e1) e0))) % 11.14/11.29 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 11.14/11.29 (Eq (op e1 e3) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) % 11.14/11.29 (Eq (op e3 e1) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.14/11.29 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.14/11.29 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.14/11.29 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 11.14/11.29 (Or (Or (Or (Eq (op e3 e0) e0) (Eq (op e3 e1) e0)) (Eq (op e3 e2) e0)) (Eq (op e3 e3) e0))) % 11.14/11.29 True % 11.14/11.29 Clause #439 (by clausification #[437]): Or (Eq (Or (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) (Eq (op e2 e3) e0)) True) (Eq (Eq (op e3 e3) e0) True) % 11.14/11.29 Clause #440 (by clausification #[439]): Or (Eq (Eq (op e3 e3) e0) True) (Or (Eq (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) True) (Eq (Eq (op e2 e3) e0) True)) % 11.14/11.29 Clause #441 (by clausification #[440]): Or (Eq (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) True) (Or (Eq (Eq (op e2 e3) e0) True) (Eq (op e3 e3) e0)) % 11.14/11.29 Clause #442 (by clausification #[441]): Or (Eq (Eq (op e2 e3) e0) True) (Or (Eq (op e3 e3) e0) (Or (Eq (Eq (op e0 e3) e0) True) (Eq (Eq (op e1 e3) e0) True))) % 11.14/11.29 Clause #443 (by clausification #[442]): Or (Eq (op e3 e3) e0) (Or (Eq (Eq (op e0 e3) e0) True) (Or (Eq (Eq (op e1 e3) e0) True) (Eq (op e2 e3) e0))) % 11.14/11.29 Clause #444 (by clausification #[443]): Or (Eq (op e3 e3) e0) (Or (Eq (Eq (op e1 e3) e0) True) (Or (Eq (op e2 e3) e0) (Eq (op e0 e3) e0))) % 11.14/11.31 Clause #445 (by clausification #[444]): Or (Eq (op e3 e3) e0) (Or (Eq (op e2 e3) e0) (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0))) % 11.14/11.31 Clause #446 (by forward demodulation #[445, 148]): Or (Eq e3 e0) (Or (Eq (op e2 e3) e0) (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0))) % 11.14/11.31 Clause #447 (by forward contextual literal cutting #[446, 207]): Or (Eq (op e2 e3) e0) (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) % 11.14/11.31 Clause #516 (by clausification #[421]): Eq (Ne (op e2 e2) (op e2 e3)) True % 11.14/11.31 Clause #517 (by clausification #[421]): Eq % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And % 11.14/11.31 (And (Ne (op e0 e0) (op e1 e0)) % 11.14/11.31 (Ne (op e0 e0) (op e2 e0))) % 11.14/11.31 (Ne (op e0 e0) (op e3 e0))) % 11.14/11.31 (Ne (op e1 e0) (op e2 e0))) % 11.14/11.31 (Ne (op e1 e0) (op e3 e0))) % 11.14/11.31 (Ne (op e2 e0) (op e3 e0))) % 11.14/11.31 (Ne (op e0 e1) (op e1 e1))) % 11.14/11.31 (Ne (op e0 e1) (op e2 e1))) % 11.14/11.31 (Ne (op e0 e1) (op e3 e1))) % 11.14/11.31 (Ne (op e1 e1) (op e2 e1))) % 11.14/11.31 (Ne (op e1 e1) (op e3 e1))) % 11.14/11.31 (Ne (op e2 e1) (op e3 e1))) % 11.14/11.31 (Ne (op e0 e2) (op e1 e2))) % 11.14/11.31 (Ne (op e0 e2) (op e2 e2))) % 11.14/11.31 (Ne (op e0 e2) (op e3 e2))) % 11.14/11.31 (Ne (op e1 e2) (op e2 e2))) % 11.14/11.31 (Ne (op e1 e2) (op e3 e2))) % 11.14/11.31 (Ne (op e2 e2) (op e3 e2))) % 11.14/11.31 (Ne (op e0 e3) (op e1 e3))) % 11.14/11.31 (Ne (op e0 e3) (op e2 e3))) % 11.14/11.33 (Ne (op e0 e3) (op e3 e3))) % 11.14/11.33 (Ne (op e1 e3) (op e2 e3))) % 11.14/11.33 (Ne (op e1 e3) (op e3 e3))) % 11.14/11.33 (Ne (op e2 e3) (op e3 e3))) % 11.14/11.33 (Ne (op e0 e0) (op e0 e1))) % 11.14/11.33 (Ne (op e0 e0) (op e0 e2))) % 11.14/11.33 (Ne (op e0 e0) (op e0 e3))) % 11.14/11.33 (Ne (op e0 e1) (op e0 e2))) % 11.14/11.33 (Ne (op e0 e1) (op e0 e3))) % 11.14/11.33 (Ne (op e0 e2) (op e0 e3))) % 11.14/11.33 (Ne (op e1 e0) (op e1 e1))) % 11.14/11.33 (Ne (op e1 e0) (op e1 e2))) % 11.14/11.33 (Ne (op e1 e0) (op e1 e3))) % 11.14/11.33 (Ne (op e1 e1) (op e1 e2))) % 11.14/11.33 (Ne (op e1 e1) (op e1 e3))) % 11.14/11.33 (Ne (op e1 e2) (op e1 e3))) % 11.14/11.33 (Ne (op e2 e0) (op e2 e1))) % 11.14/11.33 (Ne (op e2 e0) (op e2 e2))) % 11.14/11.33 (Ne (op e2 e0) (op e2 e3))) % 11.14/11.33 (Ne (op e2 e1) (op e2 e2))) % 11.14/11.33 (Ne (op e2 e1) (op e2 e3))) % 11.14/11.33 True % 11.14/11.33 Clause #518 (by clausification #[516]): Ne (op e2 e2) (op e2 e3) % 11.14/11.33 Clause #519 (by forward demodulation #[518, 168]): Ne e2 (op e2 e3) % 11.14/11.33 Clause #526 (by backward contextual literal cutting #[519, 348]): Or (Eq (op e1 e3) e1) (Eq (op e1 e3) e2) % 11.14/11.33 Clause #530 (by backward contextual literal cutting #[526, 343]): Or (Eq (op e2 e3) e1) (Eq (op e1 e3) e1) % 11.14/11.33 Clause #548 (by clausification #[438]): Eq % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (And % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.14/11.33 (Eq (op e0 e3) e0)) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.14/11.33 (Eq (op e3 e0) e0))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.14/11.33 (Eq (op e0 e3) e1))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.14/11.33 (Eq (op e3 e0) e1))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.14/11.33 (Eq (op e0 e3) e2))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.14/11.33 (Eq (op e3 e0) e2))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.14/11.33 (Eq (op e0 e3) e3))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.14/11.33 (Eq (op e3 e0) e3))) % 11.14/11.33 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.14/11.33 (Eq (op e1 e3) e0))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 11.14/11.33 (Eq (op e3 e1) e0))) % 11.14/11.33 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) % 11.14/11.33 (Eq (op e1 e3) e1))) % 11.14/11.33 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.18/11.34 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.18/11.34 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.18/11.34 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.18/11.34 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.18/11.34 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.18/11.34 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 11.18/11.34 (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3))) % 11.18/11.34 True % 11.18/11.34 Clause #647 (by clausification #[517]): Eq % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And % 11.18/11.34 (And (Ne (op e0 e0) (op e1 e0)) % 11.18/11.34 (Ne (op e0 e0) (op e2 e0))) % 11.18/11.34 (Ne (op e0 e0) (op e3 e0))) % 11.18/11.34 (Ne (op e1 e0) (op e2 e0))) % 11.18/11.34 (Ne (op e1 e0) (op e3 e0))) % 11.18/11.34 (Ne (op e2 e0) (op e3 e0))) % 11.18/11.34 (Ne (op e0 e1) (op e1 e1))) % 11.18/11.34 (Ne (op e0 e1) (op e2 e1))) % 11.18/11.34 (Ne (op e0 e1) (op e3 e1))) % 11.18/11.34 (Ne (op e1 e1) (op e2 e1))) % 11.21/11.36 (Ne (op e1 e1) (op e3 e1))) % 11.21/11.36 (Ne (op e2 e1) (op e3 e1))) % 11.21/11.36 (Ne (op e0 e2) (op e1 e2))) % 11.21/11.36 (Ne (op e0 e2) (op e2 e2))) % 11.21/11.36 (Ne (op e0 e2) (op e3 e2))) % 11.21/11.36 (Ne (op e1 e2) (op e2 e2))) % 11.21/11.36 (Ne (op e1 e2) (op e3 e2))) % 11.21/11.36 (Ne (op e2 e2) (op e3 e2))) % 11.21/11.36 (Ne (op e0 e3) (op e1 e3))) % 11.21/11.36 (Ne (op e0 e3) (op e2 e3))) % 11.21/11.36 (Ne (op e0 e3) (op e3 e3))) % 11.21/11.36 (Ne (op e1 e3) (op e2 e3))) % 11.21/11.36 (Ne (op e1 e3) (op e3 e3))) % 11.21/11.36 (Ne (op e2 e3) (op e3 e3))) % 11.21/11.36 (Ne (op e0 e0) (op e0 e1))) % 11.21/11.36 (Ne (op e0 e0) (op e0 e2))) % 11.21/11.36 (Ne (op e0 e0) (op e0 e3))) % 11.21/11.36 (Ne (op e0 e1) (op e0 e2))) % 11.21/11.36 (Ne (op e0 e1) (op e0 e3))) % 11.21/11.36 (Ne (op e0 e2) (op e0 e3))) % 11.21/11.36 (Ne (op e1 e0) (op e1 e1))) % 11.21/11.36 (Ne (op e1 e0) (op e1 e2))) % 11.21/11.36 (Ne (op e1 e0) (op e1 e3))) % 11.21/11.36 (Ne (op e1 e1) (op e1 e2))) % 11.21/11.36 (Ne (op e1 e1) (op e1 e3))) % 11.21/11.36 (Ne (op e1 e2) (op e1 e3))) % 11.21/11.36 (Ne (op e2 e0) (op e2 e1))) % 11.21/11.36 (Ne (op e2 e0) (op e2 e2))) % 11.21/11.36 (Ne (op e2 e0) (op e2 e3))) % 11.21/11.36 (Ne (op e2 e1) (op e2 e2))) % 11.21/11.36 True % 11.21/11.36 Clause #665 (by clausification #[548]): Eq (Or (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e2) e3)) True % 11.21/11.36 Clause #666 (by clausification #[548]): Eq % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (And % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.21/11.36 (Eq (op e0 e3) e0)) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.21/11.36 (Eq (op e3 e0) e0))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.21/11.36 (Eq (op e0 e3) e1))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.21/11.36 (Eq (op e3 e0) e1))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.21/11.36 (Eq (op e0 e3) e2))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.21/11.36 (Eq (op e3 e0) e2))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.21/11.36 (Eq (op e0 e3) e3))) % 11.21/11.36 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.21/11.36 (Eq (op e3 e0) e3))) % 11.21/11.36 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.21/11.39 (Eq (op e1 e3) e0))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) % 11.21/11.39 (Eq (op e3 e1) e0))) % 11.21/11.39 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.21/11.39 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.21/11.39 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.21/11.39 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.21/11.39 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.21/11.39 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.21/11.39 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.21/11.39 (Or (Or (Or (Eq (op e2 e0) e3) (Eq (op e2 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e2 e3) e3))) % 11.21/11.39 True % 11.21/11.39 Clause #667 (by clausification #[665]): Or (Eq (Or (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) (Eq (op e2 e2) e3)) True) (Eq (Eq (op e3 e2) e3) True) % 11.21/11.39 Clause #668 (by clausification #[667]): Or (Eq (Eq (op e3 e2) e3) True) (Or (Eq (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) True) (Eq (Eq (op e2 e2) e3) True)) % 11.21/11.39 Clause #669 (by clausification #[668]): Or (Eq (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) True) (Or (Eq (Eq (op e2 e2) e3) True) (Eq (op e3 e2) e3)) % 11.21/11.39 Clause #670 (by clausification #[669]): Or (Eq (Eq (op e2 e2) e3) True) (Or (Eq (op e3 e2) e3) (Or (Eq (Eq (op e0 e2) e3) True) (Eq (Eq (op e1 e2) e3) True))) % 11.21/11.39 Clause #671 (by clausification #[670]): Or (Eq (op e3 e2) e3) (Or (Eq (Eq (op e0 e2) e3) True) (Or (Eq (Eq (op e1 e2) e3) True) (Eq (op e2 e2) e3))) % 11.21/11.39 Clause #672 (by clausification #[671]): Or (Eq (op e3 e2) e3) (Or (Eq (Eq (op e1 e2) e3) True) (Or (Eq (op e2 e2) e3) (Eq (op e0 e2) e3))) % 11.21/11.39 Clause #673 (by clausification #[672]): Or (Eq (op e3 e2) e3) (Or (Eq (op e2 e2) e3) (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3))) % 11.21/11.39 Clause #674 (by forward demodulation #[673, 168]): Or (Eq (op e3 e2) e3) (Or (Eq e2 e3) (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3))) % 11.21/11.39 Clause #675 (by forward contextual literal cutting #[674, 154]): Or (Eq e2 e3) (Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3)) % 11.21/11.39 Clause #676 (by forward contextual literal cutting #[675, 125]): Or (Eq (op e0 e2) e3) (Eq (op e1 e2) e3) % 11.21/11.39 Clause #678 (by superposition #[676, 44]): Or (Eq (op e1 e2) e3) (Or (Ne e3 e3) (Ne e1 (op e3 e2))) % 11.21/11.39 Clause #683 (by eliminate resolved literals #[678]): Or (Eq (op e1 e2) e3) (Ne e1 (op e3 e2)) % 11.21/11.39 Clause #707 (by clausification #[647]): Eq % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.39 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And (Ne (op e0 e0) (op e1 e0)) % 11.21/11.41 (Ne (op e0 e0) (op e2 e0))) % 11.21/11.41 (Ne (op e0 e0) (op e3 e0))) % 11.21/11.41 (Ne (op e1 e0) (op e2 e0))) % 11.21/11.41 (Ne (op e1 e0) (op e3 e0))) % 11.21/11.41 (Ne (op e2 e0) (op e3 e0))) % 11.21/11.41 (Ne (op e0 e1) (op e1 e1))) % 11.21/11.41 (Ne (op e0 e1) (op e2 e1))) % 11.21/11.41 (Ne (op e0 e1) (op e3 e1))) % 11.21/11.41 (Ne (op e1 e1) (op e2 e1))) % 11.21/11.41 (Ne (op e1 e1) (op e3 e1))) % 11.21/11.41 (Ne (op e2 e1) (op e3 e1))) % 11.21/11.41 (Ne (op e0 e2) (op e1 e2))) % 11.21/11.41 (Ne (op e0 e2) (op e2 e2))) % 11.21/11.41 (Ne (op e0 e2) (op e3 e2))) % 11.21/11.41 (Ne (op e1 e2) (op e2 e2))) % 11.21/11.41 (Ne (op e1 e2) (op e3 e2))) % 11.21/11.41 (Ne (op e2 e2) (op e3 e2))) % 11.21/11.41 (Ne (op e0 e3) (op e1 e3))) % 11.21/11.41 (Ne (op e0 e3) (op e2 e3))) % 11.21/11.41 (Ne (op e0 e3) (op e3 e3))) % 11.21/11.41 (Ne (op e1 e3) (op e2 e3))) % 11.21/11.41 (Ne (op e1 e3) (op e3 e3))) % 11.21/11.41 (Ne (op e2 e3) (op e3 e3))) % 11.21/11.41 (Ne (op e0 e0) (op e0 e1))) % 11.21/11.41 (Ne (op e0 e0) (op e0 e2))) % 11.21/11.41 (Ne (op e0 e0) (op e0 e3))) % 11.21/11.41 (Ne (op e0 e1) (op e0 e2))) % 11.21/11.41 (Ne (op e0 e1) (op e0 e3))) % 11.21/11.41 (Ne (op e0 e2) (op e0 e3))) % 11.21/11.41 (Ne (op e1 e0) (op e1 e1))) % 11.21/11.41 (Ne (op e1 e0) (op e1 e2))) % 11.21/11.41 (Ne (op e1 e0) (op e1 e3))) % 11.21/11.41 (Ne (op e1 e1) (op e1 e2))) % 11.21/11.41 (Ne (op e1 e1) (op e1 e3))) % 11.21/11.41 (Ne (op e1 e2) (op e1 e3))) % 11.21/11.41 (Ne (op e2 e0) (op e2 e1))) % 11.21/11.41 (Ne (op e2 e0) (op e2 e2))) % 11.21/11.41 (Ne (op e2 e0) (op e2 e3))) % 11.21/11.41 True % 11.21/11.41 Clause #758 (by clausification #[666]): Eq % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.41 (And % 11.21/11.42 (And % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.21/11.42 (Eq (op e0 e3) e0)) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.21/11.42 (Eq (op e3 e0) e0))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.21/11.42 (Eq (op e0 e3) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.21/11.42 (Eq (op e3 e0) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.21/11.42 (Eq (op e0 e3) e2))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.21/11.42 (Eq (op e3 e0) e2))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.21/11.42 (Eq (op e0 e3) e3))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.21/11.42 (Eq (op e3 e0) e3))) % 11.21/11.42 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) % 11.21/11.42 (Eq (op e1 e3) e0))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) (Eq (op e3 e1) e0))) % 11.21/11.42 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.21/11.42 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.21/11.42 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.21/11.42 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.21/11.42 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.21/11.42 (Or (Or (Or (Eq (op e0 e2) e2) (Eq (op e1 e2) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e2) e2))) % 11.21/11.42 True % 11.21/11.42 Clause #798 (by clausification #[707]): Eq % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.21/11.42 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And (Ne (op e0 e0) (op e1 e0)) % 11.27/11.44 (Ne (op e0 e0) (op e2 e0))) % 11.27/11.44 (Ne (op e0 e0) (op e3 e0))) % 11.27/11.44 (Ne (op e1 e0) (op e2 e0))) % 11.27/11.44 (Ne (op e1 e0) (op e3 e0))) % 11.27/11.44 (Ne (op e2 e0) (op e3 e0))) % 11.27/11.44 (Ne (op e0 e1) (op e1 e1))) % 11.27/11.44 (Ne (op e0 e1) (op e2 e1))) % 11.27/11.44 (Ne (op e0 e1) (op e3 e1))) % 11.27/11.44 (Ne (op e1 e1) (op e2 e1))) % 11.27/11.44 (Ne (op e1 e1) (op e3 e1))) % 11.27/11.44 (Ne (op e2 e1) (op e3 e1))) % 11.27/11.44 (Ne (op e0 e2) (op e1 e2))) % 11.27/11.44 (Ne (op e0 e2) (op e2 e2))) % 11.27/11.44 (Ne (op e0 e2) (op e3 e2))) % 11.27/11.44 (Ne (op e1 e2) (op e2 e2))) % 11.27/11.44 (Ne (op e1 e2) (op e3 e2))) % 11.27/11.44 (Ne (op e2 e2) (op e3 e2))) % 11.27/11.44 (Ne (op e0 e3) (op e1 e3))) % 11.27/11.44 (Ne (op e0 e3) (op e2 e3))) % 11.27/11.44 (Ne (op e0 e3) (op e3 e3))) % 11.27/11.44 (Ne (op e1 e3) (op e2 e3))) % 11.27/11.44 (Ne (op e1 e3) (op e3 e3))) % 11.27/11.44 (Ne (op e2 e3) (op e3 e3))) % 11.27/11.44 (Ne (op e0 e0) (op e0 e1))) % 11.27/11.44 (Ne (op e0 e0) (op e0 e2))) % 11.27/11.44 (Ne (op e0 e0) (op e0 e3))) % 11.27/11.44 (Ne (op e0 e1) (op e0 e2))) % 11.27/11.44 (Ne (op e0 e1) (op e0 e3))) % 11.27/11.44 (Ne (op e0 e2) (op e0 e3))) % 11.27/11.44 (Ne (op e1 e0) (op e1 e1))) % 11.27/11.44 (Ne (op e1 e0) (op e1 e2))) % 11.27/11.44 (Ne (op e1 e0) (op e1 e3))) % 11.27/11.44 (Ne (op e1 e1) (op e1 e2))) % 11.27/11.44 (Ne (op e1 e1) (op e1 e3))) % 11.27/11.44 (Ne (op e1 e2) (op e1 e3))) % 11.27/11.44 (Ne (op e2 e0) (op e2 e1))) % 11.27/11.44 (Ne (op e2 e0) (op e2 e2))) % 11.27/11.44 True % 11.27/11.44 Clause #826 (by clausification #[758]): Eq % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (And % 11.27/11.44 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.27/11.44 (Eq (op e0 e3) e0)) % 11.27/11.44 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.27/11.44 (Eq (op e3 e0) e0))) % 11.27/11.44 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.27/11.45 (Eq (op e0 e3) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.27/11.45 (Eq (op e3 e0) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.27/11.45 (Eq (op e0 e3) e2))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.27/11.45 (Eq (op e3 e0) e2))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.27/11.45 (Eq (op e0 e3) e3))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) % 11.27/11.45 (Eq (op e3 e0) e3))) % 11.27/11.45 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) (Eq (op e1 e3) e0))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) (Eq (op e3 e1) e0))) % 11.27/11.45 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.27/11.45 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.27/11.45 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.27/11.45 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.27/11.45 (Or (Or (Or (Eq (op e2 e0) e2) (Eq (op e2 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e2 e3) e2))) % 11.27/11.45 True % 11.27/11.45 Clause #899 (by clausification #[798]): Eq % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And % 11.27/11.45 (And (Ne (op e0 e0) (op e1 e0)) % 11.27/11.45 (Ne (op e0 e0) (op e2 e0))) % 11.27/11.45 (Ne (op e0 e0) (op e3 e0))) % 11.31/11.47 (Ne (op e1 e0) (op e2 e0))) % 11.31/11.47 (Ne (op e1 e0) (op e3 e0))) % 11.31/11.47 (Ne (op e2 e0) (op e3 e0))) % 11.31/11.47 (Ne (op e0 e1) (op e1 e1))) % 11.31/11.47 (Ne (op e0 e1) (op e2 e1))) % 11.31/11.47 (Ne (op e0 e1) (op e3 e1))) % 11.31/11.47 (Ne (op e1 e1) (op e2 e1))) % 11.31/11.47 (Ne (op e1 e1) (op e3 e1))) % 11.31/11.47 (Ne (op e2 e1) (op e3 e1))) % 11.31/11.47 (Ne (op e0 e2) (op e1 e2))) % 11.31/11.47 (Ne (op e0 e2) (op e2 e2))) % 11.31/11.47 (Ne (op e0 e2) (op e3 e2))) % 11.31/11.47 (Ne (op e1 e2) (op e2 e2))) % 11.31/11.47 (Ne (op e1 e2) (op e3 e2))) % 11.31/11.47 (Ne (op e2 e2) (op e3 e2))) % 11.31/11.47 (Ne (op e0 e3) (op e1 e3))) % 11.31/11.47 (Ne (op e0 e3) (op e2 e3))) % 11.31/11.47 (Ne (op e0 e3) (op e3 e3))) % 11.31/11.47 (Ne (op e1 e3) (op e2 e3))) % 11.31/11.47 (Ne (op e1 e3) (op e3 e3))) % 11.31/11.47 (Ne (op e2 e3) (op e3 e3))) % 11.31/11.47 (Ne (op e0 e0) (op e0 e1))) % 11.31/11.47 (Ne (op e0 e0) (op e0 e2))) % 11.31/11.47 (Ne (op e0 e0) (op e0 e3))) % 11.31/11.47 (Ne (op e0 e1) (op e0 e2))) % 11.31/11.47 (Ne (op e0 e1) (op e0 e3))) % 11.31/11.47 (Ne (op e0 e2) (op e0 e3))) % 11.31/11.47 (Ne (op e1 e0) (op e1 e1))) % 11.31/11.47 (Ne (op e1 e0) (op e1 e2))) % 11.31/11.47 (Ne (op e1 e0) (op e1 e3))) % 11.31/11.47 (Ne (op e1 e1) (op e1 e2))) % 11.31/11.47 (Ne (op e1 e1) (op e1 e3))) % 11.31/11.47 (Ne (op e1 e2) (op e1 e3))) % 11.31/11.47 (Ne (op e2 e0) (op e2 e1))) % 11.31/11.47 True % 11.31/11.47 Clause #995 (by clausification #[826]): Eq % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (And % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.31/11.47 (Eq (op e0 e3) e0)) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.31/11.47 (Eq (op e3 e0) e0))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.31/11.47 (Eq (op e0 e3) e1))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.31/11.47 (Eq (op e3 e0) e1))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.31/11.47 (Eq (op e0 e3) e2))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.31/11.47 (Eq (op e3 e0) e2))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) % 11.31/11.47 (Eq (op e0 e3) e3))) % 11.31/11.47 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) (Eq (op e3 e0) e3))) % 11.31/11.47 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) (Eq (op e1 e3) e0))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) (Eq (op e3 e1) e0))) % 11.31/11.48 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.31/11.48 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.31/11.48 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.31/11.48 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.31/11.48 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.31/11.48 (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1))) % 11.31/11.48 True % 11.31/11.48 Clause #1067 (by clausification #[899]): Eq % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And % 11.31/11.48 (And (Ne (op e0 e0) (op e1 e0)) % 11.31/11.48 (Ne (op e0 e0) (op e2 e0))) % 11.31/11.48 (Ne (op e0 e0) (op e3 e0))) % 11.31/11.48 (Ne (op e1 e0) (op e2 e0))) % 11.31/11.48 (Ne (op e1 e0) (op e3 e0))) % 11.31/11.48 (Ne (op e2 e0) (op e3 e0))) % 11.31/11.48 (Ne (op e0 e1) (op e1 e1))) % 11.31/11.48 (Ne (op e0 e1) (op e2 e1))) % 11.31/11.48 (Ne (op e0 e1) (op e3 e1))) % 11.31/11.48 (Ne (op e1 e1) (op e2 e1))) % 11.31/11.48 (Ne (op e1 e1) (op e3 e1))) % 11.31/11.48 (Ne (op e2 e1) (op e3 e1))) % 11.31/11.48 (Ne (op e0 e2) (op e1 e2))) % 11.31/11.48 (Ne (op e0 e2) (op e2 e2))) % 11.31/11.48 (Ne (op e0 e2) (op e3 e2))) % 11.31/11.48 (Ne (op e1 e2) (op e2 e2))) % 11.31/11.48 (Ne (op e1 e2) (op e3 e2))) % 11.31/11.48 (Ne (op e2 e2) (op e3 e2))) % 11.31/11.50 (Ne (op e0 e3) (op e1 e3))) % 11.31/11.50 (Ne (op e0 e3) (op e2 e3))) % 11.31/11.50 (Ne (op e0 e3) (op e3 e3))) % 11.31/11.50 (Ne (op e1 e3) (op e2 e3))) % 11.31/11.50 (Ne (op e1 e3) (op e3 e3))) % 11.31/11.50 (Ne (op e2 e3) (op e3 e3))) % 11.31/11.50 (Ne (op e0 e0) (op e0 e1))) % 11.31/11.50 (Ne (op e0 e0) (op e0 e2))) % 11.31/11.50 (Ne (op e0 e0) (op e0 e3))) % 11.31/11.50 (Ne (op e0 e1) (op e0 e2))) % 11.31/11.50 (Ne (op e0 e1) (op e0 e3))) % 11.31/11.50 (Ne (op e0 e2) (op e0 e3))) % 11.31/11.50 (Ne (op e1 e0) (op e1 e1))) % 11.31/11.50 (Ne (op e1 e0) (op e1 e2))) % 11.31/11.50 (Ne (op e1 e0) (op e1 e3))) % 11.31/11.50 (Ne (op e1 e1) (op e1 e2))) % 11.31/11.50 (Ne (op e1 e1) (op e1 e3))) % 11.31/11.50 (Ne (op e1 e2) (op e1 e3))) % 11.31/11.50 True % 11.31/11.50 Clause #1157 (by clausification #[995]): Eq (Or (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e2) e1)) True % 11.31/11.50 Clause #1158 (by clausification #[995]): Eq % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (And % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.31/11.50 (Eq (op e0 e3) e0)) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.31/11.50 (Eq (op e3 e0) e0))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.31/11.50 (Eq (op e0 e3) e1))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.31/11.50 (Eq (op e3 e0) e1))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.31/11.50 (Eq (op e0 e3) e2))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) % 11.31/11.50 (Eq (op e3 e0) e2))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) (Eq (op e0 e3) e3))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) (Eq (op e3 e0) e3))) % 11.31/11.50 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) (Eq (op e1 e3) e0))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) (Eq (op e3 e1) e0))) % 11.31/11.50 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.31/11.50 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.31/11.50 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.31/11.50 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.31/11.50 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.31/11.50 (Or (Or (Or (Eq (op e2 e0) e1) (Eq (op e2 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e2 e3) e1))) % 11.31/11.50 True % 11.31/11.50 Clause #1159 (by clausification #[1157]): Or (Eq (Or (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) (Eq (op e2 e2) e1)) True) (Eq (Eq (op e3 e2) e1) True) % 11.31/11.52 Clause #1160 (by clausification #[1159]): Or (Eq (Eq (op e3 e2) e1) True) (Or (Eq (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) True) (Eq (Eq (op e2 e2) e1) True)) % 11.31/11.52 Clause #1161 (by clausification #[1160]): Or (Eq (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) True) (Or (Eq (Eq (op e2 e2) e1) True) (Eq (op e3 e2) e1)) % 11.31/11.52 Clause #1162 (by clausification #[1161]): Or (Eq (Eq (op e2 e2) e1) True) (Or (Eq (op e3 e2) e1) (Or (Eq (Eq (op e0 e2) e1) True) (Eq (Eq (op e1 e2) e1) True))) % 11.31/11.52 Clause #1163 (by clausification #[1162]): Or (Eq (op e3 e2) e1) (Or (Eq (Eq (op e0 e2) e1) True) (Or (Eq (Eq (op e1 e2) e1) True) (Eq (op e2 e2) e1))) % 11.31/11.52 Clause #1164 (by clausification #[1163]): Or (Eq (op e3 e2) e1) (Or (Eq (Eq (op e1 e2) e1) True) (Or (Eq (op e2 e2) e1) (Eq (op e0 e2) e1))) % 11.31/11.52 Clause #1165 (by clausification #[1164]): Or (Eq (op e3 e2) e1) (Or (Eq (op e2 e2) e1) (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1))) % 11.31/11.52 Clause #1166 (by forward demodulation #[1165, 168]): Or (Eq (op e3 e2) e1) (Or (Eq e2 e1) (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1))) % 11.31/11.52 Clause #1167 (by forward contextual literal cutting #[1166, 204]): Or (Eq (op e3 e2) e1) (Or (Eq (op e0 e2) e1) (Eq (op e1 e2) e1)) % 11.31/11.52 Clause #1169 (by superposition #[1167, 109]): Or (Eq (op e3 e2) e1) (Or (Eq (op e1 e2) e1) (Or (Ne e1 e1) (Ne e3 (op e1 e2)))) % 11.31/11.52 Clause #1173 (by superposition #[1167, 676]): Or (Eq (op e3 e2) e1) (Or (Eq (op e1 e2) e1) (Or (Eq e1 e3) (Eq (op e1 e2) e3))) % 11.31/11.52 Clause #1174 (by forward contextual literal cutting #[1173, 683]): Or (Eq (op e1 e2) e1) (Or (Eq e1 e3) (Eq (op e1 e2) e3)) % 11.31/11.52 Clause #1175 (by forward contextual literal cutting #[1174, 201]): Or (Eq (op e1 e2) e1) (Eq (op e1 e2) e3) % 11.31/11.52 Clause #1207 (by eliminate resolved literals #[1169]): Or (Eq (op e3 e2) e1) (Or (Eq (op e1 e2) e1) (Ne e3 (op e1 e2))) % 11.31/11.52 Clause #1208 (by forward contextual literal cutting #[1207, 1175]): Or (Eq (op e3 e2) e1) (Eq (op e1 e2) e1) % 11.31/11.52 Clause #1263 (by clausification #[1067]): Eq % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And % 11.31/11.52 (And (Ne (op e0 e0) (op e1 e0)) % 11.31/11.52 (Ne (op e0 e0) (op e2 e0))) % 11.31/11.52 (Ne (op e0 e0) (op e3 e0))) % 11.31/11.52 (Ne (op e1 e0) (op e2 e0))) % 11.31/11.52 (Ne (op e1 e0) (op e3 e0))) % 11.31/11.52 (Ne (op e2 e0) (op e3 e0))) % 11.31/11.52 (Ne (op e0 e1) (op e1 e1))) % 11.31/11.52 (Ne (op e0 e1) (op e2 e1))) % 11.31/11.52 (Ne (op e0 e1) (op e3 e1))) % 11.31/11.52 (Ne (op e1 e1) (op e2 e1))) % 11.39/11.54 (Ne (op e1 e1) (op e3 e1))) % 11.39/11.54 (Ne (op e2 e1) (op e3 e1))) % 11.39/11.54 (Ne (op e0 e2) (op e1 e2))) % 11.39/11.54 (Ne (op e0 e2) (op e2 e2))) % 11.39/11.54 (Ne (op e0 e2) (op e3 e2))) % 11.39/11.54 (Ne (op e1 e2) (op e2 e2))) % 11.39/11.54 (Ne (op e1 e2) (op e3 e2))) % 11.39/11.54 (Ne (op e2 e2) (op e3 e2))) % 11.39/11.54 (Ne (op e0 e3) (op e1 e3))) % 11.39/11.54 (Ne (op e0 e3) (op e2 e3))) % 11.39/11.54 (Ne (op e0 e3) (op e3 e3))) % 11.39/11.54 (Ne (op e1 e3) (op e2 e3))) % 11.39/11.54 (Ne (op e1 e3) (op e3 e3))) % 11.39/11.54 (Ne (op e2 e3) (op e3 e3))) % 11.39/11.54 (Ne (op e0 e0) (op e0 e1))) % 11.39/11.54 (Ne (op e0 e0) (op e0 e2))) % 11.39/11.54 (Ne (op e0 e0) (op e0 e3))) % 11.39/11.54 (Ne (op e0 e1) (op e0 e2))) % 11.39/11.54 (Ne (op e0 e1) (op e0 e3))) % 11.39/11.54 (Ne (op e0 e2) (op e0 e3))) % 11.39/11.54 (Ne (op e1 e0) (op e1 e1))) % 11.39/11.54 (Ne (op e1 e0) (op e1 e2))) % 11.39/11.54 (Ne (op e1 e0) (op e1 e3))) % 11.39/11.54 (Ne (op e1 e1) (op e1 e2))) % 11.39/11.54 (Ne (op e1 e1) (op e1 e3))) % 11.39/11.54 True % 11.39/11.54 Clause #1678 (by clausification #[1158]): Eq % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (And % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e0 e1) e0)) (Eq (op e0 e2) e0)) % 11.39/11.54 (Eq (op e0 e3) e0)) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e0) e0)) (Eq (op e2 e0) e0)) % 11.39/11.54 (Eq (op e3 e0) e0))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e0 e1) e1)) (Eq (op e0 e2) e1)) % 11.39/11.54 (Eq (op e0 e3) e1))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e1) (Eq (op e1 e0) e1)) (Eq (op e2 e0) e1)) % 11.39/11.54 (Eq (op e3 e0) e1))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e0 e1) e2)) (Eq (op e0 e2) e2)) % 11.39/11.54 (Eq (op e0 e3) e2))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e2) (Eq (op e1 e0) e2)) (Eq (op e2 e0) e2)) (Eq (op e3 e0) e2))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e0 e1) e3)) (Eq (op e0 e2) e3)) (Eq (op e0 e3) e3))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e0) e3) (Eq (op e1 e0) e3)) (Eq (op e2 e0) e3)) (Eq (op e3 e0) e3))) % 11.39/11.54 (Or (Or (Or (Eq (op e1 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e1 e2) e0)) (Eq (op e1 e3) e0))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e1) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e1) e0)) (Eq (op e3 e1) e0))) % 11.39/11.54 (Or (Or (Or (Eq (op e1 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e1 e2) e1)) (Eq (op e1 e3) e1))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e1) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e1) e1)) (Eq (op e3 e1) e1))) % 11.39/11.54 (Or (Or (Or (Eq (op e1 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e1 e2) e2)) (Eq (op e1 e3) e2))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e1) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e1) e2)) (Eq (op e3 e1) e2))) % 11.39/11.54 (Or (Or (Or (Eq (op e1 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e1 e2) e3)) (Eq (op e1 e3) e3))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e1) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e1) e3)) (Eq (op e3 e1) e3))) % 11.39/11.54 (Or (Or (Or (Eq (op e2 e0) e0) (Eq (op e2 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e2 e3) e0))) % 11.39/11.54 (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0))) % 11.39/11.54 True % 11.39/11.54 Clause #1700 (by clausification #[1263]): Eq (Ne (op e1 e1) (op e1 e3)) True % 11.39/11.55 Clause #1701 (by clausification #[1263]): Eq % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And % 11.39/11.55 (And (Ne (op e0 e0) (op e1 e0)) % 11.39/11.55 (Ne (op e0 e0) (op e2 e0))) % 11.39/11.55 (Ne (op e0 e0) (op e3 e0))) % 11.39/11.55 (Ne (op e1 e0) (op e2 e0))) % 11.39/11.55 (Ne (op e1 e0) (op e3 e0))) % 11.39/11.55 (Ne (op e2 e0) (op e3 e0))) % 11.39/11.55 (Ne (op e0 e1) (op e1 e1))) % 11.39/11.55 (Ne (op e0 e1) (op e2 e1))) % 11.39/11.55 (Ne (op e0 e1) (op e3 e1))) % 11.39/11.55 (Ne (op e1 e1) (op e2 e1))) % 11.39/11.55 (Ne (op e1 e1) (op e3 e1))) % 11.39/11.55 (Ne (op e2 e1) (op e3 e1))) % 11.39/11.55 (Ne (op e0 e2) (op e1 e2))) % 11.39/11.55 (Ne (op e0 e2) (op e2 e2))) % 11.39/11.55 (Ne (op e0 e2) (op e3 e2))) % 11.39/11.55 (Ne (op e1 e2) (op e2 e2))) % 11.39/11.55 (Ne (op e1 e2) (op e3 e2))) % 11.39/11.55 (Ne (op e2 e2) (op e3 e2))) % 11.39/11.55 (Ne (op e0 e3) (op e1 e3))) % 11.39/11.55 (Ne (op e0 e3) (op e2 e3))) % 11.39/11.55 (Ne (op e0 e3) (op e3 e3))) % 11.39/11.55 (Ne (op e1 e3) (op e2 e3))) % 11.39/11.55 (Ne (op e1 e3) (op e3 e3))) % 11.39/11.55 (Ne (op e2 e3) (op e3 e3))) % 11.39/11.55 (Ne (op e0 e0) (op e0 e1))) % 11.39/11.55 (Ne (op e0 e0) (op e0 e2))) % 11.39/11.55 (Ne (op e0 e0) (op e0 e3))) % 11.39/11.55 (Ne (op e0 e1) (op e0 e2))) % 11.39/11.55 (Ne (op e0 e1) (op e0 e3))) % 11.39/11.55 (Ne (op e0 e2) (op e0 e3))) % 11.39/11.55 (Ne (op e1 e0) (op e1 e1))) % 11.39/11.55 (Ne (op e1 e0) (op e1 e2))) % 11.39/11.55 (Ne (op e1 e0) (op e1 e3))) % 11.39/11.55 (Ne (op e1 e1) (op e1 e2))) % 11.39/11.55 True % 11.39/11.55 Clause #1702 (by clausification #[1700]): Ne (op e1 e1) (op e1 e3) % 11.39/11.55 Clause #1703 (by forward demodulation #[1702, 197]): Ne e1 (op e1 e3) % 11.39/11.55 Clause #1715 (by backward contextual literal cutting #[1703, 526]): Eq (op e1 e3) e2 % 11.39/11.55 Clause #1716 (by backward contextual literal cutting #[1703, 530]): Eq (op e2 e3) e1 % 11.39/11.55 Clause #1719 (by backward demodulation #[1716, 447]): Or (Eq e1 e0) (Or (Eq (op e0 e3) e0) (Eq (op e1 e3) e0)) % 11.39/11.55 Clause #1837 (by forward demodulation #[1719, 1715]): Or (Eq e1 e0) (Or (Eq (op e0 e3) e0) (Eq e2 e0)) % 11.39/11.55 Clause #1838 (by forward contextual literal cutting #[1837, 215]): Or (Eq (op e0 e3) e0) (Eq e2 e0) % 11.42/11.57 Clause #1839 (by forward contextual literal cutting #[1838, 214]): Eq (op e0 e3) e0 % 11.42/11.57 Clause #2190 (by clausification #[1678]): Eq (Or (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e2) e0)) True % 11.42/11.57 Clause #2192 (by clausification #[2190]): Or (Eq (Or (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) (Eq (op e2 e2) e0)) True) (Eq (Eq (op e3 e2) e0) True) % 11.42/11.57 Clause #2193 (by clausification #[2192]): Or (Eq (Eq (op e3 e2) e0) True) (Or (Eq (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) True) (Eq (Eq (op e2 e2) e0) True)) % 11.42/11.57 Clause #2194 (by clausification #[2193]): Or (Eq (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) True) (Or (Eq (Eq (op e2 e2) e0) True) (Eq (op e3 e2) e0)) % 11.42/11.57 Clause #2195 (by clausification #[2194]): Or (Eq (Eq (op e2 e2) e0) True) (Or (Eq (op e3 e2) e0) (Or (Eq (Eq (op e0 e2) e0) True) (Eq (Eq (op e1 e2) e0) True))) % 11.42/11.57 Clause #2196 (by clausification #[2195]): Or (Eq (op e3 e2) e0) (Or (Eq (Eq (op e0 e2) e0) True) (Or (Eq (Eq (op e1 e2) e0) True) (Eq (op e2 e2) e0))) % 11.42/11.57 Clause #2197 (by clausification #[2196]): Or (Eq (op e3 e2) e0) (Or (Eq (Eq (op e1 e2) e0) True) (Or (Eq (op e2 e2) e0) (Eq (op e0 e2) e0))) % 11.42/11.57 Clause #2198 (by clausification #[2197]): Or (Eq (op e3 e2) e0) (Or (Eq (op e2 e2) e0) (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0))) % 11.42/11.57 Clause #2199 (by forward demodulation #[2198, 168]): Or (Eq (op e3 e2) e0) (Or (Eq e2 e0) (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0))) % 11.42/11.57 Clause #2200 (by forward contextual literal cutting #[2199, 214]): Or (Eq (op e3 e2) e0) (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 11.42/11.57 Clause #2227 (by clausification #[1701]): Eq (Ne (op e1 e1) (op e1 e2)) True % 11.42/11.57 Clause #2228 (by clausification #[1701]): Eq % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And % 11.42/11.57 (And (Ne (op e0 e0) (op e1 e0)) % 11.42/11.57 (Ne (op e0 e0) (op e2 e0))) % 11.42/11.57 (Ne (op e0 e0) (op e3 e0))) % 11.42/11.57 (Ne (op e1 e0) (op e2 e0))) % 11.42/11.57 (Ne (op e1 e0) (op e3 e0))) % 11.42/11.57 (Ne (op e2 e0) (op e3 e0))) % 11.42/11.57 (Ne (op e0 e1) (op e1 e1))) % 11.42/11.57 (Ne (op e0 e1) (op e2 e1))) % 11.42/11.57 (Ne (op e0 e1) (op e3 e1))) % 11.42/11.57 (Ne (op e1 e1) (op e2 e1))) % 11.42/11.57 (Ne (op e1 e1) (op e3 e1))) % 11.42/11.57 (Ne (op e2 e1) (op e3 e1))) % 11.42/11.57 (Ne (op e0 e2) (op e1 e2))) % 11.42/11.57 (Ne (op e0 e2) (op e2 e2))) % 11.42/11.57 (Ne (op e0 e2) (op e3 e2))) % 11.42/11.58 (Ne (op e1 e2) (op e2 e2))) % 11.42/11.58 (Ne (op e1 e2) (op e3 e2))) % 11.42/11.58 (Ne (op e2 e2) (op e3 e2))) % 11.42/11.58 (Ne (op e0 e3) (op e1 e3))) % 11.42/11.58 (Ne (op e0 e3) (op e2 e3))) % 11.42/11.58 (Ne (op e0 e3) (op e3 e3))) % 11.42/11.58 (Ne (op e1 e3) (op e2 e3))) % 11.42/11.58 (Ne (op e1 e3) (op e3 e3))) % 11.42/11.58 (Ne (op e2 e3) (op e3 e3))) % 11.42/11.58 (Ne (op e0 e0) (op e0 e1))) % 11.42/11.58 (Ne (op e0 e0) (op e0 e2))) % 11.42/11.58 (Ne (op e0 e0) (op e0 e3))) % 11.42/11.58 (Ne (op e0 e1) (op e0 e2))) % 11.42/11.58 (Ne (op e0 e1) (op e0 e3))) % 11.42/11.58 (Ne (op e0 e2) (op e0 e3))) % 11.42/11.58 (Ne (op e1 e0) (op e1 e1))) % 11.42/11.58 (Ne (op e1 e0) (op e1 e2))) % 11.42/11.58 (Ne (op e1 e0) (op e1 e3))) % 11.42/11.58 True % 11.42/11.58 Clause #2229 (by clausification #[2227]): Ne (op e1 e1) (op e1 e2) % 11.42/11.58 Clause #2230 (by forward demodulation #[2229, 197]): Ne e1 (op e1 e2) % 11.42/11.58 Clause #2238 (by backward contextual literal cutting #[2230, 1175]): Eq (op e1 e2) e3 % 11.42/11.58 Clause #2239 (by backward contextual literal cutting #[2230, 1208]): Eq (op e3 e2) e1 % 11.42/11.58 Clause #2258 (by backward demodulation #[2239, 2200]): Or (Eq e1 e0) (Or (Eq (op e0 e2) e0) (Eq (op e1 e2) e0)) % 11.42/11.58 Clause #2348 (by forward demodulation #[2258, 2238]): Or (Eq e1 e0) (Or (Eq (op e0 e2) e0) (Eq e3 e0)) % 11.42/11.58 Clause #2349 (by forward contextual literal cutting #[2348, 215]): Or (Eq (op e0 e2) e0) (Eq e3 e0) % 11.42/11.58 Clause #2350 (by forward contextual literal cutting #[2349, 207]): Eq (op e0 e2) e0 % 11.42/11.58 Clause #2389 (by clausification #[2228]): Eq % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And % 11.42/11.58 (And (Ne (op e0 e0) (op e1 e0)) % 11.42/11.58 (Ne (op e0 e0) (op e2 e0))) % 11.42/11.58 (Ne (op e0 e0) (op e3 e0))) % 11.42/11.58 (Ne (op e1 e0) (op e2 e0))) % 11.42/11.58 (Ne (op e1 e0) (op e3 e0))) % 11.42/11.58 (Ne (op e2 e0) (op e3 e0))) % 11.42/11.58 (Ne (op e0 e1) (op e1 e1))) % 11.42/11.58 (Ne (op e0 e1) (op e2 e1))) % 11.42/11.58 (Ne (op e0 e1) (op e3 e1))) % 11.42/11.58 (Ne (op e1 e1) (op e2 e1))) % 11.42/11.58 (Ne (op e1 e1) (op e3 e1))) % 11.42/11.58 (Ne (op e2 e1) (op e3 e1))) % 11.42/11.58 (Ne (op e0 e2) (op e1 e2))) % 11.42/11.58 (Ne (op e0 e2) (op e2 e2))) % 11.42/11.58 (Ne (op e0 e2) (op e3 e2))) % 11.42/11.58 (Ne (op e1 e2) (op e2 e2))) % 11.42/11.58 (Ne (op e1 e2) (op e3 e2))) % 11.42/11.58 (Ne (op e2 e2) (op e3 e2))) % 11.42/11.60 (Ne (op e0 e3) (op e1 e3))) % 11.42/11.60 (Ne (op e0 e3) (op e2 e3))) % 11.42/11.60 (Ne (op e0 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e1 e3) (op e2 e3))) % 11.42/11.60 (Ne (op e1 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e2 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e1))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e2))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e3))) % 11.42/11.60 (Ne (op e0 e1) (op e0 e2))) % 11.42/11.60 (Ne (op e0 e1) (op e0 e3))) % 11.42/11.60 (Ne (op e0 e2) (op e0 e3))) % 11.42/11.60 (Ne (op e1 e0) (op e1 e1))) % 11.42/11.60 (Ne (op e1 e0) (op e1 e2))) % 11.42/11.60 True % 11.42/11.60 Clause #2422 (by clausification #[2389]): Eq % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And (Ne (op e0 e0) (op e1 e0)) (Ne (op e0 e0) (op e2 e0))) % 11.42/11.60 (Ne (op e0 e0) (op e3 e0))) % 11.42/11.60 (Ne (op e1 e0) (op e2 e0))) % 11.42/11.60 (Ne (op e1 e0) (op e3 e0))) % 11.42/11.60 (Ne (op e2 e0) (op e3 e0))) % 11.42/11.60 (Ne (op e0 e1) (op e1 e1))) % 11.42/11.60 (Ne (op e0 e1) (op e2 e1))) % 11.42/11.60 (Ne (op e0 e1) (op e3 e1))) % 11.42/11.60 (Ne (op e1 e1) (op e2 e1))) % 11.42/11.60 (Ne (op e1 e1) (op e3 e1))) % 11.42/11.60 (Ne (op e2 e1) (op e3 e1))) % 11.42/11.60 (Ne (op e0 e2) (op e1 e2))) % 11.42/11.60 (Ne (op e0 e2) (op e2 e2))) % 11.42/11.60 (Ne (op e0 e2) (op e3 e2))) % 11.42/11.60 (Ne (op e1 e2) (op e2 e2))) % 11.42/11.60 (Ne (op e1 e2) (op e3 e2))) % 11.42/11.60 (Ne (op e2 e2) (op e3 e2))) % 11.42/11.60 (Ne (op e0 e3) (op e1 e3))) % 11.42/11.60 (Ne (op e0 e3) (op e2 e3))) % 11.42/11.60 (Ne (op e0 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e1 e3) (op e2 e3))) % 11.42/11.60 (Ne (op e1 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e2 e3) (op e3 e3))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e1))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e2))) % 11.42/11.60 (Ne (op e0 e0) (op e0 e3))) % 11.42/11.60 (Ne (op e0 e1) (op e0 e2))) % 11.42/11.60 (Ne (op e0 e1) (op e0 e3))) % 11.42/11.60 (Ne (op e0 e2) (op e0 e3))) % 11.42/11.60 (Ne (op e1 e0) (op e1 e1))) % 11.42/11.60 True % 11.42/11.60 Clause #2456 (by clausification #[2422]): Eq % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.60 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And % 11.42/11.61 (And (And (Ne (op e0 e0) (op e1 e0)) (Ne (op e0 e0) (op e2 e0))) % 11.42/11.61 (Ne (op e0 e0) (op e3 e0))) % 11.42/11.61 (Ne (op e1 e0) (op e2 e0))) % 11.42/11.61 (Ne (op e1 e0) (op e3 e0))) % 11.42/11.61 (Ne (op e2 e0) (op e3 e0))) % 11.42/11.61 (Ne (op e0 e1) (op e1 e1))) % 11.42/11.61 (Ne (op e0 e1) (op e2 e1))) % 11.42/11.61 (Ne (op e0 e1) (op e3 e1))) % 11.42/11.61 (Ne (op e1 e1) (op e2 e1))) % 11.42/11.61 (Ne (op e1 e1) (op e3 e1))) % 11.42/11.61 (Ne (op e2 e1) (op e3 e1))) % 11.42/11.61 (Ne (op e0 e2) (op e1 e2))) % 11.42/11.61 (Ne (op e0 e2) (op e2 e2))) % 11.42/11.61 (Ne (op e0 e2) (op e3 e2))) % 11.42/11.61 (Ne (op e1 e2) (op e2 e2))) % 11.42/11.61 (Ne (op e1 e2) (op e3 e2))) % 11.42/11.61 (Ne (op e2 e2) (op e3 e2))) % 11.42/11.61 (Ne (op e0 e3) (op e1 e3))) % 11.42/11.61 (Ne (op e0 e3) (op e2 e3))) % 11.42/11.61 (Ne (op e0 e3) (op e3 e3))) % 11.42/11.61 (Ne (op e1 e3) (op e2 e3))) % 11.42/11.61 (Ne (op e1 e3) (op e3 e3))) % 11.42/11.61 (Ne (op e2 e3) (op e3 e3))) % 11.42/11.61 (Ne (op e0 e0) (op e0 e1))) % 11.42/11.61 (Ne (op e0 e0) (op e0 e2))) % 11.42/11.61 (Ne (op e0 e0) (op e0 e3))) % 11.42/11.61 (Ne (op e0 e1) (op e0 e2))) % 11.42/11.61 (Ne (op e0 e1) (op e0 e3))) % 11.42/11.61 (Ne (op e0 e2) (op e0 e3))) % 11.42/11.61 True % 11.42/11.61 Clause #2460 (by clausification #[2456]): Eq (Ne (op e0 e2) (op e0 e3)) True % 11.42/11.61 Clause #2462 (by clausification #[2460]): Ne (op e0 e2) (op e0 e3) % 11.42/11.61 Clause #2463 (by forward demodulation #[2462, 2350]): Ne e0 (op e0 e3) % 11.42/11.61 Clause #2464 (by forward demodulation #[2463, 1839]): Ne e0 e0 % 11.42/11.61 Clause #2465 (by eliminate resolved literals #[2464]): False % 11.42/11.61 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------