%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP341_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% Computer : n004.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 : Sun Sep 27 07:37:44 AM UTC 2026
% Result : Theorem 14.33s 4.79s
% Output : Refutation 15.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 291
% Syntax : Number of formulae : 584 ( 304 unt; 0 typ; 0 def)
% Number of atoms : 1237 (1153 equ; 0 cnn)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 4245 ( 142 ~; 49 |; 182 &;3450 @)
% ( 81 <=>; 341 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Number of types : 21 ( 20 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 51 ( 49 usr; 13 con; 0-4 aty)
% Number of variables : 1246 ( 0 ^;1207 !; 39 ?;1246 :)
% Comments :
%------------------------------------------------------------------------------
thf('A_n_vec_n_vec_set_set$_type',type,
'A_n_vec_n_vec_set_set$': $tType ).
thf('A_set_set$_type',type,
'A_set_set$': $tType ).
thf('A_n_vec_set$_type',type,
'A_n_vec_set$': $tType ).
thf('A_n_vec_n_vec_bool_fun$_type',type,
'A_n_vec_n_vec_bool_fun$': $tType ).
thf('A_n_vec_n_vec$_type',type,
'A_n_vec_n_vec$': $tType ).
thf('Nat$_type',type,
'Nat$': $tType ).
thf('A_n_vec_n_vec_set$_type',type,
'A_n_vec_n_vec_set$': $tType ).
thf('N$_type',type,
'N$': $tType ).
thf('Num$_type',type,
'Num$': $tType ).
thf('Num_set$_type',type,
'Num_set$': $tType ).
thf(tlbool_type,type,
tlbool: $tType ).
thf('A_bool_fun$_type',type,
'A_bool_fun$': $tType ).
thf('A_set$_type',type,
'A_set$': $tType ).
thf('A_n_vec_set_set$_type',type,
'A_n_vec_set_set$': $tType ).
thf('A$_type',type,
'A$': $tType ).
thf('A_n_vec$_type',type,
'A_n_vec$': $tType ).
thf('A_a_fun$_type',type,
'A_a_fun$': $tType ).
thf('A_n_vec_n_vec_n_vec$_type',type,
'A_n_vec_n_vec_n_vec$': $tType ).
thf('A_n_vec_bool_fun$_type',type,
'A_n_vec_bool_fun$': $tType ).
thf('N_a_n_vec_n_vec_fun$_type',type,
'N_a_n_vec_n_vec_fun$': $tType ).
thf('dbl_inc$a_decl',type,
'dbl_inc$a': 'A_n_vec$' > 'A_n_vec$' ).
thf('mat$_decl',type,
'mat$': 'A$' > 'A_n_vec_n_vec$' ).
thf('invertible$_decl',type,
'invertible$': 'A_n_vec_n_vec_bool_fun$' ).
thf('matrix_vector_mult$_decl',type,
'matrix_vector_mult$': 'A_n_vec_n_vec$' > 'A_n_vec$' > 'A_n_vec$' ).
thf('vector_matrix_mult$a_decl',type,
'vector_matrix_mult$a': 'A_n_vec$' > 'A_n_vec_n_vec$' > 'A_n_vec$' ).
thf('axis$_decl',type,
'axis$': 'N$' > 'A_n_vec$' > 'A_n_vec_n_vec$' ).
thf('columnvector$_decl',type,
'columnvector$': 'A_n_vec$' > 'A_n_vec_n_vec$' ).
thf('gauss_Jordan$_decl',type,
'gauss_Jordan$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('plus$g_decl',type,
'plus$g': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('zero$c_decl',type,
'zero$c': 'A_n_vec$' ).
thf('axis$a_decl',type,
'axis$a': 'N$' > 'A$' > 'A_n_vec$' ).
thf('plus$i_decl',type,
'plus$i': 'A_n_vec_n_vec_n_vec$' > 'A_n_vec_n_vec_n_vec$' > 'A_n_vec_n_vec_n_vec$' ).
thf('vec$a_decl',type,
'vec$a': 'A_n_vec$' > 'A_n_vec_n_vec$' ).
thf('times$a_decl',type,
'times$a': 'A_n_vec$' > 'A_n_vec$' > 'A_n_vec$' ).
thf('times$_decl',type,
'times$': 'A$' > 'A$' > 'A$' ).
thf('one$_decl',type,
'one$': 'A$' ).
thf('matrix_inv$_decl',type,
'matrix_inv$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('equivalent_matrices$_decl',type,
'equivalent_matrices$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec_bool_fun$' ).
thf(tltrue_decl,type,
tltrue: tlbool ).
thf('plus$h_decl',type,
'plus$h': 'A$' > 'A$' > 'A$' ).
thf('row_add$_decl',type,
'row_add$': 'A_n_vec_n_vec$' > 'N$' > 'N$' > 'A$' > 'A_n_vec_n_vec$' ).
thf('rowvector$_decl',type,
'rowvector$': 'A_n_vec$' > 'A_n_vec_n_vec$' ).
thf('gauss_Jordan_upt_k$_decl',type,
'gauss_Jordan_upt_k$': 'A_n_vec_n_vec$' > 'Nat$' > 'A_n_vec_n_vec$' ).
thf('a$_decl',type,
'a$': 'A_n_vec_n_vec$' ).
thf('mult_column$_decl',type,
'mult_column$': 'A_n_vec_n_vec$' > 'N$' > 'A$' > 'A_n_vec_n_vec$' ).
thf('column_add$_decl',type,
'column_add$': 'A_n_vec_n_vec$' > 'N$' > 'N$' > 'A$' > 'A_n_vec_n_vec$' ).
thf('reduced_row_echelon_form$_decl',type,
'reduced_row_echelon_form$': 'A_n_vec_n_vec_bool_fun$' ).
thf('one$a_decl',type,
'one$a': 'A_n_vec$' ).
thf('divide$_decl',type,
'divide$': 'A$' > 'A_a_fun$' ).
thf('zero$a_decl',type,
'zero$a': 'A_n_vec_n_vec$' ).
thf('matrix_matrix_mult$_decl',type,
'matrix_matrix_mult$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('transpose$_decl',type,
'transpose$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('orthogonal_matrix$_decl',type,
'orthogonal_matrix$': 'A_n_vec_n_vec_bool_fun$' ).
thf('fun_app$d_decl',type,
'fun_app$d': 'A_a_fun$' > 'A$' > 'A$' ).
thf('matrix_vector_mult$a_decl',type,
'matrix_vector_mult$a': 'A_n_vec_n_vec_n_vec$' > 'A_n_vec_n_vec$' > 'A_n_vec_n_vec$' ).
thf('column$_decl',type,
'column$': 'N$' > 'A_n_vec_n_vec$' > 'A_n_vec$' ).
thf('vec$_decl',type,
'vec$': 'A$' > 'A_n_vec$' ).
thf('zero$_decl',type,
'zero$': 'A$' ).
thf('plus$d_decl',type,
'plus$d': 'A_n_vec$' > 'A_n_vec$' > 'A_n_vec$' ).
thf('fun_app$c_decl',type,
'fun_app$c': 'N_a_n_vec_n_vec_fun$' > 'N$' > 'A_n_vec_n_vec$' ).
thf(tlfalse_decl,type,
tlfalse: tlbool ).
thf('numeral$b_decl',type,
'numeral$b': 'Num$' > 'A$' ).
thf('similar_matrices$_decl',type,
'similar_matrices$': 'A_n_vec_n_vec$' > 'A_n_vec_n_vec_bool_fun$' ).
thf('interchange_columns$_decl',type,
'interchange_columns$': 'A_n_vec_n_vec$' > 'N$' > 'N$' > 'A_n_vec_n_vec$' ).
thf('fun_app$_decl',type,
'fun_app$': 'A_n_vec_n_vec_bool_fun$' > 'A_n_vec_n_vec$' > $o ).
thf('mult_row$_decl',type,
'mult_row$': 'A_n_vec_n_vec$' > 'N$' > 'A$' > 'A_n_vec_n_vec$' ).
thf('dbl_inc$b_decl',type,
'dbl_inc$b': 'A$' > 'A$' ).
thf('interchange_rows$_decl',type,
'interchange_rows$': 'A_n_vec_n_vec$' > 'N$' > 'N_a_n_vec_n_vec_fun$' ).
thf('p$_decl',type,
'p$': 'A_n_vec_n_vec$' ).
thf(257,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
<=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom20) ).
thf(1665,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
& ( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[257]) ).
thf(141,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( A @ ( B @ 'times$' ) )
= ( A @ ( C @ 'times$' ) ) )
<=> ( B = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom141) ).
thf(1036,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( B = C )
=> ( ( A @ ( B @ 'times$' ) )
= ( A @ ( C @ 'times$' ) ) ) )
& ( ( ( A @ ( B @ 'times$' ) )
= ( A @ ( C @ 'times$' ) ) )
=> ( B = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(203,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'times$' ) )
= ( D @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom280) ).
thf(1411,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'times$' ) )
= ( D @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[203]) ).
thf(292,axiom,
! [A: 'A_n_vec_n_vec$'] :
? [B: 'A_n_vec_n_vec$'] :
( ( ( A @ 'gauss_Jordan$' )
= ( A @ ( B @ 'matrix_matrix_mult$' ) ) )
& ( B @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom27) ).
thf(1823,plain,
! [A: 'A_n_vec_n_vec$'] :
? [B: 'A_n_vec_n_vec$'] :
( ( ( A @ 'gauss_Jordan$' )
= ( A @ ( B @ 'matrix_matrix_mult$' ) ) )
& ( B @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[292]) ).
thf(163,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$a' @ ( A @ 'vector_matrix_mult$a' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom69) ).
thf(1168,plain,
! [A: 'A_n_vec$'] :
( ( 'zero$a' @ ( A @ 'vector_matrix_mult$a' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[163]) ).
thf(248,axiom,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom118) ).
thf(1633,plain,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[248]) ).
thf(119,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom300) ).
thf(893,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(43,axiom,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec_n_vec$'] :
( ( A = B )
<=> ! [C: 'A_n_vec_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$a' ) )
= ( C @ ( B @ 'matrix_vector_mult$a' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom186) ).
thf(481,plain,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec_n_vec$'] :
( ( ! [C: 'A_n_vec_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$a' ) )
= ( C @ ( B @ 'matrix_vector_mult$a' ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ! [C: 'A_n_vec_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$a' ) )
= ( C @ ( B @ 'matrix_vector_mult$a' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(15,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom360) ).
thf(347,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(274,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( A @ 'matrix_inv$' @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom24) ).
thf(1729,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( A @ 'matrix_inv$' @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[274]) ).
thf(124,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' = A )
<=> ( A = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom89) ).
thf(909,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ( A = 'zero$a' )
=> ( 'zero$a' = A ) )
& ( ( 'zero$a' = A )
=> ( A = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(74,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' )
<=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom248) ).
thf(628,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'zero$' )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ) )
& ( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' )
=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(240,axiom,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom264) ).
thf(1596,plain,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[240]) ).
thf(228,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'A$'] :
( ( C @ ( B @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'mult_column$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom36) ).
thf(1522,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'A$'] :
( ( C @ ( B @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'mult_column$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[228]) ).
thf(170,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'times$' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom134) ).
thf(1205,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'times$' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[170]) ).
thf(210,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
<=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom38) ).
thf(1437,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
& ( ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[210]) ).
thf(113,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom247) ).
thf(861,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(280,axiom,
! [A: 'A$',B: 'N$'] :
( ( A != 'zero$' )
=> ( A @ ( B @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom56) ).
thf(1750,plain,
! [A: 'A$',B: 'N$'] :
( ( A != 'zero$' )
=> ( A @ ( B @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[280]) ).
thf(25,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'plus$d' ) )
= ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom335) ).
thf(408,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'plus$d' ) )
= ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(51,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'plus$d' ) )
= ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom353) ).
thf(523,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'plus$d' ) )
= ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(162,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( A @ 'vec$' )
= ( B @ 'vec$' ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom170) ).
thf(1158,plain,
! [A: 'A$',B: 'A$'] :
( ( ( A = B )
=> ( ( A @ 'vec$' )
= ( B @ 'vec$' ) ) )
& ( ( ( A @ 'vec$' )
= ( B @ 'vec$' ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[162]) ).
thf(95,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'plus$g' ) )
= ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom337) ).
thf(741,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'plus$g' ) )
= ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(149,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'interchange_columns$' ) ) )
= ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'transpose$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom64) ).
thf(1073,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'interchange_columns$' ) ) )
= ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'transpose$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[149]) ).
thf(208,axiom,
! [A: tlbool] :
( ( A = tlfalse )
| ( A = tltrue ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_418) ).
thf(1426,plain,
! [A: tlbool] :
( ( A = tlfalse )
| ( A = tltrue ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[208]) ).
thf(243,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
<=> ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom18) ).
thf(1608,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
& ( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[243]) ).
thf(161,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C )
<=> ( ( ~ ( ( B != 'zero$' ) )
=> ( C = 'zero$' ) )
& ( ( B != 'zero$' )
=> ( A
= ( B @ ( C @ 'times$' ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom388) ).
thf(1137,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( ( B = 'zero$' )
=> ( C = 'zero$' ) )
& ( ( B != 'zero$' )
=> ( A
= ( B @ ( C @ 'times$' ) ) ) ) )
=> ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C ) )
& ( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C )
=> ( ( ( B = 'zero$' )
=> ( C = 'zero$' ) )
& ( ( B != 'zero$' )
=> ( A
= ( B @ ( C @ 'times$' ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[161]) ).
thf(185,axiom,
! [A: 'A_n_vec$'] :
( ( A @ 'rowvector$' @ 'transpose$' )
= ( A @ 'columnvector$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom202) ).
thf(1310,plain,
! [A: 'A_n_vec$'] :
( ( A @ 'rowvector$' @ 'transpose$' )
= ( A @ 'columnvector$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[185]) ).
thf(56,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$c' @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom175) ).
thf(550,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$c' @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(276,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'matrix_vector_mult$' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_vector_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom189) ).
thf(1735,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'matrix_vector_mult$' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_vector_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[276]) ).
thf(40,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom310) ).
thf(472,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(190,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'plus$h' ) )
= ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom356) ).
thf(1327,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'plus$h' ) )
= ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[190]) ).
thf(146,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom294) ).
thf(1063,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(194,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom215) ).
thf(1354,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[194]) ).
thf(83,axiom,
! [A: 'Num$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'numeral$b' @ 'times$' ) )
= ( C @ ( A @ 'numeral$b' @ 'times$' ) @ ( B @ ( A @ 'numeral$b' @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom411) ).
thf(670,plain,
! [A: 'Num$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'numeral$b' @ 'times$' ) )
= ( C @ ( A @ 'numeral$b' @ 'times$' ) @ ( B @ ( A @ 'numeral$b' @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(222,axiom,
! [A: 'A$',B: 'A$'] :
( ( 'one$'
= ( B @ ( A @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( A = B )
& ( B != 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom266) ).
thf(1497,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( A = B )
& ( B != 'zero$' ) )
=> ( 'one$'
= ( B @ ( A @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( 'one$'
= ( B @ ( A @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( A = B )
& ( B != 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[222]) ).
thf(269,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( A @ 'matrix_matrix_mult$' ) @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom322) ).
thf(1705,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( A @ 'matrix_matrix_mult$' ) @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[269]) ).
thf(153,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_columns$' ) ) @ 'transpose$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom126) ).
thf(1095,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_columns$' ) ) @ 'transpose$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[153]) ).
thf(28,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$a' @ 'times$a' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom77) ).
thf(417,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$a' @ 'times$a' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(5,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$d' ) ) )
=> ( ( A @ ( D @ 'plus$d' ) )
= ( C @ ( D @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom347) ).
thf(301,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$d' ) ) )
=> ( ( A @ ( D @ 'plus$d' ) )
= ( C @ ( D @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(196,axiom,
! [A: 'A_n_vec$'] :
( ( 'one$a' = A )
<=> ( A = 'one$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom21) ).
thf(1366,plain,
! [A: 'A_n_vec$'] :
( ( ( A = 'one$a' )
=> ( 'one$a' = A ) )
& ( ( 'one$a' = A )
=> ( A = 'one$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[196]) ).
thf(230,axiom,
! [A: 'A$'] :
( ( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) )
& ( ( A = 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom268) ).
thf(1529,plain,
! [A: 'A$'] :
( ( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) )
& ( ( A = 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[230]) ).
thf(268,axiom,
( 'a$'
= ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom7) ).
thf(1703,plain,
( 'a$'
= ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[268]) ).
thf(246,axiom,
( ( 'one$' @ 'vec$' )
= 'one$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom174) ).
thf(1623,plain,
( ( 'one$' @ 'vec$' )
= 'one$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[246]) ).
thf(22,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= A )
<=> ( B = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom233) ).
thf(389,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B = 'zero$c' )
=> ( ( B @ ( A @ 'plus$d' ) )
= A ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= A )
=> ( B = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(92,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom217) ).
thf(724,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(255,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'transpose$' )
= ( A @ 'transpose$' @ ( B @ 'transpose$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom43) ).
thf(1660,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'transpose$' )
= ( A @ 'transpose$' @ ( B @ 'transpose$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[255]) ).
thf(47,axiom,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'matrix_vector_mult$a' ) )
= ( C @ ( A @ 'matrix_vector_mult$a' ) @ ( B @ ( A @ 'matrix_vector_mult$a' ) @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom319) ).
thf(504,plain,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'matrix_vector_mult$a' ) )
= ( C @ ( A @ 'matrix_vector_mult$a' ) @ ( B @ ( A @ 'matrix_vector_mult$a' ) @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(191,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$a' @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom181) ).
thf(1330,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$a' @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[191]) ).
thf(224,axiom,
! [A: 'N$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'column$' ) )
= ( C @ ( A @ 'column$' ) @ ( B @ 'matrix_vector_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom195) ).
thf(1511,plain,
! [A: 'N$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'column$' ) )
= ( C @ ( A @ 'column$' ) @ ( B @ 'matrix_vector_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[224]) ).
thf(14,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom298) ).
thf(344,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(16,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom371) ).
thf(357,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(54,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$c' @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom177) ).
thf(542,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$c' @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(186,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$g' ) ) )
=> ( ( A @ ( D @ 'plus$g' ) )
= ( C @ ( D @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom349) ).
thf(1313,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$g' ) ) )
=> ( ( A @ ( D @ 'plus$g' ) )
= ( C @ ( D @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[186]) ).
thf(181,axiom,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom258) ).
thf(1279,plain,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[181]) ).
thf(106,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'times$' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom137) ).
thf(817,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'times$' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(59,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= C )
& ( A != 'zero$' ) )
=> ( B
= ( A @ ( C @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom385) ).
thf(559,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= C )
& ( A != 'zero$' ) )
=> ( B
= ( A @ ( C @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(251,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
<=> ? [B: 'A_n_vec_n_vec$'] :
( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom19) ).
thf(1641,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ? [B: 'A_n_vec_n_vec$'] :
( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
=> ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
& ( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[251]) ).
thf(152,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
<=> ( B = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom142) ).
thf(1087,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( B = C )
=> ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) ) )
& ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
=> ( B = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[152]) ).
thf(225,axiom,
! [A: 'A$'] :
( ( A @ 'mat$' @ 'transpose$' )
= ( A @ 'mat$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom41) ).
thf(1514,plain,
! [A: 'A$'] :
( ( A @ 'mat$' @ 'transpose$' )
= ( A @ 'mat$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[225]) ).
thf(132,axiom,
! [A: 'A$',B: 'Num$',C: 'A$'] :
( ( ( B @ 'numeral$b' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C )
<=> ( ( ~ ( ( ( B @ 'numeral$b' )
!= 'zero$' ) )
=> ( C = 'zero$' ) )
& ( ( ( B @ 'numeral$b' )
!= 'zero$' )
=> ( A
= ( B @ 'numeral$b' @ ( C @ 'times$' ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom415) ).
thf(969,plain,
! [A: 'A$',B: 'Num$',C: 'A$'] :
( ( ( ( ( ( B @ 'numeral$b' )
= 'zero$' )
=> ( C = 'zero$' ) )
& ( ( ( B @ 'numeral$b' )
!= 'zero$' )
=> ( A
= ( B @ 'numeral$b' @ ( C @ 'times$' ) ) ) ) )
=> ( ( B @ 'numeral$b' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C ) )
& ( ( ( B @ 'numeral$b' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= C )
=> ( ( ( ( B @ 'numeral$b' )
= 'zero$' )
=> ( C = 'zero$' ) )
& ( ( ( B @ 'numeral$b' )
!= 'zero$' )
=> ( A
= ( B @ 'numeral$b' @ ( C @ 'times$' ) ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(69,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'times$' ) )
= ( C @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom252) ).
thf(606,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'times$' ) )
= ( C @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(137,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( C != 'zero$' )
=> ( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'plus$h' ) )
= ( C @ ( B @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( C = 'zero$' )
=> ( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'plus$h' ) )
= A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom272) ).
thf(1013,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( C != 'zero$' )
=> ( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'plus$h' ) )
= ( C @ ( B @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( C = 'zero$' )
=> ( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'plus$h' ) )
= A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(99,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom98) ).
thf(770,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(289,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B @ ( 'invertible$' @ 'fun_app$' ) )
& ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
=> ( B @ ( A @ 'matrix_matrix_mult$' ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom17) ).
thf(1815,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B @ ( 'invertible$' @ 'fun_app$' ) )
& ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
=> ( B @ ( A @ 'matrix_matrix_mult$' ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[289]) ).
thf(221,axiom,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom80) ).
thf(1494,plain,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[221]) ).
thf(41,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom295) ).
thf(475,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(77,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom288) ).
thf(646,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(199,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom259) ).
thf(1383,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[199]) ).
thf(105,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
<=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom76) ).
thf(806,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'zero$' )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= 'zero$' ) )
& ( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(182,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom282) ).
thf(1283,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[182]) ).
thf(156,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom398) ).
thf(1109,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[156]) ).
thf(11,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'times$a' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom136) ).
thf(321,plain,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'times$a' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(23,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( A
= ( A @ ( B @ 'plus$d' ) ) )
<=> ( B = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom236) ).
thf(397,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B = 'zero$c' )
=> ( A
= ( A @ ( B @ 'plus$d' ) ) ) )
& ( ( A
= ( A @ ( B @ 'plus$d' ) ) )
=> ( B = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(93,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'times$' ) )
= ( B @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom255) ).
thf(734,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'times$' ) )
= ( B @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(1,conjecture,
( ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
= ( 'p$' @ 'matrix_inv$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture3) ).
thf(2,negated_conjecture,
( ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
!= ( 'p$' @ 'matrix_inv$' ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(293,plain,
( ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
!= ( 'p$' @ 'matrix_inv$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(36,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'plus$d' ) @ 'vec$a' )
= ( B @ 'vec$a' @ ( A @ 'vec$a' @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom332) ).
thf(453,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'plus$d' ) @ 'vec$a' )
= ( B @ 'vec$a' @ ( A @ 'vec$a' @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(26,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'times$a' ) )
= ( A @ ( B @ 'times$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom99) ).
thf(411,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'times$a' ) )
= ( A @ ( B @ 'times$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(30,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'times$a' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom107) ).
thf(428,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'times$a' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(265,axiom,
! [A: 'N$',B: 'N$'] : ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_columns$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom37) ).
thf(1697,plain,
! [A: 'N$',B: 'N$'] : ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_columns$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[265]) ).
thf(48,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( D @ ( B @ ( C @ 'times$a' ) @ 'plus$d' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) )
= ( D @ ( B @ ( C @ ( A @ 'plus$d' ) @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom313) ).
thf(507,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( D @ ( B @ ( C @ 'times$a' ) @ 'plus$d' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) )
= ( D @ ( B @ ( C @ ( A @ 'plus$d' ) @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(8,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'vector_matrix_mult$a' ) )
= ( C @ ( B @ 'vector_matrix_mult$a' ) @ ( C @ ( A @ 'vector_matrix_mult$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom382) ).
thf(312,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'vector_matrix_mult$a' ) )
= ( C @ ( B @ 'vector_matrix_mult$a' ) @ ( C @ ( A @ 'vector_matrix_mult$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(252,axiom,
'zero$' != 'one$',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom150) ).
thf(1651,plain,
'zero$' != 'one$',
inference(defexp_and_simp_and_etaexpand,[status(thm)],[252]) ).
thf(129,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom358) ).
thf(942,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(86,axiom,
! [A: 'A_n_vec_n_vec$'] : ( A @ 'gauss_Jordan$' @ ( 'reduced_row_echelon_form$' @ 'fun_app$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom121) ).
thf(678,plain,
! [A: 'A_n_vec_n_vec$'] : ( A @ 'gauss_Jordan$' @ ( 'reduced_row_echelon_form$' @ 'fun_app$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(263,axiom,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'times$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom114) ).
thf(1691,plain,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'times$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[263]) ).
thf(80,axiom,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'plus$h' ) @ 'vec$' )
= ( B @ 'vec$' @ ( A @ 'vec$' @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom331) ).
thf(661,plain,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'plus$h' ) @ 'vec$' )
= ( B @ 'vec$' @ ( A @ 'vec$' @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(283,axiom,
! [A: 'A$'] :
( ( A @ 'dbl_inc$b' )
= ( 'one$' @ ( A @ ( A @ 'plus$h' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom396) ).
thf(1768,plain,
! [A: 'A$'] :
( ( A @ 'dbl_inc$b' )
= ( 'one$' @ ( A @ ( A @ 'plus$h' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[283]) ).
thf(249,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$' @ 'mat$' @ 'matrix_vector_mult$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom179) ).
thf(1636,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$' @ 'mat$' @ 'matrix_vector_mult$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[249]) ).
thf(216,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'matrix_matrix_mult$' ) )
= 'zero$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom66) ).
thf(1470,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'matrix_matrix_mult$' ) )
= 'zero$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[216]) ).
thf(270,axiom,
! [A: 'N$',B: 'N$',C: 'A$'] :
( ( A != B )
=> ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'row_add$' ) ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom62) ).
thf(1708,plain,
! [A: 'N$',B: 'N$',C: 'A$'] :
( ( A != B )
=> ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'row_add$' ) ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[270]) ).
thf(104,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= B )
<=> ( A = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom229) ).
thf(798,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( A = 'zero$a' )
=> ( ( B @ ( A @ 'plus$g' ) )
= B ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= B )
=> ( A = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(144,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'times$' ) @ ( D @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom279) ).
thf(1057,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'times$' ) @ ( D @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(13,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom216) ).
thf(334,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(200,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( A @ 'transpose$' )
= ( B @ 'transpose$' ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom39) ).
thf(1387,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( A = B )
=> ( ( A @ 'transpose$' )
= ( B @ 'transpose$' ) ) )
& ( ( ( A @ 'transpose$' )
= ( B @ 'transpose$' ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[200]) ).
thf(130,axiom,
! [A: 'N$',B: 'A$'] :
( ( ( B @ ( A @ 'axis$a' ) )
= 'zero$c' )
<=> ( B = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom161) ).
thf(952,plain,
! [A: 'N$',B: 'A$'] :
( ( ( B = 'zero$' )
=> ( ( B @ ( A @ 'axis$a' ) )
= 'zero$c' ) )
& ( ( ( B @ ( A @ 'axis$a' ) )
= 'zero$c' )
=> ( B = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(227,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom26) ).
thf(1519,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[227]) ).
thf(259,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( 'one$' @ 'mat$' @ 'interchange_columns$' ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'interchange_columns$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom47) ).
thf(1676,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( 'one$' @ 'mat$' @ 'interchange_columns$' ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ 'interchange_columns$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[259]) ).
thf(107,axiom,
! [A: 'N$',B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'axis$' ) )
= 'zero$a' )
<=> ( B = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom160) ).
thf(820,plain,
! [A: 'N$',B: 'A_n_vec$'] :
( ( ( B = 'zero$c' )
=> ( ( B @ ( A @ 'axis$' ) )
= 'zero$a' ) )
& ( ( ( B @ ( A @ 'axis$' ) )
= 'zero$a' )
=> ( B = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(236,axiom,
! [A: 'N$',B: 'N$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'matrix_matrix_mult$' ) )
= ( B @ ( A @ ( C @ 'interchange_rows$' ) @ 'fun_app$c' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom61) ).
thf(1560,plain,
! [A: 'N$',B: 'N$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'matrix_matrix_mult$' ) )
= ( B @ ( A @ ( C @ 'interchange_rows$' ) @ 'fun_app$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[236]) ).
thf(207,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom397) ).
thf(1423,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[207]) ).
thf(39,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom375) ).
thf(467,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(111,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'plus$g' ) )
= ( A @ ( B @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom367) ).
thf(847,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'plus$g' ) )
= ( A @ ( B @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(242,axiom,
! [A: 'A_n_vec_n_vec$'] :
? [B: 'A_n_vec_n_vec$'] :
( ( A @ 'gauss_Jordan$' @ ( 'reduced_row_echelon_form$' @ 'fun_app$' ) )
& ( ( A @ 'gauss_Jordan$' )
= ( A @ ( B @ 'matrix_matrix_mult$' ) ) )
& ( B @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom59) ).
thf(1602,plain,
! [A: 'A_n_vec_n_vec$'] :
? [B: 'A_n_vec_n_vec$'] :
( ( A @ 'gauss_Jordan$' @ ( 'reduced_row_echelon_form$' @ 'fun_app$' ) )
& ( ( A @ 'gauss_Jordan$' )
= ( A @ ( B @ 'matrix_matrix_mult$' ) ) )
& ( B @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[242]) ).
thf(73,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( B @ ( C @ 'times$' ) @ 'plus$h' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) )
= ( D @ ( B @ ( C @ ( A @ 'plus$h' ) @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom315) ).
thf(625,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( D @ ( B @ ( C @ 'times$' ) @ 'plus$h' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) )
= ( D @ ( B @ ( C @ ( A @ 'plus$h' ) @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(117,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom144) ).
thf(879,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(213,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'matrix_matrix_mult$' ) )
= 'zero$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom65) ).
thf(1457,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'matrix_matrix_mult$' ) )
= 'zero$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[213]) ).
thf(45,axiom,
! [A: 'A_n_vec$'] :
( ( A @ 'dbl_inc$a' )
= ( 'one$a' @ ( A @ ( A @ 'plus$d' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom394) ).
thf(493,plain,
! [A: 'A_n_vec$'] :
( ( A @ 'dbl_inc$a' )
= ( 'one$a' @ ( A @ ( A @ 'plus$d' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(37,axiom,
! [A: 'A_n_vec_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'matrix_vector_mult$a' ) )
= 'zero$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom176) ).
thf(456,plain,
! [A: 'A_n_vec_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'matrix_vector_mult$a' ) )
= 'zero$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(12,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom171) ).
thf(324,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( A = B )
=> ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) ) )
& ( ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(193,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ ( B @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( A @ ( A @ ( C @ 'times$' ) @ ( B @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom274) ).
thf(1350,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ ( B @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( A @ ( A @ ( C @ 'times$' ) @ ( B @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[193]) ).
thf(63,axiom,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$i' ) @ 'matrix_vector_mult$a' ) )
= ( C @ ( B @ 'matrix_vector_mult$a' ) @ ( C @ ( A @ 'matrix_vector_mult$a' ) @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom329) ).
thf(578,plain,
! [A: 'A_n_vec_n_vec_n_vec$',B: 'A_n_vec_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$i' ) @ 'matrix_vector_mult$a' ) )
= ( C @ ( B @ 'matrix_vector_mult$a' ) @ ( C @ ( A @ 'matrix_vector_mult$a' ) @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(72,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom359) ).
thf(615,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(173,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( B @ ( D @ 'divide$' @ 'fun_app$d' ) @ ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( B @ ( A @ 'times$' ) @ ( A @ ( D @ 'times$' ) @ ( B @ ( C @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom273) ).
thf(1227,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( B @ ( D @ 'divide$' @ 'fun_app$d' ) @ ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( B @ ( A @ 'times$' ) @ ( A @ ( D @ 'times$' ) @ ( B @ ( C @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[173]) ).
thf(29,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( A
= ( B @ ( A @ 'plus$d' ) ) )
<=> ( B = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom239) ).
thf(420,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B = 'zero$c' )
=> ( A
= ( B @ ( A @ 'plus$d' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$d' ) ) )
=> ( B = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(201,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom278) ).
thf(1397,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[201]) ).
thf(88,axiom,
'zero$c' != 'one$a',
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom149) ).
thf(697,plain,
'zero$c' != 'one$a',
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(232,axiom,
'one$' @ 'mat$' @ ( 'orthogonal_matrix$' @ 'fun_app$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom31) ).
thf(1541,plain,
'one$' @ 'mat$' @ ( 'orthogonal_matrix$' @ 'fun_app$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[232]) ).
thf(197,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom306) ).
thf(1375,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[197]) ).
thf(158,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( A
= ( B @ ( A @ 'plus$g' ) ) )
<=> ( B = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom238) ).
thf(1121,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B = 'zero$a' )
=> ( A
= ( B @ ( A @ 'plus$g' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$g' ) ) )
=> ( B = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[158]) ).
thf(212,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= B )
<=> ( ( A = 'one$' )
| ( B = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom128) ).
thf(1446,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( A = 'one$' )
| ( B = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= B ) )
& ( ( ( B @ ( A @ 'times$' ) )
= B )
=> ( ( A = 'one$' )
| ( B = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[212]) ).
thf(204,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= ( C @ ( B @ ( A @ 'interchange_columns$' ) ) @ 'transpose$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom125) ).
thf(1414,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= ( C @ ( B @ ( A @ 'interchange_columns$' ) ) @ 'transpose$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[204]) ).
thf(52,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$d' ) ) )
=> ( ( D @ ( A @ 'plus$d' ) )
= ( D @ ( C @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom341) ).
thf(526,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$',D: 'A_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$d' ) ) )
=> ( ( D @ ( A @ 'plus$d' ) )
= ( D @ ( C @ 'plus$d' ) @ ( B @ 'plus$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(189,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom296) ).
thf(1324,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[189]) ).
thf(174,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( A = B )
<=> ! [C: 'A_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ 'matrix_vector_mult$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom187) ).
thf(1231,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ! [C: 'A_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ 'matrix_vector_mult$' ) ) )
=> ( A = B ) )
& ( ( A = B )
=> ! [C: 'A_n_vec$'] :
( ( C @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ 'matrix_vector_mult$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[174]) ).
thf(235,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_vector_mult$' ) )
= 'zero$c' )
<=> ( ( C @ ( B @ 'matrix_vector_mult$' ) )
= 'zero$c' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom193) ).
thf(1552,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( ( ( C @ ( B @ 'matrix_vector_mult$' ) )
= 'zero$c' )
=> ( ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_vector_mult$' ) )
= 'zero$c' ) )
& ( ( ( C @ ( B @ ( A @ 'matrix_matrix_mult$' ) @ 'matrix_vector_mult$' ) )
= 'zero$c' )
=> ( ( C @ ( B @ 'matrix_vector_mult$' ) )
= 'zero$c' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[235]) ).
thf(145,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_columns$' ) ) )
= ( C @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'transpose$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom127) ).
thf(1060,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$'] :
( ( C @ ( B @ ( A @ 'transpose$' @ 'interchange_columns$' ) ) )
= ( C @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) @ 'transpose$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(209,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( D @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( B @ ( C @ 'times$' ) )
= ( A @ ( D @ 'times$' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom389) ).
thf(1429,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( ( ( B @ ( C @ 'times$' ) )
= ( A @ ( D @ 'times$' ) ) )
=> ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( D @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( D @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( B @ ( C @ 'times$' ) )
= ( A @ ( D @ 'times$' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[209]) ).
thf(241,axiom,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom256) ).
thf(1599,plain,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[241]) ).
thf(272,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) )
<=> ( ( ( A @ 'transpose$' @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( A @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom46) ).
thf(1715,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ( ( ( A @ 'transpose$' @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( A @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
=> ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) ) )
& ( ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) )
=> ( ( ( A @ 'transpose$' @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( A @ ( A @ 'transpose$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[272]) ).
thf(229,axiom,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( B @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( 'one$' @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom270) ).
thf(1525,plain,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( B @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( 'one$' @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[229]) ).
thf(192,axiom,
! [A: 'N$',B: 'A$',C: 'N$',D: 'A$'] :
( ( ( B @ ( A @ 'axis$a' ) )
= ( D @ ( C @ 'axis$a' ) ) )
<=> ( ( ( D = 'zero$' )
& ( B = 'zero$' ) )
| ( ( A = C )
& ( B = D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom190) ).
thf(1333,plain,
! [A: 'N$',B: 'A$',C: 'N$',D: 'A$'] :
( ( ( ( ( D = 'zero$' )
& ( B = 'zero$' ) )
| ( ( A = C )
& ( B = D ) ) )
=> ( ( B @ ( A @ 'axis$a' ) )
= ( D @ ( C @ 'axis$a' ) ) ) )
& ( ( ( B @ ( A @ 'axis$a' ) )
= ( D @ ( C @ 'axis$a' ) ) )
=> ( ( ( D = 'zero$' )
& ( B = 'zero$' ) )
| ( ( A = C )
& ( B = D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[192]) ).
thf(187,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom226) ).
thf(1318,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'zero$a' @ ( A @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[187]) ).
thf(169,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom251) ).
thf(1202,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[169]) ).
thf(17,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom357) ).
thf(360,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(126,axiom,
! [A: tlbool,B: 'A_n_vec$'] :
( ( ( A != tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'zero$c' @ 'times$a' ) )
= 'zero$c' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'zero$c' @ 'times$a' ) )
= B ) ) ) )
& ( ( A = tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'one$a' @ 'times$a' ) )
= 'zero$c' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'one$a' @ 'times$a' ) )
= B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom152) ).
thf(921,plain,
! [A: tlbool,B: 'A_n_vec$'] :
( ( ( A != tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'zero$c' @ 'times$a' ) )
= 'zero$c' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'zero$c' @ 'times$a' ) )
= B ) ) ) )
& ( ( A = tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'one$a' @ 'times$a' ) )
= 'zero$c' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'one$a' @ 'times$a' ) )
= B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(237,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= A )
<=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom130) ).
thf(1563,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'one$' )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= A ) )
& ( ( ( B @ ( A @ 'times$' ) )
= A )
=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[237]) ).
thf(183,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ 'matrix_vector_mult$' ) @ ( C @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom330) ).
thf(1286,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'matrix_vector_mult$' ) )
= ( C @ ( B @ 'matrix_vector_mult$' ) @ ( C @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[183]) ).
thf(256,axiom,
( ( 'zero$' @ 'mat$' )
= 'zero$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom86) ).
thf(1663,plain,
( ( 'zero$' @ 'mat$' )
= 'zero$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[256]) ).
thf(244,axiom,
! [A: 'A$',B: 'N$'] :
( ( A != 'zero$' )
=> ( A @ ( B @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom123) ).
thf(1616,plain,
! [A: 'A$',B: 'N$'] :
( ( A != 'zero$' )
=> ( A @ ( B @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[244]) ).
thf(166,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ 'transpose$' )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom40) ).
thf(1185,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ 'transpose$' )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[166]) ).
thf(100,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( A @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( B = C )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom249) ).
thf(773,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( B = C )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( A @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( A @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( B = C )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(91,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ ( 'orthogonal_matrix$' @ 'fun_app$' ) )
<=> ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom42) ).
thf(718,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) )
=> ( A @ 'transpose$' @ ( 'orthogonal_matrix$' @ 'fun_app$' ) ) )
& ( ( A @ 'transpose$' @ ( 'orthogonal_matrix$' @ 'fun_app$' ) )
=> ( A @ ( 'orthogonal_matrix$' @ 'fun_app$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(275,axiom,
! [A: 'A_n_vec$'] :
( ( 'one$' @ 'mat$' @ ( A @ 'vector_matrix_mult$a' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom35) ).
thf(1732,plain,
! [A: 'A_n_vec$'] :
( ( 'one$' @ 'mat$' @ ( A @ 'vector_matrix_mult$a' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[275]) ).
thf(97,axiom,
( ( 'zero$' @ 'vec$' )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom162) ).
thf(765,plain,
( ( 'zero$' @ 'vec$' )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(271,axiom,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom81) ).
thf(1712,plain,
! [A: 'A$'] :
( ( A @ ( 'one$' @ 'times$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[271]) ).
thf(143,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom244) ).
thf(1054,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$a' @ 'plus$g' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(123,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom246) ).
thf(906,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(4,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( A @ 'matrix_vector_mult$' ) @ ( B @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom320) ).
thf(298,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( A @ 'matrix_vector_mult$' ) @ ( B @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(279,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom8) ).
thf(1747,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[279]) ).
thf(33,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom245) ).
thf(444,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(50,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom169) ).
thf(513,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( A = B )
=> ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) ) )
& ( ( ( A @ 'vec$a' )
= ( B @ 'vec$a' ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(281,axiom,
! [A: 'N$',B: 'A$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ 'matrix_matrix_mult$' ) )
= ( B @ ( A @ ( C @ 'mult_row$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom57) ).
thf(1754,plain,
! [A: 'N$',B: 'A$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ 'matrix_matrix_mult$' ) )
= ( B @ ( A @ ( C @ 'mult_row$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[281]) ).
thf(245,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'vector_matrix_mult$a' ) @ 'vector_matrix_mult$a' ) )
= ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'vector_matrix_mult$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom45) ).
thf(1620,plain,
! [A: 'A_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'vector_matrix_mult$a' ) @ 'vector_matrix_mult$a' ) )
= ( C @ ( B @ 'matrix_matrix_mult$' ) @ ( A @ 'vector_matrix_mult$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[245]) ).
thf(55,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( A
= ( C @ ( B @ 'plus$h' ) ) )
=> ( ( D @ ( A @ 'plus$h' ) )
= ( D @ ( C @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom344) ).
thf(545,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( A
= ( C @ ( B @ 'plus$h' ) ) )
=> ( ( D @ ( A @ 'plus$h' ) )
= ( D @ ( C @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(286,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
<=> ! [B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' )
=> ( B = 'zero$c' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom159) ).
thf(1795,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ! [B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' )
=> ( B = 'zero$c' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
& ( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ! [B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'matrix_vector_mult$' ) )
= 'zero$c' )
=> ( B = 'zero$c' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[286]) ).
thf(267,axiom,
( ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom6) ).
thf(1701,plain,
( ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[267]) ).
thf(285,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'similar_matrices$' @ 'fun_app$' ) )
<=> ? [C: 'A_n_vec_n_vec$'] :
( ( B
= ( C @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom30) ).
thf(1786,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ? [C: 'A_n_vec_n_vec$'] :
( ( B
= ( C @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) )
=> ( B @ ( A @ 'similar_matrices$' @ 'fun_app$' ) ) )
& ( ( B @ ( A @ 'similar_matrices$' @ 'fun_app$' ) )
=> ? [C: 'A_n_vec_n_vec$'] :
( ( B
= ( C @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[285]) ).
thf(127,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom243) ).
thf(936,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(180,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= A )
<=> ( B = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom232) ).
thf(1271,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B = 'zero$a' )
=> ( ( B @ ( A @ 'plus$g' ) )
= A ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= A )
=> ( B = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[180]) ).
thf(102,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom309) ).
thf(787,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(101,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'times$' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom74) ).
thf(784,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'times$' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(133,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'transpose$' @ 'matrix_vector_mult$' ) )
= ( A @ ( B @ 'vector_matrix_mult$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom185) ).
thf(990,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'transpose$' @ 'matrix_vector_mult$' ) )
= ( A @ ( B @ 'vector_matrix_mult$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(233,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
<=> ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom48) ).
thf(1542,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
& ( ? [B: 'A_n_vec_n_vec$'] :
( ( A @ 'transpose$' @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ? [B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[233]) ).
thf(61,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
!= 'zero$' )
=> ( ( B != 'zero$' )
& ( A != 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom147) ).
thf(567,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
!= 'zero$' )
=> ( ( B != 'zero$' )
& ( A != 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(78,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$'] :
( ( B @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom87) ).
thf(649,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$'] :
( ( B @ ( B @ ( A @ 'interchange_rows$' ) @ 'fun_app$c' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(165,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom362) ).
thf(1175,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[165]) ).
thf(238,axiom,
! [A: 'A$',B: 'A$'] :
( ( A
= ( A @ ( B @ 'times$' ) ) )
<=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom129) ).
thf(1574,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'one$' )
| ( A = 'zero$' ) )
=> ( A
= ( A @ ( B @ 'times$' ) ) ) )
& ( ( A
= ( A @ ( B @ 'times$' ) ) )
=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[238]) ).
thf(287,axiom,
( ! [A: 'A_n_vec_n_vec$'] :
( ( ( ( 'a$' @ 'gauss_Jordan$' )
= ( 'a$' @ ( A @ 'matrix_matrix_mult$' ) ) )
& ( A @ ( 'invertible$' @ 'fun_app$' ) ) )
=> $false )
=> $false ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom16) ).
thf(1806,plain,
~ ! [A: 'A_n_vec_n_vec$'] :
~ ( ( ( 'a$' @ 'gauss_Jordan$' )
= ( 'a$' @ ( A @ 'matrix_matrix_mult$' ) ) )
& ( A @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[287]) ).
thf(284,axiom,
! [A: tlbool,B: 'A$'] :
( ( ( A != tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'zero$' @ 'times$' ) )
= 'zero$' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'zero$' @ 'times$' ) )
= B ) ) ) )
& ( ( A = tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'one$' @ 'times$' ) )
= 'zero$' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'one$' @ 'times$' ) )
= B ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom153) ).
thf(1771,plain,
! [A: tlbool,B: 'A$'] :
( ( ( A != tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'zero$' @ 'times$' ) )
= 'zero$' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'zero$' @ 'times$' ) )
= B ) ) ) )
& ( ( A = tltrue )
=> ( ( ( A != tltrue )
=> ( ( B @ ( 'one$' @ 'times$' ) )
= 'zero$' ) )
& ( ( A = tltrue )
=> ( ( B @ ( 'one$' @ 'times$' ) )
= B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[284]) ).
thf(94,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'times$' ) @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom260) ).
thf(737,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'times$' ) @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(10,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom307) ).
thf(318,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(70,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$c' @ 'vector_matrix_mult$a' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom71) ).
thf(609,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'zero$c' @ 'vector_matrix_mult$a' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(89,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= A )
<=> ( B = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom231) ).
thf(700,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B = 'zero$' )
=> ( ( B @ ( A @ 'plus$h' ) )
= A ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= A )
=> ( B = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(214,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
<=> ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom13) ).
thf(1460,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
& ( ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
=> ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[214]) ).
thf(138,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( A
= ( A @ ( B @ 'plus$g' ) ) )
<=> ( B = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom235) ).
thf(1022,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B = 'zero$a' )
=> ( A
= ( A @ ( B @ 'plus$g' ) ) ) )
& ( ( A
= ( A @ ( B @ 'plus$g' ) ) )
=> ( B = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(291,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( 'one$' @ 'mat$' @ ( A @ 'matrix_matrix_mult$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom9) ).
thf(1820,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( 'one$' @ 'mat$' @ ( A @ 'matrix_matrix_mult$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[291]) ).
thf(157,axiom,
! [A: 'A$'] :
( ( 'zero$' = A )
<=> ( A = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom88) ).
thf(1112,plain,
! [A: 'A$'] :
( ( ( A = 'zero$' )
=> ( 'zero$' = A ) )
& ( ( 'zero$' = A )
=> ( A = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[157]) ).
thf(261,axiom,
'one$' @ 'mat$' @ ( 'invertible$' @ 'fun_app$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom28) ).
thf(1688,plain,
'one$' @ 'mat$' @ ( 'invertible$' @ 'fun_app$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[261]) ).
thf(164,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ ( B @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( A @ ( A @ ( C @ 'times$' ) @ ( B @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom277) ).
thf(1171,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ ( B @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( A @ ( A @ ( C @ 'times$' ) @ ( B @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[164]) ).
thf(266,axiom,
( ( 'a$' @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) )
= ( 'a$' @ ( 'p$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom5) ).
thf(1699,plain,
( ( 'a$' @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) )
= ( 'a$' @ ( 'p$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[266]) ).
thf(6,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom283) ).
thf(306,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(60,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A = 'zero$a' )
=> ( ( A @ 'gauss_Jordan$' )
= 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom120) ).
thf(563,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A = 'zero$a' )
=> ( ( A @ 'gauss_Jordan$' )
= 'zero$a' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(195,axiom,
( ( 'zero$c' @ 'dbl_inc$a' )
= 'one$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom205) ).
thf(1364,plain,
( ( 'zero$c' @ 'dbl_inc$a' )
= 'one$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[195]) ).
thf(31,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom213) ).
thf(431,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= ( C @ ( A @ 'plus$d' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(264,axiom,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom267) ).
thf(1694,plain,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[264]) ).
thf(142,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( A @ 'vec$' )
= ( B @ 'vec$' ) )
<=> ( A = B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom172) ).
thf(1044,plain,
! [A: 'A$',B: 'A$'] :
( ( ( A = B )
=> ( ( A @ 'vec$' )
= ( B @ 'vec$' ) ) )
& ( ( ( A @ 'vec$' )
= ( B @ 'vec$' ) )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(176,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom281) ).
thf(1245,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[176]) ).
thf(147,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom261) ).
thf(1066,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(211,axiom,
'p$' @ ( 'invertible$' @ 'fun_app$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom4) ).
thf(1445,plain,
'p$' @ ( 'invertible$' @ 'fun_app$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[211]) ).
thf(150,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= B )
<=> ( A = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom228) ).
thf(1076,plain,
! [A: 'A$',B: 'A$'] :
( ( ( A = 'zero$' )
=> ( ( B @ ( A @ 'plus$h' ) )
= B ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= B )
=> ( A = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[150]) ).
thf(53,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) )
<=> ( ( B = 'zero$' )
| ( A = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom72) ).
thf(531,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( B = 'zero$' )
| ( A = C ) )
=> ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) ) )
& ( ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) )
=> ( ( B = 'zero$' )
| ( A = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(87,axiom,
! [A: 'N$',B: 'A_n_vec$',C: 'N$',D: 'A_n_vec$'] :
( ( ( B @ ( A @ 'axis$' ) )
= ( D @ ( C @ 'axis$' ) ) )
<=> ( ( ( D = 'zero$c' )
& ( B = 'zero$c' ) )
| ( ( A = C )
& ( B = D ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom191) ).
thf(680,plain,
! [A: 'N$',B: 'A_n_vec$',C: 'N$',D: 'A_n_vec$'] :
( ( ( ( ( D = 'zero$c' )
& ( B = 'zero$c' ) )
| ( ( A = C )
& ( B = D ) ) )
=> ( ( B @ ( A @ 'axis$' ) )
= ( D @ ( C @ 'axis$' ) ) ) )
& ( ( ( B @ ( A @ 'axis$' ) )
= ( D @ ( C @ 'axis$' ) ) )
=> ( ( ( D = 'zero$c' )
& ( B = 'zero$c' ) )
| ( ( A = C )
& ( B = D ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(206,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom297) ).
thf(1420,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[206]) ).
thf(160,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom93) ).
thf(1134,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[160]) ).
thf(128,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom374) ).
thf(939,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(57,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom225) ).
thf(553,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(110,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
<=> ( ( B = C )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom139) ).
thf(836,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( B = C )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) ) )
& ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
=> ( ( B = C )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(44,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'plus$d' ) )
= ( A @ ( B @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom365) ).
thf(490,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'plus$d' ) )
= ( A @ ( B @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(85,axiom,
tltrue != tlfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_419) ).
thf(675,plain,
tltrue != tlfalse,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(171,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
<=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom214) ).
thf(1208,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B = C )
=> ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
=> ( B = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[171]) ).
thf(65,axiom,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom287) ).
thf(589,plain,
! [A: 'A$'] :
( ( 'zero$' @ ( A @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(3,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom304) ).
thf(295,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$d' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( C @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(27,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom301) ).
thf(414,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ ( A @ 'times$a' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(178,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom218) ).
thf(1252,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) ) )
& ( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[178]) ).
thf(154,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom312) ).
thf(1098,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( C @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[154]) ).
thf(134,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) )
<=> ( ( A = C )
| ( B = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom140) ).
thf(993,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A = C )
| ( B = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) ) )
& ( ( ( B @ ( A @ 'times$' ) )
= ( B @ ( C @ 'times$' ) ) )
=> ( ( A = C )
| ( B = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(148,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom94) ).
thf(1070,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(115,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B
= ( A @ ( C @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom386) ).
thf(872,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B
= ( A @ ( C @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(278,axiom,
! [A: 'A$',B: 'A$',C: 'N$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= 'one$' )
& ( ( B @ ( A @ 'times$' ) )
= 'one$' ) )
=> ( A @ ( C @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom122) ).
thf(1743,plain,
! [A: 'A$',B: 'A$',C: 'N$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= 'one$' )
& ( ( B @ ( A @ 'times$' ) )
= 'one$' ) )
=> ( A @ ( C @ ( 'one$' @ 'mat$' @ 'mult_row$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[278]) ).
thf(202,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
<=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom138) ).
thf(1400,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'zero$' )
| ( A = 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
= 'zero$' ) )
& ( ( ( B @ ( A @ 'times$' ) )
= 'zero$' )
=> ( ( B = 'zero$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[202]) ).
thf(84,axiom,
( ( 'zero$c' @ 'vec$a' )
= 'zero$a' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom163) ).
thf(673,plain,
( ( 'zero$c' @ 'vec$a' )
= 'zero$a' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(288,axiom,
( ( 'a$' @ ( 'p$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) )
= ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom10) ).
thf(1813,plain,
( ( 'a$' @ ( 'p$' @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) )
= ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) @ ( 'p$' @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[288]) ).
thf(167,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom376) ).
thf(1188,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[167]) ).
thf(32,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom399) ).
thf(441,plain,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(18,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( A
= ( B @ ( A @ 'plus$d' ) ) )
<=> ( B = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom402) ).
thf(370,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B = 'zero$c' )
=> ( A
= ( B @ ( A @ 'plus$d' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$d' ) ) )
=> ( B = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(179,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$c' = A )
<=> ( A = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom90) ).
thf(1262,plain,
! [A: 'A_n_vec$'] :
( ( ( A = 'zero$c' )
=> ( 'zero$c' = A ) )
& ( ( 'zero$c' = A )
=> ( A = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[179]) ).
thf(231,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'matrix_vector_mult$' ) @ 'columnvector$' )
= ( B @ 'columnvector$' @ ( A @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom194) ).
thf(1538,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$'] :
( ( B @ ( A @ 'matrix_vector_mult$' ) @ 'columnvector$' )
= ( B @ 'columnvector$' @ ( A @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[231]) ).
thf(260,axiom,
! [A: 'A$'] :
( ( 'one$' = A )
<=> ( A = 'one$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom23) ).
thf(1679,plain,
! [A: 'A$'] :
( ( ( A = 'one$' )
=> ( 'one$' = A ) )
& ( ( 'one$' = A )
=> ( A = 'one$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[260]) ).
thf(76,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom110) ).
thf(643,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(277,axiom,
! [A: 'A_n_vec_n_vec$',B: 'Nat$'] :
? [C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'gauss_Jordan_upt_k$' ) )
= ( A @ ( C @ 'matrix_matrix_mult$' ) ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom49) ).
thf(1738,plain,
! [A: 'A_n_vec_n_vec$',B: 'Nat$'] :
? [C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'gauss_Jordan_upt_k$' ) )
= ( A @ ( C @ 'matrix_matrix_mult$' ) ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[277]) ).
thf(172,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( A = 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom263) ).
thf(1218,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( A = 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[172]) ).
thf(96,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( ~ ( ( C != 'zero$' ) )
=> ( A = 'zero$' ) )
& ( ( C != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) )
= B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom387) ).
thf(744,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( ( C = 'zero$' )
=> ( A = 'zero$' ) )
& ( ( C != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) )
= B ) ) )
=> ( A
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( A
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( ( C = 'zero$' )
=> ( A = 'zero$' ) )
& ( ( C != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) )
= B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(114,axiom,
! [A: 'A$',B: 'A$'] :
( ( A
= ( B @ ( A @ 'plus$h' ) ) )
<=> ( B = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom237) ).
thf(864,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B = 'zero$' )
=> ( A
= ( B @ ( A @ 'plus$h' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$h' ) ) )
=> ( B = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(67,axiom,
! [A: 'A$',B: 'A$'] :
( ( A
= ( A @ ( B @ 'plus$h' ) ) )
<=> ( B = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom234) ).
thf(595,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B = 'zero$' )
=> ( A
= ( A @ ( B @ 'plus$h' ) ) ) )
& ( ( A
= ( A @ ( B @ 'plus$h' ) ) )
=> ( B = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(71,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'plus$g' ) )
= ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom355) ).
thf(612,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ ( A @ 'plus$g' ) @ 'plus$g' ) )
= ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(116,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom92) ).
thf(876,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(175,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom379) ).
thf(1240,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
=> ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[175]) ).
thf(239,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' )
<=> ( ( A = B )
& ( B != 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom265) ).
thf(1585,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( A = B )
& ( B != 'zero$' ) )
=> ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) )
& ( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= 'one$' )
=> ( ( A = B )
& ( B != 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[239]) ).
thf(21,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$a' @ 'times$a' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom115) ).
thf(386,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'one$a' @ 'times$a' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(58,axiom,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'times$' ) )
= ( A @ ( B @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom102) ).
thf(556,plain,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'times$' ) )
= ( A @ ( B @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(290,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( A @ ( A @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom25) ).
thf(1817,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A @ ( 'invertible$' @ 'fun_app$' ) )
=> ( ( A @ ( A @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[290]) ).
thf(188,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( A != 'zero$a' )
=> ( ( A @ 'gauss_Jordan$' )
!= 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom119) ).
thf(1321,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( A != 'zero$a' )
=> ( ( A @ 'gauss_Jordan$' )
!= 'zero$a' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[188]) ).
thf(122,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom373) ).
thf(903,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( C @ ( B @ 'plus$g' ) @ ( A @ 'plus$g' ) )
= ( C @ ( A @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(64,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( A
= ( B @ ( A @ 'plus$g' ) ) )
<=> ( B = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom401) ).
thf(581,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( B = 'zero$a' )
=> ( A
= ( B @ ( A @ 'plus$g' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$g' ) ) )
=> ( B = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(253,axiom,
! [A: 'N$',B: 'N$',C: 'A$',D: 'A_n_vec_n_vec$'] :
( ( D @ ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'row_add$' ) ) ) @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ ( D @ 'row_add$' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom63) ).
thf(1654,plain,
! [A: 'N$',B: 'N$',C: 'A$',D: 'A_n_vec_n_vec$'] :
( ( D @ ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'row_add$' ) ) ) @ 'matrix_matrix_mult$' ) )
= ( C @ ( B @ ( A @ ( D @ 'row_add$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[253]) ).
thf(226,axiom,
! [A: 'N$',B: 'N$'] : ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ ( 'invertible$' @ 'fun_app$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom60) ).
thf(1517,plain,
! [A: 'N$',B: 'N$'] : ( B @ ( A @ ( 'one$' @ 'mat$' @ 'interchange_rows$' ) @ 'fun_app$c' ) @ ( 'invertible$' @ 'fun_app$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[226]) ).
thf(184,axiom,
! [A: 'A$',B: 'A$',C: 'Num$'] :
( ( A
= ( C @ 'numeral$b' @ ( B @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( ~ ( ( ( C @ 'numeral$b' )
!= 'zero$' ) )
=> ( A = 'zero$' ) )
& ( ( ( C @ 'numeral$b' )
!= 'zero$' )
=> ( ( C @ 'numeral$b' @ ( A @ 'times$' ) )
= B ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom416) ).
thf(1289,plain,
! [A: 'A$',B: 'A$',C: 'Num$'] :
( ( ( ( ( ( C @ 'numeral$b' )
= 'zero$' )
=> ( A = 'zero$' ) )
& ( ( ( C @ 'numeral$b' )
!= 'zero$' )
=> ( ( C @ 'numeral$b' @ ( A @ 'times$' ) )
= B ) ) )
=> ( A
= ( C @ 'numeral$b' @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( A
= ( C @ 'numeral$b' @ ( B @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( ( ( C @ 'numeral$b' )
= 'zero$' )
=> ( A = 'zero$' ) )
& ( ( ( C @ 'numeral$b' )
!= 'zero$' )
=> ( ( C @ 'numeral$b' @ ( A @ 'times$' ) )
= B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[184]) ).
thf(35,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'times$a' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom103) ).
thf(450,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ ( A @ 'times$a' ) @ 'times$a' ) )
= ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(151,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom254) ).
thf(1084,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[151]) ).
thf(218,axiom,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( B @ ( A @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( 'one$' @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom269) ).
thf(1476,plain,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( B @ ( A @ 'times$' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( 'one$' @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[218]) ).
thf(120,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom303) ).
thf(896,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'plus$h' ) @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(250,axiom,
( ( 'a$' @ 'gauss_Jordan$' )
= ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom14) ).
thf(1639,plain,
( ( 'a$' @ 'gauss_Jordan$' )
= ( 'a$' @ ( 'p$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[250]) ).
thf(223,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
=> ( ( A @ 'matrix_inv$' )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom12) ).
thf(1508,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ( ( A @ ( B @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) )
& ( ( B @ ( A @ 'matrix_matrix_mult$' ) )
= ( 'one$' @ 'mat$' ) ) )
=> ( ( A @ 'matrix_inv$' )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[223]) ).
thf(155,axiom,
! [A: 'A$',B: 'A$'] :
( ( A
= ( B @ ( A @ 'plus$h' ) ) )
<=> ( B = 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom400) ).
thf(1101,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B = 'zero$' )
=> ( A
= ( B @ ( A @ 'plus$h' ) ) ) )
& ( ( A
= ( B @ ( A @ 'plus$h' ) ) )
=> ( B = 'zero$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[155]) ).
thf(79,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( B
= ( A @ ( C @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( A @ ( B @ 'times$' ) )
= C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom383) ).
thf(652,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( ( A @ ( B @ 'times$' ) )
= C )
=> ( B
= ( A @ ( C @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( B
= ( A @ ( C @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( A @ ( B @ 'times$' ) )
= C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(139,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom293) ).
thf(1030,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'plus$h' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(262,axiom,
( 'a$'
= ( 'a$' @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom11) ).
thf(1689,plain,
( 'a$'
= ( 'a$' @ ( 'one$' @ 'mat$' @ 'matrix_matrix_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[262]) ).
thf(19,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom378) ).
thf(378,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= ( B @ ( C @ 'plus$d' ) ) )
=> ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(49,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( A @ 'matrix_vector_mult$' ) @ ( B @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom321) ).
thf(510,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'plus$d' ) @ ( A @ 'matrix_vector_mult$' ) )
= ( C @ ( A @ 'matrix_vector_mult$' ) @ ( B @ ( A @ 'matrix_vector_mult$' ) @ 'plus$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(82,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= ( A @ ( C @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom91) ).
thf(667,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= ( A @ ( C @ 'times$' ) ) )
& ( A != 'zero$' ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(168,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= C )
<=> ( B
= ( A @ ( C @ 'times$' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom384) ).
thf(1193,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( B
= ( A @ ( C @ 'times$' ) ) )
=> ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= C ) )
& ( ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= C )
=> ( B
= ( A @ ( C @ 'times$' ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[168]) ).
thf(42,axiom,
! [A: 'A_n_vec$'] :
( ( 'one$a' @ ( A @ 'times$a' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom111) ).
thf(478,plain,
! [A: 'A_n_vec$'] :
( ( 'one$a' @ ( A @ 'times$a' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(20,axiom,
! [A: 'A_n_vec$'] :
( ( 'one$a' @ ( A @ 'times$a' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom82) ).
thf(383,plain,
! [A: 'A_n_vec$'] :
( ( 'one$a' @ ( A @ 'times$a' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(121,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom262) ).
thf(899,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( C @ ( A @ 'times$' ) @ ( B @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= ( C @ ( B @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(34,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom227) ).
thf(447,plain,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(109,axiom,
! [A: 'A$',B: 'A$',C: 'Num$'] :
( ( C @ 'numeral$b' @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ 'numeral$b' @ ( B @ 'times$' ) @ ( C @ 'numeral$b' @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom414) ).
thf(833,plain,
! [A: 'A$',B: 'A$',C: 'Num$'] :
( ( C @ 'numeral$b' @ ( B @ ( A @ 'plus$h' ) @ 'times$' ) )
= ( C @ 'numeral$b' @ ( B @ 'times$' ) @ ( C @ 'numeral$b' @ ( A @ 'times$' ) @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(247,axiom,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= 'one$' )
<=> ( B = A ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom390) ).
thf(1625,plain,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( ( B = A )
=> ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= 'one$' ) )
& ( ( ( A @ ( B @ 'divide$' @ 'fun_app$d' ) )
= 'one$' )
=> ( B = A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[247]) ).
thf(24,axiom,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom289) ).
thf(405,plain,
! [A: 'A_n_vec$'] :
( ( 'zero$c' @ ( A @ 'plus$d' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(258,axiom,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( A @ 'mat$' @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom124) ).
thf(1673,plain,
! [A: 'A$'] :
( ( A != 'zero$' )
=> ( A @ 'mat$' @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[258]) ).
thf(282,axiom,
! [A: 'A$',B: 'A$'] :
( ( A
= ( B @ ( A @ 'times$' ) ) )
<=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom131) ).
thf(1757,plain,
! [A: 'A$',B: 'A$'] :
( ( ( ( B = 'one$' )
| ( A = 'zero$' ) )
=> ( A
= ( B @ ( A @ 'times$' ) ) ) )
& ( ( A
= ( B @ ( A @ 'times$' ) ) )
=> ( ( B = 'one$' )
| ( A = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[282]) ).
thf(219,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ ( A @ 'equivalent_matrices$' @ 'fun_app$' ) )
<=> ? [C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( B
= ( D @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( D @ ( 'invertible$' @ 'fun_app$' ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom29) ).
thf(1480,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( ? [C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( B
= ( D @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( D @ ( 'invertible$' @ 'fun_app$' ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) )
=> ( B @ ( A @ 'equivalent_matrices$' @ 'fun_app$' ) ) )
& ( ( B @ ( A @ 'equivalent_matrices$' @ 'fun_app$' ) )
=> ? [C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( B
= ( D @ ( A @ ( C @ 'matrix_inv$' @ 'matrix_matrix_mult$' ) @ 'matrix_matrix_mult$' ) ) )
& ( D @ ( 'invertible$' @ 'fun_app$' ) )
& ( C @ ( 'invertible$' @ 'fun_app$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[219]) ).
thf(68,axiom,
! [A: 'A_n_vec$'] :
( ( A @ 'columnvector$' @ 'transpose$' )
= ( A @ 'rowvector$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom203) ).
thf(603,plain,
! [A: 'A_n_vec$'] :
( ( A @ 'columnvector$' @ 'transpose$' )
= ( A @ 'rowvector$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(9,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ 'times$a' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom95) ).
thf(315,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$',C: 'A_n_vec$'] :
( ( C @ ( B @ 'times$a' ) @ ( A @ 'times$a' ) )
= ( C @ ( A @ 'times$a' ) @ ( B @ 'times$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(273,axiom,
! [A: 'A$',B: 'A$',C: 'N$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= 'one$' )
& ( ( B @ ( A @ 'times$' ) )
= 'one$' ) )
=> ( A @ ( C @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom58) ).
thf(1725,plain,
! [A: 'A$',B: 'A$',C: 'N$'] :
( ( ( ( A @ ( B @ 'times$' ) )
= 'one$' )
& ( ( B @ ( A @ 'times$' ) )
= 'one$' ) )
=> ( A @ ( C @ ( 'one$' @ 'mat$' @ 'mult_column$' ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[273]) ).
thf(177,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ 'plus$h' ) )
= ( A @ ( C @ ( A @ ( B @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom276) ).
thf(1248,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ 'plus$h' ) )
= ( A @ ( C @ ( A @ ( B @ 'times$' ) @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[177]) ).
thf(103,axiom,
! [A: 'A_n_vec_n_vec$'] :
( ( ( A @ 'transpose$' )
= 'zero$a' )
<=> ( A = 'zero$a' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom67) ).
thf(790,plain,
! [A: 'A_n_vec_n_vec$'] :
( ( ( A = 'zero$a' )
=> ( ( A @ 'transpose$' )
= 'zero$a' ) )
& ( ( ( A @ 'transpose$' )
= 'zero$a' )
=> ( A = 'zero$a' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(125,axiom,
! [A: 'A$',B: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
!= 'zero$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom143) ).
thf(918,plain,
! [A: 'A$',B: 'A$'] :
( ( ( B != 'zero$' )
& ( A != 'zero$' ) )
=> ( ( B @ ( A @ 'times$' ) )
!= 'zero$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(254,axiom,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'times$' ) )
= A ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom85) ).
thf(1657,plain,
! [A: 'A$'] :
( ( 'one$' @ ( A @ 'times$' ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[254]) ).
thf(98,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom253) ).
thf(767,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ 'divide$' @ 'fun_app$d' ) @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ ( A @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(81,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom106) ).
thf(664,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'times$' ) @ 'times$' ) )
= ( C @ ( B @ 'times$' ) @ ( A @ 'times$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(140,axiom,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'plus$h' ) )
= ( A @ ( B @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom368) ).
thf(1033,plain,
! [A: 'A$',B: 'A$'] :
( ( B @ ( A @ 'plus$h' ) )
= ( A @ ( B @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(108,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$g' ) ) )
=> ( ( D @ ( A @ 'plus$g' ) )
= ( D @ ( C @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom343) ).
thf(828,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$',D: 'A_n_vec_n_vec$'] :
( ( A
= ( C @ ( B @ 'plus$g' ) ) )
=> ( ( D @ ( A @ 'plus$g' ) )
= ( D @ ( C @ 'plus$g' ) @ ( B @ 'plus$g' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(131,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B != 'zero$' )
=> ( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( B @ ( B @ ( C @ 'times$' ) @ ( A @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( B = 'zero$' )
=> ( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom271) ).
thf(960,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B != 'zero$' )
=> ( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= ( B @ ( B @ ( C @ 'times$' ) @ ( A @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( B = 'zero$' )
=> ( ( C @ ( B @ ( A @ 'divide$' @ 'fun_app$d' ) @ 'plus$h' ) )
= C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(217,axiom,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$',D: 'A$'] :
( ( D @ ( C @ ( B @ ( 'one$' @ 'mat$' @ 'column_add$' ) ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( D @ ( C @ ( B @ ( A @ 'column_add$' ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom33) ).
thf(1473,plain,
! [A: 'A_n_vec_n_vec$',B: 'N$',C: 'N$',D: 'A$'] :
( ( D @ ( C @ ( B @ ( 'one$' @ 'mat$' @ 'column_add$' ) ) ) @ ( A @ 'matrix_matrix_mult$' ) )
= ( D @ ( C @ ( B @ ( A @ 'column_add$' ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[217]) ).
thf(159,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom380) ).
thf(1129,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( B @ ( C @ 'plus$h' ) ) )
=> ( A = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[159]) ).
thf(62,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ 'transpose$' @ ( A @ 'vector_matrix_mult$a' ) )
= ( A @ ( B @ 'matrix_vector_mult$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom183) ).
thf(575,plain,
! [A: 'A_n_vec$',B: 'A_n_vec_n_vec$'] :
( ( B @ 'transpose$' @ ( A @ 'vector_matrix_mult$a' ) )
= ( A @ ( B @ 'matrix_vector_mult$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(198,axiom,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( A
= ( C @ ( B @ 'plus$h' ) ) )
=> ( ( A @ ( D @ 'plus$h' ) )
= ( C @ ( D @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom350) ).
thf(1378,plain,
! [A: 'A$',B: 'A$',C: 'A$',D: 'A$'] :
( ( A
= ( C @ ( B @ 'plus$h' ) ) )
=> ( ( A @ ( D @ 'plus$h' ) )
= ( C @ ( D @ 'plus$h' ) @ ( B @ 'plus$h' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[198]) ).
thf(234,axiom,
( ( 'zero$' @ 'dbl_inc$b' )
= 'one$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom206) ).
thf(1550,plain,
( ( 'zero$' @ 'dbl_inc$b' )
= 'one$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[234]) ).
thf(38,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'plus$d' ) )
= B )
<=> ( A = 'zero$c' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom230) ).
thf(459,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( A = 'zero$c' )
=> ( ( B @ ( A @ 'plus$d' ) )
= B ) )
& ( ( ( B @ ( A @ 'plus$d' ) )
= B )
=> ( A = 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(112,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
<=> ( ( A = 'zero$' )
| ( B = C ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom73) ).
thf(850,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A = 'zero$' )
| ( B = C ) )
=> ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) ) )
& ( ( ( B @ ( A @ 'times$' ) )
= ( C @ ( A @ 'times$' ) ) )
=> ( ( A = 'zero$' )
| ( B = C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(135,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
=> ( B = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom377) ).
thf(1004,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'plus$h' ) )
= ( C @ ( A @ 'plus$h' ) ) )
=> ( B = C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(136,axiom,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= B ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom257) ).
thf(1009,plain,
! [A: 'A$',B: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( A @ ( B @ 'times$' ) @ 'divide$' @ 'fun_app$d' ) )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(7,axiom,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'times$a' ) )
= 'zero$c' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom133) ).
thf(309,plain,
! [A: 'A_n_vec$'] :
( ( A @ ( 'zero$c' @ 'times$a' ) )
= 'zero$c' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(220,axiom,
! [A: 'N$',B: 'N$',C: 'A$'] :
( ( A != B )
=> ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'column_add$' ) ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom32) ).
thf(1490,plain,
! [A: 'N$',B: 'N$',C: 'A$'] :
( ( A != B )
=> ( C @ ( B @ ( A @ ( 'one$' @ 'mat$' @ 'column_add$' ) ) ) @ ( 'invertible$' @ 'fun_app$' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[220]) ).
thf(75,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ 'plus$h' ) )
= ( A @ ( A @ ( B @ 'times$' ) @ ( C @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom275) ).
thf(639,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( A != 'zero$' )
=> ( ( A @ ( C @ 'divide$' @ 'fun_app$d' ) @ ( B @ 'plus$h' ) )
= ( A @ ( A @ ( B @ 'times$' ) @ ( C @ 'plus$h' ) @ 'divide$' @ 'fun_app$d' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(46,axiom,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'times$a' ) )
!= 'zero$c' )
=> ( ( B != 'zero$c' )
& ( A != 'zero$c' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom146) ).
thf(496,plain,
! [A: 'A_n_vec$',B: 'A_n_vec$'] :
( ( ( B @ ( A @ 'times$a' ) )
!= 'zero$c' )
=> ( ( B != 'zero$c' )
& ( A != 'zero$c' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(90,axiom,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
<=> ( A = C ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom361) ).
thf(708,plain,
! [A: 'A_n_vec_n_vec$',B: 'A_n_vec_n_vec$',C: 'A_n_vec_n_vec$'] :
( ( ( A = C )
=> ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) ) )
& ( ( ( B @ ( A @ 'plus$g' ) )
= ( B @ ( C @ 'plus$g' ) ) )
=> ( A = C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(118,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ 'divide$' @ 'fun_app$d' ) ) )
<=> ( ( A = C )
| ( B = 'zero$' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom250) ).
thf(882,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( ( ( A = C )
| ( B = 'zero$' ) )
=> ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ 'divide$' @ 'fun_app$d' ) ) ) )
& ( ( ( B @ ( A @ 'divide$' @ 'fun_app$d' ) )
= ( B @ ( C @ 'divide$' @ 'fun_app$d' ) ) )
=> ( ( A = C )
| ( B = 'zero$' ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(205,axiom,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'plus$h' ) )
= ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom338) ).
thf(1417,plain,
! [A: 'A$',B: 'A$',C: 'A$'] :
( ( C @ ( B @ ( A @ 'plus$h' ) @ 'plus$h' ) )
= ( C @ ( B @ 'plus$h' ) @ ( A @ 'plus$h' ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[205]) ).
thf(66,axiom,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'times$' ) )
= 'zero$' ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom75) ).
thf(592,plain,
! [A: 'A$'] :
( ( A @ ( 'zero$' @ 'times$' ) )
= 'zero$' ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(215,axiom,
( ( 'a$' @ 'gauss_Jordan$' )
= ( 'one$' @ 'mat$' ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom15) ).
thf(1468,plain,
( ( 'a$' @ 'gauss_Jordan$' )
= ( 'one$' @ 'mat$' ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[215]) ).
thf(1828,plain,
$false,
inference(e,[status(thm)],[1665,1036,1411,1823,1168,1633,893,481,347,1729,909,628,1596,1522,1205,1437,861,1750,408,523,1158,741,1073,1426,1608,1137,1310,550,1735,472,1327,1063,1354,670,1497,1705,1095,417,301,1366,1529,1703,1623,389,724,1660,504,1330,1511,344,357,542,1313,1279,817,559,1641,1087,1514,969,606,1013,770,1815,1494,475,646,1383,806,1283,1109,321,397,734,293,453,411,428,1697,507,312,1651,942,678,1691,661,1768,1636,1470,1708,798,1057,334,1387,952,1519,1676,820,1560,1423,467,847,1602,625,879,1457,493,456,324,1350,578,615,1227,420,1397,697,1541,1375,1121,1446,1414,526,1324,1231,1552,1060,1429,1599,1715,1525,1333,1318,1202,360,921,1563,1286,1663,1616,1185,773,718,1732,765,1712,1054,906,298,1747,444,513,1754,1620,545,1795,1701,1786,936,1271,787,784,990,1542,567,649,1175,1574,1806,1771,737,318,609,700,1460,1022,1820,1112,1688,1171,1699,306,563,1364,431,1694,1044,1245,1066,1445,1076,531,680,1420,1134,939,553,836,490,675,1208,589,295,414,1252,1098,993,1070,872,1743,1400,673,1813,1188,441,370,1262,1538,1679,643,1738,1218,744,864,595,612,876,1240,1585,386,556,1817,1321,903,581,1654,1517,1289,450,1084,1476,896,1639,1508,1101,652,1030,1689,378,510,667,1193,478,383,899,447,833,1625,405,1673,1757,1480,603,315,1725,1248,790,918,1657,767,664,1033,828,960,1473,1129,575,1378,1550,459,850,1004,1009,309,1490,639,496,708,882,1417,592,1468]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP341_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.14/0.41 % Computer : n004.cluster.edu
% 0.14/0.41 % Model : x86_64 x86_64
% 0.14/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.41 % Memory : 8046.5625MB
% 0.14/0.41 % OS : Linux 6.8.0-71-generic
% 0.14/0.41 % CPULimit : 300
% 0.14/0.41 % WCLimit : 300
% 0.14/0.41 % DateTime : Fri Sep 25 19:08:06 UTC 2026
% 0.14/0.41 % CPUTime :
% 0.14/0.41 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.84/0.98 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 2.80/1.53 % [INFO] Parsing done (540ms).
% 2.80/1.54 % [INFO] Running in sequential loop mode.
% 3.91/1.93 % [INFO] eprover registered as external prover.
% 3.91/1.94 % [INFO] Scanning for conjecture ...
% 4.16/2.13 % [INFO] Found a conjecture (or negated_conjecture) and 418 axioms. Running axiom selection ...
% 4.90/2.30 % [INFO] Axiom selection finished. Selected 290 axioms (removed 128 axioms).
% 5.72/2.58 % [INFO] Problem is typed first-order (TPTP TFF).
% 6.06/2.61 % [INFO] Type checking passed.
% 6.06/2.61 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 11.14/3.94 % [INFO] [Domain constraints] Detected constraint on tlbool
% 11.14/3.94 % [INFO] [Domain constraints] dom(tlbool) ⊆ {tltrue,tlfalse}
% 14.33/4.78 % External prover 'e' found a proof!
% 14.33/4.78 % [INFO] Killing All external provers ...
% 14.33/4.78 % Time passed: 4230ms (effective reasoning time: 3237ms)
% 14.33/4.78 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 14.33/4.79 % Axioms used in derivation (290): axiom32, axiom260, axiom280, axiom127, axiom315, axiom28, axiom76, axiom273, axiom61, axiom230, axiom6, axiom295, axiom396, axiom25, axiom14, axiom214, axiom322, axiom307, axiom142, axiom169, axiom65, axiom36, axiom203, axiom131, axiom10, axiom386, axiom337, axiom119, axiom344, axiom138, axiom191, axiom17, axiom401, axiom257, axiom397, axiom172, axiom266, axiom147, axiom341, axiom329, axiom376, axiom42, axiom239, axiom300, axiom350, axiom195, axiom162, axiom358, axiom161, axiom123, axiom246, axiom383, axiom134, axiom33, axiom150, axiom87, axiom11, axiom130, axiom235, axiom98, axiom304, axiom225, axiom365, axiom39, axiom330, axiom251, axiom64, axiom27, axiom179, axiom283, axiom126, axiom289, axiom236, axiom59, axiom247, axiom48, axiom217, axiom343, axiom411, axiom294, axiom115, formula_418, axiom228, axiom94, axiom5, axiom121, axiom321, axiom35, axiom24, axiom278, axiom272, axiom60, axiom56, axiom137, axiom206, axiom13, axiom143, axiom359, axiom416, axiom387, axiom90, axiom16, axiom400, axiom258, axiom75, axiom385, axiom332, axiom9, axiom303, axiom185, axiom133, axiom80, axiom371, axiom146, axiom355, axiom202, axiom252, axiom360, axiom263, axiom415, axiom254, axiom82, formula_419, axiom45, axiom229, axiom174, axiom398, axiom382, axiom243, axiom319, axiom347, axiom67, axiom213, axiom72, axiom232, axiom310, axiom122, axiom91, axiom267, axiom163, axiom89, axiom38, axiom377, axiom218, axiom86, axiom111, axiom120, axiom297, axiom279, axiom12, axiom390, axiom37, axiom331, axiom205, axiom193, axiom152, axiom190, axiom41, axiom149, axiom189, axiom375, axiom394, axiom23, axiom227, axiom93, axiom216, axiom320, axiom30, axiom313, axiom118, axiom275, axiom63, axiom19, axiom102, axiom8, axiom259, axiom74, axiom276, axiom85, axiom233, axiom186, axiom367, axiom378, axiom57, axiom374, axiom153, axiom71, axiom282, axiom271, axiom287, axiom4, axiom255, axiom106, axiom15, axiom129, axiom114, axiom244, axiom136, axiom414, axiom170, axiom181, axiom262, axiom335, axiom268, axiom293, axiom175, axiom237, axiom26, axiom356, axiom298, axiom46, axiom248, axiom110, axiom125, axiom49, axiom18, axiom338, axiom379, axiom88, axiom92, axiom389, axiom226, axiom399, axiom66, axiom215, axiom296, axiom141, axiom357, axiom274, axiom269, axiom7, axiom81, axiom103, axiom231, axiom306, axiom253, axiom368, axiom29, axiom361, axiom99, axiom128, axiom264, axiom20, axiom349, axiom249, axiom183, axiom301, axiom380, axiom177, axiom31, axiom159, axiom402, axiom384, axiom73, axiom107, axiom171, axiom40, axiom265, axiom47, axiom270, axiom176, axiom187, axiom245, axiom288, axiom69, axiom277, axiom373, axiom144, axiom312, axiom95, axiom238, axiom281, axiom124, axiom261, axiom77, axiom256, axiom388, axiom160, axiom43, axiom309, axiom62, axiom21, axiom140, axiom139, axiom250, axiom58, axiom234, axiom362, axiom194, axiom353
% 14.33/4.79 % No. of inferences in proof: 584
% 14.33/4.79 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p : 4230 ms resp. 3237 ms w/o parsing
% 15.53/5.08 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 15.53/5.08 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------