%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP177^2 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n022.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:51:22 PM UTC 2025 % Result : Theorem 9.15s 9.40s % Output : Proof 9.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : ITP177^2 : TPTP v9.2.0. Released v7.5.0. % 0.11/0.11 % Command : duper %s % 0.11/0.31 % Computer : n022.cluster.edu % 0.11/0.31 % Model : x86_64 x86_64 % 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.31 % Memory : 8042.1875MB % 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.31 % CPULimit : 300 % 0.11/0.31 % WCLimit : 300 % 0.11/0.31 % DateTime : Fri Oct 3 00:46:23 EDT 2025 % 0.11/0.31 % CPUTime : % 9.15/9.40 SZS status Theorem for theBenchmark.p % 9.15/9.40 SZS output start Proof for theBenchmark.p % 9.15/9.40 Clause #0 (by assumption #[]): Eq % 9.15/9.40 (∀ (Xa : b), % 9.15/9.40 member b (f Xa) (labeled_vertices (standard_Constant a) b g) → % 9.15/9.40 member b Xa (labeled_vertices (standard_Constant a) b g)) % 9.15/9.40 True % 9.15/9.40 Clause #2 (by assumption #[]): Eq (member b (f x) (labeled_vertices (standard_Constant a) b g)) True % 9.15/9.40 Clause #252 (by assumption #[]): Eq (Not (member b x (labeled_vertices (standard_Constant a) b g))) True % 9.15/9.40 Clause #337 (by clausification #[0]): ∀ (a_1 : b), % 9.15/9.40 Eq % 9.15/9.40 (member b (f a_1) (labeled_vertices (standard_Constant a) b g) → % 9.15/9.40 member b a_1 (labeled_vertices (standard_Constant a) b g)) % 9.15/9.40 True % 9.15/9.40 Clause #338 (by clausification #[337]): ∀ (a_1 : b), % 9.15/9.40 Or (Eq (member b (f a_1) (labeled_vertices (standard_Constant a) b g)) False) % 9.15/9.40 (Eq (member b a_1 (labeled_vertices (standard_Constant a) b g)) True) % 9.15/9.40 Clause #616 (by clausification #[252]): Eq (member b x (labeled_vertices (standard_Constant a) b g)) False % 9.15/9.40 Clause #621 (by superposition #[2, 338]): Or (Eq (member b x (labeled_vertices (standard_Constant a) b g)) True) (Eq False True) % 9.15/9.40 Clause #1701 (by clausification #[621]): Eq (member b x (labeled_vertices (standard_Constant a) b g)) True % 9.15/9.40 Clause #1702 (by superposition #[1701, 616]): Eq True False % 9.15/9.40 Clause #1785 (by clausification #[1702]): False % 9.15/9.40 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------