%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : MGT093+1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 8 06:06:24 AM UTC 2026 % Result : Theorem 8.80s 9.05s % Output : Proof 8.80s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : MGT093+1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.04 % Command : duper %s % 0.09/0.35 % Computer : n020.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Mon Sep 7 14:01:58 UTC 2026 % 0.09/0.35 % CPUTime : % 8.80/9.05 SZS status Theorem for theBenchmark.p % 8.80/9.05 SZS output start Proof for theBenchmark.p % 8.80/9.05 Clause #13 (by assumption #[]): Eq % 8.80/9.05 (∀ (Vm Vr : Iota), % 8.80/9.05 And (And (And (is_verdict Vm) (is_verdict Vr)) (Eq Vm compatible)) (Eq Vr conflict) → % 8.80/9.05 Eq (xone_verdict Vm Vr) compatible) % 8.80/9.05 True % 8.80/9.05 Clause #25 (by assumption #[]): Eq (is_verdict conflict) True % 8.80/9.05 Clause #26 (by assumption #[]): Eq (is_verdict compatible) True % 8.80/9.05 Clause #36 (by assumption #[]): Eq (Not (Eq (xone_verdict compatible conflict) compatible)) True % 8.80/9.05 Clause #65 (by clausification #[36]): Eq (Eq (xone_verdict compatible conflict) compatible) False % 8.80/9.05 Clause #66 (by clausification #[65]): Ne (xone_verdict compatible conflict) compatible % 8.80/9.05 Clause #320 (by clausification #[13]): ∀ (a : Iota), % 8.80/9.05 Eq % 8.80/9.05 (∀ (Vr : Iota), % 8.80/9.05 And (And (And (is_verdict a) (is_verdict Vr)) (Eq a compatible)) (Eq Vr conflict) → % 8.80/9.05 Eq (xone_verdict a Vr) compatible) % 8.80/9.05 True % 8.80/9.05 Clause #321 (by clausification #[320]): ∀ (a a_1 : Iota), % 8.80/9.05 Eq % 8.80/9.05 (And (And (And (is_verdict a) (is_verdict a_1)) (Eq a compatible)) (Eq a_1 conflict) → % 8.80/9.05 Eq (xone_verdict a a_1) compatible) % 8.80/9.05 True % 8.80/9.05 Clause #322 (by clausification #[321]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (And (And (And (is_verdict a) (is_verdict a_1)) (Eq a compatible)) (Eq a_1 conflict)) False) % 8.80/9.05 (Eq (Eq (xone_verdict a a_1) compatible) True) % 8.80/9.05 Clause #323 (by clausification #[322]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (Eq (xone_verdict a a_1) compatible) True) % 8.80/9.05 (Or (Eq (And (And (is_verdict a) (is_verdict a_1)) (Eq a compatible)) False) (Eq (Eq a_1 conflict) False)) % 8.80/9.05 Clause #324 (by clausification #[323]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (And (And (is_verdict a) (is_verdict a_1)) (Eq a compatible)) False) % 8.80/9.05 (Or (Eq (Eq a_1 conflict) False) (Eq (xone_verdict a a_1) compatible)) % 8.80/9.05 Clause #325 (by clausification #[324]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (Eq a conflict) False) % 8.80/9.05 (Or (Eq (xone_verdict a_1 a) compatible) % 8.80/9.05 (Or (Eq (And (is_verdict a_1) (is_verdict a)) False) (Eq (Eq a_1 compatible) False))) % 8.80/9.05 Clause #326 (by clausification #[325]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (xone_verdict a a_1) compatible) % 8.80/9.05 (Or (Eq (And (is_verdict a) (is_verdict a_1)) False) (Or (Eq (Eq a compatible) False) (Ne a_1 conflict))) % 8.80/9.05 Clause #327 (by clausification #[326]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (xone_verdict a a_1) compatible) % 8.80/9.05 (Or (Eq (Eq a compatible) False) (Or (Ne a_1 conflict) (Or (Eq (is_verdict a) False) (Eq (is_verdict a_1) False)))) % 8.80/9.05 Clause #328 (by clausification #[327]): ∀ (a a_1 : Iota), % 8.80/9.05 Or (Eq (xone_verdict a a_1) compatible) % 8.80/9.05 (Or (Ne a_1 conflict) (Or (Eq (is_verdict a) False) (Or (Eq (is_verdict a_1) False) (Ne a compatible)))) % 8.80/9.05 Clause #329 (by destructive equality resolution #[328]): ∀ (a : Iota), % 8.80/9.05 Or (Eq (xone_verdict a conflict) compatible) % 8.80/9.05 (Or (Eq (is_verdict a) False) (Or (Eq (is_verdict conflict) False) (Ne a compatible))) % 8.80/9.05 Clause #330 (by destructive equality resolution #[329]): Or (Eq (xone_verdict compatible conflict) compatible) % 8.80/9.05 (Or (Eq (is_verdict compatible) False) (Eq (is_verdict conflict) False)) % 8.80/9.05 Clause #331 (by forward demodulation #[330, 26]): Or (Eq (xone_verdict compatible conflict) compatible) (Or (Eq True False) (Eq (is_verdict conflict) False)) % 8.80/9.05 Clause #332 (by clausification #[331]): Or (Eq (xone_verdict compatible conflict) compatible) (Eq (is_verdict conflict) False) % 8.80/9.05 Clause #333 (by forward demodulation #[332, 25]): Or (Eq (xone_verdict compatible conflict) compatible) (Eq True False) % 8.80/9.05 Clause #334 (by clausification #[333]): Eq (xone_verdict compatible conflict) compatible % 8.80/9.05 Clause #335 (by forward contextual literal cutting #[334, 66]): False % 8.80/9.05 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------