%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP325_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n016.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 : Sat Jun 21 05:12:43 AM UTC 2025
% Result : Theorem 0.19s 0.50s
% Output : Proof 0.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : ITP325_1 : TPTP v9.0.0. Released v8.0.0.
% 0.00/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n016.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 18:46:32 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.50 % SZS status Theorem
% 0.19/0.50 % SZS output start Proof
% 0.19/0.50 tff(tptp_fun__fun_app_n__type, type, (
% 0.19/0.50 tptp_fun__fun_app_n_: ( |'A_a_b_vec_n_vec_fun$'| * |'A$'| ) > |'A_b_vec_n_vec$'|)).
% 0.19/0.50 tff(tptp_fun__fun_app_m__type, type, (
% 0.19/0.50 tptp_fun__fun_app_m_: ( |'A_a_fun$'| * |'A$'| ) > |'A$'|)).
% 0.19/0.50 tff(tptp_fun__fun_app_a__type, type, (
% 0.19/0.50 tptp_fun__fun_app_a_: ( |'B_a_fun$'| * |'B$'| ) > |'A$'|)).
% 0.19/0.50 tff(tptp_fun__j___type, type, (
% 0.19/0.50 tptp_fun__j__: |'B$'|)).
% 0.19/0.50 tff(tptp_fun__vec_nth___type, type, (
% 0.19/0.50 tptp_fun__vec_nth__: |'A_b_vec$'| > |'B_a_fun$'|)).
% 0.19/0.50 tff(tptp_fun__fun_app_b__type, type, (
% 0.19/0.50 tptp_fun__fun_app_b_: ( |'N_a_b_vec_fun$'| * |'N$'| ) > |'A_b_vec$'|)).
% 0.19/0.50 tff(tptp_fun__i___type, type, (
% 0.19/0.50 tptp_fun__i__: |'N$'|)).
% 0.19/0.50 tff(tptp_fun__vec_nth_a__type, type, (
% 0.19/0.50 tptp_fun__vec_nth_a_: |'A_b_vec_n_vec$'| > |'N_a_b_vec_fun$'|)).
% 0.19/0.50 tff(tptp_fun__interchange_A___type, type, (
% 0.19/0.50 tptp_fun__interchange_A__: |'A_b_vec_n_vec$'|)).
% 0.19/0.50 tff(tptp_fun__divide___type, type, (
% 0.19/0.50 tptp_fun__divide__: |'A$'| > |'A_a_fun$'|)).
% 0.19/0.50 tff(tptp_fun__one___type, type, (
% 0.19/0.50 tptp_fun__one__: |'A$'|)).
% 0.19/0.50 tff(tptp_fun__mult_row___type, type, (
% 0.19/0.50 tptp_fun__mult_row__: ( |'A_b_vec_n_vec$'| * |'N$'| ) > |'A_a_b_vec_n_vec_fun$'|)).
% 0.19/0.50 tff(tptp_fun__a_a__type, type, (
% 0.19/0.50 tptp_fun__a_a_: |'A_b_vec_n_vec$'|)).
% 0.19/0.50 tff(1,axiom,(|'a$a'| = tptp_fun__fun_app_n_(tptp_fun__mult_row__(|'interchange_A$'|, |'i$'|), tptp_fun__fun_app_m_(tptp_fun__divide__(|'one$'|), tptp_fun__fun_app_a_(tptp_fun__vec_nth__(tptp_fun__fun_app_b_(tptp_fun__vec_nth_a_(|'interchange_A$'|), |'i$'|)), |'j$'|)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','axiom105')).
% 0.19/0.50 tff(2,axiom,(~(|'a$a'| = tptp_fun__fun_app_n_(tptp_fun__mult_row__(|'interchange_A$'|, |'i$'|), tptp_fun__fun_app_m_(tptp_fun__divide__(|'one$'|), tptp_fun__fun_app_a_(tptp_fun__vec_nth__(tptp_fun__fun_app_b_(tptp_fun__vec_nth_a_(|'interchange_A$'|), |'i$'|)), |'j$'|))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','conjecture104')).
% 0.19/0.50 tff(3,plain,
% 0.19/0.50 ($false),
% 0.19/0.50 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.19/0.50 % SZS output end Proof
% 0.19/0.51 % E exiting
%------------------------------------------------------------------------------