%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP325_1 : TPTP v9.2.0. Released v8.0.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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:52:08 PM UTC 2025 % Result : Theorem 14.17s 14.34s % Output : Proof 14.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP325_1 : TPTP v9.2.0. Released v8.0.0. % 0.03/0.13 % Command : duper %s % 0.14/0.34 % Computer : n020.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:19:23 EDT 2025 % 0.14/0.34 % CPUTime : % 14.17/14.34 SZS status Theorem for theBenchmark.p % 14.17/14.34 SZS output start Proof for theBenchmark.p % 14.17/14.34 Clause #56 (by assumption #[]): Eq % 14.17/14.34 (∀ (A__questionmark_v0 : «A_a_fun$») (A__questionmark_v1 : «A_b_vec_n_vec$») (A__questionmark_v2 : «N$») % 14.17/14.34 (A__questionmark_v3 : «B$»), % 14.17/14.34 Eq («fun_app$a» («uux$» A__questionmark_v0 A__questionmark_v1 A__questionmark_v2) A__questionmark_v3) % 14.17/14.34 («fun_app$m» A__questionmark_v0 % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» A__questionmark_v1) A__questionmark_v2)) % 14.17/14.34 A__questionmark_v3))) % 14.17/14.34 True % 14.17/14.34 Clause #104 (by assumption #[]): Eq % 14.17/14.34 (Not % 14.17/14.34 (Eq «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») % 14.17/14.34 («fun_app$m» («divide$» «one$») % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» «interchange_A$») «i$»)) «j$»))))) % 14.17/14.34 True % 14.17/14.34 Clause #105 (by assumption #[]): Eq % 14.17/14.34 (Eq «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») % 14.17/14.34 («fun_app$m» («divide$» «one$») % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» «interchange_A$») «i$»)) «j$»)))) % 14.17/14.34 True % 14.17/14.34 Clause #2025 (by clausification #[56]): ∀ (a : «A_a_fun$»), % 14.17/14.34 Eq % 14.17/14.34 (∀ (A__questionmark_v1 : «A_b_vec_n_vec$») (A__questionmark_v2 : «N$») (A__questionmark_v3 : «B$»), % 14.17/14.34 Eq («fun_app$a» («uux$» a A__questionmark_v1 A__questionmark_v2) A__questionmark_v3) % 14.17/14.34 («fun_app$m» a % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» A__questionmark_v1) A__questionmark_v2)) % 14.17/14.34 A__questionmark_v3))) % 14.17/14.34 True % 14.17/14.34 Clause #2026 (by clausification #[2025]): ∀ (a : «A_a_fun$») (a_1 : «A_b_vec_n_vec$»), % 14.17/14.34 Eq % 14.17/14.34 (∀ (A__questionmark_v2 : «N$») (A__questionmark_v3 : «B$»), % 14.17/14.34 Eq («fun_app$a» («uux$» a a_1 A__questionmark_v2) A__questionmark_v3) % 14.17/14.34 («fun_app$m» a % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» a_1) A__questionmark_v2)) A__questionmark_v3))) % 14.17/14.34 True % 14.17/14.34 Clause #2027 (by clausification #[2026]): ∀ (a : «A_a_fun$») (a_1 : «A_b_vec_n_vec$») (a_2 : «N$»), % 14.17/14.34 Eq % 14.17/14.34 (∀ (A__questionmark_v3 : «B$»), % 14.17/14.34 Eq («fun_app$a» («uux$» a a_1 a_2) A__questionmark_v3) % 14.17/14.34 («fun_app$m» a («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» a_1) a_2)) A__questionmark_v3))) % 14.17/14.34 True % 14.17/14.34 Clause #2028 (by clausification #[2027]): ∀ (a : «A_a_fun$») (a_1 : «A_b_vec_n_vec$») (a_2 : «N$») (a_3 : «B$»), % 14.17/14.34 Eq % 14.17/14.34 (Eq («fun_app$a» («uux$» a a_1 a_2) a_3) % 14.17/14.34 («fun_app$m» a («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» a_1) a_2)) a_3))) % 14.17/14.34 True % 14.17/14.34 Clause #2029 (by clausification #[2028]): ∀ (a : «A_a_fun$») (a_1 : «A_b_vec_n_vec$») (a_2 : «N$») (a_3 : «B$»), % 14.17/14.34 Eq («fun_app$a» («uux$» a a_1 a_2) a_3) % 14.17/14.34 («fun_app$m» a («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» a_1) a_2)) a_3)) % 14.17/14.34 Clause #3417 (by clausification #[104]): Eq % 14.17/14.34 (Eq «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») % 14.17/14.34 («fun_app$m» («divide$» «one$») % 14.17/14.34 («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» «interchange_A$») «i$»)) «j$»)))) % 14.17/14.34 False % 14.17/14.34 Clause #3418 (by clausification #[3417]): Ne «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») % 14.17/14.34 («fun_app$m» («divide$» «one$») («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» «interchange_A$») «i$»)) «j$»))) % 14.17/14.34 Clause #3419 (by forward demodulation #[3418, 2029]): Ne «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») («fun_app$a» («uux$» («divide$» «one$») «interchange_A$» «i$») «j$»)) % 14.17/14.34 Clause #3446 (by clausification #[105]): Eq «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») % 14.17/14.34 («fun_app$m» («divide$» «one$») («fun_app$a» («vec_nth$» («fun_app$b» («vec_nth$a» «interchange_A$») «i$»)) «j$»))) % 14.17/14.34 Clause #3447 (by forward demodulation #[3446, 2029]): Eq «a$a» % 14.17/14.34 («fun_app$n» («mult_row$» «interchange_A$» «i$») («fun_app$a» («uux$» («divide$» «one$») «interchange_A$» «i$») «j$»)) % 14.17/14.34 Clause #3448 (by forward contextual literal cutting #[3447, 3419]): False % 14.21/14.35 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------