%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP159^1 : TPTP v9.2.0. Released v7.5.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:51:20 PM UTC 2025 % Result : Theorem 5.14s 5.28s % Output : Proof 5.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP159^1 : TPTP v9.2.0. Released v7.5.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 00:15:38 EDT 2025 % 0.14/0.34 % CPUTime : % 5.14/5.28 SZS status Theorem for theBenchmark.p % 5.14/5.28 SZS output start Proof for theBenchmark.p % 5.14/5.28 Clause #1 (by assumption #[]): Eq (∀ (M : refine432681134nres_b), Eq (ord_le527798542nres_b top_to240090974nres_b M) (Eq M top_to240090974nres_b)) True % 5.14/5.28 Clause #20 (by assumption #[]): Eq % 5.14/5.28 (∀ (R : set_Product_prod_a_b) (S : refine432681134nres_b), % 5.14/5.28 Eq (Eq (refine1441824854un_a_b R S) top_to231829469nres_a) (Eq S top_to240090974nres_b)) % 5.14/5.28 True % 5.14/5.28 Clause #31 (by assumption #[]): Eq (∀ (M : refine432681134nres_b), ord_le527798542nres_b M top_to240090974nres_b) True % 5.14/5.28 Clause #265 (by assumption #[]): Eq (Not (refine412683989fail_a top_to231829469nres_a)) True % 5.14/5.28 Clause #289 (by assumption #[]): Eq % 5.14/5.28 (∀ (S4 S : refine424419629nres_a), % 5.14/5.28 (refine412683989fail_a S4 → % 5.14/5.28 And (refine412683989fail_a S) (∀ (X2 : a), refine1001002027nres_a S X2 → refine1001002027nres_a S4 X2)) → % 5.14/5.28 ord_le519537037nres_a S S4) % 5.14/5.28 True % 5.14/5.28 Clause #324 (by assumption #[]): Eq (Not (ord_le519537037nres_a x (refine1441824854un_a_b r top_to240090974nres_b))) True % 5.14/5.28 Clause #325 (by clausification #[265]): Eq (refine412683989fail_a top_to231829469nres_a) False % 5.14/5.28 Clause #328 (by clausification #[31]): ∀ (a : refine432681134nres_b), Eq (ord_le527798542nres_b a top_to240090974nres_b) True % 5.14/5.28 Clause #340 (by clausification #[1]): ∀ (a : refine432681134nres_b), Eq (Eq (ord_le527798542nres_b top_to240090974nres_b a) (Eq a top_to240090974nres_b)) True % 5.14/5.28 Clause #341 (by clausification #[340]): ∀ (a : refine432681134nres_b), Eq (ord_le527798542nres_b top_to240090974nres_b a) (Eq a top_to240090974nres_b) % 5.14/5.28 Clause #412 (by clausification #[324]): Eq (ord_le519537037nres_a x (refine1441824854un_a_b r top_to240090974nres_b)) False % 5.14/5.28 Clause #624 (by clausification #[289]): ∀ (a_1 : refine424419629nres_a), % 5.14/5.28 Eq % 5.14/5.28 (∀ (S : refine424419629nres_a), % 5.14/5.28 (refine412683989fail_a a_1 → % 5.14/5.28 And (refine412683989fail_a S) (∀ (X2 : a), refine1001002027nres_a S X2 → refine1001002027nres_a a_1 X2)) → % 5.14/5.28 ord_le519537037nres_a S a_1) % 5.14/5.28 True % 5.14/5.28 Clause #625 (by clausification #[624]): ∀ (a_1 a_2 : refine424419629nres_a), % 5.14/5.28 Eq % 5.14/5.28 ((refine412683989fail_a a_1 → % 5.14/5.28 And (refine412683989fail_a a_2) (∀ (X2 : a), refine1001002027nres_a a_2 X2 → refine1001002027nres_a a_1 X2)) → % 5.14/5.28 ord_le519537037nres_a a_2 a_1) % 5.14/5.28 True % 5.14/5.28 Clause #626 (by clausification #[625]): ∀ (a_1 a_2 : refine424419629nres_a), % 5.14/5.28 Or % 5.14/5.28 (Eq % 5.14/5.28 (refine412683989fail_a a_1 → % 5.14/5.28 And (refine412683989fail_a a_2) (∀ (X2 : a), refine1001002027nres_a a_2 X2 → refine1001002027nres_a a_1 X2)) % 5.14/5.28 False) % 5.14/5.28 (Eq (ord_le519537037nres_a a_2 a_1) True) % 5.14/5.28 Clause #627 (by clausification #[626]): ∀ (a a_1 : refine424419629nres_a), Or (Eq (ord_le519537037nres_a a a_1) True) (Eq (refine412683989fail_a a_1) True) % 5.14/5.28 Clause #629 (by superposition #[627, 412]): Or (Eq (refine412683989fail_a (refine1441824854un_a_b r top_to240090974nres_b)) True) (Eq True False) % 5.14/5.28 Clause #681 (by clausification #[629]): Eq (refine412683989fail_a (refine1441824854un_a_b r top_to240090974nres_b)) True % 5.14/5.28 Clause #979 (by clausification #[20]): ∀ (a : set_Product_prod_a_b), % 5.14/5.28 Eq % 5.14/5.28 (∀ (S : refine432681134nres_b), % 5.14/5.28 Eq (Eq (refine1441824854un_a_b a S) top_to231829469nres_a) (Eq S top_to240090974nres_b)) % 5.14/5.28 True % 5.14/5.28 Clause #980 (by clausification #[979]): ∀ (a : set_Product_prod_a_b) (a_1 : refine432681134nres_b), % 5.14/5.28 Eq (Eq (Eq (refine1441824854un_a_b a a_1) top_to231829469nres_a) (Eq a_1 top_to240090974nres_b)) True % 5.14/5.28 Clause #981 (by clausification #[980]): ∀ (a : set_Product_prod_a_b) (a_1 : refine432681134nres_b), % 5.14/5.28 Eq (Eq (refine1441824854un_a_b a a_1) top_to231829469nres_a) (Eq a_1 top_to240090974nres_b) % 5.14/5.28 Clause #982 (by forward demodulation #[981, 341]): ∀ (a : set_Product_prod_a_b) (a_1 : refine432681134nres_b), % 5.14/5.28 Eq (Eq (refine1441824854un_a_b a a_1) top_to231829469nres_a) (ord_le527798542nres_b top_to240090974nres_b a_1) % 5.14/5.28 Clause #986 (by eqHoist #[982]): ∀ (a : refine432681134nres_b) (a_1 : set_Product_prod_a_b), % 5.14/5.28 Or (Eq False (ord_le527798542nres_b top_to240090974nres_b a)) % 5.14/5.28 (Eq (refine1441824854un_a_b a_1 a) top_to231829469nres_a) % 5.14/5.29 Clause #1002 (by superposition #[986, 328]): ∀ (a : set_Product_prod_a_b), % 5.14/5.29 Or (Eq (refine1441824854un_a_b a top_to240090974nres_b) top_to231829469nres_a) (Eq False True) % 5.14/5.29 Clause #1006 (by clausification #[1002]): ∀ (a : set_Product_prod_a_b), Eq (refine1441824854un_a_b a top_to240090974nres_b) top_to231829469nres_a % 5.14/5.29 Clause #1008 (by backward demodulation #[1006, 681]): Eq (refine412683989fail_a top_to231829469nres_a) True % 5.14/5.29 Clause #1015 (by superposition #[1008, 325]): Eq True False % 5.14/5.29 Clause #1026 (by clausification #[1015]): False % 5.14/5.29 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------