%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP338_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 : Tue Sep 29 11:39:24 AM UTC 2026
% Result : Theorem 0.39s 0.67s
% Output : Refutation 0.39s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ITP338_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.20/0.44 % Computer : n014.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Sun Sep 27 12:54:46 UTC 2026
% 0.20/0.44 % CPUTime :
% 0.20/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.23/0.49 Running first-order model finding
% 0.23/0.49 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.39/0.67 % (791268)Will run a generic schedule for satisfiability detection.
% 0.39/0.67 % (791275)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2203243164:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.39/0.67 % (791274)% WARNING: option uhcvi not known.
% 0.39/0.67 % (791273)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1880075751_2999 on theBenchmark for (2999ds/0Mi)
% 0.39/0.67 % (791276)dis+10_1_sil=32000:sp=arity:random_seed=3877430971:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.39/0.67 % (791274)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2254262584:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.39/0.67 % (791279)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1875108498:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.39/0.67 % (791277)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3343192432:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.39/0.67 % (791278)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3612519554:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.39/0.67 % (791273)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 0.39/0.67 % (791273)Terminated due to inappropriate strategy.
% 0.39/0.67 % (791273)------------------------------
% 0.39/0.67 % (791273)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.67 % (791273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.67 % (791273)CaDiCaL version: 2.1.3
% 0.39/0.67 % (791273)Termination reason: Inappropriate
% 0.39/0.67 % (791273)Time elapsed: 0.053 s
% 0.39/0.67 % (791273)Peak memory usage: 12 MB
% 0.39/0.67 % (791273)Instructions burned: 60 (million)
% 0.39/0.67 % (791273)------------------------------
% 0.39/0.67 % (791273)------------------------------
% 0.39/0.67 % (791287)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3357795540:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 0.39/0.67 % (791275) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-791268-791275"...
% 0.39/0.67 % (791274) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-791268-791274"...
% 0.39/0.67 % (791276)Instruction limit reached!
% 0.39/0.67 % (791276)------------------------------
% 0.39/0.67 % (791276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.67 % (791276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.67 % (791276)CaDiCaL version: 2.1.3
% 0.39/0.67 % (791276)Termination reason: Instruction limit
% 0.39/0.67 % (791276)Termination phase: Saturation
% 0.39/0.67 % (791276)Time elapsed: 0.095 s
% 0.39/0.67 % (791276)Peak memory usage: 13 MB
% 0.39/0.67 % (791276)Instructions burned: 103 (million)
% 0.39/0.67 % (791275)...printing done.
% 0.39/0.67 % (791275)Refutation found. Thanks to Tanya!
% 0.39/0.67 % SZS status Theorem for theBenchmark
% 0.39/0.67 % SZS output start Proof for theBenchmark
% 0.39/0.67 tff(type_def_5, type, 'A_nat_a_b_vec_c_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_6, type, 'A_a_iarray_iarray_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_7, type, 'A_c_vec_c_vec$': $tType).
% 0.39/0.67 tff(type_def_8, type, 'A_nat_a_iarray_iarray_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_9, type, 'A_a_prod$': $tType).
% 0.39/0.67 tff(type_def_10, type, 'A_iarray_iarray$': $tType).
% 0.39/0.67 tff(type_def_11, type, 'A_nat_a_b_vec_c_vec_prod_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_12, type, 'A_a_c_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_13, type, 'Int_int_prod$': $tType).
% 0.39/0.67 tff(type_def_14, type, 'C_a_b_vec_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_15, type, 'A_c_vec_c_vec_a_b_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_16, type, 'A_a_b_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_17, type, 'Nat_a_iarray_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_18, type, 'A_a_iarray_iarray_prod$': $tType).
% 0.39/0.67 tff(type_def_19, type, 'Nat_a_c_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_20, type, 'A_a_b_vec_c_vec_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_21, type, 'Int_set$': $tType).
% 0.39/0.67 tff(type_def_22, type, 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_23, type, 'Int_int_fun$': $tType).
% 0.39/0.67 tff(type_def_24, type, 'A_b_vec_b_vec$': $tType).
% 0.39/0.67 tff(type_def_25, type, 'B$': $tType).
% 0.39/0.67 tff(type_def_26, type, 'A_b_vec_c_vec$': $tType).
% 0.39/0.67 tff(type_def_27, type, 'Nat_a_iarray_iarray_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_28, type, 'C_a_b_vec_fun$': $tType).
% 0.39/0.67 tff(type_def_29, type, 'A_c_vec_b_vec$': $tType).
% 0.39/0.67 tff(type_def_30, type, 'Nat_nat_fun$': $tType).
% 0.39/0.67 tff(type_def_31, type, 'C$': $tType).
% 0.39/0.67 tff(type_def_32, type, 'Nat$': $tType).
% 0.39/0.67 tff(type_def_33, type, 'A_b_vec$': $tType).
% 0.39/0.67 tff(type_def_34, type, 'A_nat_a_iarray_iarray_prod_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_35, type, 'A_iarray_iarray_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_36, type, 'B_a_fun$': $tType).
% 0.39/0.67 tff(type_def_37, type, 'Nat_a_b_vec_c_vec_prod_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_38, type, 'A_nat_a_b_vec_b_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_39, type, 'A_nat_a_c_vec_b_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_40, type, tlbool: $tType).
% 0.39/0.67 tff(type_def_41, type, 'A_b_vec_c_vec_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_42, type, 'A_nat_a_c_vec_c_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_43, type, 'A_b_vec_b_vec_a_c_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_44, type, 'A_a_b_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_45, type, 'A_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_46, type, 'Nat_a_iarray_iarray_prod$': $tType).
% 0.39/0.67 tff(type_def_47, type, 'A_c_vec_c_vec_a_c_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_48, type, 'A_int_prod$': $tType).
% 0.39/0.67 tff(type_def_49, type, 'A_set$': $tType).
% 0.39/0.67 tff(type_def_50, type, 'A_iarray_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_51, type, 'A_nat_a_iarray_iarray_prod_prod_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_52, type, 'A_c_vec$': $tType).
% 0.39/0.67 tff(type_def_53, type, 'Nat_a_b_vec_c_vec_bool_fun_fun$': $tType).
% 0.39/0.67 tff(type_def_54, type, 'A$': $tType).
% 0.39/0.67 tff(type_def_55, type, 'A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_56, type, 'Nat_a_c_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_57, type, 'Int_a_prod$': $tType).
% 0.39/0.67 tff(type_def_58, type, 'Nat_a_b_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_59, type, 'Nat_a_iarray_iarray_prod_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_60, type, 'A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_61, type, 'A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_62, type, 'A_a_c_vec_c_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_63, type, 'A_a_fun$': $tType).
% 0.39/0.67 tff(type_def_64, type, 'Nat_a_b_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_65, type, 'Nat_a_iarray_prod_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_66, type, 'A_b_vec_c_vec_c_vec$': $tType).
% 0.39/0.67 tff(type_def_67, type, 'A_iarray$': $tType).
% 0.39/0.67 tff(type_def_68, type, 'A_b_vec_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_69, type, 'Nat_a_iarray_prod$': $tType).
% 0.39/0.67 tff(type_def_70, type, 'Nat_bool_fun$': $tType).
% 0.39/0.67 tff(type_def_71, type, 'A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$': $tType).
% 0.39/0.67 tff(type_def_72, type, 'A_b_vec_b_vec_a_b_vec_b_vec_prod$': $tType).
% 0.39/0.67 tff(type_def_73, type, 'Nat_set$': $tType).
% 0.39/0.67 tff(type_def_74, type, 'B_a_bool_fun_fun$': $tType).
% 0.39/0.67 tff(func_def_0, type, 'gauss_Jordan_in_ij_det_P_iarrays$': ('A_iarray_iarray$' * 'Nat$' * 'Nat$') > 'A_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_1, type, 'times$a': ($int * $int) > $int).
% 0.39/0.67 tff(func_def_2, type, 'snd$t': 'A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$' > 'Nat_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_3, type, 'zero$i': 'Int_a_prod$').
% 0.39/0.67 tff(func_def_4, type, 'fun_app$r': ('Nat_a_iarray_bool_fun_fun$' * 'Nat$') > 'A_iarray_bool_fun$').
% 0.39/0.67 tff(func_def_5, type, 'times$b': 'Nat$' > 'Nat_nat_fun$').
% 0.39/0.67 tff(func_def_6, type, 'pair$x': ('A_c_vec_c_vec$' * 'A_b_vec_c_vec$') > 'A_c_vec_c_vec_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_7, type, 'snd$': 'Nat_a_b_vec_c_vec_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_8, type, 'plus$b': ('C$' * 'C$') > 'C$').
% 0.39/0.67 tff(func_def_9, type, 'from_nat$a': 'Nat$' > 'B$').
% 0.39/0.67 tff(func_def_10, type, 'fst$k': 'A_nat_a_c_vec_b_vec_prod_prod$' > 'A$').
% 0.39/0.67 tff(func_def_11, type, 'uu$': 'A_a_fun$').
% 0.39/0.67 tff(func_def_12, type, 'plus$c': ('B$' * 'B$') > 'B$').
% 0.39/0.67 tff(func_def_13, type, 'nrows$c': 'A_b_vec_b_vec$' > 'Nat$').
% 0.39/0.67 tff(func_def_14, type, 'uua$': 'Int_int_fun$').
% 0.39/0.67 tff(func_def_15, type, 'pair$r': ('A_c_vec_c_vec$' * 'Nat_a_c_vec_c_vec_prod$') > 'A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_16, type, 'pair$b': ('Nat$' * 'A_iarray$') > 'Nat_a_iarray_prod$').
% 0.39/0.67 tff(func_def_17, type, 'uud$': 'A_a_fun$').
% 0.39/0.67 tff(func_def_18, type, 'fst$e': 'A_nat_a_b_vec_c_vec_prod_prod$' > 'A$').
% 0.39/0.67 tff(func_def_19, type, 'gauss_Jordan_column_k_det_P_iarrays$': ('A_nat_a_iarray_iarray_prod_prod$' * 'Nat$') > 'A_nat_a_iarray_iarray_prod_prod$').
% 0.39/0.67 tff(func_def_20, type, 'snd$c': 'Nat_a_iarray_iarray_prod$' > 'A_iarray_iarray$').
% 0.39/0.67 tff(func_def_21, type, 'fun_app$t': ('Nat_a_iarray_iarray_bool_fun_fun$' * 'Nat$') > 'A_iarray_iarray_bool_fun$').
% 0.39/0.67 tff(func_def_22, type, 'uuf$': 'Int_int_fun$').
% 0.39/0.67 tff(func_def_23, type, 'fun_app$l': ('B_a_bool_fun_fun$' * 'B$') > 'A_bool_fun$').
% 0.39/0.67 tff(func_def_24, type, 'pair$u': ('A_b_vec_b_vec$' * 'A_c_vec_b_vec$') > 'A_b_vec_b_vec_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_25, type, 'pair$p': ($int * 'A$') > 'Int_a_prod$').
% 0.39/0.67 tff(func_def_26, type, 'pair$a': ('Nat$' * 'A_b_vec_c_vec$') > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_27, type, 'fun_app$d': ('C_a_b_vec_fun$' * 'C$') > 'A_b_vec$').
% 0.39/0.67 tff(func_def_28, type, 'fst$u': 'A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_29, type, 'gauss_Jordan_in_ij_det_P$b': ('A_c_vec_b_vec$' * 'B$' * 'C$') > 'A_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_30, type, 'zero$': 'Nat$').
% 0.39/0.67 tff(func_def_31, type, 'gauss_Jordan_column_k_det_P$': ('A_nat_a_c_vec_c_vec_prod_prod$' * 'Nat$') > 'A_nat_a_c_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_32, type, 'snd$e': 'A_a_iarray_iarray_prod$' > 'A_iarray_iarray$').
% 0.39/0.67 tff(func_def_33, type, 'zero$j': 'Int_int_prod$').
% 0.39/0.67 tff(func_def_34, type, 'times$': 'A$' > 'A_a_fun$').
% 0.39/0.67 tff(func_def_35, type, 'fun_app$v': ('A_nat_a_b_vec_c_vec_prod_bool_fun_fun$' * 'A$') > 'Nat_a_b_vec_c_vec_prod_bool_fun$').
% 0.39/0.67 tff(func_def_36, type, 'fst$t': 'A_b_vec_b_vec_a_c_vec_b_vec_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_37, type, 'plus$q': ('A_set$' * 'A_set$') > 'A_set$').
% 0.39/0.67 tff(func_def_38, type, 'zero$a': 'A$').
% 0.39/0.67 tff(func_def_39, type, 'row_add_iterate_PA$': ('A_c_vec_c_vec_a_b_vec_c_vec_prod$' * 'Nat$' * 'C$' * 'B$') > 'A_c_vec_c_vec_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_40, type, 'plus$o': ('A_b_vec$' * 'A_b_vec$') > 'A_b_vec$').
% 0.39/0.67 tff(func_def_41, type, 'nrows$': 'A_b_vec_c_vec$' > 'Nat$').
% 0.39/0.67 tff(func_def_42, type, 'plus$h': ('A_b_vec_c_vec$' * 'A_b_vec_c_vec$') > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_43, type, 'plus$l': ('Nat_a_iarray_prod$' * 'Nat_a_iarray_prod$') > 'Nat_a_iarray_prod$').
% 0.39/0.67 tff(func_def_44, type, 'fst$g': 'Nat_a_c_vec_c_vec_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_45, type, 'zero$g': 'A_a_prod$').
% 0.39/0.67 tff(func_def_46, type, 'plus$p': ('Int_set$' * 'Int_set$') > 'Int_set$').
% 0.39/0.67 tff(func_def_47, type, 'snd$d': 'A_nat_a_iarray_iarray_prod_prod$' > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_48, type, 'plus$n': ('Int_int_prod$' * 'Int_int_prod$') > 'Int_int_prod$').
% 0.39/0.67 tff(func_def_49, type, 'vec_nth$f': ('A_b_vec_c_vec_c_vec$' * 'C$') > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_50, type, 'zero$d': 'A_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_51, type, 'of_nat$': 'Nat$' > $int).
% 0.39/0.67 tff(func_def_52, type, 'zero$f': 'C$').
% 0.39/0.67 tff(func_def_53, type, 'gauss_Jordan_in_ij_PA$a': ('A_b_vec_b_vec_a_c_vec_b_vec_prod$' * 'B$' * 'C$') > 'A_b_vec_b_vec_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_54, type, 'times$f': ('Int_set$' * 'Int_set$') > 'Int_set$').
% 0.39/0.67 tff(func_def_55, type, 'upper_triangular_upt_k$a': 'A_b_vec_c_vec_c_vec$' > 'Nat_bool_fun$').
% 0.39/0.67 tff(func_def_56, type, 'fun_app$n': ('C_a_b_vec_bool_fun_fun$' * 'C$') > 'A_b_vec_bool_fun$').
% 0.39/0.67 tff(func_def_57, type, 'pair$h': ('Nat$' * 'A_c_vec_c_vec$') > 'Nat_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_58, type, 'times$d': ('A_b_vec_c_vec$' * 'A_b_vec_c_vec$') > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_59, type, 'uuc$': 'Nat_nat_fun$').
% 0.39/0.67 tff(func_def_60, type, 'snd$x': 'A_c_vec_c_vec_a_b_vec_c_vec_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_61, type, 'zero$b': 'A_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_62, type, 'zero$e': 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_63, type, 'snd$j': 'A_nat_a_c_vec_b_vec_prod_prod$' > 'Nat_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_64, type, 'snd$n': 'Nat_a_b_vec_b_vec_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_65, type, 'i$': 'Nat$').
% 0.39/0.67 tff(func_def_66, type, 'one$c': 'B$').
% 0.39/0.67 tff(func_def_67, type, 'fst$f': 'A_nat_a_iarray_iarray_prod_prod$' > 'A$').
% 0.39/0.67 tff(func_def_68, type, 'plus$i': ('A_nat_a_b_vec_c_vec_prod_prod$' * 'A_nat_a_b_vec_c_vec_prod_prod$') > 'A_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_69, type, 'nrows$b': 'A_c_vec_b_vec$' > 'Nat$').
% 0.39/0.67 tff(func_def_70, type, 'one$': 'A$').
% 0.39/0.67 tff(func_def_71, type, 'snd$k': 'Nat_a_c_vec_b_vec_prod$' > 'A_c_vec_b_vec$').
% 0.39/0.67 tff(func_def_72, type, 'nrows$a': 'A_c_vec_c_vec$' > 'Nat$').
% 0.39/0.67 tff(func_def_73, type, 'gauss_Jordan_column_k_det_P$a': ('A_nat_a_c_vec_b_vec_prod_prod$' * 'Nat$') > 'A_nat_a_c_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_74, type, 'fst$p': 'Int_int_prod$' > $int).
% 0.39/0.67 tff(func_def_75, type, 'vec_nth$c': ('A_c_vec_c_vec$' * 'C$') > 'A_c_vec$').
% 0.39/0.67 tff(func_def_76, type, 'snd$s': 'A_c_vec_c_vec_a_c_vec_c_vec_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_77, type, 'upper_triangular_upt_k$': 'A_b_vec_b_vec$' > 'Nat_bool_fun$').
% 0.39/0.67 tff(func_def_78, type, 'pair$o': ('A$' * $int) > 'A_int_prod$').
% 0.39/0.67 tff(func_def_79, type, 'snd$a': 'A_nat_a_b_vec_c_vec_prod_prod$' > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_80, type, 'snd$i': 'A_a_c_vec_c_vec_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_81, type, 'fst$v': 'A_b_vec_b_vec_a_b_vec_b_vec_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_82, type, 'nrows_iarray$': 'A_iarray_iarray$' > 'Nat$').
% 0.39/0.67 tff(func_def_83, type, tltrue: tlbool).
% 0.39/0.67 tff(func_def_84, type, 'gauss_Jordan_column_k_PA$a': ('A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$' * 'Nat$') > 'A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_85, type, 'plus$f': ('Nat_a_iarray_iarray_prod$' * 'Nat_a_iarray_iarray_prod$') > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_86, type, 'map_matrix$': ('A_a_fun$' * 'A_b_vec_c_vec$') > 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_87, type, 'pair$s': ('A_c_vec_c_vec$' * 'A_c_vec_c_vec$') > 'A_c_vec_c_vec_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_88, type, 'one$b': 'C$').
% 0.39/0.67 tff(func_def_89, type, 'pair$j': ('Nat$' * 'A_c_vec_b_vec$') > 'Nat_a_c_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_90, type, 'one$a': 'Nat$').
% 0.39/0.67 tff(func_def_91, type, 'to_nat$a': 'B$' > 'Nat$').
% 0.39/0.67 tff(func_def_92, type, 'plus$j': ('Nat_a_b_vec_c_vec_prod$' * 'Nat_a_b_vec_c_vec_prod$') > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_93, type, 'gauss_Jordan_column_k_PA$b': ('A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$' * 'Nat$') > 'A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_94, type, 'gauss_Jordan_in_ij_PA$': ('A_c_vec_c_vec_a_c_vec_c_vec_prod$' * 'C$' * 'C$') > 'A_c_vec_c_vec_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_95, type, 'snd$g': 'A_nat_a_c_vec_c_vec_prod_prod$' > 'Nat_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_96, type, 'fst$b': 'Nat_a_b_vec_c_vec_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_97, type, 'ncols$': 'A_b_vec_c_vec$' > 'Nat$').
% 0.39/0.67 tff(func_def_98, type, 'fst$c': 'Nat_a_iarray_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_99, type, 'fun_app$': ('Int_int_fun$' * $int) > $int).
% 0.39/0.67 tff(func_def_100, type, 'fst$j': 'Nat_a_c_vec_b_vec_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_101, type, 'gauss_Jordan_in_ij_det_P$': ('A_b_vec_c_vec$' * 'C$' * 'B$') > 'A_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_102, type, 'pair$n': ('A$' * 'A$') > 'A_a_prod$').
% 0.39/0.67 tff(func_def_103, type, 'less$': 'Nat$' > 'Nat_bool_fun$').
% 0.39/0.67 tff(func_def_104, type, 'gauss_Jordan_column_k_PA$': ('A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$' * 'Nat$') > 'A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_105, type, 'fst$m': 'Nat_a_b_vec_b_vec_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_106, type, 'fun_app$c': ('B_a_fun$' * 'B$') > 'A$').
% 0.39/0.67 tff(func_def_107, type, 'gauss_Jordan_column_k_det_P$c': ('A_nat_a_b_vec_c_vec_prod_prod$' * 'Nat$') > 'A_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_108, type, 'gauss_Jordan_column_k_PA$c': ('A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$' * 'Nat$') > 'A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_109, type, 'to_nat$': 'C$' > 'Nat$').
% 0.39/0.67 tff(func_def_110, type, 'vector_all_zero_from_index$': 'Nat_a_iarray_prod_bool_fun$').
% 0.39/0.67 tff(func_def_111, type, 'vec_nth$b': ('A_c_vec$' * 'C$') > 'A$').
% 0.39/0.67 tff(func_def_112, type, 'snd$o': 'A_a_b_vec_b_vec_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_113, type, 'snd$q': 'A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$' > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_114, type, 'snd$v': 'A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$' > 'Nat_a_b_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_115, type, 'fst$h': 'A_nat_a_c_vec_c_vec_prod_prod$' > 'A$').
% 0.39/0.67 tff(func_def_116, type, 'fun_app$x': ('A_a_iarray_iarray_bool_fun_fun$' * 'A$') > 'A_iarray_iarray_bool_fun$').
% 0.39/0.67 tff(func_def_117, type, 'one$e': 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_118, type, 'fst$l': 'A_a_c_vec_b_vec_prod$' > 'A$').
% 0.39/0.67 tff(func_def_119, type, 'times$g': ('Nat_set$' * 'Nat_set$') > 'Nat_set$').
% 0.39/0.67 tff(func_def_120, type, 'snd$r': 'A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$' > 'Nat_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_121, type, 'gauss_Jordan_in_ij_det_P$a': ('A_c_vec_c_vec$' * 'C$' * 'C$') > 'A_a_c_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_122, type, 'zero$h': 'A_int_prod$').
% 0.39/0.67 tff(func_def_123, type, 'fun_app$u': ('A_a_b_vec_c_vec_bool_fun_fun$' * 'A$') > 'A_b_vec_c_vec_bool_fun$').
% 0.39/0.67 tff(func_def_124, type, 'pair$t': ('A_b_vec_b_vec$' * 'Nat_a_c_vec_b_vec_prod$') > 'A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_125, type, 'column_iarray$': ('Nat$' * 'A_iarray_iarray$') > 'A_iarray$').
% 0.39/0.67 tff(func_def_126, type, 'gauss_Jordan_in_ij_PA$b': ('A_b_vec_b_vec_a_b_vec_b_vec_prod$' * 'B$' * 'B$') > 'A_b_vec_b_vec_a_b_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_127, type, 'fst$q': 'A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_128, type, 'zero$c': 'A_b_vec_c_vec$').
% 0.39/0.67 tff(func_def_129, type, 'fst$w': 'A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_130, type, 'fst$': 'A_a_b_vec_c_vec_prod$' > 'A$').
% 0.39/0.67 tff(func_def_131, type, 'plus$a': 'Nat$' > 'Nat_nat_fun$').
% 0.39/0.67 tff(func_def_132, type, 'fst$r': 'A_c_vec_c_vec_a_c_vec_c_vec_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_133, type, 'one$d': 'A_b_vec$').
% 0.39/0.67 tff(func_def_134, type, 'vec_nth$a': 'A_b_vec_c_vec$' > 'C_a_b_vec_fun$').
% 0.39/0.67 tff(func_def_135, type, 'snd$u': 'A_b_vec_b_vec_a_c_vec_b_vec_prod$' > 'A_c_vec_b_vec$').
% 0.39/0.67 tff(func_def_136, type, 'fun_app$p': ('Nat_a_b_vec_c_vec_bool_fun_fun$' * 'Nat$') > 'A_b_vec_c_vec_bool_fun$').
% 0.39/0.67 tff(func_def_137, type, 'snd$p': 'Int_int_prod$' > $int).
% 0.39/0.67 tff(func_def_138, type, 'pair$k': ('A$' * 'Nat_a_b_vec_b_vec_prod$') > 'A_nat_a_b_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_139, type, 'pair$': ('A$' * 'Nat_a_b_vec_c_vec_prod$') > 'A_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_140, type, 'plus$m': ('A_iarray$' * 'A_iarray$') > 'A_iarray$').
% 0.39/0.67 tff(func_def_141, type, 'fst$s': 'A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_142, type, 'plus$': 'A$' > 'A_a_fun$').
% 0.39/0.67 tff(func_def_143, type, 'snd$w': 'A_b_vec_b_vec_a_b_vec_b_vec_prod$' > 'A_b_vec_b_vec$').
% 0.39/0.67 tff(func_def_144, type, 'plus$d': ('A_a_b_vec_c_vec_prod$' * 'A_a_b_vec_c_vec_prod$') > 'A_a_b_vec_c_vec_prod$').
% 0.39/0.67 tff(func_def_145, type, 'pair$d': ('Nat$' * 'A_iarray_iarray$') > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_146, type, 'less_eq$a': 'Nat$' > 'Nat_bool_fun$').
% 0.39/0.67 tff(func_def_147, type, tlfalse: tlbool).
% 0.39/0.67 tff(func_def_148, type, 'pair$i': ('A$' * 'Nat_a_c_vec_b_vec_prod$') > 'A_nat_a_c_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_149, type, 'nat$': $int > 'Nat$').
% 0.39/0.67 tff(func_def_150, type, 'fst$a': 'A_a_iarray_iarray_prod$' > 'A$').
% 0.39/0.67 tff(func_def_151, type, 'plus$g': ('A_iarray_iarray$' * 'A_iarray_iarray$') > 'A_iarray_iarray$').
% 0.39/0.67 tff(func_def_152, type, 'pair$q': ('A_c_vec_c_vec$' * 'Nat_a_b_vec_c_vec_prod$') > 'A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$').
% 0.39/0.67 tff(func_def_153, type, 'snd$f': 'Nat_a_iarray_prod$' > 'A_iarray$').
% 0.39/0.67 tff(func_def_154, type, 'zero$k': 'B$').
% 0.39/0.67 tff(func_def_155, type, 'pair$f': ('A$' * 'A_iarray_iarray$') > 'A_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_156, type, 'uug$': 'Nat_nat_fun$').
% 0.39/0.67 tff(func_def_157, type, 'matrix_to_iarray$': 'A_b_vec_c_vec$' > 'A_iarray_iarray$').
% 0.39/0.67 tff(func_def_158, type, 'plus$e': ('A_a_iarray_iarray_prod$' * 'A_a_iarray_iarray_prod$') > 'A_a_iarray_iarray_prod$').
% 0.39/0.67 tff(func_def_159, type, 'vec_nth$': 'A_b_vec$' > 'B_a_fun$').
% 0.39/0.67 tff(func_def_160, type, 'uue$': 'Int_int_fun$').
% 0.39/0.67 tff(func_def_161, type, 'fst$o': 'A_a_b_vec_b_vec_prod$' > 'A$').
% 0.39/0.67 tff(func_def_162, type, 'snd$h': 'Nat_a_c_vec_c_vec_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.67 tff(func_def_163, type, 'times$c': ('A_b_vec$' * 'A_b_vec$') > 'A_b_vec$').
% 0.39/0.67 tff(func_def_164, type, 'fun_app$w': ('A_nat_a_iarray_iarray_prod_bool_fun_fun$' * 'A$') > 'Nat_a_iarray_iarray_prod_bool_fun$').
% 0.39/0.67 tff(func_def_165, type, 'gauss_Jordan_column_k_det_P$b': ('A_nat_a_b_vec_b_vec_prod_prod$' * 'Nat$') > 'A_nat_a_b_vec_b_vec_prod_prod$').
% 0.39/0.67 tff(func_def_166, type, 'pair$c': ('A$' * 'Nat_a_iarray_iarray_prod$') > 'A_nat_a_iarray_iarray_prod_prod$').
% 0.39/0.67 tff(func_def_167, type, 'fun_app$b': ('A_a_fun$' * 'A$') > 'A$').
% 0.39/0.67 tff(func_def_168, type, 'gauss_Jordan_in_ij_det_P$c': ('A_b_vec_b_vec$' * 'B$' * 'B$') > 'A_a_b_vec_b_vec_prod$').
% 0.39/0.67 tff(func_def_169, type, 'times$e': ('A_set$' * 'A_set$') > 'A_set$').
% 0.39/0.67 tff(func_def_170, type, 'fun_app$a': ('Nat_nat_fun$' * 'Nat$') > 'Nat$').
% 0.39/0.67 tff(func_def_171, type, 'vec_nth$e': ('A_b_vec_b_vec$' * 'B$') > 'A_b_vec$').
% 0.39/0.67 tff(func_def_172, type, 'fst$i': 'A_a_c_vec_c_vec_prod$' > 'A$').
% 0.39/0.67 tff(func_def_173, type, 'from_nat$': 'Nat$' > 'C$').
% 0.39/0.67 tff(func_def_174, type, 'fst$d': 'Nat_a_iarray_iarray_prod$' > 'Nat$').
% 0.39/0.67 tff(func_def_175, type, 'plus$k': ('A_nat_a_iarray_iarray_prod_prod$' * 'A_nat_a_iarray_iarray_prod_prod$') > 'A_nat_a_iarray_iarray_prod_prod$').
% 0.39/0.67 tff(func_def_176, type, 'fst$n': 'A_nat_a_b_vec_b_vec_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_177, type, 'pair$m': ($int * $int) > 'Int_int_prod$').
% 0.39/0.68 tff(func_def_178, type, 'n$': 'A$').
% 0.39/0.68 tff(func_def_179, type, 'fst$x': 'A_c_vec_c_vec_a_b_vec_c_vec_prod$' > 'A_c_vec_c_vec$').
% 0.39/0.68 tff(func_def_180, type, 'a$': 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_181, type, 'zero$l': 'A_b_vec$').
% 0.39/0.68 tff(func_def_182, type, 'gauss_Jordan_in_ij_PA$c': ('A_c_vec_c_vec_a_b_vec_c_vec_prod$' * 'C$' * 'B$') > 'A_c_vec_c_vec_a_b_vec_c_vec_prod$').
% 0.39/0.68 tff(func_def_183, type, 'pair$l': ('Nat$' * 'A_b_vec_b_vec$') > 'Nat_a_b_vec_b_vec_prod$').
% 0.39/0.68 tff(func_def_184, type, 'snd$l': 'A_a_c_vec_b_vec_prod$' > 'A_c_vec_b_vec$').
% 0.39/0.68 tff(func_def_185, type, 'pair$e': ('A$' * 'A_b_vec_c_vec$') > 'A_a_b_vec_c_vec_prod$').
% 0.39/0.68 tff(func_def_186, type, 'snd$m': 'A_nat_a_b_vec_b_vec_prod_prod$' > 'Nat_a_b_vec_b_vec_prod$').
% 0.39/0.68 tff(func_def_187, type, 'pair$g': ('A$' * 'Nat_a_c_vec_c_vec_prod$') > 'A_nat_a_c_vec_c_vec_prod_prod$').
% 0.39/0.68 tff(func_def_188, type, 'vec_nth$d': ('A_c_vec_b_vec$' * 'B$') > 'A_c_vec$').
% 0.39/0.68 tff(func_def_189, type, 'snd$b': 'A_a_b_vec_c_vec_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_190, type, 'pair$w': ('A_b_vec_b_vec$' * 'A_b_vec_b_vec$') > 'A_b_vec_b_vec_a_b_vec_b_vec_prod$').
% 0.39/0.68 tff(func_def_191, type, 'k$': 'Nat$').
% 0.39/0.68 tff(func_def_192, type, 'uub$': 'Int_int_fun$').
% 0.39/0.68 tff(func_def_193, type, 'pair$v': ('A_b_vec_b_vec$' * 'Nat_a_b_vec_b_vec_prod$') > 'A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$').
% 0.39/0.68 tff(func_def_199, type, sK2: 'C$').
% 0.39/0.68 tff(func_def_200, type, sK3: 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' > 'A$').
% 0.39/0.68 tff(func_def_201, type, sK4: 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.68 tff(func_def_202, type, sK5: 'Nat_a_b_vec_c_vec_prod_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_203, type, sK6: 'Nat_a_b_vec_c_vec_prod_bool_fun$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_204, type, sK7: 'Nat_a_iarray_prod_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_205, type, sK8: 'Nat_a_iarray_prod_bool_fun$' > 'A_iarray$').
% 0.39/0.68 tff(func_def_206, type, sK9: 'A_nat_a_iarray_iarray_prod_prod_bool_fun$' > 'A$').
% 0.39/0.68 tff(func_def_207, type, sK10: 'A_nat_a_iarray_iarray_prod_prod_bool_fun$' > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.68 tff(func_def_208, type, sK11: 'Nat_a_iarray_iarray_prod_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_209, type, sK12: 'Nat_a_iarray_iarray_prod_bool_fun$' > 'A_iarray_iarray$').
% 0.39/0.68 tff(func_def_210, type, sK13: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_211, type, sK14: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.68 tff(func_def_212, type, sK15: 'Nat_a_b_vec_c_vec_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_213, type, sK16: 'Nat_a_b_vec_c_vec_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_214, type, sK17: 'Nat_a_iarray_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_215, type, sK18: 'Nat_a_iarray_prod$' > 'A_iarray$').
% 0.39/0.68 tff(func_def_216, type, sK19: 'A_nat_a_iarray_iarray_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_217, type, sK20: 'A_nat_a_iarray_iarray_prod_prod$' > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.68 tff(func_def_218, type, sK21: 'Nat_a_iarray_iarray_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_219, type, sK22: 'Nat_a_iarray_iarray_prod$' > 'A_iarray_iarray$').
% 0.39/0.68 tff(func_def_220, type, sK23: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_221, type, sK24: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'Nat_a_b_vec_c_vec_prod$').
% 0.39/0.68 tff(func_def_222, type, sK25: 'Nat_a_b_vec_c_vec_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_223, type, sK26: 'Nat_a_b_vec_c_vec_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_224, type, sK27: 'Nat_a_iarray_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_225, type, sK28: 'Nat_a_iarray_prod$' > 'A_iarray$').
% 0.39/0.68 tff(func_def_226, type, sK29: 'A_nat_a_iarray_iarray_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_227, type, sK30: 'A_nat_a_iarray_iarray_prod_prod$' > 'Nat_a_iarray_iarray_prod$').
% 0.39/0.68 tff(func_def_228, type, sK31: 'Nat_a_iarray_iarray_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_229, type, sK32: 'Nat_a_iarray_iarray_prod$' > 'A_iarray_iarray$').
% 0.39/0.68 tff(func_def_230, type, sK33: 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' > 'A$').
% 0.39/0.68 tff(func_def_231, type, sK34: 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_232, type, sK35: 'A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_233, type, sK36: 'A_nat_a_iarray_iarray_prod_prod_bool_fun$' > 'A$').
% 0.39/0.68 tff(func_def_234, type, sK37: 'A_nat_a_iarray_iarray_prod_prod_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_235, type, sK38: 'A_nat_a_iarray_iarray_prod_prod_bool_fun$' > 'A_iarray_iarray$').
% 0.39/0.68 tff(func_def_236, type, sK39: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_237, type, sK40: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_238, type, sK41: 'A_nat_a_b_vec_c_vec_prod_prod$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_239, type, sK42: 'A_nat_a_iarray_iarray_prod_prod$' > 'A$').
% 0.39/0.68 tff(func_def_240, type, sK43: 'A_nat_a_iarray_iarray_prod_prod$' > 'Nat$').
% 0.39/0.68 tff(func_def_241, type, sK44: 'A_nat_a_iarray_iarray_prod_prod$' > 'A_iarray_iarray$').
% 0.39/0.68 tff(func_def_242, type, sK45: ('A_nat_a_c_vec_c_vec_prod_prod$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_243, type, sK46: ('A_nat_a_c_vec_b_vec_prod_prod$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_244, type, sK47: ('A_nat_a_b_vec_b_vec_prod_prod$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_245, type, sK48: ('A_nat_a_b_vec_c_vec_prod_prod$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_246, type, sK49: 'Nat_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_247, type, sK50: 'Nat_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_248, type, sK51: 'Nat_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_249, type, sK52: 'Nat_bool_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_250, type, sK53: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 0.39/0.68 tff(func_def_251, type, sK54: 'Nat_nat_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_252, type, sK55: 'Nat_nat_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_253, type, sK56: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 0.39/0.68 tff(func_def_254, type, sK57: ('Nat$' * 'Nat$') > 'Nat$').
% 0.39/0.68 tff(func_def_255, type, sK58: ('Nat$' * 'Nat$') > 'Nat$').
% 0.39/0.68 tff(func_def_256, type, sK59: ('Nat$' * 'Nat$') > 'Nat$').
% 0.39/0.68 tff(func_def_257, type, sK60: 'Nat_nat_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_258, type, sK61: 'Nat_nat_fun$' > 'Nat$').
% 0.39/0.68 tff(func_def_259, type, sK62: ('A_b_vec$' * 'A_b_vec$') > 'B$').
% 0.39/0.68 tff(func_def_260, type, sK63: ('A_b_vec_c_vec$' * 'A_b_vec_c_vec$') > 'C$').
% 0.39/0.68 tff(func_def_261, type, sK64: ('B_a_bool_fun_fun$' * 'B$') > 'A$').
% 0.39/0.68 tff(func_def_262, type, sK65: ('B_a_bool_fun_fun$' * 'A_b_vec$') > 'B$').
% 0.39/0.68 tff(func_def_263, type, sK66: 'B_a_bool_fun_fun$' > 'A_b_vec$').
% 0.39/0.68 tff(func_def_264, type, sK67: 'B_a_bool_fun_fun$' > 'B$').
% 0.39/0.68 tff(func_def_265, type, sK68: ('C_a_b_vec_bool_fun_fun$' * 'C$') > 'A_b_vec$').
% 0.39/0.68 tff(func_def_266, type, sK69: ('C_a_b_vec_bool_fun_fun$' * 'A_b_vec_c_vec$') > 'C$').
% 0.39/0.68 tff(func_def_267, type, sK70: 'C_a_b_vec_bool_fun_fun$' > 'A_b_vec_c_vec$').
% 0.39/0.68 tff(func_def_268, type, sK71: 'C_a_b_vec_bool_fun_fun$' > 'C$').
% 0.39/0.68 tff(func_def_269, type, sK72: ('A_c_vec_c_vec_nat_a_c_vec_c_vec_prod_prod$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_270, type, sK73: ('A_b_vec_b_vec_nat_a_c_vec_b_vec_prod_prod$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_271, type, sK74: ('A_b_vec_b_vec_nat_a_b_vec_b_vec_prod_prod$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_272, type, sK75: ('A_c_vec_c_vec_nat_a_b_vec_c_vec_prod_prod$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_273, type, sK76: ('A_b_vec_b_vec$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_274, type, sK77: ('A_b_vec_b_vec$' * 'Nat$') > 'B$').
% 0.39/0.68 tff(func_def_275, type, sK78: ('A_b_vec_c_vec_c_vec$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_276, type, sK79: ('A_b_vec_c_vec_c_vec$' * 'Nat$') > 'C$').
% 0.39/0.68 tff(func_def_277, type, sK80: ('A$' * 'A_set$' * 'A_set$') > 'A$').
% 0.39/0.68 tff(func_def_278, type, sK81: ('A$' * 'A_set$' * 'A_set$') > 'A$').
% 0.39/0.68 tff(func_def_279, type, sK82: ($int * 'Int_set$' * 'Int_set$') > $int).
% 0.39/0.68 tff(func_def_280, type, sK83: ($int * 'Int_set$' * 'Int_set$') > $int).
% 0.39/0.68 tff(func_def_281, type, sK84: ('Nat$' * 'Nat_set$' * 'Nat_set$') > 'Nat$').
% 0.39/0.68 tff(func_def_282, type, sK85: ('Nat$' * 'Nat_set$' * 'Nat_set$') > 'Nat$').
% 0.39/0.68 tff(func_def_283, type, sK86: ($int * 'Int_set$' * 'Int_set$') > $int).
% 0.39/0.68 tff(func_def_284, type, sK87: ($int * 'Int_set$' * 'Int_set$') > $int).
% 0.39/0.68 tff(pred_def_1, type, 'upper_triangular$': 'A_b_vec_b_vec$' > $o).
% 0.39/0.68 tff(pred_def_2, type, 'less_eq$c': ('A_set$' * 'A_set$') > $o).
% 0.39/0.68 tff(pred_def_3, type, 'fun_app$i': ('Nat_a_iarray_iarray_prod_bool_fun$' * 'Nat_a_iarray_iarray_prod$') > $o).
% 0.39/0.68 tff(pred_def_4, type, 'divides_aux$': 'Int_int_prod$' > $o).
% 0.39/0.68 tff(pred_def_5, type, 'less_eq$b': ('B$' * 'B$') > $o).
% 0.39/0.68 tff(pred_def_6, type, 'fun_app$k': ('A_bool_fun$' * 'A$') > $o).
% 0.39/0.68 tff(pred_def_7, type, 'fun_app$g': ('Nat_a_b_vec_c_vec_prod_bool_fun$' * 'Nat_a_b_vec_c_vec_prod$') > $o).
% 0.39/0.68 tff(pred_def_8, type, 'fun_app$o': ('A_b_vec_c_vec_bool_fun$' * 'A_b_vec_c_vec$') > $o).
% 0.39/0.68 tff(pred_def_9, type, 'fun_app$s': ('A_iarray_iarray_bool_fun$' * 'A_iarray_iarray$') > $o).
% 0.39/0.68 tff(pred_def_10, type, 'fun_app$f': ('A_nat_a_b_vec_c_vec_prod_prod_bool_fun$' * 'A_nat_a_b_vec_c_vec_prod_prod$') > $o).
% 0.39/0.68 tff(pred_def_11, type, 'fun_app$h': ('A_nat_a_iarray_iarray_prod_prod_bool_fun$' * 'A_nat_a_iarray_iarray_prod_prod$') > $o).
% 0.39/0.68 tff(pred_def_12, type, 'upper_triangular$a': 'A_b_vec_c_vec_c_vec$' > $o).
% 0.39/0.68 tff(pred_def_13, type, 'less$a': ('C$' * 'C$') > $o).
% 0.39/0.68 tff(pred_def_14, type, 'fun_app$e': ('Nat_a_iarray_prod_bool_fun$' * 'Nat_a_iarray_prod$') > $o).
% 0.39/0.68 tff(pred_def_15, type, 'member$b': ('Nat$' * 'Nat_set$') > $o).
% 0.39/0.68 tff(pred_def_16, type, 'fun_app$j': ('Nat_bool_fun$' * 'Nat$') > $o).
% 0.39/0.68 tff(pred_def_17, type, 'less$b': ('B$' * 'B$') > $o).
% 0.39/0.68 tff(pred_def_18, type, 'fun_app$q': ('A_iarray_bool_fun$' * 'A_iarray$') > $o).
% 0.39/0.68 tff(pred_def_19, type, 'member$a': ('A$' * 'A_set$') > $o).
% 0.39/0.68 tff(pred_def_20, type, 'less_eq$d': ('Int_set$' * 'Int_set$') > $o).
% 0.39/0.68 tff(pred_def_21, type, 'member$': ($int * 'Int_set$') > $o).
% 0.39/0.68 tff(pred_def_22, type, 'less_eq$': ('C$' * 'C$') > $o).
% 0.39/0.68 tff(pred_def_23, type, 'fun_app$m': ('A_b_vec_bool_fun$' * 'A_b_vec$') > $o).
% 0.39/0.68 tff(f9,conjecture,(
% 0.39/0.68 ((! [X0 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X0) => 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a') | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))))))))) & (~(! [X0 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X0) => 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a') | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))))))),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture8)).
% 0.39/0.68 tff(f10,negated_conjecture,(
% 0.39/0.68 ~(((! [X0 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X0) => 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a') | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))))))))) & (~(! [X0 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X0) => 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a') | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))))))))))),
% 0.39/0.68 inference(negated_conjecture,[status(cth)],[f9])).
% 0.39/0.68 tff(f11,axiom,(
% 0.39/0.68 $lesseq('of_nat$'('i$'),'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom9)).
% 0.39/0.68 tff(f12,axiom,(
% 0.39/0.68 ~$less('of_nat$'('i$'),'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom10)).
% 0.39/0.68 tff(f273,axiom,(
% 0.39/0.68 ! [X0 : 'Nat$',X1 : 'A_b_vec_c_vec$'] : 'snd$'('pair$a'(X0,X1)) = X1),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom271)).
% 0.39/0.68 tff(f275,axiom,(
% 0.39/0.68 ! [X0 : 'Nat$',X1 : 'A_iarray_iarray$'] : 'snd$c'('pair$d'(X0,X1)) = X1),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom273)).
% 0.39/0.68 tff(f277,axiom,(
% 0.39/0.68 ! [X0 : 'A$',X1 : 'Nat_a_b_vec_c_vec_prod$'] : 'snd$a'('pair$'(X0,X1)) = X1),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom275)).
% 0.39/0.68 tff(f278,axiom,(
% 0.39/0.68 ! [X0 : 'A$',X1 : 'Nat_a_iarray_iarray_prod$'] : 'snd$d'('pair$c'(X0,X1)) = X1),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom276)).
% 0.39/0.68 tff(f573,axiom,(
% 0.39/0.68 ! [X0 : 'A_b_vec_c_vec$'] : 'of_nat$'('nrows$'(X0)) = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'(X0)))),
% 0.39/0.68 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom571)).
% 0.39/0.68 tff(f637,plain,(
% 0.39/0.68 ~$less('of_nat$'('nrows$'('a$')),'of_nat$'('i$'))),
% 0.39/0.68 inference(theory_normalization,[],[f11])).
% 0.39/0.68 tff(f784,definition,(
% 0.39/0.68 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 0.39/0.68 introduced(theory,[tha_order_totality])).
% 0.39/0.68 tff(f795,plain,(
% 0.39/0.68 ~(((! [X0 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X0) => 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a') | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))))))))) & (~(! [X1 : 'C$'] : ('less_eq$'('from_nat$'('i$'),X1) => 'zero$a' = 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X1)),'from_nat$a'('k$'))) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))) => ((('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))) & (~('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) => 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) = 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))))))))))),
% 0.39/0.68 inference(rectify,[],[f10])).
% 0.39/0.68 tff(f862,plain,(
% 0.39/0.68 ((('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) & (~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))))) & (! [X0 : 'C$'] : ('fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a' | ~'less_eq$'('from_nat$'('i$'),X0)) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$')))) | ((('snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & (~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))))) & (? [X1 : 'C$'] : ('zero$a' != 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X1)),'from_nat$a'('k$')) & 'less_eq$'('from_nat$'('i$'),X1)) & 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$'))))),
% 0.39/0.68 inference(ennf_transformation,[],[f795])).
% 0.39/0.68 tff(f863,plain,(
% 0.39/0.68 ((('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) & ~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) & (! [X0 : 'C$'] : ('fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a' | ~'less_eq$'('from_nat$'('i$'),X0)) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$')))) | ((('snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & ~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) & ? [X1 : 'C$'] : ('zero$a' != 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X1)),'from_nat$a'('k$')) & 'less_eq$'('from_nat$'('i$'),X1)) & 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 inference(flattening,[],[f862])).
% 0.39/0.68 tff(f1312,definition,(
% 0.39/0.68 ('snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('fun_app$b'('times$'('fst$'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))),'n$'),'pair$a'('nat$'($sum('of_nat$'('i$'),1)),'snd$b'('gauss_Jordan_in_ij_det_P$'('a$','from_nat$'('i$'),'from_nat$a'('k$')))))))) & ~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))) | ~ sP0),
% 0.39/0.68 introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction])).
% 0.39/0.68 tff(f1313,definition,(
% 0.39/0.68 ((('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) & ~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) & (! [X0 : 'C$'] : ('fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a' | ~'less_eq$'('from_nat$'('i$'),X0)) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$')))) | ~ sP1),
% 0.39/0.68 introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction])).
% 0.39/0.68 tff(f1314,plain,(
% 0.39/0.68 sP1 | (sP0 & ? [X1 : 'C$'] : ('zero$a' != 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X1)),'from_nat$a'('k$')) & 'less_eq$'('from_nat$'('i$'),X1)) & 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 inference(definition_folding,[],[f863,f1313,f1312])).
% 0.39/0.68 tff(f1315,plain,(
% 0.39/0.68 ((('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) & ('fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) | 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) | ('matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('fun_app$b'('times$'('fst$a'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$'))),'n$'),'pair$d'('nat$'($sum('of_nat$'('i$'),1)),'snd$e'('gauss_Jordan_in_ij_det_P_iarrays$'('matrix_to_iarray$'('a$'),'i$','k$')))))) & ~'fun_app$e'('vector_all_zero_from_index$','pair$b'('i$','column_iarray$'('k$','matrix_to_iarray$'('a$')))) & 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))))) & (! [X0 : 'C$'] : ('fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) = 'zero$a' | ~'less_eq$'('from_nat$'('i$'),X0)) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$')))) | ~sP1),
% 0.39/0.68 inference(nnf_transformation,[],[f1313])).
% 0.39/0.68 tff(f1317,plain,(
% 0.39/0.68 sP1 | (sP0 & ? [X0 : 'C$'] : ('zero$a' != 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),X0)),'from_nat$a'('k$')) & 'less_eq$'('from_nat$'('i$'),X0)) & 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 inference(rectify,[],[f1314])).
% 0.39/0.68 tff(f1318,plain,(
% 0.39/0.68 sP1 | (sP0 & ('zero$a' != 'fun_app$c'('vec_nth$'('fun_app$d'('vec_nth$a'('a$'),sK2)),'from_nat$a'('k$')) & 'less_eq$'('from_nat$'('i$'),sK2)) & 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f1317])).
% 0.39/0.68 tff(f1609,plain,(
% 0.39/0.68 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) | 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))) | ~sP1),
% 0.39/0.68 inference(cnf_transformation,[],[f1315])).
% 0.39/0.68 tff(f1618,plain,(
% 0.39/0.68 sP1 | 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$'))),
% 0.39/0.68 inference(cnf_transformation,[],[f1318])).
% 0.39/0.68 tff(f1622,plain,(
% 0.39/0.68 ~$less('of_nat$'('nrows$'('a$')),'of_nat$'('i$'))),
% 0.39/0.68 inference(cnf_transformation,[],[f637])).
% 0.39/0.68 tff(f1623,plain,(
% 0.39/0.68 ~$less('of_nat$'('i$'),'of_nat$'('nrows$'('a$')))),
% 0.39/0.68 inference(cnf_transformation,[],[f12])).
% 0.39/0.68 tff(f2032,plain,(
% 0.39/0.68 ( ! [X0 : 'Nat$',X1 : 'A_b_vec_c_vec$'] : ('snd$'('pair$a'(X0,X1)) = X1) )),
% 0.39/0.68 inference(cnf_transformation,[],[f273])).
% 0.39/0.68 tff(f2034,plain,(
% 0.39/0.68 ( ! [X0 : 'Nat$',X1 : 'A_iarray_iarray$'] : ('snd$c'('pair$d'(X0,X1)) = X1) )),
% 0.39/0.68 inference(cnf_transformation,[],[f275])).
% 0.39/0.68 tff(f2036,plain,(
% 0.39/0.68 ( ! [X0 : 'A$',X1 : 'Nat_a_b_vec_c_vec_prod$'] : ('snd$a'('pair$'(X0,X1)) = X1) )),
% 0.39/0.68 inference(cnf_transformation,[],[f277])).
% 0.39/0.68 tff(f2037,plain,(
% 0.39/0.68 ( ! [X0 : 'A$',X1 : 'Nat_a_iarray_iarray_prod$'] : ('snd$d'('pair$c'(X0,X1)) = X1) )),
% 0.39/0.68 inference(cnf_transformation,[],[f278])).
% 0.39/0.68 tff(f2502,plain,(
% 0.39/0.68 ( ! [X0 : 'A_b_vec_c_vec$'] : ('of_nat$'('nrows$'(X0)) = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'(X0)))) )),
% 0.39/0.68 inference(cnf_transformation,[],[f573])).
% 0.39/0.68 tff(f2808,definition,(
% 0.39/0.68 spl88_2 <=> sP1),
% 0.39/0.68 introduced(definition,[new_symbols(definition,[spl88_2])],[avatar_definition])).
% 0.39/0.68 tff(f2809,plain,(
% 0.39/0.68 ~sP1 | spl88_2),
% 0.39/0.68 inference(avatar_component_clause,[],[f2808])).
% 0.39/0.68 tff(f2819,definition,(
% 0.39/0.68 spl88_5 <=> 'of_nat$'('i$') = 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$')))),
% 0.39/0.68 introduced(definition,[new_symbols(definition,[spl88_5])],[avatar_definition])).
% 0.39/0.68 tff(f2821,plain,(
% 0.39/0.68 'of_nat$'('i$') != 'of_nat$'('nrows_iarray$'('matrix_to_iarray$'('a$'))) | spl88_5),
% 0.39/0.68 inference(avatar_component_clause,[],[f2819])).
% 0.39/0.68 tff(f2823,definition,(
% 0.39/0.68 spl88_6 <=> 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) = 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$')))))),
% 0.39/0.68 introduced(definition,[new_symbols(definition,[spl88_6])],[avatar_definition])).
% 0.39/0.68 tff(f2825,plain,(
% 0.39/0.68 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('snd$d'('pair$c'('n$','pair$d'('i$','matrix_to_iarray$'('a$'))))) | spl88_6),
% 0.39/0.68 inference(avatar_component_clause,[],[f2823])).
% 0.39/0.68 tff(f2826,plain,(
% 0.39/0.68 ~spl88_2 | ~spl88_5 | ~spl88_6),
% 0.39/0.68 inference(avatar_split_clause,[],[f1609,f2823,f2819,f2808])).
% 0.39/0.68 tff(f2979,plain,(
% 0.39/0.68 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) != 'snd$c'('pair$d'('i$','matrix_to_iarray$'('a$'))) | spl88_6),
% 0.39/0.68 inference(superposition,[],[f2825,f2037])).
% 0.39/0.68 tff(f2980,plain,(
% 0.39/0.68 'matrix_to_iarray$'('a$') != 'matrix_to_iarray$'('snd$'('snd$a'('pair$'('n$','pair$a'('i$','a$'))))) | spl88_6),
% 0.39/0.68 inference(forward_demodulation,[],[f2979,f2034])).
% 0.39/0.68 tff(f2981,plain,(
% 0.39/0.68 'matrix_to_iarray$'('a$') != 'matrix_to_iarray$'('snd$'('pair$a'('i$','a$'))) | spl88_6),
% 0.39/0.68 inference(forward_demodulation,[],[f2980,f2036])).
% 0.39/0.68 tff(f2982,plain,(
% 0.39/0.68 'matrix_to_iarray$'('a$') != 'matrix_to_iarray$'('a$') | spl88_6),
% 0.39/0.68 inference(forward_demodulation,[],[f2981,f2032])).
% 0.39/0.68 tff(f2983,plain,(
% 0.39/0.68 $false | spl88_6),
% 0.39/0.68 inference(trivial_inequality_removal,[],[f2982])).
% 0.39/0.68 tff(f2984,plain,(
% 0.39/0.68 spl88_6),
% 0.39/0.68 inference(avatar_contradiction_clause,[],[f2983])).
% 0.39/0.68 tff(f5302,plain,(
% 0.39/0.68 'of_nat$'('i$') != 'of_nat$'('nrows$'('a$')) | spl88_5),
% 0.39/0.68 inference(superposition,[],[f2821,f2502])).
% 0.39/0.68 tff(f5958,plain,(
% 0.39/0.68 $less('of_nat$'('i$'),'of_nat$'('nrows$'('a$'))) | 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))),
% 0.39/0.68 inference(resolution,[],[f784,f1622])).
% 0.39/0.68 tff(f6050,plain,(
% 0.39/0.68 'of_nat$'('i$') = 'of_nat$'('nrows$'('a$'))),
% 0.39/0.68 inference(forward_subsumption_resolution,[],[f5958,f1623])).
% 0.39/0.68 tff(f6056,plain,(
% 0.39/0.68 $false | spl88_5),
% 0.39/0.68 inference(forward_subsumption_resolution,[],[f6050,f5302])).
% 0.39/0.68 tff(f6057,plain,(
% 0.39/0.68 spl88_5),
% 0.39/0.68 inference(avatar_contradiction_clause,[],[f6056])).
% 0.39/0.68 tff(f6061,plain,(
% 0.39/0.68 sP1),
% 0.39/0.68 inference(global_subsumption,[],[f1618,f6050])).
% 0.39/0.68 tff(f6078,plain,(
% 0.39/0.68 $false | spl88_2),
% 0.39/0.68 inference(global_subsumption,[],[f2809,f6061])).
% 0.39/0.68 tff(f6079,plain,(
% 0.39/0.68 spl88_2),
% 0.39/0.68 inference(avatar_contradiction_clause,[],[f6078])).
% 0.39/0.68 cnf(s918, plain, ~spl88_2 | ~spl88_5 | ~spl88_6, inference(sat_conversion,[],[f2826])).
% 0.39/0.68 cnf(s1096, plain, spl88_6, inference(sat_conversion,[],[f2984])).
% 0.39/0.68 cnf(s2367, plain, spl88_5, inference(sat_conversion,[],[f6057])).
% 0.39/0.68 cnf(s2386, plain, spl88_2, inference(sat_conversion,[],[f6079])).
% 0.39/0.68 cnf(s2413, plain, $false, inference(rat,[],[s918,s1096,s2367,s2386])).
% 0.39/0.68 tff(f6080,plain,(
% 0.39/0.68 $false),
% 0.39/0.68 inference(avatar_sat_refutation,[],[s2413])).
% 0.39/0.68 % SZS output end Proof for theBenchmark
% 0.39/0.68 % (791275)------------------------------
% 0.39/0.68 % (791275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.39/0.68 % (791275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.39/0.68 % (791275)CaDiCaL version: 2.1.3
% 0.39/0.68 % (791275)Termination reason: Refutation
% 0.39/0.68 % (791275)Time elapsed: 0.110 s
% 0.39/0.68 % (791275)Peak memory usage: 16 MB
% 0.39/0.68 % (791275)Instructions burned: 218 (million)
% 0.39/0.68 % (791268)Success in time 0.171 s
% 0.39/0.68 % Vampire exiting
%------------------------------------------------------------------------------