%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG194+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:06 PM UTC 2025 % Result : Theorem 5.25s 5.43s % Output : Proof 5.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : ALG194+1 : TPTP v9.2.0. Released v2.7.0. % 0.12/0.13 % Command : duper %s % 0.13/0.34 % Computer : n026.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:39:53 EDT 2025 % 0.13/0.34 % CPUTime : % 5.25/5.43 SZS status Theorem for theBenchmark.p % 5.25/5.43 SZS output start Proof for theBenchmark.p % 5.25/5.43 Clause #5 (by assumption #[]): Eq % 5.25/5.43 (Not % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6))) % 5.25/5.43 (And % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6)) % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6))))) % 5.25/5.43 True % 5.25/5.43 Clause #102 (by clausification #[5]): Eq % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6))) % 5.25/5.43 (And % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6)) % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)))) % 5.25/5.43 False % 5.25/5.43 Clause #103 (by clausification #[102]): Eq % 5.25/5.43 (And % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6)) % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6))) % 5.25/5.43 False % 5.25/5.43 Clause #104 (by clausification #[102]): Eq % 5.25/5.43 (Or % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 (And % 5.25/5.43 (And % 5.25/5.43 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6))) % 5.25/5.43 False % 5.25/5.43 Clause #105 (by clausification #[103]): Or % 5.25/5.43 (Eq % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.43 (Eq (op e4 e4) e4)) % 5.25/5.43 (Eq (op e5 e5) e5)) % 5.25/5.43 (Eq (op e6 e6) e6)) % 5.25/5.43 False) % 5.25/5.43 (Eq % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 False) % 5.25/5.43 Clause #106 (by clausification #[105]): Or % 5.25/5.43 (Eq % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 False) % 5.25/5.43 (Eq (Eq (op e6 e6) e6) False) % 5.25/5.43 Clause #107 (by clausification #[105]): Or % 5.25/5.43 (Eq % 5.25/5.43 (Or % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.43 (Ne (op e4 e4) e4)) % 5.25/5.43 (Ne (op e5 e5) e5)) % 5.25/5.43 (Ne (op e6 e6) e6)) % 5.25/5.43 False) % 5.25/5.43 (Eq % 5.25/5.43 (Or % 5.25/5.43 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) (Eq (op e4 e4) e4)) % 5.25/5.46 (Eq (op e5 e5) e5)) % 5.25/5.46 False) % 5.25/5.46 Clause #109 (by clausification #[106]): Or (Eq (Eq (op e6 e6) e6) False) % 5.25/5.46 (Eq % 5.25/5.46 (Or % 5.25/5.46 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) (Ne (op e4 e4) e4)) % 5.25/5.46 (Ne (op e5 e5) e5)) % 5.25/5.46 False) % 5.25/5.46 Clause #122 (by clausification #[109]): Or % 5.25/5.46 (Eq % 5.25/5.46 (Or % 5.25/5.46 (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) (Ne (op e4 e4) e4)) % 5.25/5.46 (Ne (op e5 e5) e5)) % 5.25/5.46 False) % 5.25/5.46 (Ne (op e6 e6) e6) % 5.25/5.46 Clause #123 (by clausification #[122]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e5 e5) e5) False) % 5.25/5.46 Clause #124 (by clausification #[122]): Or (Ne (op e6 e6) e6) % 5.25/5.46 (Eq (Or (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) (Ne (op e4 e4) e4)) % 5.25/5.46 False) % 5.25/5.46 Clause #125 (by clausification #[123]): Or (Ne (op e6 e6) e6) (Eq (op e5 e5) e5) % 5.25/5.46 Clause #166 (by clausification #[124]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e4 e4) e4) False) % 5.25/5.46 Clause #167 (by clausification #[124]): Or (Ne (op e6 e6) e6) % 5.25/5.46 (Eq (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) False) % 5.25/5.46 Clause #168 (by clausification #[166]): Or (Ne (op e6 e6) e6) (Eq (op e4 e4) e4) % 5.25/5.46 Clause #176 (by clausification #[167]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e3 e3) e3) False) % 5.25/5.46 Clause #177 (by clausification #[167]): Or (Ne (op e6 e6) e6) (Eq (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) False) % 5.25/5.46 Clause #178 (by clausification #[176]): Or (Ne (op e6 e6) e6) (Eq (op e3 e3) e3) % 5.25/5.46 Clause #180 (by clausification #[177]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e2 e2) e2) False) % 5.25/5.46 Clause #181 (by clausification #[177]): Or (Ne (op e6 e6) e6) (Eq (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) False) % 5.25/5.46 Clause #182 (by clausification #[180]): Or (Ne (op e6 e6) e6) (Eq (op e2 e2) e2) % 5.25/5.46 Clause #184 (by clausification #[181]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e1 e1) e1) False) % 5.25/5.46 Clause #185 (by clausification #[181]): Or (Ne (op e6 e6) e6) (Eq (Ne (op e0 e0) e0) False) % 5.25/5.46 Clause #186 (by clausification #[184]): Or (Ne (op e6 e6) e6) (Eq (op e1 e1) e1) % 5.25/5.46 Clause #191 (by clausification #[185]): Or (Ne (op e6 e6) e6) (Eq (op e0 e0) e0) % 5.25/5.46 Clause #193 (by clausification #[104]): Eq % 5.25/5.46 (And % 5.25/5.46 (And % 5.25/5.46 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.46 (Eq (op e4 e4) e4)) % 5.25/5.46 (Eq (op e5 e5) e5)) % 5.25/5.46 (Eq (op e6 e6) e6)) % 5.25/5.46 False % 5.25/5.46 Clause #194 (by clausification #[104]): Eq % 5.25/5.46 (And % 5.25/5.46 (And % 5.25/5.46 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.25/5.46 (Ne (op e4 e4) e4)) % 5.25/5.46 (Ne (op e5 e5) e5)) % 5.25/5.46 (Ne (op e6 e6) e6)) % 5.25/5.46 False % 5.25/5.46 Clause #195 (by clausification #[193]): Or % 5.25/5.46 (Eq % 5.25/5.46 (And % 5.25/5.46 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.46 (Eq (op e4 e4) e4)) % 5.25/5.46 (Eq (op e5 e5) e5)) % 5.25/5.46 False) % 5.25/5.46 (Eq (Eq (op e6 e6) e6) False) % 5.25/5.46 Clause #196 (by clausification #[195]): Or (Eq (Eq (op e6 e6) e6) False) % 5.25/5.46 (Or % 5.25/5.46 (Eq % 5.25/5.46 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.46 (Eq (op e4 e4) e4)) % 5.25/5.46 False) % 5.25/5.46 (Eq (Eq (op e5 e5) e5) False)) % 5.25/5.46 Clause #197 (by clausification #[196]): Or % 5.25/5.46 (Eq % 5.25/5.46 (And (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) % 5.25/5.46 (Eq (op e4 e4) e4)) % 5.25/5.46 False) % 5.25/5.46 (Or (Eq (Eq (op e5 e5) e5) False) (Ne (op e6 e6) e6)) % 5.25/5.46 Clause #198 (by clausification #[197]): Or (Eq (Eq (op e5 e5) e5) False) % 5.25/5.46 (Or (Ne (op e6 e6) e6) % 5.25/5.46 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) False) % 5.25/5.46 (Eq (Eq (op e4 e4) e4) False))) % 5.25/5.46 Clause #199 (by clausification #[198]): Or (Ne (op e6 e6) e6) % 5.25/5.46 (Or (Eq (And (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) False) % 5.25/5.46 (Or (Eq (Eq (op e4 e4) e4) False) (Ne (op e5 e5) e5))) % 5.25/5.46 Clause #200 (by clausification #[199]): Or (Ne (op e6 e6) e6) % 5.25/5.46 (Or (Eq (Eq (op e4 e4) e4) False) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) False) % 5.33/5.48 (Eq (Eq (op e3 e3) e3) False)))) % 5.33/5.48 Clause #201 (by clausification #[200]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) False) % 5.33/5.48 (Or (Eq (Eq (op e3 e3) e3) False) (Ne (op e4 e4) e4)))) % 5.33/5.48 Clause #202 (by clausification #[201]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Eq (Eq (op e3 e3) e3) False) % 5.33/5.48 (Or (Ne (op e4 e4) e4) % 5.33/5.48 (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) False) (Eq (Eq (op e2 e2) e2) False))))) % 5.33/5.48 Clause #203 (by clausification #[202]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Ne (op e4 e4) e4) % 5.33/5.48 (Or (Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) False) % 5.33/5.48 (Or (Eq (Eq (op e2 e2) e2) False) (Ne (op e3 e3) e3))))) % 5.33/5.48 Clause #204 (by clausification #[203]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Ne (op e4 e4) e4) % 5.33/5.48 (Or (Eq (Eq (op e2 e2) e2) False) % 5.33/5.48 (Or (Ne (op e3 e3) e3) (Or (Eq (Eq (op e0 e0) e0) False) (Eq (Eq (op e1 e1) e1) False)))))) % 5.33/5.48 Clause #205 (by clausification #[204]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Ne (op e4 e4) e4) % 5.33/5.48 (Or (Ne (op e3 e3) e3) (Or (Eq (Eq (op e0 e0) e0) False) (Or (Eq (Eq (op e1 e1) e1) False) (Ne (op e2 e2) e2)))))) % 5.33/5.48 Clause #206 (by clausification #[205]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Ne (op e4 e4) e4) % 5.33/5.48 (Or (Ne (op e3 e3) e3) (Or (Eq (Eq (op e1 e1) e1) False) (Or (Ne (op e2 e2) e2) (Ne (op e0 e0) e0)))))) % 5.33/5.48 Clause #207 (by clausification #[206]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e5 e5) e5) % 5.33/5.48 (Or (Ne (op e4 e4) e4) (Or (Ne (op e3 e3) e3) (Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)))))) % 5.33/5.48 Clause #208 (by forward contextual literal cutting #[207, 125]): Or (Ne (op e6 e6) e6) % 5.33/5.48 (Or (Ne (op e4 e4) e4) (Or (Ne (op e3 e3) e3) (Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1))))) % 5.33/5.48 Clause #209 (by forward contextual literal cutting #[208, 168]): Or (Ne (op e6 e6) e6) (Or (Ne (op e3 e3) e3) (Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)))) % 5.33/5.48 Clause #210 (by forward contextual literal cutting #[209, 178]): Or (Ne (op e6 e6) e6) (Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1))) % 5.33/5.48 Clause #211 (by forward contextual literal cutting #[210, 182]): Or (Ne (op e6 e6) e6) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) % 5.33/5.48 Clause #212 (by forward contextual literal cutting #[211, 191]): Or (Ne (op e6 e6) e6) (Ne (op e1 e1) e1) % 5.33/5.48 Clause #213 (by forward contextual literal cutting #[212, 186]): Ne (op e6 e6) e6 % 5.33/5.48 Clause #228 (by clausification #[107]): Or % 5.33/5.48 (Eq % 5.33/5.48 (Or % 5.33/5.48 (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) (Eq (op e4 e4) e4)) % 5.33/5.48 (Eq (op e5 e5) e5)) % 5.33/5.48 False) % 5.33/5.48 (Eq (Ne (op e6 e6) e6) False) % 5.33/5.48 Clause #230 (by clausification #[228]): Or (Eq (Ne (op e6 e6) e6) False) (Eq (Eq (op e5 e5) e5) False) % 5.33/5.48 Clause #231 (by clausification #[228]): Or (Eq (Ne (op e6 e6) e6) False) % 5.33/5.48 (Eq (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) (Eq (op e4 e4) e4)) % 5.33/5.48 False) % 5.33/5.48 Clause #232 (by clausification #[230]): Or (Eq (Eq (op e5 e5) e5) False) (Eq (op e6 e6) e6) % 5.33/5.48 Clause #233 (by clausification #[232]): Or (Eq (op e6 e6) e6) (Ne (op e5 e5) e5) % 5.33/5.48 Clause #234 (by forward contextual literal cutting #[233, 213]): Ne (op e5 e5) e5 % 5.33/5.48 Clause #289 (by clausification #[231]): Or % 5.33/5.48 (Eq (Or (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) (Eq (op e4 e4) e4)) % 5.33/5.48 False) % 5.33/5.48 (Eq (op e6 e6) e6) % 5.33/5.48 Clause #290 (by clausification #[289]): Or (Eq (op e6 e6) e6) (Eq (Eq (op e4 e4) e4) False) % 5.33/5.48 Clause #291 (by clausification #[289]): Or (Eq (op e6 e6) e6) % 5.33/5.48 (Eq (Or (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) (Eq (op e3 e3) e3)) False) % 5.33/5.48 Clause #292 (by clausification #[290]): Or (Eq (op e6 e6) e6) (Ne (op e4 e4) e4) % 5.33/5.48 Clause #293 (by forward contextual literal cutting #[292, 213]): Ne (op e4 e4) e4 % 5.35/5.51 Clause #294 (by clausification #[291]): Or (Eq (op e6 e6) e6) (Eq (Eq (op e3 e3) e3) False) % 5.35/5.51 Clause #295 (by clausification #[291]): Or (Eq (op e6 e6) e6) (Eq (Or (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) False) % 5.35/5.51 Clause #296 (by clausification #[294]): Or (Eq (op e6 e6) e6) (Ne (op e3 e3) e3) % 5.35/5.51 Clause #297 (by forward contextual literal cutting #[296, 213]): Ne (op e3 e3) e3 % 5.35/5.51 Clause #298 (by clausification #[295]): Or (Eq (op e6 e6) e6) (Eq (Eq (op e2 e2) e2) False) % 5.35/5.51 Clause #299 (by clausification #[295]): Or (Eq (op e6 e6) e6) (Eq (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) False) % 5.35/5.51 Clause #300 (by clausification #[298]): Or (Eq (op e6 e6) e6) (Ne (op e2 e2) e2) % 5.35/5.51 Clause #301 (by forward contextual literal cutting #[300, 213]): Ne (op e2 e2) e2 % 5.35/5.51 Clause #302 (by clausification #[299]): Or (Eq (op e6 e6) e6) (Eq (Eq (op e1 e1) e1) False) % 5.35/5.51 Clause #303 (by clausification #[299]): Or (Eq (op e6 e6) e6) (Eq (Eq (op e0 e0) e0) False) % 5.35/5.51 Clause #304 (by clausification #[302]): Or (Eq (op e6 e6) e6) (Ne (op e1 e1) e1) % 5.35/5.51 Clause #305 (by forward contextual literal cutting #[304, 213]): Ne (op e1 e1) e1 % 5.35/5.51 Clause #309 (by clausification #[303]): Or (Eq (op e6 e6) e6) (Ne (op e0 e0) e0) % 5.35/5.51 Clause #310 (by forward contextual literal cutting #[309, 213]): Ne (op e0 e0) e0 % 5.35/5.51 Clause #331 (by clausification #[194]): Or % 5.35/5.51 (Eq % 5.35/5.51 (And % 5.35/5.51 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.35/5.51 (Ne (op e4 e4) e4)) % 5.35/5.51 (Ne (op e5 e5) e5)) % 5.35/5.51 False) % 5.35/5.51 (Eq (Ne (op e6 e6) e6) False) % 5.35/5.51 Clause #332 (by clausification #[331]): Or (Eq (Ne (op e6 e6) e6) False) % 5.35/5.51 (Or % 5.35/5.51 (Eq % 5.35/5.51 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.35/5.51 (Ne (op e4 e4) e4)) % 5.35/5.51 False) % 5.35/5.51 (Eq (Ne (op e5 e5) e5) False)) % 5.35/5.51 Clause #333 (by clausification #[332]): Or % 5.35/5.51 (Eq % 5.35/5.51 (And (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) % 5.35/5.51 (Ne (op e4 e4) e4)) % 5.35/5.51 False) % 5.35/5.51 (Or (Eq (Ne (op e5 e5) e5) False) (Eq (op e6 e6) e6)) % 5.35/5.51 Clause #334 (by clausification #[333]): Or (Eq (Ne (op e5 e5) e5) False) % 5.35/5.51 (Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) False) % 5.35/5.51 (Eq (Ne (op e4 e4) e4) False))) % 5.35/5.51 Clause #335 (by clausification #[334]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (And (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) False) % 5.35/5.51 (Or (Eq (Ne (op e4 e4) e4) False) (Eq (op e5 e5) e5))) % 5.35/5.51 Clause #336 (by clausification #[335]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (Ne (op e4 e4) e4) False) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) False) % 5.35/5.51 (Eq (Ne (op e3 e3) e3) False)))) % 5.35/5.51 Clause #337 (by clausification #[336]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (And (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) False) % 5.35/5.51 (Or (Eq (Ne (op e3 e3) e3) False) (Eq (op e4 e4) e4)))) % 5.35/5.51 Clause #338 (by clausification #[337]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (Ne (op e3 e3) e3) False) % 5.35/5.51 (Or (Eq (op e4 e4) e4) % 5.35/5.51 (Or (Eq (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) False) (Eq (Ne (op e2 e2) e2) False))))) % 5.35/5.51 Clause #339 (by clausification #[338]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (op e4 e4) e4) % 5.35/5.51 (Or (Eq (And (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) False) % 5.35/5.51 (Or (Eq (Ne (op e2 e2) e2) False) (Eq (op e3 e3) e3))))) % 5.35/5.51 Clause #340 (by clausification #[339]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (op e4 e4) e4) % 5.35/5.51 (Or (Eq (Ne (op e2 e2) e2) False) % 5.35/5.51 (Or (Eq (op e3 e3) e3) (Or (Eq (Ne (op e0 e0) e0) False) (Eq (Ne (op e1 e1) e1) False)))))) % 5.35/5.51 Clause #341 (by clausification #[340]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.35/5.51 (Or (Eq (op e4 e4) e4) % 5.35/5.51 (Or (Eq (op e3 e3) e3) (Or (Eq (Ne (op e0 e0) e0) False) (Or (Eq (Ne (op e1 e1) e1) False) (Eq (op e2 e2) e2)))))) % 5.35/5.51 Clause #342 (by clausification #[341]): Or (Eq (op e6 e6) e6) % 5.35/5.51 (Or (Eq (op e5 e5) e5) % 5.37/5.52 (Or (Eq (op e4 e4) e4) % 5.37/5.52 (Or (Eq (op e3 e3) e3) (Or (Eq (Ne (op e1 e1) e1) False) (Or (Eq (op e2 e2) e2) (Eq (op e0 e0) e0)))))) % 5.37/5.52 Clause #343 (by clausification #[342]): Or (Eq (op e6 e6) e6) % 5.37/5.52 (Or (Eq (op e5 e5) e5) % 5.37/5.52 (Or (Eq (op e4 e4) e4) (Or (Eq (op e3 e3) e3) (Or (Eq (op e2 e2) e2) (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)))))) % 5.37/5.52 Clause #344 (by forward contextual literal cutting #[343, 213]): Or (Eq (op e5 e5) e5) % 5.37/5.52 (Or (Eq (op e4 e4) e4) (Or (Eq (op e3 e3) e3) (Or (Eq (op e2 e2) e2) (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1))))) % 5.37/5.52 Clause #345 (by forward contextual literal cutting #[344, 234]): Or (Eq (op e4 e4) e4) (Or (Eq (op e3 e3) e3) (Or (Eq (op e2 e2) e2) (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)))) % 5.37/5.52 Clause #346 (by forward contextual literal cutting #[345, 293]): Or (Eq (op e3 e3) e3) (Or (Eq (op e2 e2) e2) (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1))) % 5.37/5.52 Clause #347 (by forward contextual literal cutting #[346, 297]): Or (Eq (op e2 e2) e2) (Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) % 5.37/5.52 Clause #348 (by forward contextual literal cutting #[347, 301]): Or (Eq (op e0 e0) e0) (Eq (op e1 e1) e1) % 5.37/5.52 Clause #349 (by forward contextual literal cutting #[348, 310]): Eq (op e1 e1) e1 % 5.37/5.52 Clause #350 (by forward contextual literal cutting #[349, 305]): False % 5.37/5.52 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------