%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG017+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:43:54 PM UTC 2025 % Result : Theorem 6.23s 6.42s % Output : Proof 6.31s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ALG017+1 : TPTP v9.2.0. Released v2.7.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n007.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Fri Oct 3 09:20:08 EDT 2025 % 0.13/0.34 % CPUTime : % 6.23/6.42 SZS status Theorem for theBenchmark.p % 6.23/6.42 SZS output start Proof for theBenchmark.p % 6.23/6.42 Clause #9 (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 % 6.23/6.42 Clause #10 (by assumption #[]): Eq (And (Eq e0 (op e3 e3)) (Eq e1 (op e2 e3))) True % 6.23/6.42 Clause #11 (by assumption #[]): Eq % 6.23/6.42 (Not % 6.23/6.42 (Not % 6.23/6.42 (And % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 6.23/6.42 (Not % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))))))) % 6.23/6.42 True % 6.23/6.42 Clause #14 (by clausification #[10]): Eq (Eq e0 (op e3 e3)) True % 6.23/6.42 Clause #16 (by clausification #[14]): Eq e0 (op e3 e3) % 6.23/6.42 Clause #40 (by clausification #[9]): Eq (And (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) (Ne e1 e3)) True % 6.23/6.42 Clause #43 (by clausification #[40]): Eq (And (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) (Ne e1 e2)) True % 6.23/6.42 Clause #46 (by clausification #[43]): Eq (And (And (Ne e0 e1) (Ne e0 e2)) (Ne e0 e3)) True % 6.23/6.42 Clause #53 (by clausification #[46]): Eq (Ne e0 e3) True % 6.23/6.42 Clause #54 (by clausification #[46]): Eq (And (Ne e0 e1) (Ne e0 e2)) True % 6.23/6.42 Clause #55 (by clausification #[53]): Ne e0 e3 % 6.23/6.42 Clause #56 (by clausification #[54]): Eq (Ne e0 e2) True % 6.23/6.42 Clause #57 (by clausification #[54]): Eq (Ne e0 e1) True % 6.23/6.42 Clause #58 (by clausification #[56]): Ne e0 e2 % 6.23/6.42 Clause #59 (by clausification #[57]): Ne e0 e1 % 6.23/6.42 Clause #120 (by clausification #[11]): Eq % 6.23/6.42 (Not % 6.23/6.42 (And % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 6.23/6.42 (Not % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))))) % 6.23/6.42 False % 6.23/6.42 Clause #121 (by clausification #[120]): Eq % 6.23/6.42 (And % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 6.23/6.42 (Not % 6.23/6.42 (Or % 6.23/6.42 (Or % 6.23/6.42 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.42 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))))) % 6.23/6.42 True % 6.23/6.42 Clause #122 (by clausification #[121]): Eq % 6.23/6.45 (Not % 6.23/6.45 (Or % 6.23/6.45 (Or % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)))) % 6.23/6.45 True % 6.23/6.45 Clause #123 (by clausification #[121]): Eq % 6.23/6.45 (Or % 6.23/6.45 (Or % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 6.23/6.45 True % 6.23/6.45 Clause #124 (by clausification #[122]): Eq % 6.23/6.45 (Or % 6.23/6.45 (Or % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3))) % 6.23/6.45 False % 6.23/6.45 Clause #126 (by clausification #[124]): Eq % 6.23/6.45 (Or % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.45 False % 6.23/6.45 Clause #216 (by clausification #[123]): Or % 6.23/6.45 (Eq % 6.23/6.45 (Or % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2))) % 6.23/6.45 True) % 6.23/6.45 (Eq (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)) True) % 6.23/6.45 Clause #217 (by clausification #[216]): Or (Eq (And (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) (Eq (op e3 e3) e3)) True) % 6.23/6.45 (Or % 6.23/6.45 (Eq % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 True) % 6.23/6.45 (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True)) % 6.23/6.45 Clause #218 (by clausification #[217]): Or % 6.23/6.45 (Eq % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 True) % 6.23/6.45 (Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 6.23/6.45 (Eq (Eq (op e3 e3) e3) True)) % 6.23/6.45 Clause #219 (by clausification #[217]): Or % 6.23/6.45 (Eq % 6.23/6.45 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.45 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.45 True) % 6.23/6.45 (Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 6.23/6.45 (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True)) % 6.23/6.45 Clause #220 (by clausification #[218]): Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 6.23/6.45 (Or (Eq (Eq (op e3 e3) e3) True) % 6.23/6.45 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.45 (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True))) % 6.23/6.45 Clause #221 (by clausification #[220]): Or (Eq (Eq (op e3 e3) e3) True) % 6.23/6.45 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Eq (Eq (op e3 e3) e2) True))) % 6.23/6.48 Clause #223 (by clausification #[221]): Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (op e3 e3) e3))) % 6.23/6.48 Clause #225 (by clausification #[223]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Or (Eq (Eq (op e3 e3) e2) True) % 6.23/6.48 (Or (Eq (op e3 e3) e3) (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True))) % 6.23/6.48 Clause #228 (by clausification #[126]): Eq % 6.23/6.48 (Or (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) % 6.23/6.48 (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1))) % 6.23/6.48 False % 6.23/6.48 Clause #331 (by clausification #[219]): Or (Eq (And (And (And (Eq (op e0 e0) e2) (Eq (op e1 e1) e2)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e2)) True) % 6.23/6.48 (Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.48 (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True))) % 6.23/6.48 Clause #332 (by clausification #[331]): Or (Eq (And (And (Eq (op e0 e0) e3) (Eq (op e1 e1) e3)) (Eq (op e2 e2) e3)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Eq (Eq (op e3 e3) e2) True))) % 6.23/6.48 Clause #334 (by clausification #[332]): Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) True) % 6.23/6.48 (Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Or (Eq (Eq (op e3 e3) e2) True) (Eq (Eq (op e2 e2) e3) True))) % 6.23/6.48 Clause #337 (by clausification #[334]): Or (Eq (And (And (And (Eq (op e0 e0) e1) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e1)) (Eq (op e3 e3) e1)) True) % 6.23/6.48 (Or (Eq (Eq (op e3 e3) e2) True) % 6.23/6.48 (Or (Eq (Eq (op e2 e2) e3) True) (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True))) % 6.23/6.48 Clause #372 (by clausification #[225]): Or (Eq (Eq (op e3 e3) e2) True) % 6.23/6.48 (Or (Eq (op e3 e3) e3) % 6.23/6.48 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) (Eq (Eq (op e3 e3) e1) True))) % 6.23/6.48 Clause #374 (by clausification #[372]): Or (Eq (op e3 e3) e3) % 6.23/6.48 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 6.23/6.48 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (op e3 e3) e2))) % 6.23/6.48 Clause #375 (by clausification #[374]): Or (Eq (op e3 e3) e3) (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (op e3 e3) e2) (Eq (Eq (op e2 e2) e0) True))) % 6.23/6.48 Clause #377 (by clausification #[375]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (Eq (op e2 e2) e0) True) (Eq (op e3 e3) e1))) % 6.23/6.48 Clause #378 (by clausification #[377]): Or (Eq (op e3 e3) e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e1) (Eq (op e2 e2) e0))) % 6.23/6.48 Clause #379 (by forward demodulation #[378, 16]): Or (Eq e0 e3) (Or (Eq (op e3 e3) e2) (Or (Eq (op e3 e3) e1) (Eq (op e2 e2) e0))) % 6.23/6.48 Clause #380 (by forward demodulation #[379, 16]): Or (Eq e0 e3) (Or (Eq e0 e2) (Or (Eq (op e3 e3) e1) (Eq (op e2 e2) e0))) % 6.23/6.48 Clause #381 (by forward demodulation #[380, 16]): Or (Eq e0 e3) (Or (Eq e0 e2) (Or (Eq e0 e1) (Eq (op e2 e2) e0))) % 6.23/6.48 Clause #382 (by forward contextual literal cutting #[381, 55]): Or (Eq e0 e2) (Or (Eq e0 e1) (Eq (op e2 e2) e0)) % 6.23/6.48 Clause #383 (by forward contextual literal cutting #[382, 58]): Or (Eq e0 e1) (Eq (op e2 e2) e0) % 6.23/6.48 Clause #384 (by forward contextual literal cutting #[383, 59]): Eq (op e2 e2) e0 % 6.23/6.48 Clause #414 (by clausification #[228]): Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) (Eq (op e3 e3) e0)) False % 6.31/6.51 Clause #599 (by clausification #[337]): Or (Eq (Eq (op e3 e3) e2) True) % 6.31/6.51 (Or (Eq (Eq (op e2 e2) e3) True) % 6.31/6.51 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) (Eq (Eq (op e3 e3) e1) True))) % 6.31/6.51 Clause #601 (by clausification #[599]): Or (Eq (Eq (op e2 e2) e3) True) % 6.31/6.51 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 6.31/6.51 (Or (Eq (Eq (op e3 e3) e1) True) (Eq (op e3 e3) e2))) % 6.31/6.51 Clause #602 (by clausification #[601]): Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) True) % 6.31/6.51 (Or (Eq (Eq (op e3 e3) e1) True) (Or (Eq (op e3 e3) e2) (Eq (op e2 e2) e3))) % 6.31/6.51 Clause #604 (by clausification #[602]): Or (Eq (Eq (op e3 e3) e1) True) % 6.31/6.51 (Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e3) (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True))) % 6.31/6.51 Clause #632 (by clausification #[414]): Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) (Eq (op e2 e2) e0)) False) (Eq (Eq (op e3 e3) e0) False) % 6.31/6.51 Clause #633 (by clausification #[632]): Or (Eq (Eq (op e3 e3) e0) False) % 6.31/6.51 (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) False) (Eq (Eq (op e2 e2) e0) False)) % 6.31/6.51 Clause #634 (by clausification #[633]): Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) False) (Or (Eq (Eq (op e2 e2) e0) False) (Ne (op e3 e3) e0)) % 6.31/6.51 Clause #635 (by clausification #[634]): Or (Eq (Eq (op e2 e2) e0) False) % 6.31/6.51 (Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e0 e0) e0) False) (Eq (Eq (op e1 e1) e0) False))) % 6.31/6.51 Clause #636 (by clausification #[635]): Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e0 e0) e0) False) (Or (Eq (Eq (op e1 e1) e0) False) (Ne (op e2 e2) e0))) % 6.31/6.51 Clause #637 (by clausification #[636]): Or (Ne (op e3 e3) e0) (Or (Eq (Eq (op e1 e1) e0) False) (Or (Ne (op e2 e2) e0) (Ne (op e0 e0) e0))) % 6.31/6.51 Clause #638 (by clausification #[637]): Or (Ne (op e3 e3) e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 6.31/6.51 Clause #639 (by forward demodulation #[638, 16]): Or (Ne e0 e0) (Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0))) % 6.31/6.51 Clause #640 (by eliminate resolved literals #[639]): Or (Ne (op e2 e2) e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 6.31/6.51 Clause #641 (by forward demodulation #[640, 384]): Or (Ne e0 e0) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0)) % 6.31/6.51 Clause #642 (by eliminate resolved literals #[641]): Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e0) % 6.31/6.51 Clause #658 (by clausification #[604]): Or (Eq (op e3 e3) e2) % 6.31/6.51 (Or (Eq (op e2 e2) e3) (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e0)) True) (Eq (op e3 e3) e1))) % 6.31/6.51 Clause #659 (by clausification #[658]): Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (Eq (op e1 e1) e0) True))) % 6.31/6.51 Clause #660 (by clausification #[658]): Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (Eq (op e0 e0) e0) True))) % 6.31/6.51 Clause #661 (by clausification #[659]): Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (op e1 e1) e0))) % 6.31/6.51 Clause #662 (by forward demodulation #[661, 16]): Or (Eq e0 e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (op e1 e1) e0))) % 6.31/6.51 Clause #663 (by forward demodulation #[662, 16]): Or (Eq e0 e2) (Or (Eq (op e2 e2) e3) (Or (Eq e0 e1) (Eq (op e1 e1) e0))) % 6.31/6.51 Clause #664 (by forward contextual literal cutting #[663, 58]): Or (Eq (op e2 e2) e3) (Or (Eq e0 e1) (Eq (op e1 e1) e0)) % 6.31/6.51 Clause #665 (by forward contextual literal cutting #[664, 59]): Or (Eq (op e2 e2) e3) (Eq (op e1 e1) e0) % 6.31/6.51 Clause #666 (by superposition #[665, 384]): Or (Eq (op e1 e1) e0) (Eq e3 e0) % 6.31/6.51 Clause #667 (by forward contextual literal cutting #[666, 55]): Eq (op e1 e1) e0 % 6.31/6.51 Clause #671 (by backward contextual literal cutting #[667, 642]): Ne (op e0 e0) e0 % 6.31/6.51 Clause #858 (by clausification #[660]): Or (Eq (op e3 e3) e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e0))) % 6.31/6.51 Clause #859 (by forward demodulation #[858, 16]): Or (Eq e0 e2) (Or (Eq (op e2 e2) e3) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e0))) % 6.31/6.51 Clause #860 (by forward demodulation #[859, 384]): Or (Eq e0 e2) (Or (Eq e0 e3) (Or (Eq (op e3 e3) e1) (Eq (op e0 e0) e0))) % 6.31/6.51 Clause #861 (by forward demodulation #[860, 16]): Or (Eq e0 e2) (Or (Eq e0 e3) (Or (Eq e0 e1) (Eq (op e0 e0) e0))) % 6.31/6.51 Clause #862 (by forward contextual literal cutting #[861, 58]): Or (Eq e0 e3) (Or (Eq e0 e1) (Eq (op e0 e0) e0)) % 6.31/6.51 Clause #863 (by forward contextual literal cutting #[862, 55]): Or (Eq e0 e1) (Eq (op e0 e0) e0) % 6.31/6.51 Clause #864 (by forward contextual literal cutting #[863, 59]): Eq (op e0 e0) e0 % 6.31/6.51 Clause #865 (by forward contextual literal cutting #[864, 671]): False % 6.31/6.51 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------