%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ALG200+1 : TPTP v9.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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.26s 5.44s % Output : Proof 5.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : ALG200+1 : TPTP v9.2.0. Released v2.7.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n021.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:53:23 EDT 2025 % 0.13/0.34 % CPUTime : % 5.26/5.44 SZS status Theorem for theBenchmark.p % 5.26/5.44 SZS output start Proof for theBenchmark.p % 5.26/5.44 Clause #6 (by assumption #[]): Eq % 5.26/5.44 (Not % 5.26/5.44 (Not % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6)) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6))) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Ne (op e4 e4) e4)) % 5.26/5.44 (Ne (op e5 e5) e5)) % 5.26/5.44 (Ne (op e6 e6) e6))))) % 5.26/5.44 True % 5.26/5.44 Clause #103 (by clausification #[6]): Eq % 5.26/5.44 (Not % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6)) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6))) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Ne (op e4 e4) e4)) % 5.26/5.44 (Ne (op e5 e5) e5)) % 5.26/5.44 (Ne (op e6 e6) e6)))) % 5.26/5.44 False % 5.26/5.44 Clause #104 (by clausification #[103]): Eq % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6)) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6))) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Ne (op e4 e4) e4)) % 5.26/5.44 (Ne (op e5 e5) e5)) % 5.26/5.44 (Ne (op e6 e6) e6))) % 5.26/5.44 True % 5.26/5.44 Clause #105 (by clausification #[104]): Eq % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Ne (op e5 e5) e5)) % 5.26/5.44 (Ne (op e6 e6) e6)) % 5.26/5.44 True % 5.26/5.44 Clause #106 (by clausification #[104]): Eq % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (And % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6)) % 5.26/5.44 (Or % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Eq (op e4 e4) e4)) % 5.26/5.44 (Eq (op e5 e5) e5)) % 5.26/5.44 (Eq (op e6 e6) e6))) % 5.26/5.44 True % 5.26/5.44 Clause #107 (by clausification #[105]): Or % 5.26/5.44 (Eq % 5.26/5.44 (Or % 5.26/5.44 (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.26/5.44 (Ne (op e5 e5) e5)) % 5.26/5.44 True) % 5.26/5.44 (Eq (Ne (op e6 e6) e6) True) % 5.26/5.44 Clause #108 (by clausification #[107]): Or (Eq (Ne (op e6 e6) e6) True) % 5.26/5.44 (Or % 5.26/5.44 (Eq % 5.26/5.44 (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.26/5.44 True) % 5.26/5.44 (Eq (Ne (op e5 e5) e5) True)) % 5.26/5.44 Clause #109 (by clausification #[108]): Or % 5.26/5.44 (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.26/5.44 True) % 5.26/5.44 (Or (Eq (Ne (op e5 e5) e5) True) (Ne (op e6 e6) e6)) % 5.26/5.44 Clause #110 (by clausification #[109]): Or (Eq (Ne (op e5 e5) e5) True) % 5.26/5.44 (Or (Ne (op e6 e6) e6) % 5.26/5.44 (Or (Eq (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) True) % 5.26/5.44 (Eq (Ne (op e4 e4) e4) True))) % 5.26/5.44 Clause #111 (by clausification #[110]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Eq (Or (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) (Ne (op e3 e3) e3)) True) % 5.26/5.47 (Or (Eq (Ne (op e4 e4) e4) True) (Ne (op e5 e5) e5))) % 5.26/5.47 Clause #112 (by clausification #[111]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Eq (Ne (op e4 e4) e4) True) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Eq (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) True) (Eq (Ne (op e3 e3) e3) True)))) % 5.26/5.47 Clause #113 (by clausification #[112]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Eq (Or (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) (Ne (op e2 e2) e2)) True) % 5.26/5.47 (Or (Eq (Ne (op e3 e3) e3) True) (Ne (op e4 e4) e4)))) % 5.26/5.47 Clause #114 (by clausification #[113]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Eq (Ne (op e3 e3) e3) True) % 5.26/5.47 (Or (Ne (op e4 e4) e4) (Or (Eq (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) True) (Eq (Ne (op e2 e2) e2) True))))) % 5.26/5.47 Clause #115 (by clausification #[114]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Ne (op e4 e4) e4) % 5.26/5.47 (Or (Eq (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) True) (Or (Eq (Ne (op e2 e2) e2) True) (Ne (op e3 e3) e3))))) % 5.26/5.47 Clause #116 (by clausification #[115]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Ne (op e4 e4) e4) % 5.26/5.47 (Or (Eq (Ne (op e2 e2) e2) True) % 5.26/5.47 (Or (Ne (op e3 e3) e3) (Or (Eq (Ne (op e0 e0) e0) True) (Eq (Ne (op e1 e1) e1) True)))))) % 5.26/5.47 Clause #117 (by clausification #[116]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Ne (op e4 e4) e4) % 5.26/5.47 (Or (Ne (op e3 e3) e3) (Or (Eq (Ne (op e0 e0) e0) True) (Or (Eq (Ne (op e1 e1) e1) True) (Ne (op e2 e2) e2)))))) % 5.26/5.47 Clause #118 (by clausification #[117]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (Or (Ne (op e4 e4) e4) % 5.26/5.47 (Or (Ne (op e3 e3) e3) (Or (Eq (Ne (op e1 e1) e1) True) (Or (Ne (op e2 e2) e2) (Ne (op e0 e0) e0)))))) % 5.26/5.47 Clause #119 (by clausification #[118]): Or (Ne (op e6 e6) e6) % 5.26/5.47 (Or (Ne (op e5 e5) e5) % 5.26/5.47 (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.26/5.47 Clause #209 (by clausification #[106]): Eq % 5.26/5.47 (And % 5.26/5.47 (And % 5.26/5.47 (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.26/5.47 (Eq (op e4 e4) e4)) % 5.26/5.47 (Eq (op e5 e5) e5)) % 5.26/5.47 (Eq (op e6 e6) e6)) % 5.26/5.47 True % 5.26/5.47 Clause #223 (by clausification #[209]): Eq (Eq (op e6 e6) e6) True % 5.26/5.47 Clause #224 (by clausification #[209]): Eq % 5.26/5.47 (And % 5.26/5.47 (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.26/5.47 (Eq (op e4 e4) e4)) % 5.26/5.47 (Eq (op e5 e5) e5)) % 5.26/5.47 True % 5.26/5.47 Clause #225 (by clausification #[223]): Eq (op e6 e6) e6 % 5.26/5.47 Clause #237 (by backward contextual literal cutting #[225, 119]): Or (Ne (op e5 e5) e5) % 5.26/5.47 (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.26/5.47 Clause #296 (by clausification #[224]): Eq (Eq (op e5 e5) e5) True % 5.26/5.47 Clause #297 (by clausification #[224]): Eq % 5.26/5.47 (And (And (And (And (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.26/5.47 True % 5.26/5.47 Clause #298 (by clausification #[296]): Eq (op e5 e5) e5 % 5.26/5.47 Clause #300 (by backward contextual literal cutting #[298, 237]): 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.26/5.47 Clause #301 (by clausification #[297]): Eq (Eq (op e4 e4) e4) True % 5.26/5.47 Clause #302 (by clausification #[297]): 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 % 5.26/5.47 Clause #303 (by clausification #[301]): Eq (op e4 e4) e4 % 5.26/5.47 Clause #305 (by backward contextual literal cutting #[303, 300]): Or (Ne (op e3 e3) e3) (Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1))) % 5.26/5.47 Clause #348 (by clausification #[302]): Eq (Eq (op e3 e3) e3) True % 5.26/5.47 Clause #349 (by clausification #[302]): Eq (And (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) (Eq (op e2 e2) e2)) True % 5.26/5.47 Clause #350 (by clausification #[348]): Eq (op e3 e3) e3 % 5.26/5.47 Clause #352 (by backward contextual literal cutting #[350, 305]): Or (Ne (op e2 e2) e2) (Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1)) % 5.26/5.47 Clause #356 (by clausification #[349]): Eq (Eq (op e2 e2) e2) True % 5.26/5.47 Clause #357 (by clausification #[349]): Eq (And (Eq (op e0 e0) e0) (Eq (op e1 e1) e1)) True % 5.26/5.47 Clause #358 (by clausification #[356]): Eq (op e2 e2) e2 % 5.26/5.47 Clause #360 (by backward contextual literal cutting #[358, 352]): Or (Ne (op e0 e0) e0) (Ne (op e1 e1) e1) % 5.26/5.47 Clause #361 (by clausification #[357]): Eq (Eq (op e1 e1) e1) True % 5.26/5.47 Clause #362 (by clausification #[357]): Eq (Eq (op e0 e0) e0) True % 5.26/5.47 Clause #363 (by clausification #[361]): Eq (op e1 e1) e1 % 5.26/5.47 Clause #365 (by backward contextual literal cutting #[363, 360]): Ne (op e0 e0) e0 % 5.26/5.47 Clause #371 (by clausification #[362]): Eq (op e0 e0) e0 % 5.26/5.47 Clause #372 (by forward contextual literal cutting #[371, 365]): False % 5.26/5.47 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------